Age | Commit message (Collapse) | Author | |
---|---|---|---|
2012-04-04 | * added propagation as lemmas to TheoryBV: | Liana Hadarean | |
* modified BVMinisat to work incrementally * added more bv regressions | |||
2012-04-03 | Fix for make dist. | Tim King | |
2012-04-02 | Fix for broken unit tests from the previous commit. | Tim King | |
2012-04-02 | - Merged in the branch cdlist-cleanup. | Tim King | |
- This adds a CleanUp template argument to CDList. - CDChunkList<T> replaces the CDList specialization for ContextMemoryAllocator. - CDVector<T> has been simplified and improved. - The expected performance impact is negligible. | |||
2012-04-02 | fix for cvc4_logic dump | Kshitij Bansal | |
2012-04-02 | Removing large and unused regress2 benchmarks to decrease the size of checkouts. | Tim King | |
2012-03-30 | some more build system fixes | Dejan Jovanović | |
2012-03-30 | fixing some build systme warnings | Dejan Jovanović | |
2012-03-29 | Fix for bug 316. If the flag @CVC4_TLS_SUPPORTED@ is false, function ↵ | Tim King | |
pointers cannot be directly used with the CVC4_THREADLOCAL macro. This is why there were problems on macs. | |||
2012-03-29 | Fixes a linking problem with the new SatSolverConstructor on Mac. | Tim King | |
2012-03-29 | bringing cryptominisat into the main branch | Dejan Jovanović | |
2012-03-28 | enabling the --disable-arithmetic-propagation option in the arithmetic code ↵ | Dejan Jovanović | |
(it wasn't used) | |||
2012-03-28 | fix swig-ignored interface name; hopefully fixes Debian package nightly builds | Morgan Deters | |
2012-03-28 | Update to the ArithRewriter to remove REWRITE_AGAIN_FULL and limit ↵ | Tim King | |
REWRITE_AGAIN calls. | |||
2012-03-28 | Some renaming and refactoring in SAT | Dejan Jovanović | |
2012-03-28 | getting rid of a rewrite in uf sharing, speeds things up a bit | Dejan Jovanović | |
2012-03-28 | fixed faulty bv rewrite rule | Liana Hadarean | |
2012-03-28 | adding an extra cache check in the rewriter, speeds things a bit | Dejan Jovanović | |
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3828&category=&p=5&reference_id=3820 | |||
2012-03-26 | Global registry of SAT solvers, where they are registered at compile time. ↵ | Dejan Jovanović | |
The available SAT solvers can be seen with the --show-sat-solvers option. | |||
2012-03-26 | More cleaning up. | Dejan Jovanović | |
2012-03-26 | more datail from the build failure | Dejan Jovanović | |
2012-03-26 | with a small fix | Dejan Jovanović | |
2012-03-26 | forgot to commit this one, fixing build errors | Dejan Jovanović | |
2012-03-25 | moving minisat implementation into their respective directories (regular and bv) | Dejan Jovanović | |
2012-03-25 | sat_module.h,cpp -> sat_solver.h,cpp (as intended) | Dejan Jovanović | |
2012-03-25 | sat.h,cpp -> theory_proxy.h,cpp (this is what it defines) | Dejan Jovanović | |
2012-03-24 | a cute script to make a video of development from the svn logs | Dejan Jovanović | |
2012-03-23 | Removed the variableRemovalEnabled option and d_removedRows from ↵ | Tim King | |
TheoryArith. This had been disabled for several months. | |||
2012-03-22 | * improving arithmetic getEqualityStatus | Dejan Jovanović | |
* some sharing improvements based on model | |||
2012-03-22 | Merged updated version of the bitvector theory: | Liana Hadarean | |
* added simplification rewrites | |||
2012-03-22 | some improvements to the sharing mechanism/interface | Dejan Jovanović | |
2012-03-21 | Disable nonclausal simplification for QF_SAT benchmarks by default. | Morgan Deters | |
(Can be overridden with --simplification=batch, for example.) | |||
2012-03-09 | Some work on the dump infrastructure to support portfolio work. | Morgan Deters | |
Dump("foo") << FooCommand(...); now "dumps" the textual representation of the command (in the current output language) to a file, IF dumping is on at configure-time, AND the "muzzle" feature is off, AND the "foo" flag is turned on for the dump stream during this run. If it's a portfolio build, the above will also store the command in a CommandSequence, IF the "foo" flag is turned on for the dump stream during this run. This is done even if the muzzle is on. This commit also cleans up some code that used the dump feature (in arrays, particularly). | |||
2012-03-09 | fix a "lost command" bug and associated memory leak in SMT-LIBv1 parser due ↵ | Morgan Deters | |
to an out-of-place parenthesis | |||
2012-03-09 | Strengthen minisat assertion regarding t-propagations that was ↵ | Morgan Deters | |
unintentionally allowing a theory to propagate p and ~p at the same time (and the conflict was undetected, leading to an incorrect answer). Credit to Clark for finding this. | |||
2012-03-09 | minor fixes: to "make dist" in build directories with language bindings ↵ | Morgan Deters | |
enabled; and to makefile standards conformance | |||
2012-03-08 | fix "make dist" | Morgan Deters | |
2012-03-08 | Fixin the bug Clark found. In final check, enqueued propagations were not ↵ | Dejan Jovanović | |
discharged. | |||
2012-03-08 | Removing QUICK_CHECK, and other unused ones, from the Theory::Effort. | Dejan Jovanović | |
Seems to be working better <http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3749&category=&p=5&reference_id=3739>, and should fix the failing cases in the regressions. Removing one test case from the integer regress0. | |||
2012-03-07 | cdqueue : fix size(). Thank you Clark for spotting this silly mistake. | François Bobot | |
2012-03-07 | fix some Java compatibility-layer interface problems; also fix some Mac OS X ↵ | Morgan Deters | |
build issues | |||
2012-03-06 | updating the equality engine to be able to give explanations for terms that ↵ | Dejan Jovanović | |
were not in the databas (queried by areEqual and areDisequal) and it's a bit better http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3738&category=&p=-1&reference_id=3731 | |||
2012-03-03 | Changing the dependency checking; GMP is required (and sometimes must be ↵ | Morgan Deters | |
explicitly linked in with -l) when using CLN. Fixes a bug on recent Debian that Francois reported. Hopefully this doesn't break anything.. | |||
2012-03-02 | Remove some commented out code from sat.h | Kshitij Bansal | |
2012-03-02 | This commit merges in the changes from branches/arithmetic/refactor0 | Tim King | |
- Improved the checks in AssertLower and AssertUpper so that redundant bounds cause less work. - Because of the above change, d_constantIntegerVariables now cannot have duplicate elements enqueued. This allows removing d_varsInDioSolver. - Fix to an assertion in CDQueue. - Implements a CDArithVarSet using a vector of booleans and CDList. - Refactored ArithVar out of arith_utilities.h. Miscellaneous cleanup of arithmetic. | |||
2012-03-02 | CDMap -> CDHashMap | Dejan Jovanović | |
CDSet -> CDHashSet | |||
2012-03-02 | committing the TNode/Node fix that was in the kind-backend branch; there's ↵ | Morgan Deters | |
still something fishy here, I think I need to merge in a few more things to support incrementality properly. But this fixes "make check" for now | |||
2012-03-02 | Renamed CDQueue to CDTrailQueue and CDQueue2 to CDQueue. Small changes to ↵ | Tim King | |
function names and documentation. | |||
2012-03-01 | Partial merge from kind-backend branch, including Minisat and CNF work to | Morgan Deters | |
support incrementality. Some clean-up work will likely follow, but the CNF/Minisat stuff should be left pretty much untouched. Expected performance change negligible; slightly better on memory: http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5 Note that there are crashes, but that these are exhibited in the nightly regression run too! | |||
2012-03-01 | cdqueue2 : cdlist that can be used like queue and can delete element that ↵ | François Bobot | |
will never be restored |