git.unchartedbackwaters.co.uk Git - francis/stp.git/log

]> git.unchartedbackwaters.co.uk Git - francis/stp.git/log

projects / francis / stp.git / log

summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next

commit | commitdiff | tree

trevor_hansen [Mon, 14 Jun 2010 13:20:54 +0000 (13:20 +0000)]

Add some unit tests (which run when regressall is run) to check that simplifications are turning problems into TRUE or FALSE.

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

commit | commitdiff | tree

trevor_hansen [Mon, 14 Jun 2010 12:34:52 +0000 (12:34 +0000)]

Bugfix. Enable the same options for when the parser is automatically detected based on filename, and when the parser is explicitly specified.

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

commit | commitdiff | tree

trevor_hansen [Mon, 14 Jun 2010 07:17:05 +0000 (07:17 +0000)]

Change the properties so that SMTLIB2 format files are ignored.

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

commit | commitdiff | tree

trevor_hansen [Mon, 14 Jun 2010 04:06:32 +0000 (04:06 +0000)]

Bugfix. Save the value of print counter example as per the bug report from Markus Groß

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

commit | commitdiff | tree

trevor_hansen [Mon, 14 Jun 2010 03:04:47 +0000 (03:04 +0000)]

Fix regresscapi. This file wasn't checked in

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

commit | commitdiff | tree

trevor_hansen [Sun, 13 Jun 2010 14:32:53 +0000 (14:32 +0000)]

Fix the build. Add doug Lea's malloc implementation

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

commit | commitdiff | tree

trevor_hansen [Sun, 13 Jun 2010 14:19:33 +0000 (14:19 +0000)]

Put the clauses of the SAT solver in a separate heap. This reduces the number of cache misses in the inner loop of the SAT solver, but increases the amount of memory STP uses.

I'm not yet sure if the extra memory usage is justified.

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

commit | commitdiff | tree

trevor_hansen [Sat, 12 Jun 2010 14:55:37 +0000 (14:55 +0000)]

Free up more memory before SAT solving. In particular this deletes the Tseitin variables before calling the SAT solver. This makes good sense for problems that aren't solved by abstraction / refinement. However, I'm not sure how it impacts difficult array problems.

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

commit | commitdiff | tree

trevor_hansen [Sat, 12 Jun 2010 01:22:56 +0000 (01:22 +0000)]

Fix. I didn't update al l the function calls I should have in r832

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

commit | commitdiff | tree

trevor_hansen [Fri, 11 Jun 2010 15:23:37 +0000 (15:23 +0000)]

Remove no longer used bitblaster

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

commit | commitdiff | tree

trevor_hansen [Fri, 11 Jun 2010 15:23:04 +0000 (15:23 +0000)]

Remove the experimental bvsolver. I've copied its changes into the main bvsolver.

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

commit | commitdiff | tree

trevor_hansen [Fri, 11 Jun 2010 05:29:42 +0000 (05:29 +0000)]

* Make GetUnsignedConst a member function of ASTNode.
* In GetUnsignedConst check the position of the maximum bit only if the size is > , not >=

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

commit | commitdiff | tree

trevor_hansen [Fri, 11 Jun 2010 03:05:51 +0000 (03:05 +0000)]

Refactoring. Move all the substitutionmap functions into the one class.

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

commit | commitdiff | tree

trevor_hansen [Fri, 11 Jun 2010 02:04:18 +0000 (02:04 +0000)]

This makes SimplifyTerm idempotent. My hope is that this will reduce the number of times that the toplevel function needs to be called. If a term at the bottom of the graph doesn't map to itself when SimplifyTerm is run, then all the nodes above it will need to be re-created next time SimplifyTerm is called on the graph.

This patch adds an assertion function that isn't enabled.

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

commit | commitdiff | tree

trevor_hansen [Fri, 11 Jun 2010 01:01:39 +0000 (01:01 +0000)]

Adds a simplification rule to replace BVANDS with zeroes at the front with a CONCAT.

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

commit | commitdiff | tree

trevor_hansen [Wed, 9 Jun 2010 13:41:37 +0000 (13:41 +0000)]

bugfix. Constraints were ignored when they should have been.

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

commit | commitdiff | tree

