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 [Fri, 6 Aug 2010 01:59:14 +0000 (01:59 +0000)]

Fix slowdown.

r965 removed a cache update that caused bitblaster.cvc to run 10 times slower. This update adds back in the cache update as well as changes to ensure that by the end of SimplifyTerm the invariant that actualInput maps to something that hasBeenSimplified(output) holds for.

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

commit | commitdiff | tree

trevor_hansen [Thu, 5 Aug 2010 15:17:31 +0000 (15:17 +0000)]

Speedup the bvsolver. Use the applySubstitutionMap function to apply the discovered replacements rather than using simplifyFormula. This means that the simplification caches don't need to be cleaned out (saving time).

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

commit | commitdiff | tree

trevor_hansen [Thu, 5 Aug 2010 05:07:06 +0000 (05:07 +0000)]

Bugfix. The prior revision sometimes returned the wrong result (very rarely).

In the prior revision I removed some explicit calls to simplifyTerm.
Wrongly believing that the term was already simplified at the point.
To check that it was simplified I asserted the "hasBeenSimplified" function.
But the hasBeenSimplified function only checked that the term was present in the simplifyMap.
That is that simplifyTerm had been called on it.
Which isn't the same thing as being simplified.
i.e. term A is not simplified if in the SimplifyMap it's mapped to term B.
It's only simplified if A maps to A.

Some simplification functions expect their children to already be simplified.
This wasn't the case so we'd get the wrong answer.

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

commit | commitdiff | tree

trevor_hansen [Sun, 1 Aug 2010 04:20:59 +0000 (04:20 +0000)]

Bugfix. Infinite loop. My fourth attempt to fix the problem introduced in r947. I've been careful this time.

Refactor. Remove explicit calls to SimplifyTerm if simplify_upfront is enabled. This is a precursor to removing many of the SimplifyTerm calls in the SimplifyTerm function, nearly all are redundant because at the end of the function we have:

if (inputterm != output)
output = SimplifyTerm(output);

i.e. we fixed point it.

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

commit | commitdiff | tree

trevor_hansen [Sat, 31 Jul 2010 13:26:37 +0000 (13:26 +0000)]

Bugfix. Oops. When using the quick statistics (the -t option), record the time spent generating the CNF.

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

commit | commitdiff | tree

trevor_hansen [Wed, 28 Jul 2010 13:23:12 +0000 (13:23 +0000)]

Speedup. I've measured the performance of bit blasted comparisons on a (single) test case. I've selected the fastest encoding.

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

commit | commitdiff | tree

trevor_hansen [Wed, 28 Jul 2010 11:53:41 +0000 (11:53 +0000)]

Bugfix. Infinite loop. A third fix for r947.

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

commit | commitdiff | tree

trevor_hansen [Wed, 28 Jul 2010 07:01:58 +0000 (07:01 +0000)]

Bugfix. STP may produce the wrong answer. Introduced revision 947.

I enabled creation of multiplication nodes with >2 children. But the DistributeMultOverPlus function ignores the third (and later) children.

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

commit | commitdiff | tree

trevor_hansen [Wed, 28 Jul 2010 03:09:57 +0000 (03:09 +0000)]

Speed up of the unsigned division encoding. Update the runtimes for the different variants of unsigned division.

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

commit | commitdiff | tree

trevor_hansen [Wed, 28 Jul 2010 02:05:38 +0000 (02:05 +0000)]

Refactoring.
* CreateSymbol now takes the indexWidth and the valueWidth.
* I've removed most of the calls to setIndexWidth.
* CreateSymbol has been moved into the NodeFactory class.

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

commit | commitdiff | tree

trevor_hansen [Mon, 26 Jul 2010 23:26:50 +0000 (23:26 +0000)]

Bugfix. Stop a null pointer error.

The simplifier can create something like: (BVMULT 1 3 5). i.e. a mutliplication node of constants with arity > 2. This patch makes that work.

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

commit | commitdiff | tree

msoos [Mon, 26 Jul 2010 12:21:20 +0000 (12:21 +0000)]

Further fixing of spurious printing in CryptoMiniSat

As per report by Trevor Hansen

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

commit | commitdiff | tree

msoos [Mon, 26 Jul 2010 12:17:44 +0000 (12:17 +0000)]

Fixing verbosity-related problems in CryptoMiniSat2

Reported by Trevor Hansen

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

commit | commitdiff | tree

trevor_hansen [Sat, 10 Jul 2010 14:49:13 +0000 (14:49 +0000)]

A QF_ABV division has been added to the smt-lib. Update parser to read, update printer to write it.

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

commit | commitdiff | tree

trevor_hansen [Sat, 10 Jul 2010 14:24:13 +0000 (14:24 +0000)]

Bugfix. Properly print out the counter example of booleans.

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

commit | commitdiff | tree

trevor_hansen [Sat, 10 Jul 2010 09:55:19 +0000 (09:55 +0000)]

Fix the build + extra options for constant bit propagation (not currently enabled).

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

commit | commitdiff | tree

trevor_hansen [Sat, 10 Jul 2010 09:46:47 +0000 (09:46 +0000)]

Speedup. Flatten multiplications, sort, then re-assable into 2-arity functions. This detects some associativity.

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

commit | commitdiff | tree

trevor_hansen [Sat, 10 Jul 2010 09:45:19 +0000 (09:45 +0000)]

Extra code (not enabled), for constant bit propagation.

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

commit | commitdiff | tree

trevor_hansen [Sat, 10 Jul 2010 09:43:33 +0000 (09:43 +0000)]

Extra code (that's not currently enabled), so reduce the unncessary clearing of the simplification map during bit-vector solving. This patch causes some instances to fail.

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

commit | commitdiff | tree

trevor_hansen [Sat, 10 Jul 2010 04:54:09 +0000 (04:54 +0000)]

Output quick statistics if enabled, and exiting after generating the CNF.

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

commit | commitdiff | tree

trevor_hansen [Fri, 9 Jul 2010 14:06:23 +0000 (14:06 +0000)]

Decision. This optimisation helps our cvc regressions but hurts our smtlib ones. So I'm taking it out..

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

commit | commitdiff | tree

trevor_hansen [Fri, 9 Jul 2010 08:28:46 +0000 (08:28 +0000)]

Add the option to exit after generating the CNF. Currently only works for bit-vectors (which don't have abstraction refinement).

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

commit | commitdiff | tree

trevor_hansen [Fri, 9 Jul 2010 08:25:48 +0000 (08:25 +0000)]

Bugfix. If a new-line occured in a string literal, it wasn't matched by the lexer, so would be printed out to the console.

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

commit | commitdiff | tree

petercol [Thu, 8 Jul 2010 17:12:36 +0000 (17:12 +0000)]

Introduce vc_setInterfaceFlags function

This patch adds a vc_setInterfaceFlags function to the C interface
with one possible flag, EXPRDELETE, which is set by default. The flag
controls whether the C interface deletes types and integer constant
expressions at vc_Destroy time. It is intended that clients which
perform their own memory management of these objects will be able to
clear this flag.

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

commit | commitdiff | tree

trevor_hansen [Thu, 8 Jul 2010 05:16:17 +0000 (05:16 +0000)]

Fix some small leaks when performing division by zero, and in the smtlib1 parser.

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

commit | commitdiff | tree

trevor_hansen [Thu, 8 Jul 2010 05:14:38 +0000 (05:14 +0000)]

Only run the bvsolver if optimisations have been enabled. The bvsolver relies on optimisations being performed for correctness.

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

commit | commitdiff | tree

trevor_hansen [Thu, 8 Jul 2010 05:10:55 +0000 (05:10 +0000)]

Fix the unit test script:
* To not explicitly call simplifying minisat (which isn't an option if compiled with cms).
* To remove comments and blank lines (which are introduced by AIG's conversion).

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

commit | commitdiff | tree

trevor_hansen [Wed, 7 Jul 2010 13:33:08 +0000 (13:33 +0000)]

Bugfix. Remove a null pointer reference.

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

commit | commitdiff | tree

trevor_hansen [Wed, 7 Jul 2010 13:17:57 +0000 (13:17 +0000)]

Simplify (bvdiv x x ) to one. Likewise for the other multiplication like operations.

Other changes are for constant bit propagation (aren't active yet).

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

commit | commitdiff | tree

trevor_hansen [Wed, 7 Jul 2010 07:51:08 +0000 (07:51 +0000)]

Fix the building of the stp library.

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

commit | commitdiff | tree

trevor_hansen [Wed, 7 Jul 2010 07:37:55 +0000 (07:37 +0000)]

Fix the build.

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

commit | commitdiff | tree

trevor_hansen [Wed, 7 Jul 2010 07:33:58 +0000 (07:33 +0000)]

Neaten up the code for constant bit propagation. Note this code doesn't run by default, so this patch shouldn't change anything.

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

commit | commitdiff | tree

trevor_hansen [Tue, 6 Jul 2010 14:38:52 +0000 (14:38 +0000)]

Bugfix. Fix a check to ensure that the type of nodes doesn't change for the worst.

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

commit | commitdiff | tree

trevor_hansen [Tue, 6 Jul 2010 05:03:02 +0000 (05:03 +0000)]

* Interface changes for constant bit propagation. Not currently enabled.
* Add code to bitblast etc. for bvzx. BVZX can be created via the interface, and might not be simplified out before reaching the bitblaster.

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

commit | commitdiff | tree

trevor_hansen [Tue, 6 Jul 2010 01:35:43 +0000 (01:35 +0000)]

Fix. stp.a didn't have necessary cbitp file included. Thanks to Peter Collingbourne for the patch.

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

commit | commitdiff | tree

trevor_hansen [Tue, 6 Jul 2010 01:34:44 +0000 (01:34 +0000)]

Fix. The unit tests expect the cnf's to be called output_*.cnf. If going to CNF via AIGs it was called output.cnf

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

commit | commitdiff | tree

trevor_hansen [Tue, 6 Jul 2010 01:33:40 +0000 (01:33 +0000)]

Revert. In r915 I removed the default -m32 flag by accident.

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

commit | commitdiff | tree

trevor_hansen [Mon, 5 Jul 2010 13:26:19 +0000 (13:26 +0000)]

More getting ready for constant bit propagation. This code doesn't run, so nothing should change.

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

commit | commitdiff | tree

msoos [Mon, 5 Jul 2010 09:27:00 +0000 (09:27 +0000)]

CryptoMiniSat can now be built

How to build CryptoMS:
1) install cmake
2) go to the "src/sat/cryptominisat2/" directory
3) create new dir: "mkdir build"
4) go to new dir: "cd build"
5) type "cmake ../"
6) type "make"
7) the "cryptominisat" binary is now in the directory

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

commit | commitdiff | tree

msoos [Mon, 5 Jul 2010 08:48:57 +0000 (08:48 +0000)]

For low-cutoff speed reasons, it's best not to subsume learnts

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

commit | commitdiff | tree

trevor_hansen [Mon, 5 Jul 2010 04:43:52 +0000 (04:43 +0000)]

Add the interface code for constant bit propagation. This isn't all of the code, just the code required to interface with the bit blaster.

This code isn't called. So this patch doesn't change STP at all.

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

commit | commitdiff | tree

msoos [Sun, 4 Jul 2010 18:17:55 +0000 (18:17 +0000)]

Cleaning up some bugs in CryptoMS

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

commit | commitdiff | tree

trevor_hansen [Sun, 4 Jul 2010 12:23:07 +0000 (12:23 +0000)]

Free the memory allocatated to the AIGs before SAT solving.

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

commit | commitdiff | tree

trevor_hansen [Sun, 4 Jul 2010 08:25:47 +0000 (08:25 +0000)]

Tiny speedup. Generate the encoding of multiplication slightly more efficiently.

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

commit | commitdiff | tree

trevor_hansen [Sun, 4 Jul 2010 07:58:00 +0000 (07:58 +0000)]

I didn't enable capturing of quick statistics (the -t flag) for the time spent bitblasting when using AIGS.

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

commit | commitdiff | tree

trevor_hansen [Sun, 4 Jul 2010 07:45:38 +0000 (07:45 +0000)]

Bugfix. The SMTLIB2 defines the outer bars (if present) to not be part of the symbol name.

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

commit | commitdiff | tree

trevor_hansen [Sun, 4 Jul 2010 05:42:13 +0000 (05:42 +0000)]

Get cryptominisat2 compiling:

* Add a cutdown copy of the Boost library.
* Comment out most of the Cryptominisat2 custom code. I've changed the IFDEFs to cryptominisat__2, which leaves the code in, but which isn't defined.

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

commit | commitdiff | tree

trevor_hansen [Sat, 3 Jul 2010 13:15:31 +0000 (13:15 +0000)]

Bitblast formula that don't contain arrays into and-inverter graphs. This uses the AIG implementation provided by the ABC package.

This has some advantages:
* The AIG nodes are smaller than our ASTNodes, so it uses less memory.
* The CNFs generated by ABC are smaller, so generally solving is quicker.

Some notes:
* I haven't made the CNF converter incremental, so bitblasting to AIGs is only enabled for bit-vector problems (which STP bitblasts eagerly).
* AIG re-writing isn't enabled yet.
* From prior experience some big problems fail in CNF encoding. All of our test cases pass though.

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

commit | commitdiff | tree

msoos [Fri, 2 Jul 2010 14:58:09 +0000 (14:58 +0000)]

Correcting small bug in CMS2

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

commit | commitdiff | tree

msoos [Fri, 2 Jul 2010 14:49:00 +0000 (14:49 +0000)]

Updating CMS2 to get rid of a small bug

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

commit | commitdiff | tree

msoos [Fri, 2 Jul 2010 14:36:16 +0000 (14:36 +0000)]

Removing trailing code related to pools' #ifdefs in CryptoMS

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

commit | commitdiff | tree

msoos [Fri, 2 Jul 2010 14:36:03 +0000 (14:36 +0000)]

Further updating of CryptoMiniSat2

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

commit | commitdiff | tree

msoos [Fri, 2 Jul 2010 14:35:49 +0000 (14:35 +0000)]

Updating CryptoMiniSat2 to fix some minor bugs

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

commit | commitdiff | tree

msoos [Fri, 2 Jul 2010 14:35:28 +0000 (14:35 +0000)]

Updating CryptoMiniSat2

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

commit | commitdiff | tree

trevor_hansen [Fri, 2 Jul 2010 12:06:37 +0000 (12:06 +0000)]

Rename the bitblaster class fron BitBlasterNew to BitBlaster.

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

commit | commitdiff | tree

trevor_hansen [Thu, 1 Jul 2010 14:58:47 +0000 (14:58 +0000)]

Refactor, getting ready for AIGs. This does add additional code, but that code isn't currently enabled.

* Provide a base class for ToSAT. Bitblasting via ASTNodes and AIGs both implement this class.
* BBNodeManagerAIG creates AIGs that are wrapped with a BBNode object.
* BitBlastNew is now templated on the node type and the node factory.

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

commit | commitdiff | tree

trevor_hansen [Tue, 29 Jun 2010 15:14:23 +0000 (15:14 +0000)]

Speedup. Generate nicer circuits for unsigned division.

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

commit | commitdiff | tree

trevor_hansen [Mon, 28 Jun 2010 15:12:43 +0000 (15:12 +0000)]

Change how the counter example is built. Previously the counter example relied on specific nodes existing that wont be created when we bitblast via AIGs.

I needed to reimplement the code to print the sat model too. I didn't preserve the format. I suspect though no one is parsing it.

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

commit | commitdiff | tree

trevor_hansen [Mon, 28 Jun 2010 11:48:38 +0000 (11:48 +0000)]

Speedup. Add solving for xors to the bitvector solver.

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

commit | commitdiff | tree

trevor_hansen [Mon, 28 Jun 2010 01:46:11 +0000 (01:46 +0000)]

Speedup. if (xor a b) is found, replaced a with (not b) throughout.

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

commit | commitdiff | tree

trevor_hansen [Sun, 27 Jun 2010 13:52:41 +0000 (13:52 +0000)]

Speedup. Sort EQ nodes. This prevents duplicate nodes like (= 0 a), (=a 0), from being created. The bvsolver expected nodes reversed to how they are now created.

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

commit | commitdiff | tree

trevor_hansen [Sun, 27 Jun 2010 10:59:46 +0000 (10:59 +0000)]

Speedup. Don't push extracts through ites. Sometimes this may be good to do. But usually not.

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

commit | commitdiff | tree

trevor_hansen [Sun, 27 Jun 2010 03:38:00 +0000 (03:38 +0000)]

Default to bash shell rather than sh for some calls. The call to cat was failing on a redhat machine with an "argument too long error". Hopefully this fixes it.

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

commit | commitdiff | tree

trevor_hansen [Sun, 27 Jun 2010 01:52:41 +0000 (01:52 +0000)]

Speedup. Revert back to minisat's default parameters.

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

commit | commitdiff | tree

trevor_hansen [Sun, 27 Jun 2010 01:50:22 +0000 (01:50 +0000)]

Speedup. Flatten ands at the start of the bvsolver.

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

commit | commitdiff | tree

trevor_hansen [Sat, 26 Jun 2010 14:59:32 +0000 (14:59 +0000)]

clean up two regression log names

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

commit | commitdiff | tree

trevor_hansen [Sat, 26 Jun 2010 08:44:09 +0000 (08:44 +0000)]

Speedups.

* The substitution map now substitutes for (IFF SYMBOL SYMBOL)
* sim.smt2 is the test case to check the above substitution is working.
* The ArrayTransformer creates fewer new nodes.

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

commit | commitdiff | tree

trevor_hansen [Sat, 26 Jun 2010 04:16:34 +0000 (04:16 +0000)]

Speedups.
* Call topLevel simplify only if something has changed.
* If there is a symbol on the rhs put it on the lhs, which simplifies more eqns.

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

commit | commitdiff | tree

trevor_hansen [Fri, 25 Jun 2010 08:22:50 +0000 (08:22 +0000)]

Speedups.
* Cache the max, one and zero values inside the Create__Const() functions.
* Return a reference from the [] operator to reduce unncessary copies.

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

commit | commitdiff | tree

trevor_hansen [Fri, 25 Jun 2010 05:25:17 +0000 (05:25 +0000)]

Measure the difficulty of formula by using a simple function, that amongst other things counts the number of multiplications in the input. If after simplifications the difficulty has increased. Then the original formula is used instead of the not-simplified one.

This is a very rough way of performing DAG aware simplifications.

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

commit | commitdiff | tree

trevor_hansen [Fri, 25 Jun 2010 05:19:52 +0000 (05:19 +0000)]

Use the new method to determine whether the sub-graph contains arrays.

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

commit | commitdiff | tree

trevor_hansen [Fri, 25 Jun 2010 05:16:40 +0000 (05:16 +0000)]

The array transformer now respects optimisations being disabled.

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

commit | commitdiff | tree

trevor_hansen [Fri, 25 Jun 2010 05:09:28 +0000 (05:09 +0000)]

* Add containsArrayOps(..) to check if any array terms are in the graph.
* Add missing types to the typecheck function. Clean up the type check function.

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

commit | commitdiff | tree

trevor_hansen [Thu, 24 Jun 2010 14:36:08 +0000 (14:36 +0000)]

Fix the build.

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

commit | commitdiff | tree

trevor_hansen [Thu, 24 Jun 2010 14:28:31 +0000 (14:28 +0000)]

Add a new function to replace using the substitution/solver map. It's not currently used by anything. So this checkin does nothing.

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

commit | commitdiff | tree

trevor_hansen [Thu, 24 Jun 2010 14:25:59 +0000 (14:25 +0000)]

Removing duplicate files

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

commit | commitdiff | tree

trevor_hansen [Thu, 24 Jun 2010 14:21:37 +0000 (14:21 +0000)]

Remove bio tests from regressstp. They are all included in regressbio.

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

commit | commitdiff | tree

trevor_hansen [Thu, 24 Jun 2010 14:16:34 +0000 (14:16 +0000)]

Adding realistic expected times to these test cases

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

commit | commitdiff | tree

trevor_hansen [Thu, 24 Jun 2010 14:03:37 +0000 (14:03 +0000)]

Bugfix. The script that was called by regressstp didn't record errors when some test cases failed. So I've removed it, and use the generic test runner instead. There are two differences: multiples log files are now created, and the timeout is 180 sec.

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

commit | commitdiff | tree

trevor_hansen [Thu, 24 Jun 2010 11:38:31 +0000 (11:38 +0000)]

Speedup. Better cache the variables that are discovered when looking for duplicate symbols.

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

