Fix to the bvsolver. Some cases were missing when identifying monomials.

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

Bugfix in cbitp. Currently not enabled.

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

Fix error in experimental constant bit propagation code

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

Bugfix. Memory was sometimes read after it had been freed by the garbage collector

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

Fix. I thought the code I checked-in just now wasn't active. But it was. This patch adds a flag to disable the prior patch.

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

Changes to inactive by default code.

This patch makes the term-level simplifier, the bit-blaster and the constant bit propagation co-operate during simplification. If the cbitp or the bitblaster discover a new constant. Then the term-level simplifier will be re-ran.

I haven't experimented whether this is useful yet.

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

Remove some assertion checks from code that's not enabled by default.

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

Bugfix. STP returned the wrong answer when something like bitwidth of 1: (0 = (1+1)) made it to the bitblaster. Simplifying terms collapses (as we do now), collapses this down to (0 =0) which returns the correct answer. The bitvector solver didn't expect to see two constant in a plus.

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

minor changes to INSTALL instructions

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

Fix the build script

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

Remove variables from the configure script which controlled the choice of SAT solver

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

Remove binaries I checked in by mistake

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

Fix build. Forgot to checkin these

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

* Replace minisat 2 with minisat 2.2.
* Replace simplifying-minisat 2 with simplifying-minisat 2.2
* It's no longer necessary to compile cryptominisat separately. The choice of solver is controlled by a command line flag now.

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

Add regresssmtcomp2007 which runs the bitvector benchmarks from the 2007 contest

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

Changes to inactive code. Use simple AIG simplifications on complex problems.

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

Update to currently inactive code.

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

Code for AIG rewriting with ABC. This code is not currently enabled by default.

I'll enable it when I understand when it's useful.

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

Extra tests for inactive by-default code

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

Refactor. Remove unncessary code.

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

Change non-enabled code.

This improves the bounds aware multiplication encoding (which is not the default encoding for multiplication).

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

Improvement? FlattenKind now recursively flattens it's children.

I was surprised that it didn't already do this.

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

Should cause not runtime effects.

Add a new multiplication variant that uses bounds discovered during constant bit propagation to more efficiently encode multiplications.

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

Speedup. Reduce the number of times that SortByArith is called. Previously:
* If was explicitly called
* Then it was implicitly called when CreateTerm ran.
* Then it was implicitly called again when CombineLikeTerms called CreateTerm.

Remove an unecessary flatten.

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

Print out a not yet supported error.

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

Add a sorting network implementation. This code is not currently enabled so this patch should do nothing.

Sorting networks should have better propagation (at higher cost) than addition networks (which we currently encode multiplication to).

In my experiments the sorting networks aren't clearly better than the addition networks.

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

Cleanup. Remove experimental (not active) code.

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

Improve the encoding of the full adder used by the multiplication circuit.

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

Correct a comment

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

Bugfix. --output-CNF was broken when outputting with Cryptominisat. A signed / unsigned problem.

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

Fix slowdown.

r965 removed a cache update that caused bitblaster.cvc to run 10 times slower. This update adds back in the cache update as well as changes to ensure that by the end of SimplifyTerm the invariant that actualInput maps to something that hasBeenSimplified(output) holds for.

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

Speedup the bvsolver. Use the applySubstitutionMap function to apply the discovered replacements rather than using simplifyFormula. This means that the simplification caches don't need to be cleaned out (saving time).

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

Bugfix. The prior revision sometimes returned the wrong result (very rarely).

In the prior revision I removed some explicit calls to simplifyTerm.
Wrongly believing that the term was already simplified at the point.
To check that it was simplified I asserted the "hasBeenSimplified" function.
But the hasBeenSimplified function only checked that the term was present in the simplifyMap.
That is that simplifyTerm had been called on it.
Which isn't the same thing as being simplified.
i.e. term A is not simplified if in the SimplifyMap it's mapped to term B.
It's only simplified if A maps to A.

Some simplification functions expect their children to already be simplified.
This wasn't the case so we'd get the wrong answer.

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

Bugfix. Infinite loop. My fourth attempt to fix the problem introduced in r947. I've been careful this time.