trevor_hansen [Wed, 9 Jun 2010 06:57:14 +0000 (06:57 +0000)]

Bugfix. Recursively simplify array ITES.

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

commit | commitdiff | tree

trevor_hansen [Wed, 9 Jun 2010 05:06:09 +0000 (05:06 +0000)]

Add back code I removed in the last revision. Without this code fd_query_cheung2010.cvc timesout.

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

commit | commitdiff | tree

trevor_hansen [Wed, 9 Jun 2010 04:00:08 +0000 (04:00 +0000)]

Bugfix. Simplify the proposition of array-ITEs. I don't simplify the "then" and "else" branch so I'm not sure if this fixes all the problems.

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

commit | commitdiff | tree

trevor_hansen [Wed, 9 Jun 2010 03:15:23 +0000 (03:15 +0000)]

* In the bvsolver perform cheap tests which maybe short-cut before expensive tests.
* Lazily count the number of symbols in the bvsolver.

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

commit | commitdiff | tree

trevor_hansen [Tue, 8 Jun 2010 14:18:04 +0000 (14:18 +0000)]

Bugfix. Avoid creating cycles with the bvsolver.

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

commit | commitdiff | tree

trevor_hansen [Tue, 8 Jun 2010 12:52:46 +0000 (12:52 +0000)]

Bugfix. The bvsolver would replace a variable with an equation that contained that same variable. It did so because there was a special case that let it. I removed the special case.

I don't understand why the special case was there, so aren't sure if this will slow down some other instances?

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

commit | commitdiff | tree

trevor_hansen [Tue, 8 Jun 2010 11:28:27 +0000 (11:28 +0000)]

Copy the cleaner new SplitEven_into_Oddnum_PowerOf2 function from bvsolverExp. I'm comparing the values from the old and new version of the function still.

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

commit | commitdiff | tree

msoos [Fri, 4 Jun 2010 18:11:26 +0000 (18:11 +0000)]

Last commit was wrong. Importing again CryptoMiniSat-'Cluster56'

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

commit | commitdiff | tree

msoos [Fri, 4 Jun 2010 17:56:12 +0000 (17:56 +0000)]

Importing CryptoMiniSat version 'Cluster56'.

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

commit | commitdiff | tree

trevor_hansen [Sun, 30 May 2010 13:05:21 +0000 (13:05 +0000)]

Fix the method to count the number of instances in an expression. Previously it was counting no more than one.

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

commit | commitdiff | tree

trevor_hansen [Sun, 30 May 2010 13:02:47 +0000 (13:02 +0000)]

Split out the class which lazily builds the variables in terms.

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

commit | commitdiff | tree

trevor_hansen [Sun, 30 May 2010 10:40:40 +0000 (10:40 +0000)]

Small speedup in the cnf generator.

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

commit | commitdiff | tree

trevor_hansen [Sun, 30 May 2010 01:07:40 +0000 (01:07 +0000)]

Add histar to regressall. We use far far too much memory on these tests. Not sure why.

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

commit | commitdiff | tree

trevor_hansen [Sun, 30 May 2010 00:57:24 +0000 (00:57 +0000)]

Moving histar tests to the main test directory.

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

commit | commitdiff | tree

trevor_hansen [Sat, 29 May 2010 13:38:59 +0000 (13:38 +0000)]

Add my experimental BVSolver. It's much slower than the current bvsolver, but is more reliable. I'll gradually move its innovations into the main bvsolver.

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

commit | commitdiff | tree

trevor_hansen [Sat, 29 May 2010 13:36:55 +0000 (13:36 +0000)]

Enable upfront simplifications of terms.

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

commit | commitdiff | tree

trevor_hansen [Sat, 29 May 2010 05:52:37 +0000 (05:52 +0000)]

* Make the constant evaluator a non member function. This allows the simplifying node factory to use it without holding a reference to a Simplifier object.
* Change the simplifier to use the simplifying node factory by default.

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

commit | commitdiff | tree

trevor_hansen [Sat, 29 May 2010 05:04:50 +0000 (05:04 +0000)]

Simplifyin BVSX to CONCAT if the topmost bit of the thing being extended is known.

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

commit | commitdiff | tree

trevor_hansen [Sat, 29 May 2010 04:22:11 +0000 (04:22 +0000)]

