]>
git.unchartedbackwaters.co.uk Git - francis/stp.git/log
trevor_hansen [Sun, 13 Mar 2011 13:30:23 +0000 (13:30 +0000)]
* Clean up the simplifier some.
* Add times for the basic interval analysis.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1207
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 13 Mar 2011 04:19:20 +0000 (04:19 +0000)]
Refactor. Remove the simplify_upfront option. It's now hardcoded.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1206
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 13 Mar 2011 04:09:22 +0000 (04:09 +0000)]
Refactor. Remove code that's not used.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1205
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 12 Mar 2011 23:36:07 +0000 (23:36 +0000)]
Fix. Missing break; in a switch. Dumb luck meant it didn't cause any problems.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1204
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 12 Mar 2011 12:49:33 +0000 (12:49 +0000)]
Fix. r1201 added a message to cout.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1203
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 12 Mar 2011 12:28:33 +0000 (12:28 +0000)]
Improvement. Add a size reducing phase prior to performing simplifications that may increase the size of the problem. If the the DAG gets bigger by some amount, then we revert back to the saved copy of the problem.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1202
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 12 Mar 2011 12:13:26 +0000 (12:13 +0000)]
Improvements.
* The BVSolver doesn't necessarily apply the simplify..() functions (which can increase the DAGs size).
* Unsimplified input doesn't cause it to fail.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1201
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 12 Mar 2011 11:42:58 +0000 (11:42 +0000)]
Fix. This assert() was very slow sometimes.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1200
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 10 Mar 2011 14:35:13 +0000 (14:35 +0000)]
Bugfix. r1194 didn't preserve the doubly linked list.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1199
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 10 Mar 2011 05:12:44 +0000 (05:12 +0000)]
Fiddle with the difficulty scorer.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1198
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 10 Mar 2011 02:01:49 +0000 (02:01 +0000)]
Fiddle with the difficulty scorer to better estimate how hard the problem becomes.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1197
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 9 Mar 2011 06:42:07 +0000 (06:42 +0000)]
Miscellaneous improvements.
* Use the simplifying node factory in more places.
* If simplifications are turned off, don't simplify in the transformer.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1196
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 9 Mar 2011 04:14:36 +0000 (04:14 +0000)]
Fix. In the prior checkin I didn't keep track of which nodes had been visited.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1195
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 9 Mar 2011 03:45:26 +0000 (03:45 +0000)]
Improvement. Now do unconstrained elimination for all inequalities.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1194
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 7 Mar 2011 12:18:54 +0000 (12:18 +0000)]
Extra simplification rules for BVAND, and EQ. These sometimes make one of the grep big-array tests use 2.5GB of RAM during solving.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1193
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 7 Mar 2011 02:48:14 +0000 (02:48 +0000)]
Improvement. Add an extra simplification rule for BVDIV/ BVMOD.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1192
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 6 Mar 2011 23:15:48 +0000 (23:15 +0000)]
Add simplification of the top-most propositional part of the problem using AIGs. This is currently disabled by default.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1191
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 5 Mar 2011 11:57:10 +0000 (11:57 +0000)]
improvement. Use the simplifying node factory be default in the substitution map.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1190
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 5 Mar 2011 03:23:46 +0000 (03:23 +0000)]
Tiny improvement. Create slightly fewer nodes.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1189
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 5 Mar 2011 03:21:07 +0000 (03:21 +0000)]
Fix a leak. I'd forgotten to call fclose().
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1188
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 5 Mar 2011 03:14:50 +0000 (03:14 +0000)]
Fix a leak introduced in r1184.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1187
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 3 Mar 2011 12:44:08 +0000 (12:44 +0000)]
Improvement. Specialise the replace function more for replacing symbols by other things. This is considerably faster.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1186
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 3 Mar 2011 06:12:23 +0000 (06:12 +0000)]
Refactor. Neaten up the CreateSubstitutionMap function.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1185
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 3 Mar 2011 06:03:24 +0000 (06:03 +0000)]
Fixes / Improvements.
* Fix. No longer create NOT(NOT(..)) nodes because their node numbers aren't unique.
* Improvement. Change the AlwaysTrueFormMap (which was a set), to use node numbers ---which allows the nodes to be garbage collected.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1184
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 3 Mar 2011 03:51:48 +0000 (03:51 +0000)]
Improvement. Only create possible values if it can help.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1183
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 3 Mar 2011 03:46:53 +0000 (03:46 +0000)]
Enable ITE Context stuff by default.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1182
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 3 Mar 2011 01:32:14 +0000 (01:32 +0000)]
Refactor. I experimented with changing the allocator used when parsing. But, it didn't make any measurable difference in the time taken.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1181
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 1 Mar 2011 12:30:42 +0000 (12:30 +0000)]
Improvement. Add an equality simplification.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1180
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 28 Feb 2011 13:31:43 +0000 (13:31 +0000)]
Improvement. Enable ITE context simplifications again.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1179
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 27 Feb 2011 13:43:44 +0000 (13:43 +0000)]
Disable ITE context simplifications. It's too slow on some CVC test cases to justify it.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1178
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 27 Feb 2011 13:33:16 +0000 (13:33 +0000)]
Bugfix. Terrible. Forgot to delete debugging code. Too late.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1177
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 27 Feb 2011 13:28:39 +0000 (13:28 +0000)]
Bugfix. Terrible. The last checkin causes STP to sometimes return the wrong answer I suspect.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1176
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 27 Feb 2011 11:04:04 +0000 (11:04 +0000)]
Improvement. An analysis that simplifies ITES by determining what must be true/false down each branch.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1175
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 26 Feb 2011 05:14:40 +0000 (05:14 +0000)]
No semantic change. Fix a mistake that caused no effect.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1172
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 26 Feb 2011 05:06:58 +0000 (05:06 +0000)]
Fix. XORs with >2 children sometimes reached the simplifier. This patch adds simplification for those, rather than generating an assertion error.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1171
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 26 Feb 2011 03:56:39 +0000 (03:56 +0000)]
Bugfix. Terrible! Another fix. STP r1149 to here will sometimes return the wrong answer.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1170
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 26 Feb 2011 02:54:10 +0000 (02:54 +0000)]
Bugfix. Terrible! STP r1149 to here will sometimes return the wrong answer. I was wrong about the semantics of .insert(..), I thought it replaced the new value if it was already present.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1169
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 24 Feb 2011 02:00:15 +0000 (02:00 +0000)]
Bugfix. The prior checkin added an assertion that didn't always hold.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1168
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 24 Feb 2011 01:42:37 +0000 (01:42 +0000)]
Finish refactoring of the ArrayTransformer class.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1167
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 24 Feb 2011 01:15:57 +0000 (01:15 +0000)]
Partial refactor. Remove the Arrayread_SymbolMap.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1166
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 24 Feb 2011 01:02:33 +0000 (01:02 +0000)]
Partial refactor. Removing the Arrayname_ReadindicesMap.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1165
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 24 Feb 2011 00:46:48 +0000 (00:46 +0000)]
Partial refactoring. Removing the arrayread_itemap.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1164
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 23 Feb 2011 14:54:22 +0000 (14:54 +0000)]
Refactoring.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1163
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 23 Feb 2011 14:11:31 +0000 (14:11 +0000)]
Bugfix. Fix the prior checkin.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1162
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 23 Feb 2011 13:43:18 +0000 (13:43 +0000)]
Partial Refactor. I'm reducing the number of collections in the ArrayTransformer class, but it's causing difficult to find defects. This adds a new collection. I'll remove the old ones later.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1161
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 23 Feb 2011 07:09:20 +0000 (07:09 +0000)]
Extra test cases that should be simplified down to nothing.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1160
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 22 Feb 2011 11:44:12 +0000 (11:44 +0000)]
Refactor. Overcome a temporary static fetish. Now better.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1159
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 22 Feb 2011 11:34:18 +0000 (11:34 +0000)]
Improvement. Match the difficulty score better to the number of AIG nodes created.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1158
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 22 Feb 2011 00:19:08 +0000 (00:19 +0000)]
Improvement. The start of an unsigned interval simplification.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1157
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 22 Feb 2011 00:16:17 +0000 (00:16 +0000)]
Improvement. Handle extracts especially when doing unconstrained variable elimination.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1156
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 21 Feb 2011 06:14:33 +0000 (06:14 +0000)]
Bugfix. r1152 was broken. It got the widths wrong.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1154
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 21 Feb 2011 04:26:59 +0000 (04:26 +0000)]
A new test case for the special unconstrained extract handling.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1153
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 21 Feb 2011 04:06:29 +0000 (04:06 +0000)]
Improvement. Simplifying EQ a little better.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1152
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 14 Feb 2011 01:23:43 +0000 (01:23 +0000)]
Add find pure literals code.oooops.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1149
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 14 Feb 2011 01:22:10 +0000 (01:22 +0000)]
Enable pure literal elimination, and unconstrained variable elimination by default.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1148
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 14 Feb 2011 01:15:57 +0000 (01:15 +0000)]
Remove unused configuration option. Update qualifiers.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1147
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 14 Feb 2011 01:14:05 +0000 (01:14 +0000)]
Add --config options to enable CNF conversion via Tseitin, and AIG rewrites.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1146
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 14 Feb 2011 01:11:30 +0000 (01:11 +0000)]
Add the code for unconstrained variable elimination. This is not currently enabled.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1145
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 14 Feb 2011 01:01:57 +0000 (01:01 +0000)]
Improvements.
* Add a function to update the substitution map that avoids the expensive checks. This is used by unconstrained variable elimination.
* use a --config flag to enable the xor solver.
* Update the dependencies with functions for unconstrained elimination.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1144
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 11 Feb 2011 00:43:00 +0000 (00:43 +0000)]
Add categories to the RunTime class for new simplifications
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1143
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 10 Feb 2011 06:57:44 +0000 (06:57 +0000)]
Fix a leak in _asserts. I know of no other leaks.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1141
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 10 Feb 2011 05:48:48 +0000 (05:48 +0000)]
Improvement. The SMTLIB1 & SMTLIB2 parsers were holding references to nodes when they didn't need to.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1140
e59a4935 -1847-0410-ae03-
e826735625c1
khooyp [Thu, 10 Feb 2011 01:59:06 +0000 (01:59 +0000)]
Add conditional workaround for flex < 2.5.20, such as in RedHat.
- Old versions of flex did not support the -f flag, and did not provide a destroy function.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1139
e59a4935 -1847-0410-ae03-
e826735625c1
khooyp [Thu, 10 Feb 2011 01:59:02 +0000 (01:59 +0000)]
Clean up the build system for src/parser.
- Rename files consistently to be usable in pattern rules, and use patterns rules for flex/bison.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1138
e59a4935 -1847-0410-ae03-
e826735625c1
khooyp [Thu, 10 Feb 2011 01:58:51 +0000 (01:58 +0000)]
Temporarily rename CVC.* to cvclib.*; to be renamed in the next patch to cvc.* (workaround to handle case-only renames).
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1137
e59a4935 -1847-0410-ae03-
e826735625c1
khooyp [Thu, 10 Feb 2011 01:31:59 +0000 (01:31 +0000)]
Fix inconsistent line endings, and execute bit on a couple of .sh files (so that SVN with eol-style/mime-type auto-props won't complain).
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1136
e59a4935 -1847-0410-ae03-
e826735625c1
khooyp [Thu, 10 Feb 2011 01:21:54 +0000 (01:21 +0000)]
Fix a typo in the help string.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1135
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 8 Feb 2011 14:35:17 +0000 (14:35 +0000)]
Fix. For r1131 I deleted the wrong file.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1133
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 8 Feb 2011 13:17:21 +0000 (13:17 +0000)]
Patch from Khoo Yit Phang.
Delete several files to address "ranlib: ... has no symbols" warnings (they actually are completely empty).
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1132
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 8 Feb 2011 13:13:04 +0000 (13:13 +0000)]
Patch from Khoo Yit Phang.
Remove extlib-abc/vecAtt.h to eliminate warnings (it's unused anyway).
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1131
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 8 Feb 2011 13:08:40 +0000 (13:08 +0000)]
Patch from Khoo Yit Phang.
Fix typo for FreeBSD (untested).
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1130
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 8 Feb 2011 12:29:21 +0000 (12:29 +0000)]
Patch from Khoo Yit Phang.
Fix the weird type of STPMgr::CreateBVConst (to have only one reference level).
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1129
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 8 Feb 2011 12:22:10 +0000 (12:22 +0000)]
Patch from Khoo Yit Phang.
Add a workaround for GCC 4.0 which doesn't extend friendship to nested classes.
See http://stackoverflow.com/questions/
3584385 /friend-access-to-protected-nested-class for details.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1128
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 8 Feb 2011 12:20:23 +0000 (12:20 +0000)]
Patch from Khoo Yit Phang.
Clean up scripts/configure, and add flags to set CC and -fpic.
- Use POSIX shell parameter expansion when parsing flags, instead of expr.
- Fix the test for $CC/$CXX to work when they contain spaces (e.g., "gcc -m32").
- Export flags in config.info to ensure that the entire build, including recursive Makefiles, consistently use the given flags.
- Don't create the installation directories when configuring; do it when installing.
- Remove minisat configuration flags from scripts/configure, since they are unused.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1127
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 8 Feb 2011 12:18:01 +0000 (12:18 +0000)]
Patch from Khoo Yit Phang.
General clean-up of the build system.
- Remove unused or unnecessary flags and rules.
- Fix up automatic dependency generation.
- Move final linking of bin/stp to the topmost Makefile for better dependency control.
- Update versionString.cpp only if the version changed, to avoid unnecessary rebuild.
- Build src/sat/libminisat.a and lib/libstp.a by concatenating their constituent archives, rather than by relisting their contained object files.
- Add dependencies for bin/stp and lib/libstp.a to rebuild them only when necessary.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1126
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 8 Feb 2011 12:00:08 +0000 (12:00 +0000)]
Patch from Khoo Yit Phang.
Drop support for building universal binaries on OS X, since it raises rather annoying build issues.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1125
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 8 Feb 2011 11:51:42 +0000 (11:51 +0000)]
Patch from Khoo Yit Phang.
uRemove -I../AST from CFLAGS, and change all affected #include to use relative paths.
This is in preparation to fix up automatic dependencies generation to use "gcc -MG" to handle the generated
src/AST/ASTKind.h file, which works more reliably when #include uses relative paths.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1124
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 8 Feb 2011 11:48:30 +0000 (11:48 +0000)]
Patch from Khoo Yit Phang.
Clean up the build system of MiniSat.
- Set up dependencies for recursive Makefile to avoid unnecessary rebuilds.
- Correctly propagate configuration to recursive Makefiles by exporting flags and removing unnecessary rules.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1123
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 8 Feb 2011 11:41:47 +0000 (11:41 +0000)]
Patch from Khoo Yit Phang. Fix typos that caused main() to be linked into MiniSat's libraries.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1122
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 7 Feb 2011 14:05:30 +0000 (14:05 +0000)]
Speedup the test harness. For the CVC tests STP is taking about 200 seconds, and the harness about 60.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1121
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 5 Feb 2011 14:04:31 +0000 (14:04 +0000)]
Improvement. Simplifiy from (X bvdiv 1) to X.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1120
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 5 Feb 2011 01:34:36 +0000 (01:34 +0000)]
Speedup. When performing constant bit propagation, there is now a slow & a fast worklist. The cheap propagators in the slow worklist are called first.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1119
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 3 Feb 2011 04:00:54 +0000 (04:00 +0000)]
Improvement. Reduce the scope of the bvsolver.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1118
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 3 Feb 2011 03:47:13 +0000 (03:47 +0000)]
Convert these tests from cvc to smtlib2 format. The model seems to contain a division by zero. The currently implementation of the CVC language treats that as bad. It probably shouldn't, but I don't want to change the semantics. However, division by zero is defined in smtlib2. So I've converted them.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1117
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 3 Feb 2011 01:57:49 +0000 (01:57 +0000)]
Bugfix. The c-api calls ~STP and ~STPMgr. The changes I made to the destructors in r1115 broke the c-api.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1116
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 2 Feb 2011 12:32:36 +0000 (12:32 +0000)]
Improvement. Cleanup memory better at the end.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1115
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 2 Feb 2011 05:39:54 +0000 (05:39 +0000)]
Improvement. Use ABC's CNF converter by default when solving array problems using minisat.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1114
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 2 Feb 2011 03:10:05 +0000 (03:10 +0000)]
Remove no longer used code.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1113
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 2 Feb 2011 00:55:06 +0000 (00:55 +0000)]
Fix. Apply substitutions in another place to avoid an assertion error.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1112
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 1 Feb 2011 12:41:57 +0000 (12:41 +0000)]
Less Memory. Cache less frequently.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1111
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 1 Feb 2011 12:40:57 +0000 (12:40 +0000)]
Speedup. Track which sets have already being added to a cache, and don't add them again.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1110
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 31 Jan 2011 14:12:12 +0000 (14:12 +0000)]
Fix. Without a CallSAT_Result check call sometimes we get the wrong result. No idea why yet.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1109
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 31 Jan 2011 14:06:53 +0000 (14:06 +0000)]
Fix. If not simplifying during parsing an assertion was violated.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1108
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 30 Jan 2011 13:26:06 +0000 (13:26 +0000)]
Bugfix. Substitutions need to be written through arrays too. 2/2.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1103
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 30 Jan 2011 13:13:17 +0000 (13:13 +0000)]
Bugfix. Substitutions need to be written through arrays too.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1101
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 30 Jan 2011 13:11:58 +0000 (13:11 +0000)]
* The -t option now tracks time spent applying the substitution map.
* Some functions that should be private in the SubstitutionMap were made private.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1100
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 30 Jan 2011 12:45:32 +0000 (12:45 +0000)]
Fix. The last revision has some debugging messages enabled. Ooops.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1099
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 30 Jan 2011 05:44:01 +0000 (05:44 +0000)]
Improvement. Add substitution for variables by arbitary terms when creating substitution maps. The difficult part is check that substitutions don't create loops. This code replaces the old --config_full_bvsolve=1 option.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1098
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 30 Jan 2011 02:26:28 +0000 (02:26 +0000)]
Remove the full bvsolve option. I'm soon to commit a much better replacement of this.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1097
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 27 Jan 2011 07:06:19 +0000 (07:06 +0000)]
Cleanup. Remove Doug Lea's Malloc which is no longer used. We used to use dl malloc to give minisat a region of memory to allocate its data structures in. This meant that they were all close together in memory so that when cache line were stored, the lines would more often contain minisat data, rather than STP's data. However, Minisat 2.2 has a better allocator, so it allocates more of its stuff together in memory. The difference between the embedded minisat 2.2 in STP, and running it from the command line, is about 4%. Not a large enough difference to worry about.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1096
e59a4935 -1847-0410-ae03-
e826735625c1
projects / francis / stp.git / log