]>
git.unchartedbackwaters.co.uk Git - francis/stp.git/log
vijay_ganesh [Fri, 4 Sep 2009 23:47:29 +0000 (23:47 +0000)]
Major code refactoring. Moved main.cpp to main. Globals to Globals.cpp. Also made the parser return an actual object for the AST
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@187
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 4 Sep 2009 19:08:11 +0000 (19:08 +0000)]
cleaned up FOR-construct parsing, and printing
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@186
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 4 Sep 2009 18:11:36 +0000 (18:11 +0000)]
Basic finite-FOR loop coded up. Testing/Debugging under way
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@185
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 4 Sep 2009 13:56:44 +0000 (13:56 +0000)]
Header file I meant to checkin with #180
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@184
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 4 Sep 2009 13:48:51 +0000 (13:48 +0000)]
* The prior version would not compile without -NDEBUG because it was null instead of NULL
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@183
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 4 Sep 2009 13:27:00 +0000 (13:27 +0000)]
Reverted to version 164. I didn't realise Vijay runs these.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@182
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 4 Sep 2009 12:42:25 +0000 (12:42 +0000)]
* Whitespace changes to reduce compiler warnings.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@181
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 4 Sep 2009 12:37:55 +0000 (12:37 +0000)]
* Remove NEQ. NEQ is converted by the CVC parser into NOT(=(..)). This makes our internal format slightly more canonical. If this change works OK, I'd like to later remove: NAND, NOR, etc.
* Move the sat headers into sat/sat.h. AST.h now contains a forward declaration of just the types it needs. This should speed up compilation.
* Reduce the number of compiler warnings.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@180
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 3 Sep 2009 23:47:32 +0000 (23:47 +0000)]
added enum for Solver returntype
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@179
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 3 Sep 2009 22:17:47 +0000 (22:17 +0000)]
more cleanup
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@178
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 3 Sep 2009 21:59:12 +0000 (21:59 +0000)]
more cleanup
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@177
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 3 Sep 2009 20:15:06 +0000 (20:15 +0000)]
moved many BeevMgr and related classes print functions into a separate file printers/AssortedPrinters.cpp
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@176
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 3 Sep 2009 20:14:06 +0000 (20:14 +0000)]
moved many BeevMgr and related classes print functions into a separate file printers/AssortedPrinters.cpp
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@175
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 3 Sep 2009 19:22:47 +0000 (19:22 +0000)]
added scripts to do emacs formatting
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@174
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 3 Sep 2009 17:53:59 +0000 (17:53 +0000)]
Moved abstraction refinement function to a separate file
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@173
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 3 Sep 2009 17:38:12 +0000 (17:38 +0000)]
lots of small useful edits. Has some untested FOR-construct code as well
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@172
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 3 Sep 2009 08:32:16 +0000 (08:32 +0000)]
Adding version number to help output of the binary.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@171
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 3 Sep 2009 08:28:45 +0000 (08:28 +0000)]
Trying to get version number in the executable
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@170
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 3 Sep 2009 08:25:29 +0000 (08:25 +0000)]
Setting svn:keywords property on main.cpp. Trying to get version number in the executable.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@169
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 2 Sep 2009 22:32:47 +0000 (22:32 +0000)]
Removed lots of useless code. The FOR loop code is still being written
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@168
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 2 Sep 2009 12:53:15 +0000 (12:53 +0000)]
Deleting SimplifyTermAux(), which seems redundant.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@167
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 1 Sep 2009 04:09:37 +0000 (04:09 +0000)]
* lhsminusrhs(..) does not perform its simplification if it will increase the number of PLUS nodes (which are expensive).
* The Transform functions are now mostly non-member. The cache is created on entry to TopLevel and deleted on exit.
* regress_smt only checks the smt-test folder, not its subfolders! These regression tests take under a minute to run.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@165
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 31 Aug 2009 19:40:25 +0000 (19:40 +0000)]
minor edits
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@164
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 31 Aug 2009 18:00:05 +0000 (18:00 +0000)]
removed SMTLIB C-flag
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@163
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 30 Aug 2009 10:44:51 +0000 (10:44 +0000)]
When using the SMT parser (x % 0) and (x /0) both evaluate to 1. This isn't in keeping with the semantics of the SMTLIB language which says that the formula should only be satisfiable for all interpretations of division by zero (rather than just (x/0 ==1)).
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@162
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 29 Aug 2009 14:26:52 +0000 (14:26 +0000)]
* Test file generator for mul, div, rem.
* Speed up the signed div, signed mod & signed rem encodings.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@160
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 28 Aug 2009 21:41:03 +0000 (21:41 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@159
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 28 Aug 2009 21:38:48 +0000 (21:38 +0000)]
made some minor edits to info files
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@158
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 28 Aug 2009 21:22:30 +0000 (21:22 +0000)]
comments added to vc_cvcParseExpr in c_interface
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@157
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 28 Aug 2009 20:55:08 +0000 (20:55 +0000)]
minor Makefile edits
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@155
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 28 Aug 2009 20:44:33 +0000 (20:44 +0000)]
Changed Makefile so that cvc/smt/c-api regressions have individualized names
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@154
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 28 Aug 2009 20:28:03 +0000 (20:28 +0000)]
Introduced a C API regression option 'make regress_c_api'. Only one test fails: due to printing error in cvc-2-C
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@153
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 28 Aug 2009 19:40:51 +0000 (19:40 +0000)]
Got rid of the annoying warning in AST.cpp compilation due to more than 64 bit shifting. No error. The compiler was over-zealous
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@152
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 28 Aug 2009 18:37:34 +0000 (18:37 +0000)]
More minor changes to Makefiles. Added Unsound
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@151
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 28 Aug 2009 18:36:00 +0000 (18:36 +0000)]
More minor changes to Makefiles. Added Unsound
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@150
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 28 Aug 2009 18:25:48 +0000 (18:25 +0000)]
added FOR loop construct to parser.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@149
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 28 Aug 2009 18:24:24 +0000 (18:24 +0000)]
Minor changes to make scripts. Since files got moved around, the libstp.a was broken. The c-api-tests were failing. everything seems to work now
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@148
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 28 Aug 2009 12:42:32 +0000 (12:42 +0000)]
Fix a small (24 byte) memory leak per call to CNF generation.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@147
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 27 Aug 2009 05:15:44 +0000 (05:15 +0000)]
Moving the Lisp & Presentation Language (PL) printers to the "printer" namespace.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@146
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 24 Aug 2009 04:52:52 +0000 (04:52 +0000)]
* Stop compiler warnings from the smtlib parser.
* Fix "make clean" to not try to delete a non-existant path.
* Fix "make clean" to remove all the .o files.
* Delete config.info from svn.
* Pre-size some vectors during CNF generation. When solving a single 64-bit multiply, this reduces total runtime by about 5%.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@143
e59a4935 -1847-0410-ae03-
e826735625c1
katelman [Sat, 22 Aug 2009 16:26:55 +0000 (16:26 +0000)]
Fixed -x bug in the CNF converter, and added a test, rna2.cvc, to the
regressions. All of the modified files in the various branches, I am not sure
about, except that since they are my branches, it doesn't really matter.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@142
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 21 Aug 2009 23:19:42 +0000 (23:19 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@141
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 21 Aug 2009 23:10:21 +0000 (23:10 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@140
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 21 Aug 2009 22:28:05 +0000 (22:28 +0000)]
added rna2.cvc to tests/bio-tests dir
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@139
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 21 Aug 2009 22:27:18 +0000 (22:27 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@138
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 18 Aug 2009 19:22:35 +0000 (19:22 +0000)]
added an option for pure binary printing
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@137
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 14 Aug 2009 17:20:47 +0000 (17:20 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@135
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 14 Aug 2009 17:11:05 +0000 (17:11 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@134
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 14 Aug 2009 17:02:47 +0000 (17:02 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@133
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 14 Aug 2009 16:57:27 +0000 (16:57 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@132
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 14 Aug 2009 16:47:10 +0000 (16:47 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@131
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 14 Aug 2009 16:31:36 +0000 (16:31 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@130
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 14 Aug 2009 16:26:42 +0000 (16:26 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@129
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 14 Aug 2009 16:24:42 +0000 (16:24 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@128
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 14 Aug 2009 16:10:10 +0000 (16:10 +0000)]
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
vijay_ganesh [Thu, 13 Aug 2009 16:36:57 +0000 (16:36 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@121
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 12 Aug 2009 23:24:32 +0000 (23:24 +0000)]
minor changes
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@119
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 12 Aug 2009 19:09:36 +0000 (19:09 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@118
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 12 Aug 2009 16:54:33 +0000 (16:54 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@116
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 12 Aug 2009 16:08:32 +0000 (16:08 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@115
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 12 Aug 2009 15:33:20 +0000 (15:33 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@114
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 12 Aug 2009 15:02:44 +0000 (15:02 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@113
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 11 Aug 2009 22:54:03 +0000 (22:54 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@112
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 11 Aug 2009 21:36:15 +0000 (21:36 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@111
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 11 Aug 2009 17:22:08 +0000 (17:22 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@110
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 11 Aug 2009 17:19:45 +0000 (17:19 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@109
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 11 Aug 2009 17:18:04 +0000 (17:18 +0000)]
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
vijay_ganesh [Tue, 11 Aug 2009 17:11:54 +0000 (17:11 +0000)]
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
vijay_ganesh [Tue, 11 Aug 2009 16:18:36 +0000 (16:18 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@106
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 11 Aug 2009 16:10:55 +0000 (16:10 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@105
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 11 Aug 2009 16:03:46 +0000 (16:03 +0000)]
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
trevor_hansen [Tue, 11 Aug 2009 07:02:50 +0000 (07:02 +0000)]
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
vijay_ganesh [Fri, 7 Aug 2009 18:17:22 +0000 (18:17 +0000)]
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
trevor_hansen [Sat, 1 Aug 2009 18:04:12 +0000 (18:04 +0000)]
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
trevor_hansen [Sat, 1 Aug 2009 17:46:10 +0000 (17:46 +0000)]
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
trevor_hansen [Sat, 1 Aug 2009 16:12:17 +0000 (16:12 +0000)]
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
trevor_hansen [Wed, 29 Jul 2009 04:03:44 +0000 (04:03 +0000)]
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
trevor_hansen [Wed, 29 Jul 2009 02:32:05 +0000 (02:32 +0000)]
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
trevor_hansen [Tue, 28 Jul 2009 11:14:04 +0000 (11:14 +0000)]
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
trevor_hansen [Mon, 27 Jul 2009 15:35:56 +0000 (15:35 +0000)]
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
trevor_hansen [Mon, 27 Jul 2009 13:16:22 +0000 (13:16 +0000)]
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
trevor_hansen [Mon, 27 Jul 2009 11:59:44 +0000 (11:59 +0000)]
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
trevor_hansen [Sat, 25 Jul 2009 06:14:49 +0000 (06:14 +0000)]
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
trevor_hansen [Thu, 23 Jul 2009 14:03:09 +0000 (14:03 +0000)]
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
trevor_hansen [Thu, 23 Jul 2009 11:12:04 +0000 (11:12 +0000)]
* 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
trevor_hansen [Tue, 21 Jul 2009 05:20:44 +0000 (05:20 +0000)]
* 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
trevor_hansen [Thu, 16 Jul 2009 06:24:43 +0000 (06:24 +0000)]
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
trevor_hansen [Sat, 23 May 2009 15:11:23 +0000 (15:11 +0000)]
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
trevor_hansen [Sat, 23 May 2009 14:37:26 +0000 (14:37 +0000)]
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
trevor_hansen [Sat, 23 May 2009 14:26:17 +0000 (14:26 +0000)]
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
ar2rd [Sun, 10 May 2009 08:51:16 +0000 (08:51 +0000)]
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
trevor_hansen [Fri, 8 May 2009 14:45:22 +0000 (14:45 +0000)]
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
trevor_hansen [Tue, 28 Apr 2009 17:09:20 +0000 (17:09 +0000)]
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
katelman [Tue, 28 Apr 2009 14:53:23 +0000 (14:53 +0000)]
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
katelman [Mon, 27 Apr 2009 20:30:16 +0000 (20:30 +0000)]
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
trevor_hansen [Sun, 19 Apr 2009 13:05:21 +0000 (13:05 +0000)]
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
trevor_hansen [Sat, 18 Apr 2009 15:23:04 +0000 (15:23 +0000)]
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
trevor_hansen [Sat, 11 Apr 2009 08:25:49 +0000 (08:25 +0000)]
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
vijay_ganesh [Mon, 23 Mar 2009 18:09:02 +0000 (18:09 +0000)]
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
smccam [Fri, 13 Feb 2009 01:36:20 +0000 (01:36 +0000)]
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
projects / francis / stp.git / log