Age | Commit message (Collapse) | Author | |
---|---|---|---|
2012-06-09 | Dagification of output expressions. | Morgan Deters | |
By default, common subexpressions are dagified if they appear > 1 time and are not constants or variables. This can be changed with --default-expr-dag=N --- N is a threshold such that if the subexpression occurs > N times, it is dagified; a setting of 0 turns off dagification entirely. If you notice strange dumping behavior (taking too long to print anything, e.g.), revert to the old behavior with --default-expr-dag=0 and let me know of the problem. | |||
2012-06-08 | The option --arith-presolve-lemmas had previously been renamed --unate-lemmas. | Morgan Deters | |
This commit just renames it in --help documentation, etc. | |||
2012-06-08 | Extend Printer infrastructure also to the "Result" class, meaning that ↵ | Morgan Deters | |
different output languages can write "sat", "unsat", etc., in different ways. No output is changed by this commit, but the flexibility is added that Francois wanted at today's meeting. | |||
2012-06-08 | minor fixes, for Mac OS | Morgan Deters | |
2012-06-08 | very small fast example for the bv fail | Dejan Jovanović | |
2012-06-08 | Fix SMT-LIBv2 ALL_SUPPORTED logic inference (by inferring it earlier). | Morgan Deters | |
2012-06-08 | handle BitVectorSignExtend in pickler | Kshitij Bansal | |
2012-06-08 | threadlocal | Kshitij Bansal | |
2012-06-08 | Merge from decision branch (till r3663) | Kshitij Bansal | |
(no performace or search behavior changes expected) | |||
2012-06-08 | small fuzz examples where bv fails | Dejan Jovanović | |
2012-06-07 | fixing the wrong results. arrays equality adaptor had a missing case when ↵ | Dejan Jovanović | |
propagating disequalities between shared terms. | |||
2012-06-07 | LogicInfo locking implemented, and some initialization-order issues in ↵ | Morgan Deters | |
SmtEngine resolved. ALL_SUPPORTED and QF_ALL_SUPPORTED logics now supported by SMT-LIB parsers. In SMT-LIBv2, if a (set-logic..) command is missing, ALL_SUPPORTED is assumed, and a warning is issued, as discussed on the cvc4-devel mailing list. | |||
2012-06-07 | Fixed performance issue with ite_simplifier on some QF_AUFBV benchmarks | Clark Barrett | |
2012-06-07 | Adding EchoCommand and associated printer and parser rules: | Morgan Deters | |
* SMT-LIBv2 parser now supports (echo...). * Dump() gestures can now dump EchoCommands in CVC and SMT-LIB formats. This can make it much easier to interpret output. | |||
2012-06-07 | cleaning up the expample for the future | Dejan Jovanović | |
2012-06-07 | Added small test case for diseq propagation | Clark Barrett | |
2012-06-07 | fixing some bugs in propagation of disequalities | Dejan Jovanović | |
still doesnt fix the wrong answers thought :( | |||
2012-06-06 | Don't ever call nonclausalSimplify if simplificationMode = NONE (even if | Clark Barrett | |
repeatSimp is true) | |||
2012-06-06 | Fixed assertion failures | Clark Barrett | |
2012-06-06 | removing std::cout from trunk | Morgan Deters | |
2012-06-06 | also remove now-incorrect comment from makefile | Morgan Deters | |
2012-06-06 | Fixed broken test case, removed one that is a mistake | Clark Barrett | |
2012-06-06 | unconstrained regressions are now run with "make check", but with ↵ | Morgan Deters | |
--unconstrained-simp option | |||
2012-06-06 | Fixing numerous issues with tests and "make dist": | Morgan Deters | |
* test/regress/regress0/unconstrained wasn't being distributed. This caused the debian build failure last night. (It still doesn't run on "make check", but had to be distributed properly.) * Fixing an issue where a test name was longer than 99 characters and couldn't be distributed in the "old" tar format. (Told automake to use a newer tar format.) | |||
2012-06-06 | disabling a super-expensive assertions to speed up debug runs | Dejan Jovanović | |
2012-06-06 | Changes to the combination mechanism, lots of details. Not done yet, there ↵ | Dejan Jovanović | |
are still the AUFBV wrong results, but it seems better. http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4382&reference_id=4359&p=5 | |||
2012-06-06 | Fixed problem causing crash at destruction time | Clark Barrett | |
2012-06-05 | More clean-up | Clark Barrett | |
2012-06-05 | Fixed a performance issue with unconstrained simplifier | Clark Barrett | |
2012-06-05 | Adding missing files... | Clark Barrett | |
2012-06-04 | Added preprocessing pass that propagates unconstrained values - solves all of | Clark Barrett | |
the unconstrained examples in QF_AUFBV/brummayerbiere3 - should also help generally on at least BV and maybe others. Off by default for now - results are mixed and it's hard to evaluate with so many existing assertion failures and segfaults - will re-evaluate once those are fixed | |||
2012-06-01 | add a global user-context push/pop in smt engine, just like clark's addition ↵ | Morgan Deters | |
the other day of a push/pop of the sat context | |||
2012-05-31 | Fixed bug in bv: one more case where non-shared equality was getting propagated | Clark Barrett | |
Added a global push and pop around solving - fixes an assertion failure when TNodes are still around in a CDHashMap at destruction time. | |||
2012-05-31 | svn:ignore a parallel-tests driver file that automake deposits in config/ | Morgan Deters | |
2012-05-31 | pass JAVA_CPPFLAGS properly | Morgan Deters | |
2012-05-30 | Added BitwiseEq bitvector rewrite | Clark Barrett | |
Added option "--repeat-simp" which repeats nonclausal simplification: 4 times, twice before ite removal and twice after Enabled these options (plus ite-simp) on QF_AUFBV, obtaining significant speedup on dwp examples | |||
2012-05-30 | Fixed problem with array queue growing too large | Clark Barrett | |
2012-05-30 | remove unused/broken check build target | Morgan Deters | |
2012-05-29 | removing now-unused TheoryEngine::setLogic() interface function | Morgan Deters | |
2012-05-29 | Enabled SolveEq bv rewrite | Clark Barrett | |
2012-05-28 | Added some BV rewrites, fixed bugs in array theory, made ite simp work with BV | Clark Barrett | |
2012-05-27 | some reordering to keep invariants | Dejan Jovanović | |
2012-05-27 | Committing the work on equality engine, I need to see how it does on the ↵ | Dejan Jovanović | |
regressions. New additions: * areDisequal(x, y) -> areDisequal(x, y, needProof): when asking for a disequality you must say needProof if you will ask for an explanation later. * propagation of shared dis-equalities (not yet complete, once case missing) * changes to the theories that use it, authors should check up on the changes | |||
2012-05-27 | Another expensive function call in a Debug trace | Clark Barrett | |
2012-05-27 | Another expensive function call in a Debug line | Clark Barrett | |
2012-05-25 | init bug fix | Kshitij Bansal | |
2012-05-25 | Checking in fix for bug 340 - somehow didn't get checked in earlier | Clark Barrett | |
2012-05-24 | Separating the subtheory implementations in the bitvector theory. | Dejan Jovanović | |
2012-05-24 | Significant changes to the internals of the equality engine. Equality is not ↵ | Dejan Jovanović | |
handled natively and not as a generic predicate. The changes also change the order of propagation, and can produce different conflicts. Since the engine is now used everywhere this means that so some crazy results are to be expected. | |||
2012-05-22 | This commit merges in the branch arithmetic/cprop. | Tim King | |