| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
just the header comments at the top, though. Don't update to this rev if
you don't have time for a complete rebuild, and exclude this rev if you
want to see what's new across a range of commits.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
* Ensure Rewriter::init() is called before ::rewrite().
The array type enumerator recently gave us an end-run around
::init(). TheoryEngine no longer calls these, they're done
via static initialization.
* Respect scope for declare-sort/declare-fun/define-sort/define-fun... (resolves bug 412).
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
|
|
disabled in bitvectors due to non-stably infinite problems
the option to enable it is --theoryof-mode=term
|
|
* theories now get either an assertion from the SAT solver (normalized) or an (dis-)equality between two shared terms that is non-normalized
|
|
to catch any that I may have missed
|
|
* array now only propagates thropugh the equality engine
* assertions in the equality rewriting to ensure eq -> { eq, T, F }
|
|
|
|
Also fixed one bv rewrite failure (more to come)
|
|
"REWRITE_DONE" is idempotent
Found several problems where this is not the case and fixed them
|
|
|
|
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3828&category=&p=5&reference_id=3820
|
|
|
|
Dumping infrastructure. Can dump preprocessed queries and clauses. Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc. For a
full list of options see --dump=help.
CUDD building much cleaner.
Documentation and assertion fixes.
Printer improvements, printing of commands in language-defined way, etc.
Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.
CVC3 compatibility layer (builds as libcompat).
SWIG detection and language binding support (infrastructure).
Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).
Copyright and file headers regenerated.
|
|
|
|
caused a number of latent errors in sources and headers to come up. Those are now fixed (by adding "using" or "std::" depending on the context). Took the opportunity to bring many rewriter sources in line with coding conventions.
|
|
and not yet finalized but I need to put it in to work further with the theory writers. Please check the files that you 'own'. Any comments or discussion is welcome. Further details will be coming in a follow up email later.
|