Refactor. Remove explicit calls to SimplifyTerm if simplify_upfront is enabled. This is a precursor to removing many of the SimplifyTerm calls in the SimplifyTerm function, nearly all are redundant because at the end of the function we have:

    if (inputterm != output)
     output = SimplifyTerm(output);

i.e. we fixed point it.

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

Bugfix. Oops. When using the quick statistics (the -t option), record the time spent generating the CNF.

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

Speedup. I've measured the performance of bit blasted comparisons on a (single) test case. I've selected the fastest encoding.

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

Bugfix. Infinite loop. A third fix for r947.

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

Bugfix. STP may produce the wrong answer. Introduced revision 947.

I enabled creation of multiplication nodes with >2 children. But the DistributeMultOverPlus function ignores the third (and later) children.

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

Speed up of the unsigned division encoding. Update the runtimes for the different variants of unsigned division.

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

Refactoring.
* CreateSymbol now takes the indexWidth and the valueWidth.
* I've removed most of the calls to setIndexWidth.
* CreateSymbol has been moved into the NodeFactory class.

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

Bugfix. Stop a null pointer error.

The simplifier can create something like: (BVMULT 1 3 5). i.e. a mutliplication node of constants with arity > 2. This patch makes that work.

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

Further fixing of spurious printing in CryptoMiniSat

As per report by Trevor Hansen

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

Fixing verbosity-related problems in CryptoMiniSat2

Reported by Trevor Hansen

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

A QF_ABV division has been added to the smt-lib. Update parser to read, update printer to write it.

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

Bugfix. Properly print out the counter example of booleans.

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

Fix the build + extra options for constant bit propagation (not currently enabled).

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

Speedup. Flatten multiplications, sort, then re-assable into 2-arity functions. This detects some associativity.

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

Extra code (not enabled), for constant bit propagation.

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

Extra code (that's not currently enabled), so reduce the unncessary clearing of the simplification map during bit-vector solving.  This patch causes some instances to fail.

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

Output quick statistics if enabled, and exiting after generating the CNF.

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

Decision. This optimisation helps our cvc regressions but hurts our smtlib ones. So I'm taking it out..

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

Add the option to exit after generating the CNF. Currently only works for bit-vectors (which don't have abstraction refinement).

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

Bugfix. If a new-line occured in a string literal, it wasn't matched by the lexer, so would be printed out to the console.

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

Introduce vc_setInterfaceFlags function

This patch adds a vc_setInterfaceFlags function to the C interface
with one possible flag, EXPRDELETE, which is set by default.  The flag
controls whether the C interface deletes types and integer constant
expressions at vc_Destroy time.  It is intended that clients which
perform their own memory management of these objects will be able to
clear this flag.

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

Fix some small leaks when performing division by zero, and in the smtlib1 parser.

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

Only run the bvsolver if optimisations have been enabled. The bvsolver relies on optimisations being performed for correctness.

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

Fix the unit test script:
* To not explicitly call simplifying minisat (which isn't an option if compiled with cms).
* To remove comments and blank lines (which are introduced by AIG's conversion).

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

Bugfix. Remove a null pointer reference.

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

Simplify (bvdiv x x ) to one. Likewise for the other multiplication like operations.

Other changes are for constant bit propagation (aren't active yet).

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

Fix the building of the stp library.

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

Fix the build.

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

Neaten up the code for constant bit propagation. Note this code doesn't run by default, so this patch shouldn't change anything.

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

Bugfix. Fix a check to ensure that the type of nodes doesn't change for the worst.

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

* Interface changes for constant bit propagation. Not currently enabled.
* Add code to bitblast etc. for bvzx. BVZX can be created via the interface, and might not be simplified out before reaching the bitblaster.

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

Fix. stp.a didn't have necessary cbitp file included. Thanks to Peter Collingbourne for the patch.

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

Fix. The unit tests expect the cnf's to be called output_*.cnf. If going to CNF via AIGs it was called output.cnf

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

Revert. In r915 I removed the default -m32 flag by accident.

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

More getting ready for constant bit propagation. This code doesn't run, so nothing should change.

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

CryptoMiniSat can now be built

How to build CryptoMS:
1) install cmake
2) go to the "src/sat/cryptominisat2/" directory
3) create new dir: "mkdir build"
4) go to new dir: "cd build"
5) type "cmake ../"
6) type "make"
7) the "cryptominisat" binary is now in the directory

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

