ipasir modification without CI integration #884

nmanthey · 2017-05-02T19:33:40Z

I split my IPASIR patch series into the functional part and the CI integration, such that the first part can be merged already while the integration into CI can still be figured out lateron.

kroening · 2017-05-03T15:07:51Z

src/Makefile

@@ -84,4 +84,41 @@ glucose-download:
 	@(cd ../glucose-syrup; patch -p1 < ../scripts/glucose-syrup-patch)
 	@rm glucose-syrup.tgz

-.PHONY: minisat2-download glucose-download
+zlib-download:


The zlib/libzip download got removed; this seems to be an artefact from an older version.

kroening · 2017-05-03T15:10:06Z

src/config.inc

 #GLUCOSE = ../../glucose-syrup
 #SMVSAT =

+LIBZIPLIB = ../../libzip/lib/.libs/libzip.a ../../zlib/libz.a


Not in use any more.

kroening · 2017-05-03T15:11:02Z

src/common

+ifndef MINISAT
+ifndef MINISAT2
+ifndef GLUCOSE
+MINISAT2 = ../../minisat-2.2.1


This will be the only path in common -- a bit of a deviation from the current scheme.
I see you want to be able to switch solvers by giving a command line option to make.
Can that be achieved in any other way?

I am not sure this can be achieved in a different way, as you only want to set the default path in case none of the other variables is set already.

Shouldn't we just fail if no solver has been set? No need for defaults, the user should be forced to choose at least one. I'd do

ifeq ($(BOOLEFORCE)$(CHAFF)$(GLUCOSE)$(IPASIR)$(LINGELING)$(MINISAT)$(MINISAT2)$(PICOSAT)$(PRECOSAT),) $(error Please select a SAT solver) endif

mgudemann

maybe this has already been discussed in the community, so please excuse my ignorance, but why is there no support for variable freezing? Doesn't that prevent most solvers from using their preprocessor?

mgudemann · 2017-05-03T15:07:22Z

src/Makefile

+	@rm -Rf ../libzip
+	@mv libzip-1.1.2 ../libzip
+	@rm libzip_1.1.2.orig.tar.gz
+


we switched to internal miniz so this download is not necessary anymore

mgudemann · 2017-05-03T15:07:43Z

src/Makefile

+ipasir-build: ipasir-download
+	# build libpicaso, and create a libipasir.a in ipasir directory
+	# make sure that the ipasir.h file is located there as well (ships with 2016 package)
+	@echo "Build Picaso 961 from ipasir 2016 package"


nmanthey · 2017-05-04T06:32:56Z

I'll remove the zip based code, and update the pull request.

nmanthey · 2017-05-04T06:36:32Z

I am not aware of a broad discusion whether variable freezing should become part of the interface, as IPASIR is designed to be simple (and hence SAT solvers can be easily integrated into applications without much knowledge about solver internals). I assume this pull request is not the best place to have this discussion.

The reason for adding the interface here is to allow CBMC to link against "recent" SAT solvers easily (also in the future). In case the interface is improved, the integration in CBMC could be patched again.

nmanthey · 2017-05-05T06:43:26Z

I'd love to get the three patches in before 8th of May, so that I can use the master branch of the repository to submit CBMC to the SAT competition as part of the incremental SAT track. Otherwise, I'd have to use my fork.

mgudemann

in the first commit Not, to compile ... -> Note, to compile ...

in goto-instrument there are 6 regression tests that fail
const-struct1, const-struct2, const-union1, data-flow1, dependence-graph1, volatile-struct1

I also remarked that picoSAT prints some summary information at the end, I presume this is intended?

mgudemann · 2017-05-05T16:52:28Z

src/cbmc/Makefile

@@ -37,7 +37,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
      ../langapi/langapi$(LIBEXT) \
      ../xmllang/xmllang$(LIBEXT) \
      ../assembler/assembler$(LIBEXT) \
-      ../solvers/solvers$(LIBEXT) \
+      ../solvers/solvers$(LIBEXT) $(LIBSOLVER) \
      ../util/util$(LIBEXT) \


please put this on its own line, analogous for the other makefiles

mgudemann · 2017-05-05T16:55:18Z

src/solvers/sat/satcheck_ipasir.h

+  satcheck_ipasirt();
+  virtual ~satcheck_ipasirt();
+
+  virtual const std::string solver_text();


please mark as override

mgudemann · 2017-05-05T17:14:26Z

@nmanthey I did not intend to start this discussion, just curious about this. The failed tests are at least for the --show-symbol-table cases due to the exit code not matching, maybe a problem with picosat exiting early?
for building I used env IPASIR=../../ipasir env LIBSOLVER=../../ipasir/libipasir.a make, env IPASIR=../../ipasir env LIBSOLVER=$(pwd)/ipasir/libipasir.a make did not work

peterschrammel · 2017-05-11T21:40:43Z

src/common

@@ -150,6 +150,64 @@ else
  $(error Invalid setting for BUILD_ENV: $(BUILD_ENV_))
 endif

+# select default solver to be minisat2 if no other is specified
+ifndef IPASIR


Maybe use !defined(...) && ... to avoid the if cascade.

peterschrammel · 2017-05-11T21:47:33Z

src/solvers/sat/satcheck_ipasir.cpp

