git.unchartedbackwaters.co.uk Git

]> git.unchartedbackwaters.co.uk Git - francis/stp.git/log

smccam [Fri, 13 Feb 2009 01:15:05 +0000 (01:15 +0000)]

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

commit | commitdiff | tree

pgbovine [Wed, 4 Feb 2009 17:58:43 +0000 (17:58 +0000)]

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

commit | commitdiff | tree

vijay_ganesh [Mon, 2 Feb 2009 21:11:35 +0000 (21:11 +0000)]

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

commit | commitdiff | tree

trevor_hansen [Fri, 16 Jan 2009 15:28:25 +0000 (15:28 +0000)]

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

commit | commitdiff | tree

trevor_hansen [Tue, 13 Jan 2009 14:02:57 +0000 (14:02 +0000)]

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

commit | commitdiff | tree

trevor_hansen [Mon, 12 Jan 2009 13:23:35 +0000 (13:23 +0000)]

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

commit | commitdiff | tree

trevor_hansen [Sun, 11 Jan 2009 12:54:36 +0000 (12:54 +0000)]

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

commit | commitdiff | tree

trevor_hansen [Tue, 6 Jan 2009 12:38:33 +0000 (12:38 +0000)]

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

commit | commitdiff | tree

trevor_hansen [Tue, 6 Jan 2009 03:41:16 +0000 (03:41 +0000)]

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

commit | commitdiff | tree

trevor_hansen [Tue, 6 Jan 2009 02:31:09 +0000 (02:31 +0000)]

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

commit | commitdiff | tree

katelman [Tue, 30 Dec 2008 06:17:29 +0000 (06:17 +0000)]

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

commit | commitdiff | tree

vijay_ganesh [Thu, 18 Dec 2008 00:22:36 +0000 (00:22 +0000)]

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

commit | commitdiff | tree

vijay_ganesh [Thu, 18 Dec 2008 00:21:59 +0000 (00:21 +0000)]

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

commit | commitdiff | tree

vijay_ganesh [Wed, 19 Nov 2008 00:24:33 +0000 (00:24 +0000)]

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

commit | commitdiff | tree

vijay_ganesh [Tue, 18 Nov 2008 20:14:57 +0000 (20:14 +0000)]

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

commit | commitdiff | tree

vijay_ganesh [Tue, 18 Nov 2008 20:13:18 +0000 (20:13 +0000)]

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

commit | commitdiff | tree

katelman [Tue, 18 Nov 2008 18:36:25 +0000 (18:36 +0000)]

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

commit | commitdiff | tree

katelman [Tue, 18 Nov 2008 17:49:46 +0000 (17:49 +0000)]

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

commit | commitdiff | tree

smccam [Fri, 31 Oct 2008 23:28:04 +0000 (23:28 +0000)]

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

commit | commitdiff | tree

smccam [Fri, 31 Oct 2008 23:26:17 +0000 (23:26 +0000)]

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

commit | commitdiff | tree

smccam [Fri, 31 Oct 2008 23:24:01 +0000 (23:24 +0000)]

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

commit | commitdiff | tree

smccam [Fri, 31 Oct 2008 18:50:00 +0000 (18:50 +0000)]

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

commit | commitdiff | tree

smccam [Fri, 31 Oct 2008 18:45:04 +0000 (18:45 +0000)]

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

commit | commitdiff | tree

smccam [Fri, 31 Oct 2008 18:38:37 +0000 (18:38 +0000)]

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

commit | commitdiff | tree

smccam [Fri, 31 Oct 2008 18:36:07 +0000 (18:36 +0000)]

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

commit | commitdiff | tree

katelman [Wed, 22 Oct 2008 19:18:17 +0000 (19:18 +0000)]

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

STP Constraint Solver.

RSS Atom