]>
git.unchartedbackwaters.co.uk Git - francis/stp.git/log
vijay_ganesh [Tue, 20 Oct 2009 00:44:40 +0000 (00:44 +0000)]
added an abstraction/refinement loop for clause-addition to the SAT solver
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@320
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 19 Oct 2009 18:25:20 +0000 (18:25 +0000)]
minor edits and indentation
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@319
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 18 Oct 2009 11:34:38 +0000 (11:34 +0000)]
Speed up grep0084.stp.cvc & grep0117.stp.cvc, by reducing unnecessary memory copying in the CNF generator
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@313
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 16 Oct 2009 18:24:56 +0000 (18:24 +0000)]
minor edits
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@312
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 16 Oct 2009 18:08:59 +0000 (18:08 +0000)]
minor edits
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@311
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 16 Oct 2009 18:06:45 +0000 (18:06 +0000)]
changed some files to fit into 80 characters terminal
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@310
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 15 Oct 2009 22:45:29 +0000 (22:45 +0000)]
Cleaned up the printing of bitblasted formula and clauses. This will help me figure out how efficient the bitblaster/cnf translator are
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@308
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 15 Oct 2009 21:52:58 +0000 (21:52 +0000)]
minor edit
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@306
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 15 Oct 2009 21:52:37 +0000 (21:52 +0000)]
marked completed tasks in the task-list
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@305
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 14 Oct 2009 20:27:36 +0000 (20:27 +0000)]
formatted using gnu style
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@304
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 14 Oct 2009 19:53:48 +0000 (19:53 +0000)]
All userdefined flags are now local to STPManager. not global anymore
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@303
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 14 Oct 2009 17:05:17 +0000 (17:05 +0000)]
code indented using emacs
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@302
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 13 Oct 2009 19:12:36 +0000 (19:12 +0000)]
push/pop now working through the c_interface. Clearalltabes has been implemented correctly and tested
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@300
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 13 Oct 2009 15:44:00 +0000 (15:44 +0000)]
added cleartables for each of the big classes
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@299
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 12 Oct 2009 21:12:00 +0000 (21:12 +0000)]
minor edits
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@298
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 12 Oct 2009 20:58:21 +0000 (20:58 +0000)]
removed ASTUtil.h and merged with UsefulDefs.h
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@297
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 12 Oct 2009 20:48:11 +0000 (20:48 +0000)]
replaced hash_map/hash_set with defines HASHMAP and HASHSET resp.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@296
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 11 Oct 2009 02:09:52 +0000 (02:09 +0000)]
minor edits
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@292
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 11 Oct 2009 02:06:21 +0000 (02:06 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@291
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 11 Oct 2009 01:41:31 +0000 (01:41 +0000)]
minor edits
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@290
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 11 Oct 2009 01:31:34 +0000 (01:31 +0000)]
minor edits
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@289
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 11 Oct 2009 00:57:35 +0000 (00:57 +0000)]
renamed BeevMgr to STPMgr
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@288
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 11 Oct 2009 00:12:49 +0000 (00:12 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@287
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 11 Oct 2009 00:12:23 +0000 (00:12 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@286
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 11 Oct 2009 00:11:39 +0000 (00:11 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@285
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 11 Oct 2009 00:07:43 +0000 (00:07 +0000)]
big reorganization almost complete. I believe there is a slight slowdown.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@284
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 6 Oct 2009 01:16:35 +0000 (01:16 +0000)]
moved all LET-variables related stuff into a separate class
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@282
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 5 Oct 2009 23:10:08 +0000 (23:10 +0000)]
reorganized ToCNF
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@281
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 5 Oct 2009 17:28:56 +0000 (17:28 +0000)]
more reorganization. introduced STPManager directory, and move BeevMgr class to it
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@280
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 2 Oct 2009 22:37:12 +0000 (22:37 +0000)]
minor edits
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@276
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 2 Oct 2009 22:27:30 +0000 (22:27 +0000)]
removed symbol table from AST
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@275
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 2 Oct 2009 21:39:34 +0000 (21:39 +0000)]
more AST reorganization
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@274
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 2 Oct 2009 21:36:33 +0000 (21:36 +0000)]
more AST reorganization
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@273
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 2 Oct 2009 21:19:59 +0000 (21:19 +0000)]
moved function defintions for AST classes to appropriate cpp files
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@272
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 2 Oct 2009 20:08:29 +0000 (20:08 +0000)]
massiv code cleanup. Created separate files for ASTNode, ASTInternal, ASTInterior, ASTSymbol, ASTBVConst
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@271
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 2 Oct 2009 15:21:03 +0000 (15:21 +0000)]
added logs
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@270
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 1 Oct 2009 18:08:32 +0000 (18:08 +0000)]
massive changes. Added a LESSBYTES_PER_NODE option. Cuts down the bytesize of nodes by more than 20%
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@269
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 30 Sep 2009 23:14:43 +0000 (23:14 +0000)]
shaved off 4 bytes from each ASTInternal node
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@268
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 29 Sep 2009 16:03:40 +0000 (16:03 +0000)]
fixed bug in c_interface bvconstExprFromInt
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@266
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 28 Sep 2009 18:14:38 +0000 (18:14 +0000)]
changed the var decay. It improved performace
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@265
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 27 Sep 2009 22:35:22 +0000 (22:35 +0000)]
added checks for bvconst construction. checks if the n_bits is adequate to represent the constant
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@262
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 27 Sep 2009 19:26:38 +0000 (19:26 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@261
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sat, 26 Sep 2009 19:37:00 +0000 (19:37 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@258
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sat, 26 Sep 2009 01:32:37 +0000 (01:32 +0000)]
minor
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@257
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 25 Sep 2009 20:13:02 +0000 (20:13 +0000)]
added more tests
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@256
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 24 Sep 2009 14:46:50 +0000 (14:46 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@253
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 24 Sep 2009 13:46:11 +0000 (13:46 +0000)]
minor edits
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@252
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 24 Sep 2009 10:47:08 +0000 (10:47 +0000)]
Different flex options as provided by Peter Collingbourne.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@251
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 23 Sep 2009 02:41:03 +0000 (02:41 +0000)]
* get biosat-rna.cpp compiling on my machine.
* add const to some char* in the c_interface to remove compiler warnings.
* %ld -> %llu to remove compiler warnings in tests.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@249
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 22 Sep 2009 16:46:44 +0000 (16:46 +0000)]
fixed the regression scripts so that we can run them one after another with one command
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@248
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 22 Sep 2009 00:43:54 +0000 (00:43 +0000)]
added new testing perl script. minor edits to Makefiles.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@247
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 21 Sep 2009 23:42:04 +0000 (23:42 +0000)]
All fixed. RNA example is running again. I had introduced some Abstraction-refinement code in AST.h. It seems to have pushed the system to limits of memory consumption
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@246
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 21 Sep 2009 21:34:38 +0000 (21:34 +0000)]
added biosat-rna.cpp file. It is crashing now. Previously it was running smoothly in 133 seconds
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@245
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 21 Sep 2009 18:26:39 +0000 (18:26 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@244
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 20 Sep 2009 15:47:09 +0000 (15:47 +0000)]
* Don't allow creation of zero-width bitvector literals. Previously bv0[0] would parse via the SMTLIB input language
* If optimisations were disabled, sign_extend[0], would segfault in the bitblaster.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@243
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 20 Sep 2009 13:46:04 +0000 (13:46 +0000)]
* Bug-fix. Prior checkin broke zero_extend by greater than the machine's unsigned size. So zero_extend[100] would fail.
* Remove old code from the parser.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@241
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 19 Sep 2009 13:40:13 +0000 (13:40 +0000)]
Remove BVZX. Bit vector zero extend is now replaced by a prepend with a zero bitvector at parse time.
The simplification rules over concatentations are better than those that were over BVZX.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@240
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 17 Sep 2009 15:40:50 +0000 (15:40 +0000)]
* -t times how long sending the clauses to the SAT solver takes.
* Remove unreachable code in the loop sending clauses to the SAT solver.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@239
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 17 Sep 2009 04:54:11 +0000 (04:54 +0000)]
* Add back -m32. All should now make at 32-bit
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@237
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 17 Sep 2009 04:37:49 +0000 (04:37 +0000)]
* Add -m32 flag to c-api-tests to get it compiling
* -t now tracks the bvsolver, and the substitution mapper (which sometimes takes a freakishly large amount of time).
* SimplifyCaches are no longer cleared at the start of topLevel simplify. Sometimes there is good stuff in there.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@236
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 16 Sep 2009 22:23:59 +0000 (22:23 +0000)]
minor edits to scrips/Makefile.common
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@235
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 16 Sep 2009 22:23:25 +0000 (22:23 +0000)]
minor edits to AST/Makefile
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@234
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 16 Sep 2009 00:50:50 +0000 (00:50 +0000)]
minor edits. Lot more work remains in optimizing FOR construct
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@232
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 15 Sep 2009 13:57:42 +0000 (13:57 +0000)]
Fixes an off-by-one defect introduced in #230
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@231
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 15 Sep 2009 12:49:45 +0000 (12:49 +0000)]
* Add signed & unsigned shifts to a test generator
* Speed up the shifting circuit, by treating specially bits beyond log2 of the bitwidth.
* During simplification if the shift amount is known, then remove the shift replacing it with a concat and extract.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@230
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 15 Sep 2009 02:39:39 +0000 (02:39 +0000)]
The constant evaluator can now evaluate shifts by amounts > MAX_INT. Prior, if an attempt was made to shift a value, by say, 2^100, it would fail because the shift amount was loaded into an integer.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@227
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 14 Sep 2009 14:42:42 +0000 (14:42 +0000)]
* Build by defualt a 32-bit executable.
* My last checkin doesn't compile. Get it compiling again.
The 64-bit version has twice the peak memory usage of the 32-bit version on testcase15.stp.smt.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@226
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 14 Sep 2009 14:28:29 +0000 (14:28 +0000)]
The result of the -t option (quick statistics), also gives solver time
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@225
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 14 Sep 2009 10:46:14 +0000 (10:46 +0000)]
Add a new class for tracking the runtimes. e.g. SimplifyTopLevel was called 5 times, and took 100ms.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@224
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 13 Sep 2009 21:10:54 +0000 (21:10 +0000)]
added FOR-construct tests
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@223
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 13 Sep 2009 21:08:23 +0000 (21:08 +0000)]
added parameterized boolean variables
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@222
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sat, 12 Sep 2009 21:11:26 +0000 (21:11 +0000)]
some changes to abs-refinement
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@221
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 11 Sep 2009 20:50:30 +0000 (20:50 +0000)]
minor edits
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@220
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 11 Sep 2009 02:38:17 +0000 (02:38 +0000)]
fixed some issues with FOR-construct
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@218
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 10 Sep 2009 19:40:49 +0000 (19:40 +0000)]
Added EXCEPT construct for the FOR-construct
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@217
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 10 Sep 2009 13:36:22 +0000 (13:36 +0000)]
Rough version of smtlib print back. The output version is form information only, it won't parse back in.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@216
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 10 Sep 2009 12:37:37 +0000 (12:37 +0000)]
Improve dependency generation:
* Don't delete the dependencies when making clean.
* Don't build the dependencies for automatically generated code.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@215
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 9 Sep 2009 20:14:44 +0000 (20:14 +0000)]
moved bitvec directory to const-evaluator. moved constantbv directory extlib-constbv
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@214
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 9 Sep 2009 20:06:17 +0000 (20:06 +0000)]
For-construct seems to be working
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@213
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 9 Sep 2009 15:08:24 +0000 (15:08 +0000)]
minor edits
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@212
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 9 Sep 2009 15:06:00 +0000 (15:06 +0000)]
There was link error due to versionString.cpp. It has been fixed
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@211
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 9 Sep 2009 14:36:19 +0000 (14:36 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@210
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 9 Sep 2009 14:35:40 +0000 (14:35 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@209
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 9 Sep 2009 11:06:19 +0000 (11:06 +0000)]
* Use svnversion at build time to insert the current global build revision into a version string.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@208
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 9 Sep 2009 07:22:51 +0000 (07:22 +0000)]
* Flatten AND, OR & BVPLUS completely via SimplifyTerm
* When simplifying don't cache leaves
* Disable the ReferenceCount (which prevents splitting of plus nodes), when using the CVC parser. This was making grep-slow-on-libstp.cvc very slow. SimplifyTerm() was taking more than 5 times as long to achieve a fixed point. The interaction is quite complicated, so for now, I've disabled it.
* Propagate BVUMINUS up through BVMULT.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@207
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 9 Sep 2009 04:00:00 +0000 (04:00 +0000)]
* Automatically build dependencies during make. This isn't perfect because the dependencies are only rebuilt when the source files change. They don't get rebuilt when the header files change. So changes to the dependencies inside headers wont be identified until the source file changes, triggering the dependencies to be rebuilt.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@206
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 9 Sep 2009 02:51:38 +0000 (02:51 +0000)]
* Delete the bvsolver object as soon as we're finished with it. This frees any references it might hold to otherwise dead objects before the SAT solving starts.
* Returns were missing on some helper functions.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@205
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 8 Sep 2009 16:52:00 +0000 (16:52 +0000)]
minor edits
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@204
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 7 Sep 2009 19:59:26 +0000 (19:59 +0000)]
added new directories abstraction-refinement and to-sat. moved files from AST to these directories
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@203
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 7 Sep 2009 19:26:10 +0000 (19:26 +0000)]
emacs indentation done
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@202
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 7 Sep 2009 01:33:04 +0000 (01:33 +0000)]
coded up abstraction-refinement
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@201
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 7 Sep 2009 00:26:29 +0000 (00:26 +0000)]
minor edits
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@200
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 7 Sep 2009 00:07:31 +0000 (00:07 +0000)]
changed regression names
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@199
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 6 Sep 2009 23:41:17 +0000 (23:41 +0000)]
changed regressall to regresscvc
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@198
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 6 Sep 2009 23:39:32 +0000 (23:39 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@197
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 6 Sep 2009 21:58:03 +0000 (21:58 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@196
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 6 Sep 2009 21:55:22 +0000 (21:55 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@195
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 6 Sep 2009 21:50:09 +0000 (21:50 +0000)]
Added capability to print back CVC-language input to STP
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@194
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 6 Sep 2009 21:02:01 +0000 (21:02 +0000)]
added vc_ExtractBit_One
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@193
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 6 Sep 2009 20:52:21 +0000 (20:52 +0000)]
minor changes to c_interface
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@192
e59a4935 -1847-0410-ae03-
e826735625c1
projects / francis / stp.git / log