For low-cutoff speed reasons, it's best not to subsume learnts

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

Add the interface code for constant bit propagation.  This isn't all of the code, just the code required to interface with the bit blaster.

This code isn't called. So this patch doesn't change STP at all.

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

Cleaning up some bugs in CryptoMS

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

Free the memory allocatated to the AIGs before SAT solving.

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

Tiny speedup. Generate the encoding of multiplication slightly more efficiently.

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

I didn't enable capturing of quick statistics (the -t flag) for the time spent bitblasting when using AIGS.

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

Bugfix. The SMTLIB2 defines the outer bars (if present) to not be part of the symbol name.

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

Get cryptominisat2 compiling:

* Add a cutdown copy of the Boost library.
* Comment out most of the Cryptominisat2 custom code. I've changed the IFDEFs to cryptominisat__2, which leaves the code in, but which isn't defined.

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

Bitblast formula that don't contain arrays into and-inverter graphs. This uses the AIG implementation provided by the ABC package.

This has some advantages:
* The AIG nodes are smaller than our ASTNodes, so it uses less memory.
* The CNFs generated by ABC are smaller, so generally solving is quicker.

Some notes:
* I haven't made the CNF converter incremental, so bitblasting to AIGs is only enabled for bit-vector problems (which STP bitblasts eagerly).
* AIG re-writing isn't enabled yet.
* From prior experience some big problems fail in CNF encoding. All of our test cases pass though.

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

Correcting small bug in CMS2

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

Updating CMS2 to get rid of a small bug

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

Removing trailing code related to pools' #ifdefs in CryptoMS

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

Further updating of CryptoMiniSat2

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

Updating CryptoMiniSat2 to fix some minor bugs

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

Updating CryptoMiniSat2

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

Rename the bitblaster class fron BitBlasterNew to BitBlaster.

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

Refactor, getting ready for AIGs. This does add additional code, but that code isn't currently enabled.

* Provide a base class for ToSAT. Bitblasting via ASTNodes and AIGs both implement this class.
* BBNodeManagerAIG creates AIGs that are wrapped with a BBNode object.
* BitBlastNew is now templated on the node type and the node factory.

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

Speedup. Generate nicer circuits for unsigned division.

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

Change how the counter example is built. Previously the counter example relied on specific nodes existing that wont be created when we bitblast via AIGs.

I needed to reimplement the code to print the sat model too. I didn't preserve the format. I suspect though no one is parsing it.

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

Speedup. Add solving for xors to the bitvector solver.

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

Speedup. if (xor a b) is found, replaced a with (not b) throughout.

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

Speedup. Sort EQ nodes. This prevents duplicate nodes like (= 0 a), (=a 0), from being created. The bvsolver expected nodes reversed to how they are now created.

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

Speedup. Don't push extracts through ites. Sometimes this may be good to do. But usually not.

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

Default to bash shell rather than sh for some calls. The call to cat was failing on a redhat machine with an "argument too long error". Hopefully this fixes it.

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

Speedup. Revert back to minisat's default parameters.

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

Speedup. Flatten ands at the start of the bvsolver.

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

clean up two regression log names

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

Speedups.

* The substitution map now substitutes for (IFF SYMBOL SYMBOL)
* sim.smt2 is the test case to check the above substitution is working.
* The ArrayTransformer creates fewer new nodes.

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

Speedups.
* Call topLevel simplify only if something has changed.
* If there is a symbol on the rhs put it on the lhs, which simplifies more eqns.

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

Speedups.
* Cache the max, one and zero values inside the Create__Const() functions.
* Return a reference from the [] operator to reduce unncessary copies.

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

Measure the difficulty of formula by using a simple function, that amongst other things counts the number of multiplications in the input. If after simplifications the difficulty has increased. Then the original formula is used instead of the not-simplified one.

This is a very rough way of performing DAG aware simplifications.

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