* Add containsArrayOps(..) to check if any array terms are in the graph.
* Add missing types to the typecheck function. Clean up the type check function.

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

Fix the build.

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

Add a new function to replace using the substitution/solver map. It's not currently used by anything. So this checkin does nothing.

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

Removing duplicate files

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

Remove bio tests from regressstp. They are all included in regressbio.

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

Adding realistic expected times to these test cases

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

Bugfix. The script that was called by regressstp didn't record errors when some test cases failed. So I've removed it, and use the generic test runner instead. There are two differences: multiples log files are now created, and the timeout is 180 sec.

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

Speedup. Better cache the variables that are discovered when looking for duplicate symbols.

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

Use simplifying minisat for unit tests.

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

Bugfix. Simplifying minisat wasn't using the separate malloc/free routines.

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

Speedup/bugfix. Change how duplicate symbols are searched for. This fixed failing2.smt

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

Short cut on constant evaluation

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

Bugfix. Keep track of which symbols* have been deleted. Lots of them are duplicated in the map.

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

Don't perform simplifications when creating the substitution map. I'm not sure if this is justified, but it makes STP easier to understand. I'll check if it's useful.

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

Reduce memory usage. Clear out the caches from the bvsolver before calling the SAT solver.

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

Fix grammar. Extra assertion.

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

Speedup. Remove some unnecessary tests.

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

Refactor. Make the TermOrder function a non-member function with the SubstitutionMap class.

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

Speedup. Shortcut if the thing we are simplifying is already a constant.

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

Speedup. The bvsolver now uses a reduced version of the ASTNode graph which contains nodes just for nodes where the number of descendant symbols changes.

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

Check for duplicate variables using a different function

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

Bugfix. Variables were reported as only occuring a single time, when they actually occured multiple times.

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

Refactor & slight performance improvement for the bvsolver.

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

Bugfix. Fix rotate_left and rotate_right to take the modulus of the shift amount. I'd misinterpreted the specification.

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

Speedup. When printing out the counter example, don't call the toplevel print (which does lots of extra work). Instead call the low level print.

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

Speedup. Reduce the amount of checking that the bvsolver performs.

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

Speed up VarSeenInTerm(..) slightly.

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

Add some unit tests (which run when regressall is run) to check that simplifications are turning problems into TRUE or FALSE.

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

Bugfix. Enable the same options for when the parser is automatically detected based on filename, and when the parser is explicitly specified.

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

Change the properties so that SMTLIB2 format files are ignored.

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

Bugfix. Save the value of print counter example as per the bug report from  Markus Groß

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

Fix regresscapi. This file wasn't checked in

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

Fix the build. Add doug Lea's malloc implementation

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

Put the clauses of the SAT solver in a separate heap. This reduces the number of cache misses in the inner loop of the SAT solver, but increases the amount of memory STP uses.

I'm not yet sure if the extra memory usage is justified.

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

Free up more memory before SAT solving. In particular this deletes the Tseitin variables before calling the SAT solver. This makes good sense for problems that aren't solved by abstraction / refinement. However, I'm not sure how it impacts difficult array problems.

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

Fix. I didn't update al l the function calls I should have in r832

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

Remove no longer used bitblaster

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

Remove the experimental bvsolver. I've copied its changes into the main bvsolver.

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

* Make GetUnsignedConst a member function of ASTNode.
* In GetUnsignedConst check the position of the maximum bit only if the size is > , not >=

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

Refactoring. Move all the substitutionmap functions into the one class.

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

This makes SimplifyTerm idempotent. My hope is that this will reduce the number of times that the toplevel function needs to be called. If a term at the bottom of the graph doesn't map to itself when SimplifyTerm is run, then all the nodes above it will need to be re-created next time SimplifyTerm is called on the graph.

This patch adds an assertion function that isn't enabled.

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

Adds a simplification rule to replace BVANDS with zeroes at the front with a CONCAT.

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

bugfix. Constraints were ignored when they should have been.

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

Bugfix. Recursively simplify array ITES.

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

Add back code I removed in the last revision. Without this code fd_query_cheung2010.cvc timesout.

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

Bugfix. Simplify the proposition of array-ITEs. I don't simplify the "then" and "else" branch so I'm not sure if this fixes all the problems.

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

* In the bvsolver perform cheap tests which maybe short-cut before expensive tests.
* Lazily count the number of symbols in the bvsolver.

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

Bugfix. Avoid creating cycles with the bvsolver.

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

Bugfix. The bvsolver would replace a variable with an equation that contained that same variable. It did so because there was a special case that let it. I removed the special case.

I don't understand why the special case was there, so aren't sure if this will slow down some other instances?

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

Copy the cleaner new SplitEven_into_Oddnum_PowerOf2 function from bvsolverExp. I'm comparing the values from the old and new version of the function still.

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

Last commit was wrong. Importing again CryptoMiniSat-'Cluster56'

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

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