+
+/*******************************************************************\
+
+Function: satcheck_minisat_no_simplifiert::solver_text


documentation does not match function

peterschrammel · 2017-05-11T21:49:55Z

src/solvers/sat/satcheck.h

+
+#include "satcheck_ipasir.h"
+
+typedef satcheck_ipasirt satcheckt;


This will only work with --no-sat-preprocessor (or --stop-on-fail in most cases).

peterschrammel · 2017-05-11T22:04:15Z

src/Makefile

+	# build libpicosat, and create a libipasir.a in ipasir directory
+	# make sure that the ipasir.h file is located there as well (ships with 2016 package)
+	@echo "Build Picosat 961 from ipasir 2016 package"
+	$(MAKE) -C ../ipasir/sat/picosat961 libipasirpicosat961.a


How can a solver be easily selected for use with ipasir?

This requires a rebuild of CBMC. Solvers that implement the ipasir interface should be able to produce a library, which can be used during link time. The compilation of CBMC has to know about that file. Furthermore, each such rebuild has to make sure that the solver.a file is properly updated. Build instructions can be found in the top commit of this series.

Could the build instructions be added to the "COMPILING" file, please?

peterschrammel · 2017-05-11T22:05:27Z

IPASIR does not provide support for the preprocessors of Minisat and Glucose, which is a known issue. Hence, it can only be used with --no-sat-preprocessing in CBMC (or better set the option sat-preprocessing to false #ifdef HAVE_IPASIR so that the regression tests can be run normally).
Still, I think that it is a valuable addition to easily benchmark more solvers.

nmanthey · 2017-10-04T21:43:18Z

I rebased on top of origin/develop.

I fixed the pattern matching for the failing test I spotted so far - where the failure is usually due to the test matching an iteration number, which seems to depend on the SAT solver behaviour. I dropped these patterns in all tests in a new commit.

I also applied some suggestions from the reviewers, and modified the commands to build the solver for IPASIR support.

nmanthey · 2017-10-04T21:52:06Z

I also fixed the wrong comment (copy paste error) that mentions minisat

nmanthey · 2017-10-11T06:02:27Z

The problem reported in travis is not touched by my code path. As far as I can tell, I resolved all blockers that have been introduced with my patches! Please tell me how I can move forward!

https://travis-ci.org/diffblue/cbmc/builds/286241919?utm_source=github_status&utm_medium=notification

tautschnig · 2017-10-25T07:48:38Z

@reuk Just in case you have a moment to spare: I just looked at the clang-format suggestions in https://travis-ci.org/diffblue/cbmc/jobs/292240624 and it seems there is some missing indentation? Or is that just travis not getting quite right the output of leading space?

romainbrenguier · 2017-10-25T07:39:14Z

src/solvers/sat/satcheck_ipasir.cpp

+
+bool satcheck_ipasirt::is_in_conflict(literalt a) const
+{
+  int v=a.var_no();


romainbrenguier · 2017-10-25T07:40:01Z

src/solvers/sat/satcheck_ipasir.cpp

+
+  if(ipasir_failed(solver, v))
+      return true;
+  return false;


what about return ipasir_failed(solver, a.var_no()); ?

romainbrenguier · 2017-10-25T07:45:22Z

src/solvers/sat/satcheck_ipasir.cpp

+  forall_literals(it, bv)
+    if(it->is_true())
+    {
+      assumptions.clear();


It seems assumptions can be cleared several times, I suggest using std::find_if instead.

I'll replace it with a find_if.
However, the next line is a return, so that clear() is only called once.

reuk · 2017-10-25T08:49:01Z

it seems there is some missing indentation? Or is that just travis not getting quite right the output of leading space?

I see this too, but if I run git diff --color > patch.diff; cat patch.diff locally the output has the correct number of spaces. It seems that Travis is collapsing one-or-more consecutive spaces into a single space.

tautschnig · 2017-10-25T08:53:54Z

It seems that Travis is collapsing one-or-more consecutive spaces into a single space.

Thank you very much for confirming! (Also I should have looked at the raw log yet that's pretty messy as well.)

reuk · 2017-10-25T08:55:51Z

Maybe the solution is to disable colourising the diff - then at least the raw output will look right

nmanthey · 2017-10-25T09:31:54Z

I applied the comments

tautschnig

Two issues noted by the linter.

tautschnig · 2017-10-25T09:38:44Z

src/solvers/sat/satcheck_ipasir.cpp

+  else
+  {
+    // if assumptions contains false, we need this to be UNSAT
+    bvt::const_iterator it = std::find_if(assumptions.begin(), assumptions.end(), is_false);


Please line-wrap:

src/solvers/sat/satcheck_ipasir.cpp:114: Lines should be <= 80 characters long [whitespace/line_length] [2]

yes, spotted both of them locally. will install the linter githook before the next contribution ...

tautschnig · 2017-10-25T09:39:01Z

src/solvers/sat/satcheck_ipasir.cpp

+      {
+        messaget::status() <<
+          "SAT checker: solving returned without solution" << eom;
+        throw "Solving inside IPASIR SAT solver has been interrupted";


Lowercase:

src/solvers/sat/satcheck_ipasir.cpp:146: First character of throw error message should be lower case [readability/throw] [4]

tautschnig · 2017-10-25T09:41:55Z

Maybe the solution is to disable colourising the diff - then at least the raw output will look right

True, but at the same time human readability would be impacted. I think we should stick with the current approach, unless @forejtv can work something similar to the Cpp Linter CI job, which would yield the raw diff in some easy-to-download form.

kroening · 2017-10-25T09:44:50Z

src/solvers/sat/satcheck_ipasir.cpp

+    {
+      // add literal with correct sign
+      ipasir_add(solver, it->sign()?-it->var_no():it->var_no());
+    }


Another little tweak: the above can simply be it->dimacs()

kroening · 2017-10-25T09:45:28Z

src/solvers/sat/satcheck_ipasir.cpp

+      forall_literals(it, assumptions)
+        if(!it->is_false())
+          ipasir_assume(solver, it->sign()?-it->var_no():it->var_no());
+


Use it->dimacs() as well.

kroening · 2017-10-25T09:45:56Z

src/solvers/sat/satcheck_ipasir.cpp

+
+      // solve the formula, and handle the return code (10=SAT, 20=UNSAT)
+      int solver_state==ipasir_solve(solver);
+      if(10==solver_state)


I am surprised that the == parses?

That slipped through copy and paste, and the compiler was happy ... if fixed it and tested another round with the LIBSOLVER build locally.

kroening · 2017-10-25T09:49:33Z

COMPILING.md

+   Note: the LIBSOLVER variable could be pointed towards other solvers
+   ```
+   make -C src IPASIR=../../ipasir LIBSOLVER=$(pwd)/ipasir/libipasir.a
+   ```


We've got the names for the libraries of the other solvers in the config; why not for IPASIR as well?

Then it would be enough to say
make -C src IPASIR=../../ipasir

Because typically (except you always want to use picosat) you want to push people to select their most favourite IPASIR solver explicitly at compile time.

tautschnig · 2017-10-26T17:40:15Z

@mgudemann @romainbrenguier Could you please review/approve the changes or add further comments?

mgudemann

almost done, I built the picosat Version and documented what I needed to adapt in order to do so, no blocker to approval, once this is done

mgudemann · 2017-10-27T09:33:46Z

COMPILING.md

+
+   Get an IPASIR package and build picosat by default
+   ```
+   make -C ipasir-build


should be make -C ipasir which is the folder after doing make -C src ipasir-download

genipamax hard-codes g++-4.7, unsure how to fix, maybe use just g++ in the C++11 file

File: genipamax/README
7:26:The makefiles expect g++-4.7, if you want to use a different compiler

NOTE: A C++ compiler supporting the std=c++0x flag is required. The makefiles expect g++-4.7, if you want to use a different compiler update the 'C++11' file.

ok, but then again, this is only needed if one explicitely wants those solvers

I agree. This is an external package. I will raise this for that package, so that it eventually gets resolved there.

mgudemann · 2017-10-27T09:42:48Z

src/solvers/sat/satcheck_ipasir.cpp

+#include <inttypes.h>
+#endif
+
+#include <cassert>


I needed <algorithm> here, too, for find_if

tautschnig · 2017-10-27T15:11:04Z

Assigning to @nmanthey for a final set of changes following @mgudemann's testing/comments.

When building solvers.a while aiming at building CBMC with support for IPASIR solvers, all projects that need SAT checkers would require to link against the provided libipasir.a library. To make this library visible for all subprojects at the same time, but furthermore allow the user to choose which library to pick, the variable LIBSOLVER was introduced, which is set to an empty value by default. To get started with the default ipasir package, run the following commands in the root directory of the repository: make ipasir-build -C src make -C src IPASIR=../../ipasir LIBSOLVER=$(pwd)/ipasir/libipasir.a

Add the necessary source changes to allow CBMC to use IPASIR solvers.

Add necessary steps to set variables for IPASIR Furthermore, allow to select SAT solver from make command line, for example by calling IPASIR=../../ipasir LIBSOLVER=$(pwd)/ipasir/libipasir.a make Note, to compile with a different SAT solver, e.g. GLUCOSE=../../glucose-syrup make it has to be ensured, that the solvers.a library is rebuild, and all components that link against this library are renewed as well. This can be achieved by touching the satcheck.h flie, i.e.: touch src/solvers/sat/satcheck.h

When checking for success or failure of a test, the number of iterations in the actual test should be irrelevant. As MiniSAT and PicoSAT seem to disagree on this number, do not check for it, so that the testis pass again.

During tests, the number of used iterations has been matched. When using different SAT solvers, these numbers differ. Without the numbers, the line is actually useless, so that we drop it completely.

Add the steps to link against an IPASIR solver to the COMPILING notes.

4820601 Merge remote-tracking branch 'diffblue/develop' into merge-dev-to-ss 278f309 Merge pull request diffblue#1526 from reuk/reuk/fixup-unified-diff 69ba9e7 Merge pull request diffblue#1546 from smowton/smowton/feature/expose_tarjan 05dc65c Use lower-case characters to start error messages 8d0b23b Change asserts to invariants a7afc6c Return from get_diff by value 6833af6 Fix formatting 4555d9f Remove unused parameter e32c6c5 Make instructions_equal static f815cc0 Move instructions_equal definition 11c9acc Add getter for data member 8c35211 Make data member private f54db47 Rename differences map data member b67d6e8 Merge pull request diffblue#1543 from chrisr-diffblue/cleanup/add-java-array-element-type-helper c9241cd Make generic Tarjan's algorithm publically available ebabdb9 Merge pull request diffblue#1542 from smowton/smowton/cleanup/sharing-node-assertion a523d6f Add a helper function for accessing the element type of a Java array type d8e8a68 Use INVARIANT rather than assert for sharing-node assertions 64d5dd2 Merge pull request diffblue#1538 from smowton/smowton/cleanup/remove-returns-asserts-to-invariants fca7c04 Merge pull request diffblue#1537 from smowton/smowton/cleanup/sharing-node-test-to-catch e35372a Merge pull request diffblue#1539 from romainbrenguier/bugfix/char-array-in-java-strings#TG-58#newpr 4d011b5 Merge pull request diffblue#1541 from owen-jones-diffblue/replace-unsigned-with-number-type b2a4e39 Merge pull request diffblue#1540 from owen-jones-diffblue/rename-detach 2f6ceed Replace unsigned with appropriate type 938ab2b Replace 'detatch' with 'detach' c219663 Convert sharing-node test to run under Catch dec5ddf Remove-returns: asserts -> invariants 3b1f485 Merge pull request diffblue#1535 from andreast271/ignore-eclipse-vs-dirs 6cea5aa Ignore files and directories created by Eclipse and Visual Studio aa94fe8 Style: add nolint marker on lines formated by clang ee4a887 Merge pull request diffblue#1458 from LAJW/perl-platform 4da5a94 Add templating functionality to the perl script 21b2641 Move make_function_application to java_utils 5196e40 Merge pull request diffblue#884 from nmanthey/ipasir-no-ci 3ee3b25 Refactor: remove m_ prefix from member fields 539ff9f Refactoring: simplify and remove unused expression 5a0d6b4 Rename first_index in array_expr d03b8cc Remove regression test that is not checking anything 90c8495 Improve tests for StringBuilder.append([C) 232617c Add code for String constructor from array a2d7811 Use dynamic object instead of tmp_object in init daef30f Splitting is_string and init_string parts of init ad65847 Style: rename i in chr_int to avoid clash e59349f Remove redundant check in from_int_with_radix 038b476 Allow index for argument of associate array to pointer 73d51fc Remove insert_long which duplicates insert_int bb22700 Cleanup unused fields of constraint generator 2355e8e Fix set of created strings in generator and use it 26e895d Distinguish strings and char arrays in get 4b8a421 Make get_array return array of unknown expr ca8213f Simplify not_contains constraints before negation 92897f7 Style fixes in string_constraint_generator.h 145364c String refinement: Improve debug information 3e5b3f1 Minor code improvements in string refinement 3d5465e Minor code improvements in generator_insert 86e1444 Refactoring: use begin()+3 instead of 3 times next fef1c5f Correction in debug model 28590fe Correction in constraints for concat 6861b9d Documentation fixes in stirng constraint generator c410159 Regression: StringBuilder append with int argument e6700ff Minor improvements in bytecode typecheck 61f0e1b Making check_axioms for string_constraints and not_contains_constraints more uniform f2122c6 Correct signature of convert_exprt_to_string_exprt_unit_test 9edbb90 [string-refinement] Change get_array to return optional 86e4782 [string-refinement] Allow index set saturation if not_contains_constraints are present c9c612d [string-refinement] Do not update index set of constant arrays b88fe35 [string-refinement] Check for char type 1a22916 [string-refinement] Display debug info for index-set 982a5fc Style and documentation fixes in preprocessing a83daa7 Minor indentation, naming and const-fixes 15fd1b4 Fix typos in strings and comments of string solver 26ae9a9 Unit test improve convert exprt to string exprt b76b116 Minor improvements in string preprocessing 05a6b09 [constraint-generator] Removing declarations of unimplemented functions 302f92e Make string primitives return return_code_type b80d063 Doxygen corrections 369dd62 Unit test: adapte instantiate_nc for new signature dcae158 [string-refinement] Removing unused functions b6b2669 Style changes in string_constraint_generator_testing edf7057 Complete string solver rework 9ea2eda Unit tests for union_find_replacet 4adf5d0 New class for union find replace 1d112d5 Java object factory for nondet strings 0ae71b0 [string-preprocessing] New functions for calling string primitives in initialization e89f5e4 [string-preprocess] Refactor java_types_matches_tag 2505982 Extra preconditions in string solver 6378400 Style improvements in the string solver 36d6e6d [util/irep_ids] Additional identifiers fa45b34 Regression test mprovement for if expressions 76cd14d Unit test for gen_nondet_string_init c71c64b Regression: include model for string to char array c3d527c compiling: add IPASIR notes for Linux 900a0fc tests: do not match iterations line 751208d tests: drop number of iterations 12a6917 build: add ipasir solver support 14419d2 solvers: add ipasir driver 8aa89be build: introduce LIBSOLVER environment variable df45bdb Merge pull request diffblue#1524 from reuk/reuk/fix-linter 4b39446 Merge pull request diffblue#1518 from diffblue/taint-for-C 25e18c0 Merge pull request diffblue#1529 from smowton/smowton/fix/float128 3cf67f7 Merge pull request diffblue#1531 from reuk/reuk/expr-cast-fixup 2169a39 Add _Float128 spelling for 128-bit float type a3cf849 Merge pull request diffblue#1530 from martin-cs/feature/document-return-codes 188f263 Enable casting from derived types to other derived types 3dd7f6c first regression tests 29bc3b8 custom_bitvector_domain: allow objects that are members ab7270e check taint on sinks _before_ the call 6daa8bd Merge pull request diffblue#1528 from tautschnig/shl-overflow 2df2abb Change a few erronious return codes so that they are more internally consistent. cf96cef Minor changes to erronious exit behaviour. c8dfd48 Replace constants exit codes with meaningfully named macros. 961d33a Replace literal constants in returns / exits with their symbolic names. e74b442 Named, possibly even descriptive macros for the exit codes that are used. 1e3712c Shifts of non-integers and left shifts of negative integers are undefined 6bb3872 Check for overflow on left shift of signed ints f9af374 Merge pull request diffblue#1512 from thk123/bugfix/TG-1058/crash-inner-class-generic-class bd2e9c2 Merge pull request diffblue#1522 from reuk/reuk/clang-format-plain-diff f892f4a Added tests for bracket matcher to include different types of brackets 3beab8b Fixed error in find_closing_delimiter 0b3058f Tightened up exception for unknown handling 9f87a80 Assertion on unmatched ; for parsing reference types 5922826 Adding doubly nested generic tests 4a62b07 Simplifying method names for unit test ee39620 Extended tests to verify the generic information is being parsed correctly. 465a473 Parse multiple nested generic type informations b8d43ab Pulled out method for parsing a list of multiple types 2a5c280 Correctly parse multiple input parameters for functions 35d974f Add method for finding the matching ; corresponding to a reference L e1621a3 Hide methods relating to getting multiple type variables for specific param e952708 Adding tests for parsing methods of generic classes with inner classes 958c006 Adding utilities for code_type structures 72a041b Don't crash when found an invalid reference type ed545cb Refactored out the code for erasing generic types effc1b2 Parse the whole class when generics are present d23a0cc Added function for getting the full class name of a type 34c185e Unit test reproducing the bug described in TG-1058 5b92002 Adding utilities for checking types in unit tests a00edd3 Disable dowhile brace check by default d38b5d8 Disable colour in travis diff display git-subtree-dir: cbmc git-subtree-split: 4820601

kroening reviewed May 3, 2017

View reviewed changes

mgudemann reviewed May 3, 2017

View reviewed changes

nmanthey force-pushed the ipasir-no-ci branch 2 times, most recently from 37d6880 to 620f66d Compare May 5, 2017 06:41

mgudemann suggested changes May 5, 2017

View reviewed changes

peterschrammel reviewed May 11, 2017

View reviewed changes

tautschnig assigned nmanthey Aug 20, 2017

tautschnig changed the base branch from master to develop August 22, 2017 12:26

nmanthey force-pushed the ipasir-no-ci branch 3 times, most recently from a095e77 to dfb10cf Compare August 28, 2017 20:48

nmanthey force-pushed the ipasir-no-ci branch 2 times, most recently from 0ef38ea to 7233c43 Compare October 4, 2017 21:41

nmanthey force-pushed the ipasir-no-ci branch from 7233c43 to bd4f259 Compare October 4, 2017 21:51

nmanthey force-pushed the ipasir-no-ci branch 2 times, most recently from ee965a1 to a7c106f Compare October 10, 2017 20:51

kroening assigned tautschnig and mgudemann and unassigned nmanthey Oct 10, 2017

romainbrenguier reviewed Oct 25, 2017

View reviewed changes

nmanthey force-pushed the ipasir-no-ci branch from 6673556 to d26b8bc Compare October 25, 2017 09:31

tautschnig requested changes Oct 25, 2017

View reviewed changes

kroening reviewed Oct 25, 2017

View reviewed changes

nmanthey force-pushed the ipasir-no-ci branch from d26b8bc to 60f4194 Compare October 25, 2017 14:06

tautschnig approved these changes Oct 26, 2017

View reviewed changes

tautschnig assigned romainbrenguier Oct 26, 2017

mgudemann suggested changes Oct 27, 2017

View reviewed changes

romainbrenguier approved these changes Oct 27, 2017

View reviewed changes

tautschnig assigned nmanthey and unassigned mgudemann and romainbrenguier Oct 27, 2017

Norbert Manthey added 6 commits October 27, 2017 21:00

solvers: add ipasir driver

14419d2

Add the necessary source changes to allow CBMC to use IPASIR solvers.

tests: drop number of iterations

751208d

When checking for success or failure of a test, the number of iterations in the actual test should be irrelevant. As MiniSAT and PicoSAT seem to disagree on this number, do not check for it, so that the testis pass again.

tests: do not match iterations line

900a0fc

During tests, the number of used iterations has been matched. When using different SAT solvers, these numbers differ. Without the numbers, the line is actually useless, so that we drop it completely.

compiling: add IPASIR notes for Linux

c3d527c

Add the steps to link against an IPASIR solver to the COMPILING notes.

nmanthey force-pushed the ipasir-no-ci branch from 60f4194 to c3d527c Compare October 27, 2017 20:53

mgudemann approved these changes Oct 28, 2017

View reviewed changes

kroening merged commit 5196e40 into diffblue:develop Oct 30, 2017


		/*******************************************************************\

		Function: satcheck_minisat_no_simplifiert::solver_text


		#include "satcheck_ipasir.h"

		typedef satcheck_ipasirt satcheckt;

ipasir modification without CI integration #884

ipasir modification without CI integration #884

Conversation

nmanthey commented May 2, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mgudemann left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

nmanthey commented May 4, 2017

nmanthey commented May 4, 2017

nmanthey commented May 5, 2017

mgudemann left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mgudemann commented May 5, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

peterschrammel commented May 11, 2017

nmanthey commented Oct 4, 2017

nmanthey commented Oct 4, 2017

nmanthey commented Oct 11, 2017

tautschnig commented Oct 25, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

reuk commented Oct 25, 2017

tautschnig commented Oct 25, 2017

reuk commented Oct 25, 2017

nmanthey commented Oct 25, 2017

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig commented Oct 25, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig commented Oct 26, 2017

mgudemann left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig commented Oct 27, 2017