Age | Commit message (Collapse) | Author | |
---|---|---|---|
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-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 | fix bug 272, array unsoundness, and some array cleanup | Morgan Deters | |
2011-07-11 | fixing out of place typename (error on g++ 4.4.3-4ubuntu5) | 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 | 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 | 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 | 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-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 | 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 | |||
2011-06-29 | Fixed spelling mistake and documentation for --enable-variable-removal. | Tim King | |
2011-06-18 | Some fixes inspired by Fedora 15: | Morgan Deters | |
* compilation fixes for GCC 4.6.x + ptrdiff_t is now in std:: * fix some make rules that are ok in Make 3.81 but broke in Make 3.82 * look for cxxtestgen.py as well as cxxtestgen.pl, and look for cxxtest headers in /usr/include | |||
2011-06-06 | compilation fix for x86 (from previous commit) | Morgan Deters | |
2011-06-06 | Fix for Mac OS breakage (x86 didn't crash, but probably would, eventually, ↵ | Morgan Deters | |
on some problems---valgrind gave many complaints): the problem was that calloc() (in the Backtracker) wasn't allocating enough space for the type located at the resulting address. Resolves bug #263. Also, some debugging improvements. | |||
2011-06-03 | fixed various bugs related to ambiguous parametric datatype constructors, ↵ | Andrew Reynolds | |
parametric datatype versions of paper benchmarks are now working | |||
2011-06-03 | datatypes work | Morgan Deters | |
2011-06-02 | added (temporary) support for ensuring that all ambiguously typed ↵ | Andrew Reynolds | |
constructor nodes created internally are given a type ascription | |||
2011-06-01 | minor fix, and better output for type errors | Morgan Deters | |
2011-06-01 | type ascriptions (casts) for parameterized datatypes, e.g. "nil :: list[INT] | Morgan Deters | |
2011-05-31 | This commit contains the code for allowing arbitrary equalities in the ↵ | Tim King | |
theory of arithmetic. * This code has been partially tested. (My testing situation is currently not so great.) The code for testing not preregistering equalities can be compile time enabled by setting the boolean turnOffEqualityPreRegister. Don't be shocked by slowdowns or failures. This does pass make regress as well as a fresh checkout does. (The Mac version has issues.) * I need to disable the permanent row removal heuristic by default. We need to discuss why this needs to happen. We should probably detect pure QF_LRA/QF_RDL problems and enable this when this can safely be done. * I have disabled the arithmetic rewrite equality flag. This code needs to be added to the parser. * For all of the above changes, I have annotated the code with the key word BREADCRUMB. * I have renamed ArithUnatePropagator to ArithAtomDatabase. | |||
2011-05-28 | fix unit test linking issue | Morgan Deters | |
2011-05-28 | include subversion information used for each build in the --show-config ↵ | Morgan Deters | |
output and as a banner in --interactive mode; intended to resolve confusion in cases where you don't know where a CVC4 binary came from | |||
2011-05-26 | apply arithmetic static learner's miplibtrick in a consistent order (for ↵ | Morgan Deters | |
easier replication of experiment) | |||
2011-05-23 | fixes for "make dist" and "make doc", minor cleanups | Morgan Deters | |
2011-05-23 | Merge from arrays2 branch. | Morgan Deters | |
2011-05-14 | fix production-build compiler warning | Morgan Deters | |
2011-05-14 | re-add a removed Datatype constructor that was causing a unit test failure, ↵ | Morgan Deters | |
so nightlies go through tonight | |||
2011-05-14 | reverting node manager change from 1881; also part of parameterized ↵ | Morgan Deters | |
datatypes review |