Importing CryptoMiniSat version 'Cluster56'.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@812 e59a4935-1847-0410-ae03-e826735625c1

Fix the method to count the number of instances in an expression. Previously it was counting no more than one.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@811 e59a4935-1847-0410-ae03-e826735625c1

Split out the class which lazily builds the variables in terms.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@810 e59a4935-1847-0410-ae03-e826735625c1

Small speedup in the cnf generator.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@808 e59a4935-1847-0410-ae03-e826735625c1

Add histar to regressall. We use far far too much memory on these tests. Not sure why.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@806 e59a4935-1847-0410-ae03-e826735625c1

Moving histar tests to the main test directory.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@804 e59a4935-1847-0410-ae03-e826735625c1

Add my experimental BVSolver. It's much slower than the current bvsolver, but is more reliable. I'll gradually move its innovations into the main bvsolver.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@803 e59a4935-1847-0410-ae03-e826735625c1

Enable upfront simplifications of terms.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@802 e59a4935-1847-0410-ae03-e826735625c1

* Make the constant evaluator a non member function. This allows the simplifying node factory to use it without holding a reference to a Simplifier object.
* Change the simplifier to use the simplifying node factory by default.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@801 e59a4935-1847-0410-ae03-e826735625c1

Simplifyin BVSX to CONCAT if the topmost bit of the thing being extended is known.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@800 e59a4935-1847-0410-ae03-e826735625c1

* Add a disabled-by-default option to simplify the arguments of a function first.
* Check explicitly the kind returned from some functions that create nodes to ensure the returned type is what we expect. With the simplifying node factory enabled, the type can sometimes change.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@798 e59a4935-1847-0410-ae03-e826735625c1

Add a simplification so that (ite(p,5,7) <= 8) is always true is detected.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@797 e59a4935-1847-0410-ae03-e826735625c1

Bugfix. If given bad input, the SMTLIB2 parser would match as much as it could then stop, without warning. It now checks that an end of file has been reached.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@796 e59a4935-1847-0410-ae03-e826735625c1

* Improve the simplifications of inequalities and equalities.
* Add code to print out each of the expressions that are simplified by the bit blaster.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@795 e59a4935-1847-0410-ae03-e826735625c1

Implements booth recoding when bitblasting multiplication.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@793 e59a4935-1847-0410-ae03-e826735625c1

Add the "eric-tests" to regressall.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@791 e59a4935-1847-0410-ae03-e826735625c1

bugfix. Allow distinct to be used for both formulae and terms.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@790 e59a4935-1847-0410-ae03-e826735625c1

These scripts (though I don't know what they do) seem to belong with the other test generation scripts.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@787 e59a4935-1847-0410-ae03-e826735625c1

Bugfix. Rare types of array reads were causing a type-error.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@784 e59a4935-1847-0410-ae03-e826735625c1

* Letize booleans when printing back smb2lib format.
* Print back in smtlib/smtlib2 format arity > 2 and, xor, or.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@783 e59a4935-1847-0410-ae03-e826735625c1

Run tests with the .smt2 extension.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@782 e59a4935-1847-0410-ae03-e826735625c1

Fix the memory leaks in the SMTLIB2 parser.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@780 e59a4935-1847-0410-ae03-e826735625c1

* fix reduce/reduce error in the smtlib2 format.
* fix dependencies of smtlib2 format in the makefile.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@779 e59a4935-1847-0410-ae03-e826735625c1

The SMTLIB2 parser now accepts valid, but extremely improbable symbol names, such as: ?

It's not finished, it still leaks badly, ignores most of the commands it's sent, and doesn't allow annotations to be used.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@778 e59a4935-1847-0410-ae03-e826735625c1

Fix the defintion of what a symbol is in the SMTLIB2 format.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@777 e59a4935-1847-0410-ae03-e826735625c1

Use the flex options recommended by its manual.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@776 e59a4935-1847-0410-ae03-e826735625c1

* Add binary & hexidecimal for smtlib2 format.
* Fix the syntax of the smtlib2 repeat function.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@775 e59a4935-1847-0410-ae03-e826735625c1

An initial version of an smtlib2 format parser. It has these problems:
* Leaks memory
* Doesn't allow for annotations on terms.
* Ignores the commands sent to it. It just solves the problem specified.

Other changes:
* Long options are no longer case senstive.
* If the input file ends with .smt2 or .smt the appropriate parser is selected.
* The simplifying node factory is disabled during parsing when printing back is enabled. This allows STP to be used as a better, but still low-fidelity translator between formats.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@774 e59a4935-1847-0410-ae03-e826735625c1

* The bvsmod operation can now be output by the printers.
* Output the status i.e. sat, unsat if known.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@773 e59a4935-1847-0410-ae03-e826735625c1

Fix the build by adding a missing function.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@772 e59a4935-1847-0410-ae03-e826735625c1

Fix: lets, types, extends and extracts in the SMTLIB2 format.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@771 e59a4935-1847-0410-ae03-e826735625c1

The SMT-LIB2 format changes names from "implies" to "=>", and "IFF" to "=".

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@770 e59a4935-1847-0410-ae03-e826735625c1

A first attempt at an SMT-LIB2 output printer. I haven't tried to parse this so I'm not sure it's right.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@769 e59a4935-1847-0410-ae03-e826735625c1

BOOLEXTRACT seems to have been implemented backward. It did an equality test on
the extracted bit against *zero*, instead of *one*.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@768 e59a4935-1847-0410-ae03-e826735625c1

* Convert BVAND( ite(p,1,1) , ite(p2,0,1)) to ite(p and p2, 0,1).
* Add back simplify() for minisat.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@767 e59a4935-1847-0410-ae03-e826735625c1

Delete an unnecessary copy of c_interface.h, ammend the README to suggest updating the TEST_PREFIX>

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@766 e59a4935-1847-0410-ae03-e826735625c1

Remove the code for the "ReferenceCount". This was my first attempt to make the simplifications DAG-aware (sometimes called sharing-aware). The approach I chose was fundamentally broken (oops). I'm working on a new approach.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@765 e59a4935-1847-0410-ae03-e826735625c1

* Use the simplifying node factory and the type checking node factory when parsing the CVC format via the main method. I haven't changed the c-interface to simplify as it build.
* Remove some explicit type checks in the CVC parser. Since the type checking node factory type checks each node it creates, there's no reason to have so many explicit type checks. So I've removed some of them.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@764 e59a4935-1847-0410-ae03-e826735625c1

Add an encoding of multiplication that explicitly uses addition networks. This is copied from r482. I've not yet experimented with which bbmult() function is the best.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@761 e59a4935-1847-0410-ae03-e826735625c1

First attempt at tracking time spent building the counter example. Doesn't properly include abstraction refinement checking time (I think). This introduces changes from r316

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@760 e59a4935-1847-0410-ae03-e826735625c1

Fix the flattenOneLevel function as per r294

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@759 e59a4935-1847-0410-ae03-e826735625c1

* Make the arguments to ==, !=, > for ASTNode references to reduce unnecessary copies.
* Include the BBVLE from r254 for later experimentation.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@758 e59a4935-1847-0410-ae03-e826735625c1

* Fix the use of an invalidated iterator in the CVC parser.
* Fix a small memory leak in the CVC parser.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@756 e59a4935-1847-0410-ae03-e826735625c1

When sending clauses to the SAT solver, create fewer objects. This speeds up sending to the sat solver by about 15%.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@755 e59a4935-1847-0410-ae03-e826735625c1

Remove iterators from BBLShift to remove a spurious(?) warning when running in g++'s debug mode. i.e. with -D_GLIBCXX_DEBUG

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@754 e59a4935-1847-0410-ae03-e826735625c1

Added info to the INSTALL file about the various configure script options

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@753 e59a4935-1847-0410-ae03-e826735625c1

Simplify the division operation. An unnecessary comparison has been removed from the division. This division as measured on the factoring12bitx12.cvc benchmark is about 20% faster.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@752 e59a4935-1847-0410-ae03-e826735625c1

fixed the problem with Alvin Cheung's testcase. The problem was that ITE-array expressions were not being handled correctly in SimplifyWrite_InPlace(). Fixed that

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@749 e59a4935-1847-0410-ae03-e826735625c1

Refactoring. Take out some ASTNodes from the bitblaster.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@748 e59a4935-1847-0410-ae03-e826735625c1

fixed the order in which the regressions are run. The C API regressions are run last

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@747 e59a4935-1847-0410-ae03-e826735625c1

Perennial problem with svn. Does not give me the list of all modified files before check-in, and hence I end up checking-in experimental code. Fixed minor mod in STP.cpp

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@746 e59a4935-1847-0410-ae03-e826735625c1

fixed TEST_PREFIX in Makefile.common. Ideally this should be fixed in the configure script. Also added new testcase eric1.stp to the repo

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@745 e59a4935-1847-0410-ae03-e826735625c1

Small changes to the array transformer:
* Use the node factory directly where possible.
* Use the general read(ite(...)..) case rather than handling specially read(write(ite...)..)..)
* Unless NDEBUG is defined check that no operations that should have been removed remain in the formula.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@743 e59a4935-1847-0410-ae03-e826735625c1

Enable counter example checking by default.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@742 e59a4935-1847-0410-ae03-e826735625c1

Don't test a22 in valgrind because it leaks

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@741 e59a4935-1847-0410-ae03-e826735625c1

CMS2: Hyper-binary resolution was wrong. Removed.

Hyper-binary resolution added binary clauses that lead to wrong UNSAT
answers, when the solution was in fact possible to find. I disabled it.
Also, other, minor problems have been fixed.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@739 e59a4935-1847-0410-ae03-e826735625c1

Applying a patch provided by Hume to parse cvc and smtlib format constraints from c-strings.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@738 e59a4935-1847-0410-ae03-e826735625c1

* Send the -t flag to STP when running regressstp. This outputs statistics that are useful to sum up.
* Delete my old eclipse formatting configuration. I don't use this anymore. Suspect no one else does either.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@737 e59a4935-1847-0410-ae03-e826735625c1

Removing an .o file accidently checked in.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@734 e59a4935-1847-0410-ae03-e826735625c1

Bugfix. Refactoring of ToCNF broke some ifdef CRYPTOMINISAT2 code.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@733 e59a4935-1847-0410-ae03-e826735625c1

Turning on simplification&subpart-solving in CMS2

Simplification is carried if the problem seems difficult. It is carried
out in steps, so the complete algorithm's time demands do not have to
absorbed the first time it is run. Subpart-solving regularly checks for
parts of the problem that are disconnected, solves them, and returns to
the original problem instance -- essentially executing a
divide-and-conquer algorithm

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@732 e59a4935-1847-0410-ae03-e826735625c1

Updating CMS2

There have been some bugs fixed, and some performance increases added.
Hopefully these will fix up all remaining bugs

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@731 e59a4935-1847-0410-ae03-e826735625c1

Remove some unnecesarry memory churn. Extra objects were created and destroyed that didn't need to be.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@730 e59a4935-1847-0410-ae03-e826735625c1

Refactoring. This creates a separate ClauseList class that holds the pointers to the CNF's clauses. I've just moved stuff around, so nothing should break/ work better.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@729 e59a4935-1847-0410-ae03-e826735625c1

Making some functions ASTNode memberfunctions

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@727 e59a4935-1847-0410-ae03-e826735625c1

* Delete a test script that's no longer used
* regressstp now copies all the test cases to /dev/null to prime the disk cachde (like the other regression tests do).

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@724 e59a4935-1847-0410-ae03-e826735625c1

Fix regressbio. I missed an 's' in its path

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@723 e59a4935-1847-0410-ae03-e826735625c1

Include the STP version in the regression log

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@721 e59a4935-1847-0410-ae03-e826735625c1

Add crypto and bio regression targets

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@720 e59a4935-1847-0410-ae03-e826735625c1

Use gunzip so that we can run tests that are gzipped.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@711 e59a4935-1847-0410-ae03-e826735625c1

* Make regressall depend on "all". If any changes have occured to STP's source code before you test, there will be a rebuilt. This prevents the problem of testing an old version of STP.
* Fix the regressstp target. It wasn't outputting to the log file.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@710 e59a4935-1847-0410-ae03-e826735625c1

* Reduce the number of scripts we use to run regression tests.
* Remove redundacy from the Makefile.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@707 e59a4935-1847-0410-ae03-e826735625c1

Fix the renameAllSiblings option in the CNF generator. It is still disabled by default until I measure its usefulnes..

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@705 e59a4935-1847-0410-ae03-e826735625c1

Reverting r465. Based on Stephen's example: stp-tests/crypto-tests/factoring-12bitsx12.stp this makes division about 50% faster.

Confirming what Stephen identified, varying just the bvdiv encoding:

crypto2: 42sec vs 32sec
simplifying minisat: 65s vs 37s
core minisat: 65s vs 43s

However, r600 solved this problem the fastest I've seen: 14 seconds. But that was cryptominisat. Cryptominisat2 is now in the trunk. So I suspect that this reverts a change that made division faster on cryptominisat, but slowed it down on the others (including cryptominisat2).

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@704 e59a4935-1847-0410-ae03-e826735625c1

Fix leaks in the CVC parser

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@702 e59a4935-1847-0410-ae03-e826735625c1

Fix memory leaks in the SMT-LIB parser.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@701 e59a4935-1847-0410-ae03-e826735625c1

Updating CMS2 to fix some bugs

* Conglomerate was freeing the same clause. Fixed.
* Gaussian elimination is now disabled (was broken)
* Some code cleanup
* After solution extension, propagate was not called when decisionLevel
  was 0. This lead to assertion failure when adding clause during
  library usage

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@699 e59a4935-1847-0410-ae03-e826735625c1

Updating CMS2 to correct destructor segfault

XorFinder left the state in an unstable manner when UNSAT was found this
later lead to a segfault when trying to destruct the solver. Fixed.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@696 e59a4935-1847-0410-ae03-e826735625c1

Fixing CMS2's library debug routine

It didn't work correctly when re-adding removed clauses: variable
elimination, conglomeration, and part-handling all dumped data, but they
shouldn't have been

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@693 e59a4935-1847-0410-ae03-e826735625c1

Updating CMS2 to fix bug in Conglomerate.cpp

The Conglomeration aborted early when re-adding clauses, leading to a
bug that occured when UNSAT was found out while re-adding clauses. The
state of Conglomerate was left in a half-freed position, which lead to
Segfault when calling ~Conglomerate

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@692 e59a4935-1847-0410-ae03-e826735625c1

CMS2 update missed out on the MTL library changes. Fixed.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@691 e59a4935-1847-0410-ae03-e826735625c1

CMS2 now has two types of learnt clause evaluation

CryptoMiniSat2 now has two types of learnt clause activity measures.
This means that different type of problems can be effectively solved
with the same solver that uses radically different measures of learnt
clause effectiveness. There are some rough edges for the moment: it's
really difficult which type of instance we are dealing with. So, the
'heuristic' that decides is really dumb. You can find it in
RestarTypeChooser.cpp. If you have a more refined heuristic in mind,
please share it with me!

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@688 e59a4935-1847-0410-ae03-e826735625c1

Importing new version of CMS2

* bug with Conglomerate fixed. Conglomerate will in the future be
  callable in the middle of solving
