summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Collapse)Author
2011-09-30more push/pop infrastructure, some SAT stuffMorgan Deters
2011-09-30fixes to incremental simplification, cnf routines, other stuff in ↵Morgan Deters
preparation of user push/pop in SAT solver
2011-09-29build system fixesMorgan Deters
2011-09-29Some 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-28variety of visibility fixes (should clean up some of the many warnings on ↵Morgan Deters
MacOS-production-dynamic builds)
2011-09-16include example theory (former "UF-Tim") that's included in the dist but not ↵Morgan Deters
built for the library
2011-09-16final(?) documentation fixesMorgan Deters
2011-09-16fix up more documentationMorgan Deters
2011-09-16fix serious issue with copyright-updating scriptMorgan Deters
2011-09-16fix numerous documentation issues; doxygen complains much less, nowMorgan Deters
2011-09-15tim's fixes for context-dependent pre-registrationDejan Jovanović
2011-09-15additional stuff for sharing, Dejan Jovanović
2011-09-07fixes for uf/equality engine from the quantifiers branch. mainly ↵Dejan Jovanović
backtracking issues.
2011-09-03removing an assert i forgot to remove that andy foundDejan Jovanović
2011-09-02Merge 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-02Partial merge of integers work; this is simple B&B and some pseudobooleanMorgan 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-27Removing 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-24Simplification 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-23some uf cleanupDejan Jovanović
2011-08-17new implementation of lemmas on demandDejan Jovanović
comparison <http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2673&&p=5&reference_id=2637>
2011-07-12fix bug 272, array unsoundness, and some array cleanupMorgan Deters
2011-07-11fixing out of place typename (error on g++ 4.4.3-4ubuntu5)Morgan Deters
2011-07-11Adding static_fact_managerClark Barrett
2011-07-11Clark's work on array theory - can now solve all QF_AX problemsClark Barrett
2011-07-11fix some confusing debug output (bogus counter)Morgan Deters
2011-07-11if 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-11adding disequality propagationDejan Jovanović
relevant comparison http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2602&reference_id=2590&p=5
2011-07-11merge from symmetry branchMorgan Deters
2011-07-10Reverting mistaken check-inClark Barrett
2011-07-10Fixed bug in default solve - wasn't returning when it was supposed toClark Barrett
2011-07-10another typoDejan Jovanović
2011-07-10yet another uf bug fix, hopefully the lastDejan Jovanović
2011-07-10another bugfix for ufDejan Jovanović
2011-07-09some immediate bug fixesDejan Jovanović
2011-07-09minor fixupsMorgan Deters
2011-07-09surprize surprizeDejan Jovanović
2011-07-06Fixing 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-05updated preprocessing and rewriting input equalities into inequalities for LRADejan Jovanović
2011-06-30Merging the playground branch upto r1957 into trunk.Tim King
2011-06-30only 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-03fixed various bugs related to ambiguous parametric datatype constructors, ↵Andrew Reynolds
parametric datatype versions of paper benchmarks are now working
2011-06-03datatypes workMorgan Deters
2011-06-02added (temporary) support for ensuring that all ambiguously typed ↵Andrew Reynolds
constructor nodes created internally are given a type ascription
2011-06-01minor fix, and better output for type errorsMorgan Deters
2011-06-01type ascriptions (casts) for parameterized datatypes, e.g. "nil :: list[INT]Morgan Deters
2011-05-31This 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-26apply arithmetic static learner's miplibtrick in a consistent order (for ↵Morgan Deters
easier replication of experiment)
2011-05-23fixes for "make dist" and "make doc", minor cleanupsMorgan Deters
2011-05-23Merge from arrays2 branch.Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback