summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-30Fixin 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-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-25Fixing the broken unit testsDejan Jovanović
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-12forgot to reflect naming change in makefile. fixedMorgan Deters
2011-07-12fix bug 272, array unsoundness, and some array cleanupMorgan Deters
2011-07-11remove some array regressions from "make check" so nightly regressions runMorgan Deters
2011-07-11status of examplesMorgan Deters
2011-07-11new array bugs ?Morgan Deters
2011-07-11fixing out of place typename (error on g++ 4.4.3-4ubuntu5)Morgan Deters
2011-07-11submission scriptMorgan 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-11mark the new minimized benchmark as unsatMorgan 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-11minimized exampleMorgan Deters
2011-07-11array benchmarksMorgan Deters
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-10changing the sat solver remove clauses constantsDejan 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-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-09fix submission makefileMorgan Deters
2011-07-09minor fixupsMorgan Deters
2011-07-09surprize surprizeDejan Jovanović
2011-07-07removing duplicate clauses in ite cnf conversionDejan Jovanović
2011-07-07cudd-building prefs with --with-cudd / --without-cuddMorgan Deters
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-05missing test caseDejan Jovanović
2011-07-05updated preprocessing and rewriting input equalities into inequalities for LRADejan Jovanović
2011-06-30Allow (- 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-30Changed 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-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-30some 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-29Fixed spelling mistake and documentation for --enable-variable-removal.Tim King
2011-06-18Some 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-06compilation fix for x86 (from previous commit)Morgan Deters
2011-06-06Fix 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-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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback