git.unchartedbackwaters.co.uk Git

trevor_hansen [Tue, 12 Jul 2011 12:25:32 +0000 (12:25 +0000)]

Output the peak memory used when using -s.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1371 e59a4935-1847-0410-ae03-e826735625c1

commit | commitdiff | tree

trevor_hansen [Tue, 12 Jul 2011 11:58:32 +0000 (11:58 +0000)]

Fix to get it compiling with Cygwin. Thanks to Marzio De Biasi.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1370 e59a4935-1847-0410-ae03-e826735625c1

commit | commitdiff | tree

trevor_hansen [Tue, 12 Jul 2011 07:04:35 +0000 (07:04 +0000)]

Fix. unit_test script was not working. Adds another test.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1368 e59a4935-1847-0410-ae03-e826735625c1

commit | commitdiff | tree

trevor_hansen [Tue, 12 Jul 2011 06:17:00 +0000 (06:17 +0000)]

Bugfix. Thanks to Jingyue Wu for reporting sbvdiv was broken through the c-api.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1367 e59a4935-1847-0410-ae03-e826735625c1

commit | commitdiff | tree

trevor_hansen [Tue, 12 Jul 2011 05:09:42 +0000 (05:09 +0000)]

Patch from Peter Collingbourne to enable compiling with clang. Thanks\!

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1366 e59a4935-1847-0410-ae03-e826735625c1

commit | commitdiff | tree

trevor_hansen [Tue, 12 Jul 2011 05:06:59 +0000 (05:06 +0000)]

Remove the include directory. It shouldn't be here.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1365 e59a4935-1847-0410-ae03-e826735625c1

commit | commitdiff | tree

trevor_hansen [Sat, 9 Jul 2011 06:56:51 +0000 (06:56 +0000)]

Fix. The SMTLIB2 parser now outputs "success" in reply to commands if the option is enabled.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1364 e59a4935-1847-0410-ae03-e826735625c1

commit | commitdiff | tree

trevor_hansen [Thu, 7 Jul 2011 10:48:46 +0000 (10:48 +0000)]

Move functions around so that clang links.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1363 e59a4935-1847-0410-ae03-e826735625c1

commit | commitdiff | tree

trevor_hansen [Thu, 7 Jul 2011 06:57:48 +0000 (06:57 +0000)]

Remove clang warnings.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1362 e59a4935-1847-0410-ae03-e826735625c1

commit | commitdiff | tree

trevor_hansen [Thu, 7 Jul 2011 06:45:58 +0000 (06:45 +0000)]

Fix clang warnings.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1361 e59a4935-1847-0410-ae03-e826735625c1

commit | commitdiff | tree

trevor_hansen [Thu, 7 Jul 2011 06:34:54 +0000 (06:34 +0000)]

Silence a clang warning message.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1360 e59a4935-1847-0410-ae03-e826735625c1

commit | commitdiff | tree

trevor_hansen [Thu, 30 Jun 2011 15:33:11 +0000 (15:33 +0000)]

Improvement. Needed for using STP interactively.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1359 e59a4935-1847-0410-ae03-e826735625c1

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

trevor_hansen [Thu, 7 Apr 2011 13:22:05 +0000 (13:22 +0000)]