* Add a disabled-by-default option to simplify the arguments of a function first.
* Check explicitly the kind returned from some functions that create nodes to ensure the returned type is what we expect. With the simplifying node factory enabled, the type can sometimes change.

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

commit | commitdiff | tree

trevor_hansen [Sat, 29 May 2010 01:10:22 +0000 (01:10 +0000)]

Add a simplification so that (ite(p,5,7) <= 8) is always true is detected.

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

commit | commitdiff | tree

trevor_hansen [Fri, 28 May 2010 01:07:03 +0000 (01:07 +0000)]

Bugfix. If given bad input, the SMTLIB2 parser would match as much as it could then stop, without warning. It now checks that an end of file has been reached.

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

commit | commitdiff | tree

trevor_hansen [Thu, 27 May 2010 13:58:44 +0000 (13:58 +0000)]

* Improve the simplifications of inequalities and equalities.
* Add code to print out each of the expressions that are simplified by the bit blaster.

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

commit | commitdiff | tree

trevor_hansen [Wed, 26 May 2010 14:32:26 +0000 (14:32 +0000)]

Implements booth recoding when bitblasting multiplication.

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

commit | commitdiff | tree

trevor_hansen [Mon, 24 May 2010 05:53:15 +0000 (05:53 +0000)]

Add the "eric-tests" to regressall.

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

commit | commitdiff | tree

trevor_hansen [Mon, 24 May 2010 05:50:57 +0000 (05:50 +0000)]

bugfix. Allow distinct to be used for both formulae and terms.

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

commit | commitdiff | tree

trevor_hansen [Mon, 24 May 2010 02:23:57 +0000 (02:23 +0000)]

