Age | Commit message (Collapse) | Author | |
---|---|---|---|
2011-09-30 | more push/pop infrastructure, some SAT stuff | Morgan Deters | |
2011-09-30 | fixes to incremental simplification, cnf routines, other stuff in ↵ | Morgan Deters | |
preparation of user push/pop in SAT solver | |||
2011-09-29 | build system fixes | Morgan Deters | |
2011-09-29 | Some base infrastructure for user push/pop; a few bugfixes to user push/pop ↵ | Morgan Deters | |
and model gen also. I also expect this commit to fix bug #273. No performance change is expected on regressions with this commit, see http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2871&reference_id=2863 | |||
2011-09-28 | variety of visibility fixes (should clean up some of the many warnings on ↵ | Morgan Deters | |
MacOS-production-dynamic builds) | |||
2011-09-16 | include example theory (former "UF-Tim") that's included in the dist but not ↵ | Morgan Deters | |
built for the library | |||
2011-09-16 | final(?) documentation fixes | Morgan Deters | |
2011-09-16 | fix up more documentation | Morgan Deters | |
2011-09-16 | fix serious issue with copyright-updating script | Morgan Deters | |
2011-09-16 | fix numerous documentation issues; doxygen complains much less, now | Morgan Deters | |
2011-09-15 | tim's fixes for context-dependent pre-registration | Dejan Jovanović | |
2011-09-15 | additional stuff for sharing, | Dejan Jovanović | |
2011-09-07 | fixes for uf/equality engine from the quantifiers branch. mainly ↵ | Dejan Jovanović | |
backtracking issues. | |||
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 | 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-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 | 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-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 | 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-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-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 | |