summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2011-06-02minor fix to build system for system testsMorgan 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-28fix unit test linking issueMorgan Deters
2011-05-28include 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-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
2011-05-14fix production-build compiler warningMorgan Deters
2011-05-14re-add a removed Datatype constructor that was causing a unit test failure, ↵Morgan Deters
so nightlies go through tonight
2011-05-14reverting node manager change from 1881; also part of parameterized ↵Morgan Deters
datatypes review
2011-05-14add AscriptionType stuff to support nullary parameterized datatypes; also, ↵Morgan Deters
review of Andy's earlier commit, with some minor code clean-up and documentation
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback