]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commit
projects / francis / stp.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 25e5a9f) | patch
Use the advanced CNF generator to encode array problems into CNF. Array axioms are...
authortrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Sun, 19 Jun 2011 09:06:06 +0000 (09:06 +0000)
committertrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Sun, 19 Jun 2011 09:06:06 +0000 (09:06 +0000)
commit1aa3f10a67b0037793f112d13798b707846d0651
treed9e7d56f37bbd126c17da94aef3734e9d9675396tree | snapshot
parent25e5a9ffd4c980630082213d96ff239e4b9f4e37commit | diff
Use the advanced CNF generator to encode array problems into CNF. Array axioms are generated by hand. NB. This slows down the CVC regressions substantially. Adding about 40 seconds to them. The CVC array problems are very easy, so the extra effort in generating a better CNF is wasted.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1345 e59a4935-1847-0410-ae03-e826735625c1
src/AST/ArrayTransformer.cpp diff | blob | history
src/AST/ArrayTransformer.h diff | blob | history
src/absrefine_counterexample/AbstractionRefinement.cpp diff | blob | history
src/to-sat/AIG/ToCNFAIG.cpp diff | blob | history
src/to-sat/AIG/ToCNFAIG.h diff | blob | history
src/to-sat/AIG/ToSATAIG.cpp diff | blob | history
src/to-sat/AIG/ToSATAIG.h diff | blob | history
STP Constraint Solver.