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

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

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

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

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

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

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

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

added directory for QF_BV examples

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

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

minor changes

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

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

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

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

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

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

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

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

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

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

moved regression logs and TALKS directories

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

moved sources into the src directory

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

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

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

made some changes to the MiniSAT Makefiles

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

Improve type checking for BVZX & BVSX.

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

added some smt tests as sample for users

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

I broke the division family in #100. Fixing.

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

Hack to avoid some of the division by zero errors that occur when evaluating the models that are produced.

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

Clear the simplify maps after each transformation of div/mod/rem. This reverts back a change I tentatively made. Not clearing the simplify maps after transforming means they will be in memory during SAT solving. Which is a very bad idea.

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

Pull up ITEs when two ITEs with the same conditional are arguments to a binary operation.

e.g. turns (bvslt (ite a  b c) (ite a d e)) INTO (ite a (bvslt b d) (bvslt c e)

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

Fix some write over ite cases.

Some arrays still cause infinite loops because the bvsolver stores mappings that
 self-refer into the SolverMap. For example b = read(B, select(A,b)). arrayBroke
n1.smt in misc-tests is such an example.

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

Fixes defects in how arrays, especially writes over ITE expressions work.  I generated 25,000 problems with the attached array generator. All files pass if optimisations are disabled. There are still defects in the array simplification code.

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

Signed right shift is implemented. Disable two very expensive assertion functions.

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

Implementation of rotate_left & rotate_right

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

Partial fix of bvsmod, bvsrem. Both operations still report spurious division by zero errors. They work much better than they used to. But not perfectly. See the test cases in misc-tests for examples they currently fail on.

Also, updated BVTypeCheck to return a boolean (so it is easy to use in asserts()). A trivial recursive typecheck function.

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

No semantic change. Automatically layout the code using Eclipse. The layout configuation file is added to the root directory "format_config.xml"

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

Fix for: "array_simple_broken.smt" values were incorrectly cached.

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

* When parsing SMTLIB format. Consider :formula and :assumption to be the same. Previously we took just the final :formula, discarding the prior ones. There shouldn't be multiple :formula elements, but there sometimes are.
* Remove some old/odd array accesses synatax.

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

* In SMTLIB parsing mode, warn if the expected and actual satisfiability differ.
* Fixed a memory leak in ClearTables(), ClearCaches().
* Added back the "if_then_else" token which some SMTLIB benchmarks rely on
* Removed unnecessary tokens from the lexer.

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

Move printers to a new namespace. Create a DOT graph format printer. Add extra warnings during compilation.

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

Propositional ITEs as per SMTLIB.

* Previously the "if_then_else" function not the "ite" function handled "then" and "else"'s which were propositional. Now the "ite" does both.
* Remove deprecation warnings.. Will fix later.
* Fix the BVTypecheck for ITEs.

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

Updating install message to describe how to get the regression tests.

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

Removing the "broken" directory. The contents of this directory have already been moved to /stp-tests/smt-problems

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

Fixed path to testcases in bin_tests.smt to  use current SVN tree structure.

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

bug-fix. Disable rewritting multiplication by constants

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

bug fix. Falling through BVMULT as it should. Removing bit constant propagation for Equality, going to replace this anyway (it doesn't look like it works for CVC? )

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

make regress now points to ../../stp-tests/test

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

IMPORTANT:

STP appears to be failing about half of the regressions in stp-tests/test. I
have just noticed this an made no attempt to fix it. I suspect it is due to
recent changes, as my personal branch 02_07_2009 does not have the same
problem.

OTHER:

I fixed a CNF conversion memory bug. IMPLIES and ITE cases were not setting the
sibling rename flag correctly, well, at all.

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

small bug fixes for problems introduced the last checkin.

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

Simplifications to speed up convert-tiff2jpg-query-1831.smt by >100,000 times.

* Some SMT-LIB format outputting of expression.
* Parsing arbitary length bitvector input strings via the C-interface.
* No more memory leaks from the _letid_expr_map & co.
* const& to reduce copy constructor usage in BVTypeCheck.
* Checks for equality on some fixed bits. e.g. (= bv0[16] (concat bv1[15] x)) == false.
* Reduces multiplications with leading 1's to a minus. e.g. 255*x == -1*x.

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

Reset simplify and expression hashmaps when clearing.

If a hashmap got very big, some methods like clear would take a long time (using the hasmap that is linked to on my machine). The clear()
function traverses each of the buckets in the hashmap seeing whether it had children. If the hashmap previously had millions of elements, even if it
now contains just a single element, then there would still be millions of buckets. The clear() function would take much longer than it needed to.

These changes were inspired by testcase15.stp.smt. On my machine, this patch speeds up STP on that benchmark by 20 times.

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

changed Makefile.in

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

Fix a couple of memory leaks that existed even if you did
vc_Destroy(): make a constant table used in the bitvector code static,
and delete temporary ASTNode objects in vc_simplify. A simple
createVC, build expression, simplify, destroy loop (test included) now
can run forever without leaking.

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

svn:ignore some new automatically-generated source files.

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

added functionality for converting CVC to C code

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

fixed Makefile.in

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

USER VISIBLE CHANGE: smtlib parser now enabled with "-m" flag.

A common makefile builds both parsers. -m is a terrible choice for
switch, but at present we only allow one character switches..

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

Fix off-by-one in bitvector right shift.

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

Right shift by a variable amount. Add two broken SMT files.

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

Allow >32-bit bit-vector constants on 32-bit machines.

The previous changes worked on 64-bit, not 32-bit machines. When I
compiled with -m32 it broke. This patch fixes it.

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

Left shift, >32 bit constants, fixed zero_extend, fixed (?) SBVREM.

Now left shifts by a variable amount. Previously the shift amount needed to a constant.

The smtlib parser reads bitvector constants into strings rather than into ints. This allows formula to
contain constants greater than the size of the machine's integer.

Fixed zero_extend. I didn't add code for it into the SimplifyTermAux function. SBVREM was sometimes failing
because it also wasn't included in the same function. Added it in. Not sure what the function does though..

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

Added zero_extend function. Renamed bvdiv to bvudiv as per specification. Fixed off-by-one check in BV_SX.

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

Fix compiling of the SMT-LIB Parser, Fix regression test script on bash.

The make files for the smtlib parser referred to to old locations of the SAT solver. The regression tests used
lots to many arguments to ulimit, it didn't run in my bash shell.

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

Fixed correctness bug in TermToConstTermUsingModel. CounterExampleMap
originally gets a copy of SubstitutionMap by way of SolverMap, and since
SubstitutionMap may not have fully reduced terms, we need to call
TermToConstTermUsingModel on anything read from CounterExampleMap. This was not
done for an array read case.

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

added parsing capability in c_interface

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

added parsing capability in c_interface

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

added some slow tests

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

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

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

actually pushing this copy out for realase...

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

More test directory cleanup. This version will be released.

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

Add an OPTIMIZE Makefile flag to make it easier to enable optimization
or debugging without otherwise breaking the build. Plus some other
cosmetic changes to Makefile comments.

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

Add -DTR1_UNORDERED_MAP, analogous to -DEXT_HASH_MAP, to allow use of
another, newer, quasi-standard STL hash table class.

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

Die with an explicit error message if the user tries a multi-character
option, rather than silently ignoring the remaining characters

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

Add svn:ignore properties for a number of files that are automatically
generated in the build process, so they don't clutter the output of
"svn stat".

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

Remove from SVN files that are automatically generated in the
configure and build processes. Copy the changes to Makefile back to
the original Makefile.in. After this change, you'll need to re-run
"configure".

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

Fix a couple of apparent precedence problems in AST (pointed out by
GCC warnings). Interestingly, these don't seem to change any regression
results.

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

Include <cstring> in ASTUtil.h, for its use of strcmp(). Good
practice, and required by picky newer versions of g++.

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

Round $n$ as I try to incorporate my work from the summer. Major updates
include (a) the newest version of MiniSat, (b) improved CNF conversion, and (c)
various other improvements.

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