Age | Commit message (Collapse) | Author |
|
arrays, as well as pre-registration of free constants of uninterpreted sort, etc..
|
|
relevant comparison http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2602&reference_id=2590&p=5
|
|
|
|
|
|
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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
|
|
|
|
when --strict-parsing is off (which it is by default). The danoint benchmarks
have such monsters.
|
|
16. Enabled arithmetic propagation and variable removal by default. Changed the command line arguments for both propagation and variable removal allow for disabling these.
|
|
|
|
more than one "real" theory (not BUILTIN or BOOL) active
|
|
minor fix-ups to documentation and some node stuff
|
|
|
|
* 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
|
|
|
|
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.
|
|
parametric datatype versions of paper benchmarks are now working
|
|
|
|
constructor nodes created internally are given a type ascription
|
|
|
|
|
|
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.
|
|
|
|
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
|
|
easier replication of experiment)
|
|
|
|
|
|
|
|
so nightlies go through tonight
|
|
datatypes review
|
|
review of Andy's earlier commit, with some minor code clean-up and documentation
|
|
parametric datatypes, type ascriptions are not implemented yet
|
|
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
|
|
|
|
|
|
* Preprocessing-time, non-clausal, Boolean simplification round to
support "quasi-non-linear rewrites" as discussed at last few meetings.
* --simplification=none is the default for now, but we'll probably
change that to --simplification=incremental. --simplification=batch
is also a possibility. See --simplification=help for details.
* RecursionBreaker<T> now uses a hash set for the seen trail.
* Fixes to TLS stuff to support that.
* Fixes to theory and SmtEngine documentation.
* Fixes to stream indentation.
* Other miscellaneous stuff.
|
|
simplifications for the "muzzled" (i.e. competition) design, which had
been broken. Addition of some new unit test bits to ensure that
nothing is ever called in muzzled builds, e.g. things like
Warning() << expensiveFunction();
Also, fix some compiler warnings.
|
|
|
|
closure module, theory datatypes now uses transitive closure for cycle detection, bug 261 fixed
|
|
|
|
|
|
|