commit | commitdiff | tree

trevor_hansen [Wed, 23 Jun 2010 15:47:01 +0000 (15:47 +0000)]

Use simplifying minisat for unit tests.

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

commit | commitdiff | tree

trevor_hansen [Wed, 23 Jun 2010 14:46:24 +0000 (14:46 +0000)]

Bugfix. Simplifying minisat wasn't using the separate malloc/free routines.

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

commit | commitdiff | tree

trevor_hansen [Wed, 23 Jun 2010 14:13:31 +0000 (14:13 +0000)]

Speedup/bugfix. Change how duplicate symbols are searched for. This fixed failing2.smt

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

commit | commitdiff | tree

trevor_hansen [Wed, 23 Jun 2010 14:12:16 +0000 (14:12 +0000)]

Short cut on constant evaluation

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

commit | commitdiff | tree

trevor_hansen [Wed, 23 Jun 2010 14:07:25 +0000 (14:07 +0000)]

Bugfix. Keep track of which symbols* have been deleted. Lots of them are duplicated in the map.

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

commit | commitdiff | tree

trevor_hansen [Wed, 23 Jun 2010 14:06:31 +0000 (14:06 +0000)]

Don't perform simplifications when creating the substitution map. I'm not sure if this is justified, but it makes STP easier to understand. I'll check if it's useful.

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

commit | commitdiff | tree

trevor_hansen [Wed, 23 Jun 2010 14:04:41 +0000 (14:04 +0000)]

Reduce memory usage. Clear out the caches from the bvsolver before calling the SAT solver.

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

commit | commitdiff | tree

trevor_hansen [Wed, 23 Jun 2010 14:02:20 +0000 (14:02 +0000)]

Fix grammar. Extra assertion.

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

commit | commitdiff | tree

trevor_hansen [Wed, 23 Jun 2010 07:48:44 +0000 (07:48 +0000)]

Speedup. Remove some unnecessary tests.

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

commit | commitdiff | tree

trevor_hansen [Wed, 23 Jun 2010 07:11:55 +0000 (07:11 +0000)]

Refactor. Make the TermOrder function a non-member function with the SubstitutionMap class.

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

commit | commitdiff | tree

trevor_hansen [Wed, 23 Jun 2010 06:05:08 +0000 (06:05 +0000)]

Speedup. Shortcut if the thing we are simplifying is already a constant.

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

commit | commitdiff | tree

trevor_hansen [Wed, 23 Jun 2010 03:53:02 +0000 (03:53 +0000)]

Speedup. The bvsolver now uses a reduced version of the ASTNode graph which contains nodes just for nodes where the number of descendant symbols changes.

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

commit | commitdiff | tree

trevor_hansen [Fri, 18 Jun 2010 11:34:10 +0000 (11:34 +0000)]

Check for duplicate variables using a different function

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

commit | commitdiff | tree

trevor_hansen [Fri, 18 Jun 2010 06:48:44 +0000 (06:48 +0000)]

Bugfix. Variables were reported as only occuring a single time, when they actually occured multiple times.

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

commit | commitdiff | tree

trevor_hansen [Fri, 18 Jun 2010 06:38:05 +0000 (06:38 +0000)]

Refactor & slight performance improvement for the bvsolver.

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

commit | commitdiff | tree

trevor_hansen [Fri, 18 Jun 2010 05:46:17 +0000 (05:46 +0000)]

Bugfix. Fix rotate_left and rotate_right to take the modulus of the shift amount. I'd misinterpreted the specification.

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

commit | commitdiff | tree

trevor_hansen [Wed, 16 Jun 2010 03:51:37 +0000 (03:51 +0000)]

Speedup. When printing out the counter example, don't call the toplevel print (which does lots of extra work). Instead call the low level print.

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

commit | commitdiff | tree

trevor_hansen [Wed, 16 Jun 2010 03:43:54 +0000 (03:43 +0000)]

Speedup. Reduce the amount of checking that the bvsolver performs.

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

commit | commitdiff | tree

trevor_hansen [Wed, 16 Jun 2010 03:22:39 +0000 (03:22 +0000)]

Speed up VarSeenInTerm(..) slightly.

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

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

STP Constraint Solver.