Age | Commit message (Collapse) | Author |
|
(*myCDMap.find(foo)).second = bar;
fail with a compile-time error (rather than being silently ignored, like
they had been).
Resolves bug #276.
|
|
infrastructure, and takes care not to affect CVC4's performance on LRA
benchmarks.
|
|
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
|
|
will be reissued. Some unexpected slowdowns, but not too much.
|
|
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).
|
|
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.
|
|
|
|
comparison <http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2673&&p=5&reference_id=2637>
|
|
|
|
|
|
|
|
|
|
|
|
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
|