]>
git.unchartedbackwaters.co.uk Git - francis/stp.git/log
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
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
projects / francis / stp.git / log