]>
git.unchartedbackwaters.co.uk Git - francis/stp.git/log
trevor_hansen [Mon, 27 Jun 2011 02:12:57 +0000 (02:12 +0000)]
Adds the push(n) and pop(n) instructions to the SMTLIB2 command language. Previously hitting the EOF would trigger a check for satisfiability. Now, you need to explicitly call (check-sat).
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1357
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 26 Jun 2011 16:23:55 +0000 (16:23 +0000)]
Move the filename counter out so it's saved between CNF converter objects.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1356
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 26 Jun 2011 15:14:31 +0000 (15:14 +0000)]
Improvement. Additional simplification rules.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1355
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 23 Jun 2011 06:06:59 +0000 (06:06 +0000)]
Fix. Look for fatal errors when running tests.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1354
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 23 Jun 2011 02:17:24 +0000 (02:17 +0000)]
Improvement. Simplifying minisat now uses the advanced CNF generator by default.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1353
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 22 Jun 2011 06:28:23 +0000 (06:28 +0000)]
Improvement. Create fewer clauses when creating an array axiom. I was adding extra variables that weren't required.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1352
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 21 Jun 2011 14:06:48 +0000 (14:06 +0000)]
Automatically format this code. No semantic change.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1351
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 21 Jun 2011 14:04:48 +0000 (14:04 +0000)]
Check axioms for indexes in order of the number of constants that they have. Adds some extra code for applying all the axioms that is currently disabled..
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1350
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 20 Jun 2011 14:15:13 +0000 (14:15 +0000)]
Improvement. During abstraction refinement process arrays in order of the number of indexes.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1349
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 20 Jun 2011 05:26:31 +0000 (05:26 +0000)]
Fix. I forgot to remove the descriptions of -e -f from help.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1348
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 20 Jun 2011 05:17:02 +0000 (05:17 +0000)]
Remove the code for the not-working FOR construct.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1347
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 20 Jun 2011 04:29:10 +0000 (04:29 +0000)]
Vijay advised we aren't going to do fors.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1346
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 19 Jun 2011 09:06:06 +0000 (09:06 +0000)]
Use the advanced CNF generator to encode array problems into CNF. Array axioms are generated by hand. NB. This slows down the CVC regressions substantially. Adding about 40 seconds to them. The CVC array problems are very easy, so the extra effort in generating a better CNF is wasted.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1345
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 16 Jun 2011 05:31:00 +0000 (05:31 +0000)]
Add boost to the licence, fix bitvector description.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1344
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 16 Jun 2011 03:54:40 +0000 (03:54 +0000)]
Bugfix. Fix the semantics of BVSMOD to always give the remainder rounding towards zero.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1343
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 16 Jun 2011 02:19:27 +0000 (02:19 +0000)]
Speedup for easy instances. Don't call the SAT solver if we already know the problem is true/false.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1339
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 14 Jun 2011 12:53:10 +0000 (12:53 +0000)]
Add cloud9 test cases.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1337
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 9 Jun 2011 04:28:54 +0000 (04:28 +0000)]
A windows patch to r446 from Hume.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1336
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 12 May 2011 04:56:59 +0000 (04:56 +0000)]
Improvement. Make error checking more normal.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1335
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 12 May 2011 04:28:04 +0000 (04:28 +0000)]
Extra simplification rule.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1334
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 11 May 2011 05:17:11 +0000 (05:17 +0000)]
Extra test cases that simplify down to nothing.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1332
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 11 May 2011 05:14:36 +0000 (05:14 +0000)]
ITE context is mostly bad. Now disabled by default.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1331
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 11 May 2011 04:24:39 +0000 (04:24 +0000)]
No longer default to the simple CNF generator for big AIGs, i.e >=2Million nodes. We used to do this because of a bug(?) now fixed in ABC.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1329
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 11 May 2011 04:23:04 +0000 (04:23 +0000)]
Improvement. Exit-after-cnf would exit after sending the CNF to the SAT solver. We used to read the CNF back out of the SAT solver, but don't any longer, so there's no reason to do this.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1328
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 11 May 2011 04:15:15 +0000 (04:15 +0000)]
Fix. Creating the node (v + v), where v is greater than 64 bits would fail.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1326
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 11 May 2011 03:34:42 +0000 (03:34 +0000)]
Bugfix. Arithmetic shifts by constants that didn't fit in 32-bits would cause an assertion error.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1323
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 11 May 2011 01:57:12 +0000 (01:57 +0000)]
Revert the change to run_tests, I didn't mean to submit this.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1321
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 11 May 2011 01:53:42 +0000 (01:53 +0000)]
Remove the comment that 32-bit is best for arrays. No longer the case because we use ABC's AIG CNF conversion by default.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1320
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 11 May 2011 01:49:00 +0000 (01:49 +0000)]
Improvement. Add array size statistics when printing out stats.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1319
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 11 May 2011 01:28:38 +0000 (01:28 +0000)]
Bugfix. Maybe. Disable a comparison so that CNF conversion doesn't fail. This fixes the assertion error.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1318
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 9 May 2011 03:57:25 +0000 (03:57 +0000)]
Adds two extra simplfication rules.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1316
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 9 May 2011 00:31:06 +0000 (00:31 +0000)]
More simplification rules.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1315
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 7 May 2011 12:14:51 +0000 (12:14 +0000)]
Extra simplification rules for the simplifying node factory.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1314
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 7 May 2011 12:02:20 +0000 (12:02 +0000)]
Signed division now returns what is should. Signed division is defined by unsigned division. Unsigned division returns 1, if the flag is set, now signed division returns 1 or -1 as appropriate.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1313
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 7 May 2011 12:00:42 +0000 (12:00 +0000)]
Add a public function that calls sizeReducing until fixed point (under some conditions.)
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1312
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 5 May 2011 03:45:03 +0000 (03:45 +0000)]
Adds an extra BVPLUS simplification rule. Cleans up the BVPLUS rules.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1311
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 5 May 2011 01:46:13 +0000 (01:46 +0000)]
Important bugfix. r1291 through to this revision, about once per 200M random instances, return the wrong result.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1310
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 5 May 2011 00:13:34 +0000 (00:13 +0000)]
Add an extra simplification rule.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1309
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 4 May 2011 05:04:31 +0000 (05:04 +0000)]
Replace variables before calling the interval analysis.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1308
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 4 May 2011 03:53:48 +0000 (03:53 +0000)]
Function to reset the stopwatch.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1307
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 4 May 2011 02:45:04 +0000 (02:45 +0000)]
Another fix to the same
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1306
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 4 May 2011 02:41:00 +0000 (02:41 +0000)]
Correct the last patch. I don't think this code runs.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1305
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 4 May 2011 01:41:39 +0000 (01:41 +0000)]
Apply simplifications through arrayterms too.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1304
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 2 May 2011 14:14:58 +0000 (14:14 +0000)]
Bugfix. Rarely we get the wrong answer; I got two broken instances in 140 days of fuzzing. This fixes those two instances, but, almost any change to STP fixes it, i.e. causes the problem to go away.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1299
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 1 May 2011 14:20:34 +0000 (14:20 +0000)]
Compiling with -D_GLIBCXX_DEBUG reported warnings because we sometimes derefferenced an iterator that was at the end. I'm not sure if this is really a problem or not..
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1298
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 1 May 2011 12:48:53 +0000 (12:48 +0000)]
Code to apply the alwaysTrueSet. Not currently enabled.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1297
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 1 May 2011 03:38:53 +0000 (03:38 +0000)]
Enable bitblast simplifications by default
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1296
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 30 Apr 2011 15:29:59 +0000 (15:29 +0000)]
Turn off the ite-context simplification by default.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1295
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 30 Apr 2011 12:28:07 +0000 (12:28 +0000)]
Important Bugfix. The prior checkin sometimes, but rarely, returned the wrong result.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1294
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 30 Apr 2011 05:09:02 +0000 (05:09 +0000)]
Bugfix. The last checkin caused an infinite loop (often).
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1293
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 30 Apr 2011 05:00:44 +0000 (05:00 +0000)]
Extra simplification rules
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1292
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 30 Apr 2011 04:18:02 +0000 (04:18 +0000)]
Extra simplification rules.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1291
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 30 Apr 2011 02:07:39 +0000 (02:07 +0000)]
Convert subtraction to addition in the simplifying node factory.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1290
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 29 Apr 2011 05:57:36 +0000 (05:57 +0000)]
Bugfix. Reads might have been simplified down which was causing an assertion error.
Thanks for Yunho Kim for reporting this!
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1288
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 27 Apr 2011 07:10:09 +0000 (07:10 +0000)]
Important Bugfix. The prior checkin causes the WRONG answer sometimes.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1287
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 27 Apr 2011 06:52:58 +0000 (06:52 +0000)]
Extra simplification rules. In particular a simple signed interval analysis.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1286
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 27 Apr 2011 02:36:30 +0000 (02:36 +0000)]
Add extra simplifying rules.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1285
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 27 Apr 2011 01:33:46 +0000 (01:33 +0000)]
Fix. I thought that extracts don't add any information but they do, if the underlying term has only partial fixed information.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1284
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 27 Apr 2011 00:37:21 +0000 (00:37 +0000)]
Remove signed division, modulus and remainder when creating nodes via the simplifying node factory.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1283
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 26 Apr 2011 23:56:29 +0000 (23:56 +0000)]
Two extra simplification rules.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1282
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 21 Apr 2011 02:06:24 +0000 (02:06 +0000)]
Change the sorting network based adder (which isn't used by default).
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1281
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 20 Apr 2011 14:23:50 +0000 (14:23 +0000)]
Refactor. Less verbose.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1280
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 20 Apr 2011 13:35:50 +0000 (13:35 +0000)]
Improvement. Add a warning when parsing problems that use array extensionality.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1279
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 16 Apr 2011 13:32:28 +0000 (13:32 +0000)]
Extra upfront simplification rules.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1278
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 14 Apr 2011 06:34:08 +0000 (06:34 +0000)]
Add some missing simplification rules for AND/OR/ propositional ITE.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1277
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 14 Apr 2011 05:32:21 +0000 (05:32 +0000)]
Shortcut in a rare circumstance.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1276
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 14 Apr 2011 05:31:06 +0000 (05:31 +0000)]
Extra BVXOR simplification rules.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1275
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 13 Apr 2011 14:21:58 +0000 (14:21 +0000)]
Adds the reverse of rules to catch an obscure but important for some of our benchmarks rule.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1274
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 13 Apr 2011 12:58:34 +0000 (12:58 +0000)]
Improvement. Add a warning message when using --exit-after-CNF with arrays, without -r.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1273
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 13 Apr 2011 12:41:03 +0000 (12:41 +0000)]
Improvement. Fix the difficulty score for subtraction.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1272
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 13 Apr 2011 04:52:49 +0000 (04:52 +0000)]
Fix the build. Without -NDEBUG wouldn't compile.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1271
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 13 Apr 2011 04:41:09 +0000 (04:41 +0000)]
Improvement. Look for nodes that are true/false when conjoined to the top.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1270
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 13 Apr 2011 04:30:17 +0000 (04:30 +0000)]
Remove some assertions that don't necessarily hold.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1269
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 13 Apr 2011 02:00:29 +0000 (02:00 +0000)]
Improvement. Replace the hashing node factory with the simplifying node factory. Add an extra obscure simplification rule.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1268
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 13 Apr 2011 01:43:16 +0000 (01:43 +0000)]
Extra simplification rule.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1267
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 11 Apr 2011 15:11:08 +0000 (15:11 +0000)]
oops. Meant to add this too.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1266
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 11 Apr 2011 15:09:31 +0000 (15:09 +0000)]
Add an extra simplification rule to the simplifying node factory.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1265
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 11 Apr 2011 13:26:53 +0000 (13:26 +0000)]
Move some division be zero code into the bitblaster. I'm trying to make the array transformer (which also transforms signed div/mod) idempotent.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1264
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 10 Apr 2011 11:37:02 +0000 (11:37 +0000)]
Adds code, that's not currently enabled, to read-out all the nodes that the bitblaster discovers should be constant.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1263
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 10 Apr 2011 04:13:22 +0000 (04:13 +0000)]
Improvement. Use the simplifying node factory in transformer.
This is a hopefully correct implementation of r1260.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1262
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 10 Apr 2011 03:53:14 +0000 (03:53 +0000)]
Revert the previous revision. It broke lots.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1261
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 8 Apr 2011 14:57:20 +0000 (14:57 +0000)]
Improvement. Use the simplifying node factory in transformer.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1260
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 8 Apr 2011 04:33:28 +0000 (04:33 +0000)]
Improvement. Don't add NOT FALSE at the end of the input..
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1259
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 7 Apr 2011 14:36:10 +0000 (14:36 +0000)]
Improvement. When a node is simplified set a value so that we can avoid simplifying it later.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1258
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 7 Apr 2011 13:43:19 +0000 (13:43 +0000)]
Improvement. Output the time spent in a stage with -s.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1257
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 7 Apr 2011 13:38:52 +0000 (13:38 +0000)]
Hack. The ITE context simplification blows out ff.stp, i.e. it takes > 5 minutes. This limits ITE context simplifications to small contexts.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1256
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 7 Apr 2011 13:36:23 +0000 (13:36 +0000)]
Revert. I didn't mean to checkin all those changes.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1255
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 7 Apr 2011 13:22:05 +0000 (13:22 +0000)]
Hack. The ITE context simplification blows out ff.stp, i.e. it takes > 5 minutes. This limits ITE context simplifications to small contexts.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1254
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 6 Apr 2011 03:42:57 +0000 (03:42 +0000)]
Remove junk.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1253
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 6 Apr 2011 03:42:07 +0000 (03:42 +0000)]
Improve the bvsolver.If the substitution of a monomial fails, then the bvsolver will loop looking for more candidates.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1252
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 6 Apr 2011 02:59:50 +0000 (02:59 +0000)]
Refactor. Remove junk.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1251
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 3 Apr 2011 14:14:56 +0000 (14:14 +0000)]
Improvement. Some extra simplifications for the simplifyingNF.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1250
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 3 Apr 2011 09:49:09 +0000 (09:49 +0000)]
Improvement. The simplifying node factory never creates x + y = y + 2 (say). Instead it removes terms that are common on both sides. Creating x = 2.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1249
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 31 Mar 2011 13:02:27 +0000 (13:02 +0000)]
Tiny improvement. Add the one-bit operations that evaluate to a child or a constant.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1248
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 31 Mar 2011 12:39:46 +0000 (12:39 +0000)]
Small improvement. Discard the inner write if the two WRITEs are to the same index.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1247
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 29 Mar 2011 13:18:23 +0000 (13:18 +0000)]
Work around rare problem caused by the simplifying node factory.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1246
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 28 Mar 2011 03:49:09 +0000 (03:49 +0000)]
Make applySubstitutionMap idempotent (I hope).
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1245
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 28 Mar 2011 03:47:25 +0000 (03:47 +0000)]
Improvement. The simplifying node factory now eliminates extract over extracts, as well as some extract over concats.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1244
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 28 Mar 2011 00:36:48 +0000 (00:36 +0000)]
During the size reducing transformations, now set the top node to true during constant bit propagation.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1243
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 28 Mar 2011 00:35:17 +0000 (00:35 +0000)]
Change the names for some statistics.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1242
e59a4935 -1847-0410-ae03-
e826735625c1
projects / francis / stp.git / log