These scripts (though I don't know what they do) seem to belong with the other test generation scripts.

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

commit | commitdiff | tree

trevor_hansen [Mon, 24 May 2010 02:09:23 +0000 (02:09 +0000)]

Bugfix. Rare types of array reads were causing a type-error.

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

commit | commitdiff | tree

trevor_hansen [Mon, 24 May 2010 02:03:46 +0000 (02:03 +0000)]

* Letize booleans when printing back smb2lib format.
* Print back in smtlib/smtlib2 format arity > 2 and, xor, or.

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

commit | commitdiff | tree

trevor_hansen [Mon, 24 May 2010 01:35:39 +0000 (01:35 +0000)]

Run tests with the .smt2 extension.

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

commit | commitdiff | tree

trevor_hansen [Sun, 23 May 2010 12:55:41 +0000 (12:55 +0000)]

Fix the memory leaks in the SMTLIB2 parser.

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

commit | commitdiff | tree

trevor_hansen [Sun, 23 May 2010 06:36:26 +0000 (06:36 +0000)]

* fix reduce/reduce error in the smtlib2 format.
* fix dependencies of smtlib2 format in the makefile.

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

commit | commitdiff | tree

trevor_hansen [Sun, 23 May 2010 04:53:02 +0000 (04:53 +0000)]

The SMTLIB2 parser now accepts valid, but extremely improbable symbol names, such as: ?

It's not finished, it still leaks badly, ignores most of the commands it's sent, and doesn't allow annotations to be used.

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

commit | commitdiff | tree

trevor_hansen [Sat, 22 May 2010 14:08:29 +0000 (14:08 +0000)]

Fix the defintion of what a symbol is in the SMTLIB2 format.

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

commit | commitdiff | tree

trevor_hansen [Fri, 21 May 2010 18:23:07 +0000 (18:23 +0000)]

Use the flex options recommended by its manual.

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

commit | commitdiff | tree

trevor_hansen [Fri, 21 May 2010 18:21:41 +0000 (18:21 +0000)]

* Add binary & hexidecimal for smtlib2 format.
* Fix the syntax of the smtlib2 repeat function.

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

commit | commitdiff | tree

trevor_hansen [Fri, 21 May 2010 15:55:33 +0000 (15:55 +0000)]

An initial version of an smtlib2 format parser. It has these problems:
* Leaks memory
* Doesn't allow for annotations on terms.
* Ignores the commands sent to it. It just solves the problem specified.

Other changes:
* Long options are no longer case senstive.
* If the input file ends with .smt2 or .smt the appropriate parser is selected.
* The simplifying node factory is disabled during parsing when printing back is enabled. This allows STP to be used as a better, but still low-fidelity translator between formats.

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

commit | commitdiff | tree

trevor_hansen [Fri, 21 May 2010 15:21:11 +0000 (15:21 +0000)]

* The bvsmod operation can now be output by the printers.
* Output the status i.e. sat, unsat if known.

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

commit | commitdiff | tree

trevor_hansen [Thu, 20 May 2010 03:28:27 +0000 (03:28 +0000)]

Fix the build by adding a missing function.

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

commit | commitdiff | tree

trevor_hansen [Wed, 19 May 2010 14:09:45 +0000 (14:09 +0000)]

Fix: lets, types, extends and extracts in the SMTLIB2 format.

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

commit | commitdiff | tree

trevor_hansen [Wed, 19 May 2010 04:35:26 +0000 (04:35 +0000)]

The SMT-LIB2 format changes names from "implies" to "=>", and "IFF" to "=".

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

commit | commitdiff | tree

trevor_hansen [Tue, 18 May 2010 13:44:32 +0000 (13:44 +0000)]

A first attempt at an SMT-LIB2 output printer. I haven't tried to parse this so I'm not sure it's right.

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

commit | commitdiff | tree

katelman [Mon, 17 May 2010 18:31:51 +0000 (18:31 +0000)]

BOOLEXTRACT seems to have been implemented backward. It did an equality test on
the extracted bit against *zero*, instead of *one*.

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

commit | commitdiff | tree

trevor_hansen [Sat, 15 May 2010 12:28:53 +0000 (12:28 +0000)]

* Convert BVAND( ite(p,1,1) , ite(p2,0,1)) to ite(p and p2, 0,1).
* Add back simplify() for minisat.

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

commit | commitdiff | tree

trevor_hansen [Thu, 13 May 2010 14:26:32 +0000 (14:26 +0000)]

Delete an unnecessary copy of c_interface.h, ammend the README to suggest updating the TEST_PREFIX>

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

commit | commitdiff | tree

trevor_hansen [Thu, 13 May 2010 05:40:09 +0000 (05:40 +0000)]

Remove the code for the "ReferenceCount". This was my first attempt to make the simplifications DAG-aware (sometimes called sharing-aware). The approach I chose was fundamentally broken (oops). I'm working on a new approach.

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

commit | commitdiff | tree

trevor_hansen [Thu, 13 May 2010 05:34:34 +0000 (05:34 +0000)]

* Use the simplifying node factory and the type checking node factory when parsing the CVC format via the main method. I haven't changed the c-interface to simplify as it build.
* Remove some explicit type checks in the CVC parser. Since the type checking node factory type checks each node it creates, there's no reason to have so many explicit type checks. So I've removed some of them.

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

commit | commitdiff | tree

trevor_hansen [Wed, 12 May 2010 14:29:38 +0000 (14:29 +0000)]

Add an encoding of multiplication that explicitly uses addition networks. This is copied from r482. I've not yet experimented with which bbmult() function is the best.

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

commit | commitdiff | tree

trevor_hansen [Wed, 12 May 2010 14:07:36 +0000 (14:07 +0000)]

First attempt at tracking time spent building the counter example. Doesn't properly include abstraction refinement checking time (I think). This introduces changes from r316

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

commit | commitdiff | tree

trevor_hansen [Wed, 12 May 2010 13:49:05 +0000 (13:49 +0000)]

Fix the flattenOneLevel function as per r294

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

commit | commitdiff | tree

trevor_hansen [Wed, 12 May 2010 13:44:42 +0000 (13:44 +0000)]

* Make the arguments to ==, !=, > for ASTNode references to reduce unnecessary copies.
* Include the BBVLE from r254 for later experimentation.

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

commit | commitdiff | tree

trevor_hansen [Mon, 10 May 2010 13:26:58 +0000 (13:26 +0000)]

* Fix the use of an invalidated iterator in the CVC parser.
* Fix a small memory leak in the CVC parser.

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

commit | commitdiff | tree

trevor_hansen [Mon, 10 May 2010 02:45:50 +0000 (02:45 +0000)]

When sending clauses to the SAT solver, create fewer objects. This speeds up sending to the sat solver by about 15%.

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

commit | commitdiff | tree

trevor_hansen [Mon, 10 May 2010 02:37:05 +0000 (02:37 +0000)]

Remove iterators from BBLShift to remove a spurious(?) warning when running in g++'s debug mode. i.e. with -D_GLIBCXX_DEBUG

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

commit | commitdiff | tree

vijay_ganesh [Fri, 7 May 2010 16:12:43 +0000 (16:12 +0000)]

Added info to the INSTALL file about the various configure script options

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

commit | commitdiff | tree

trevor_hansen [Fri, 7 May 2010 05:05:12 +0000 (05:05 +0000)]

Simplify the division operation. An unnecessary comparison has been removed from the division. This division as measured on the factoring12bitx12.cvc benchmark is about 20% faster.

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

commit | commitdiff | tree

vijay_ganesh [Thu, 6 May 2010 17:06:42 +0000 (17:06 +0000)]

fixed the problem with Alvin Cheung's testcase. The problem was that ITE-array expressions were not being handled correctly in SimplifyWrite_InPlace(). Fixed that

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

commit | commitdiff | tree

trevor_hansen [Thu, 6 May 2010 04:34:28 +0000 (04:34 +0000)]

Refactoring. Take out some ASTNodes from the bitblaster.

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

commit | commitdiff | tree

vijay_ganesh [Wed, 5 May 2010 16:50:00 +0000 (16:50 +0000)]

fixed the order in which the regressions are run. The C API regressions are run last

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

commit | commitdiff | tree

vijay_ganesh [Wed, 5 May 2010 16:33:47 +0000 (16:33 +0000)]

Perennial problem with svn. Does not give me the list of all modified files before check-in, and hence I end up checking-in experimental code. Fixed minor mod in STP.cpp

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

commit | commitdiff | tree

vijay_ganesh [Wed, 5 May 2010 16:31:35 +0000 (16:31 +0000)]

fixed TEST_PREFIX in Makefile.common. Ideally this should be fixed in the configure script. Also added new testcase eric1.stp to the repo

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

commit | commitdiff | tree

trevor_hansen [Wed, 5 May 2010 13:12:13 +0000 (13:12 +0000)]

Small changes to the array transformer:
* Use the node factory directly where possible.
* Use the general read(ite(...)..) case rather than handling specially read(write(ite...)..)..)
* Unless NDEBUG is defined check that no operations that should have been removed remain in the formula.

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

commit | commitdiff | tree

trevor_hansen [Wed, 5 May 2010 13:08:10 +0000 (13:08 +0000)]

Enable counter example checking by default.

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

commit | commitdiff | tree

trevor_hansen [Sun, 2 May 2010 14:43:11 +0000 (14:43 +0000)]

Don't test a22 in valgrind because it leaks

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

commit | commitdiff | tree

msoos [Fri, 30 Apr 2010 14:12:46 +0000 (14:12 +0000)]

CMS2: Hyper-binary resolution was wrong. Removed.

Hyper-binary resolution added binary clauses that lead to wrong UNSAT
answers, when the solution was in fact possible to find. I disabled it.
Also, other, minor problems have been fixed.

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

commit | commitdiff | tree

trevor_hansen [Thu, 29 Apr 2010 13:27:44 +0000 (13:27 +0000)]

Applying a patch provided by Hume to parse cvc and smtlib format constraints from c-strings.

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

commit | commitdiff | tree

trevor_hansen [Thu, 29 Apr 2010 12:58:51 +0000 (12:58 +0000)]

* Send the -t flag to STP when running regressstp. This outputs statistics that are useful to sum up.
* Delete my old eclipse formatting configuration. I don't use this anymore. Suspect no one else does either.

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

commit | commitdiff | tree

trevor_hansen [Wed, 28 Apr 2010 12:40:39 +0000 (12:40 +0000)]

Removing an .o file accidently checked in.

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

commit | commitdiff | tree

trevor_hansen [Wed, 28 Apr 2010 12:33:15 +0000 (12:33 +0000)]

Bugfix. Refactoring of ToCNF broke some ifdef CRYPTOMINISAT2 code.

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

commit | commitdiff | tree

msoos [Wed, 28 Apr 2010 12:25:09 +0000 (12:25 +0000)]

Turning on simplification&subpart-solving in CMS2

Simplification is carried if the problem seems difficult. It is carried
out in steps, so the complete algorithm's time demands do not have to
absorbed the first time it is run. Subpart-solving regularly checks for
parts of the problem that are disconnected, solves them, and returns to
the original problem instance -- essentially executing a
divide-and-conquer algorithm

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

commit | commitdiff | tree

msoos [Wed, 28 Apr 2010 12:24:57 +0000 (12:24 +0000)]

Updating CMS2

There have been some bugs fixed, and some performance increases added.
Hopefully these will fix up all remaining bugs

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

commit | commitdiff | tree

trevor_hansen [Wed, 28 Apr 2010 11:38:00 +0000 (11:38 +0000)]

Remove some unnecesarry memory churn. Extra objects were created and destroyed that didn't need to be.

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

commit | commitdiff | tree

trevor_hansen [Wed, 28 Apr 2010 10:53:16 +0000 (10:53 +0000)]

Refactoring. This creates a separate ClauseList class that holds the pointers to the CNF's clauses. I've just moved stuff around, so nothing should break/ work better.

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

commit | commitdiff | tree

trevor_hansen [Wed, 28 Apr 2010 04:09:16 +0000 (04:09 +0000)]

Making some functions ASTNode memberfunctions

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

commit | commitdiff | tree

trevor_hansen [Tue, 27 Apr 2010 06:24:53 +0000 (06:24 +0000)]

* Delete a test script that's no longer used
* regressstp now copies all the test cases to /dev/null to prime the disk cachde (like the other regression tests do).

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

commit | commitdiff | tree

trevor_hansen [Tue, 27 Apr 2010 05:18:07 +0000 (05:18 +0000)]

Fix regressbio. I missed an 's' in its path

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

commit | commitdiff | tree

trevor_hansen [Mon, 26 Apr 2010 13:52:27 +0000 (13:52 +0000)]

Include the STP version in the regression log

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

commit | commitdiff | tree

trevor_hansen [Mon, 26 Apr 2010 13:46:39 +0000 (13:46 +0000)]

Add crypto and bio regression targets

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

commit | commitdiff | tree

trevor_hansen [Mon, 26 Apr 2010 05:12:49 +0000 (05:12 +0000)]

Use gunzip so that we can run tests that are gzipped.

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

commit | commitdiff | tree

trevor_hansen [Mon, 26 Apr 2010 04:59:42 +0000 (04:59 +0000)]

* Make regressall depend on "all". If any changes have occured to STP's source code before you test, there will be a rebuilt. This prevents the problem of testing an old version of STP.
* Fix the regressstp target. It wasn't outputting to the log file.

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

commit | commitdiff | tree

trevor_hansen [Sun, 25 Apr 2010 16:13:40 +0000 (16:13 +0000)]

* Reduce the number of scripts we use to run regression tests.
* Remove redundacy from the Makefile.

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

commit | commitdiff | tree

trevor_hansen [Sun, 25 Apr 2010 14:28:32 +0000 (14:28 +0000)]

Fix the renameAllSiblings option in the CNF generator. It is still disabled by default until I measure its usefulnes..

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

commit | commitdiff | tree

trevor_hansen [Sun, 25 Apr 2010 11:00:20 +0000 (11:00 +0000)]

Reverting r465. Based on Stephen's example: stp-tests/crypto-tests/factoring-12bitsx12.stp this makes division about 50% faster.

Confirming what Stephen identified, varying just the bvdiv encoding:

crypto2: 42sec vs 32sec
simplifying minisat: 65s vs 37s
core minisat: 65s vs 43s

However, r600 solved this problem the fastest I've seen: 14 seconds. But that was cryptominisat. Cryptominisat2 is now in the trunk. So I suspect that this reverts a change that made division faster on cryptominisat, but slowed it down on the others (including cryptominisat2).

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

commit | commitdiff | tree

trevor_hansen [Sat, 24 Apr 2010 12:06:16 +0000 (12:06 +0000)]

Fix leaks in the CVC parser

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

commit | commitdiff | tree

trevor_hansen [Sat, 24 Apr 2010 09:54:10 +0000 (09:54 +0000)]

Fix memory leaks in the SMT-LIB parser.

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

STP Constraint Solver.