Age | Commit message (Collapse) | Author | |
---|---|---|---|
2011-09-07 | fixes for uf/equality engine from the quantifiers branch. mainly ↵ | Dejan Jovanović | |
backtracking issues. | |||
2011-09-03 | this should fix the build; doxygen documentation now gets built in ↵ | Morgan Deters | |
srcdir/doc/doxygen | |||
2011-09-03 | Disable a warning to address bug 277. (This doesn't really resolve the ↵ | Morgan Deters | |
issue, but the warning isn't dangerous here. See the bugzilla comments.) | |||
2011-09-03 | removing an assert i forgot to remove that andy found | Dejan Jovanović | |
2011-09-02 | Merge from my post-smtcomp branch. Includes: | Morgan Deters | |
Dumping infrastructure. Can dump preprocessed queries and clauses. Can also dump queries (for testing with another solver) to see if any conflicts are missed, T-propagations are missed, all lemmas are T-valid, etc. For a full list of options see --dump=help. CUDD building much cleaner. Documentation and assertion fixes. Printer improvements, printing of commands in language-defined way, etc. Typechecker stuff in expr package now autogenerated, no need to manually edit the expr package when adding a new theory. CVC3 compatibility layer (builds as libcompat). SWIG detection and language binding support (infrastructure). Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode (when not in compliance mode). Copyright and file headers regenerated. | |||
2011-09-02 | Ensure that assignment gestures through CDMap iterators like: | Morgan Deters | |
(*myCDMap.find(foo)).second = bar; fail with a compile-time error (rather than being silently ignored, like they had been). Resolves bug #276. | |||
2011-09-02 | Partial merge of integers work; this is simple B&B and some pseudoboolean | Morgan Deters | |
infrastructure, and takes care not to affect CVC4's performance on LRA benchmarks. | |||
2011-09-02 | * Changing pre-registration to be context dependent -- it is called from the ↵ | Dejan Jovanović | |
SAT solver on every backtrack * Updated UF to handle the context dependent pre-registration * Additionally some small changes in order to satisfy warnings of the eclipse code analysis tool | |||
2011-08-30 | Fixin the SAT solver for Andy. Even if a SAT lemma is added, a FULL-CHECK ↵ | Dejan Jovanović | |
will be reissued. Some unexpected slowdowns, but not too much. | |||
2011-08-27 | Removing Theory::registerTerm() as discussed in the meeting. Now ↵ | Dejan Jovanović | |
pre-register is called on all the theory terms and the foreign-terms also. This means, if x: REAL and f:REAL, that in f(x) >= 0, arithmetic gets pre-register call with x, f(x) and f(x) >= 0, while UF gets pre-register call with x, f(x). | |||
2011-08-25 | Fixing the broken unit tests | Dejan Jovanović | |
2011-08-24 | Simplification of the preregister and register throught a NodeVisitor class. ↵ | Dejan Jovanović | |
The theoryOf is not all in one place, theory::theoryOf. The uninterpreted sorts belong to the builtin theory and are dispatched to the apropriate theory (QF_UF, QF_AX) through theoryOf based on the setting in the Theory class. | |||
2011-08-23 | some uf cleanup | Dejan Jovanović | |
2011-08-17 | new implementation of lemmas on demand | Dejan Jovanović | |
comparison <http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2673&&p=5&reference_id=2637> | |||
2011-07-12 | forgot to reflect naming change in makefile. fixed | Morgan Deters | |
2011-07-12 | fix bug 272, array unsoundness, and some array cleanup | Morgan Deters | |
2011-07-11 | remove some array regressions from "make check" so nightly regressions run | Morgan Deters | |
2011-07-11 | status of examples | Morgan Deters | |
2011-07-11 | new array bugs ? | Morgan Deters | |
2011-07-11 | fixing out of place typename (error on g++ 4.4.3-4ubuntu5) | Morgan Deters | |
2011-07-11 | submission script | Morgan Deters | |
2011-07-11 | Adding static_fact_manager | Clark Barrett | |
2011-07-11 | Clark's work on array theory - can now solve all QF_AX problems | Clark Barrett | |
2011-07-11 | fix some confusing debug output (bogus counter) | Morgan Deters | |
2011-07-11 | mark the new minimized benchmark as unsat | Morgan Deters | |
2011-07-11 | if running in QF_AX, equalities over terms of uninterpreted sort go to ↵ | Morgan Deters | |
arrays, as well as pre-registration of free constants of uninterpreted sort, etc.. | |||
2011-07-11 | minimized example | Morgan Deters | |
2011-07-11 | array benchmarks | Morgan Deters | |
2011-07-11 | adding disequality propagation | Dejan Jovanović | |
relevant comparison http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2602&reference_id=2590&p=5 | |||
2011-07-11 | merge from symmetry branch | Morgan Deters | |
2011-07-10 | Reverting mistaken check-in | Clark Barrett | |
2011-07-10 | changing the sat solver remove clauses constants | Dejan Jovanović | |
with these we get closer to yices on uf and it seems better on lra vs yices uf http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2590&category=&p=5&reference_id=1471 vs trunk on lra http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2591&category=&p=5&reference_id=2576 | |||
2011-07-10 | Fixed bug in default solve - wasn't returning when it was supposed to | Clark Barrett | |
2011-07-10 | another typo | Dejan Jovanović | |
2011-07-10 | yet another uf bug fix, hopefully the last | Dejan Jovanović | |
2011-07-10 | another bugfix for uf | Dejan Jovanović | |
2011-07-09 | some immediate bug fixes | Dejan Jovanović | |
2011-07-09 | fix submission makefile | Morgan Deters | |
2011-07-09 | minor fixups | Morgan Deters | |
2011-07-09 | surprize surprize | Dejan Jovanović | |
2011-07-07 | removing duplicate clauses in ite cnf conversion | Dejan Jovanović | |
2011-07-07 | cudd-building prefs with --with-cudd / --without-cudd | Morgan Deters | |
2011-07-06 | Fixing two bugs: | Dejan Jovanović | |
1) arithmetic should check for subterms when solving equations, for instance x = if b then x + 1 else x -1 is not a valid substitution 2) a memory problem in minisat - explanations are constructed during conflict analysis, so the clause database might resize and relocate, which invalidates any references to clauses | |||
2011-07-05 | missing test case | Dejan Jovanović | |
2011-07-05 | updated preprocessing and rewriting input equalities into inequalities for LRA | Dejan Jovanović | |
2011-06-30 | Allow (- x) for unary minus in SMT-LIBv1, in addition to the standard (~ x), | Morgan Deters | |
when --strict-parsing is off (which it is by default). The danoint benchmarks have such monsters. | |||
2011-06-30 | Changed the defaults for arithPivotThreshold and arithPropagateMaxLength to ↵ | Tim King | |
16. Enabled arithmetic propagation and variable removal by default. Changed the command line arguments for both propagation and variable removal allow for disabling these. | |||
2011-06-30 | Merging the playground branch upto r1957 into trunk. | Tim King | |
2011-06-30 | only use theory registration if (1) a theory requests it, or (2) if there's ↵ | Morgan Deters | |
more than one "real" theory (not BUILTIN or BOOL) active | |||
2011-06-30 | some things I had laying around in a directory but never got committed; ↵ | Morgan Deters | |
minor fix-ups to documentation and some node stuff |