* variable activity is now uint32_t. No more floating point code.
  This change also means a more conservative variable activity
  heuristic. Should help on most problems (but not crypto, I
  believe)
* Removed useless code around logging
* No more warnings on (deprecated) const char* to string conversion

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@687 e59a4935-1847-0410-ae03-e826735625c1

Don't clean non-existing CryptoMiniSat1 dir

Cleaning script doesn't need to clean the 'cryptominisat' directory
since that doesn't exist any more. The clean script failed because of
this, fixed.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@686 e59a4935-1847-0410-ae03-e826735625c1

Removing CryptoMiniSat ver. 1

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@685 e59a4935-1847-0410-ae03-e826735625c1

Merge branch 'cryptominisat1_removed_and_rest_cleaned'

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@684 e59a4935-1847-0410-ae03-e826735625c1

Updating CMS2 to fix two bugs

One was a bug relating to binarary xor-finding while doing failed
var searching: the xor-clauses were not cleaned beforehand.

The second bug was an inverted shrinking of memory contents in
operator= of Heap.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@683 e59a4935-1847-0410-ae03-e826735625c1

CMS2 update: Extending the conglomerated clauses was done too early. Also, some non-decision variables were set for no reason in the model

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@680 e59a4935-1847-0410-ae03-e826735625c1

Last commit contained some strange merging information that made a mess. Sorry, reverting.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@679 e59a4935-1847-0410-ae03-e826735625c1

Merge branch 'newcrypto'

updated CMS2 so that segfault will no longer happen when UNSAT is found
in the middle of a varreplacement. The clause database was left in an
undefined state, which caused ~Solver to double-free some clauses

no longer be create

Conflicts:
src/sat/cryptominisat2/PartHandler.cpp
src/sat/cryptominisat2/Solver.cpp
src/sat/cryptominisat2/Solver.h
src/sat/cryptominisat2/Subsumer.cpp
src/sat/cryptominisat2/VERSION
src/sat/cryptominisat2/VarReplacer.cpp
src/sat/cryptominisat2/mtl/Vec.h

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@678 e59a4935-1847-0410-ae03-e826735625c1

Importing the new cryptominisat

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@676 e59a4935-1847-0410-ae03-e826735625c1

bugfix. r671 re-enabled checking counter-examples. However it checks the "query" which is sometimes (always ?) left undefined by the smtlib parser.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@675 e59a4935-1847-0410-ae03-e826735625c1

Bugfix to r667. I discarded a variable instead of adding it into the solver map. This fixes the alvin.cvc problems (r666).

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@674 e59a4935-1847-0410-ae03-e826735625c1

Change a reference to a regular variable. This fixes an intermittent valgrind warning about accessing uninitialised memory

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@673 e59a4935-1847-0410-ae03-e826735625c1

* Bugfix. Fix the printed counterexample sometimes missing assignments, sometimes printing duplicate assignments.
* Updated the BoolVecToBVConst function to be faster.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@672 e59a4935-1847-0410-ae03-e826735625c1

Bugfix. r284 or earlier removed checking of counter-examples. i.e. -d did nothing.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@671 e59a4935-1847-0410-ae03-e826735625c1

If STP is compiled with minisat-core, add a command line option to enable simplifying minisat. This removes the need to separately compile a "simplifying minisat" version.

We now have two versions of STP: one for cryptominisat1/2 another for minisat/simplifying minisat.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@670 e59a4935-1847-0410-ae03-e826735625c1

Remove unsound-minisat as per Vijay's advice.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@669 e59a4935-1847-0410-ae03-e826735625c1

Add configuration options for selecting SAT solver, plus some related
cleanups to how scripts and Makefiles include and invoke each other.
Patch from Peter Collingbourne.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@668 e59a4935-1847-0410-ae03-e826735625c1

Fix for failure reported by Alvin Cheung (r666)

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@667 e59a4935-1847-0410-ae03-e826735625c1