]>
git.unchartedbackwaters.co.uk Git - francis/stp.git/log
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
trevor_hansen [Sun, 6 Sep 2009 15:53:00 +0000 (15:53 +0000)]
Adding SVN property to replace $Id$ with the version number
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@191
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 6 Sep 2009 15:35:43 +0000 (15:35 +0000)]
* Update the AST/Makefile to automatically build a "depend" file that contains the dependencies of all the source files each time the library is built. If the new version works OK, I'll update the other directories too.
* Move AST tests into a test sub-directory.
* Clean up the make file to remove redundant rules, and to use wildcard rules
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@190
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sat, 5 Sep 2009 00:31:17 +0000 (00:31 +0000)]
adding printback code.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@189
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sat, 5 Sep 2009 00:13:52 +0000 (00:13 +0000)]
changed the smt parser as well to return objects
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@188
e59a4935 -1847-0410-ae03-
e826735625c1
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
projects / francis / stp.git / log