Age | Commit message (Collapse) | Author | |
---|---|---|---|
2011-07-11 | mark the new minimized benchmark as unsat | 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 | minimized example | Morgan Deters | |
2011-07-11 | array benchmarks | Morgan Deters | |
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 | fix submission makefile | Morgan Deters | |
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-07 | cudd-building prefs with --with-cudd / --without-cudd | Morgan Deters | |
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 | missing test case | Dejan Jovanović | |
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 | minor fix to build system for system tests | 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 | |||
2011-05-14 | add AscriptionType stuff to support nullary parameterized datatypes; also, ↵ | Morgan Deters | |
review of Andy's earlier commit, with some minor code clean-up and documentation | |||
2011-05-13 | added support for parametric datatypes, updated cvc parser to handle ↵ | Andrew Reynolds | |
parametric datatypes, type ascriptions are not implemented yet | |||
2011-05-13 | * fix for Mac OS (includes some ThreadLocal stuff copied in from portfolio | Morgan Deters | |
branch) * add Theory::isSharedTermFact() -- it currently always returns false, pending theory combination work * Add "unknown" cardinalities to Cardinality class * Fix run_regression script to handle CRLF line terminators on Macs (where sed is non-GNU) * Convert CRLF line terminators in datatypes regressions to LF | |||
2011-05-06 | Deleting dead code. | Tim King | |
2011-05-06 | added 10 benchmarks to regress/regress0/datatypes from paper | Andrew Reynolds | |