| Age | Commit message (Collapse) | Author |
|---|
|
(extended) SMT command get-model. added collectModelInfo and removed getValue from theory interface. merge also includes major updates to finite model finding module (from CASC), added fmf options, some updates to strong solver and quantifiers engine interface. The test recursion_breaker_black currently fails for me on production builds, Morgan is planning to look into this.
|
|
|
|
- please look at the diff and make sure I didn't do something stupid
|
|
See below for details.
* Fix the "assert" name-collision bug (resolves bug #364).
Our identifiers should never be named "assert", as that's a preprocessor
definition in <assert.h>, which is often #included indirectly (so simply
having a policy of not including <assert.h> isn't good enough---one of
our dependences might include it). It was once the case that we didn't
have anything named "assert", but "assert()" has now crept back in.
Instead, name things "assertFoo()" or similar. Thanks to Tim for the
report.
To fix this, I've changed some of Dejan's circuit-propagator code from
"assert()" to "assertTrue()". Ditto for Andy's explanation manager.
Guys, if you prefer a different name in your code, please change it.
* Fix the incorrect parsing of lets in SMT-LIBv2 parser (resolves bug #365).
Inner lets now shadow outer lets (previously, they incorrectly gave an
error). Additionally, while looking at this, I found that a sequential let
was implemented rather than a parallel let. This is now fixed. Thanks to
Liana for the report.
* Remove ANTLR parser generation warnings in CVC parser (resolves bug #314).
* There were a lot of Debug lines in bitvectors that had embedded toString()
calls. This wasted a LOT of time in debug builds for BV benchmarks
(like in "make regress"). Added if(Debug.isOn(...)) guards; much faster
now.
* Support for building public-facing interface documentation only (as opposed
to all internals documentation). Now "make doc" does the public-facing and
"make doc-internals" does documentation of everything. (Along with changes
to the nightly build script---which will now build and publish both types
of Doxygen documentation---this resolves bug #359).
* Fix the lambda typechecking bug (resolves bug #322). Thanks to Andy for the
report (a long long time ago--sorry).
* The default output language for all streams is now based on the current set
of Options (if there is one). This has been a constant annoyance, especially
when stringstreams are used to construct output. However, it doesn't work
for calls from outside the library, so it's mainly an annoyance-fixer for
CVC4 library code itself.
* Add some CVC4_UNUSED markers to local variables in theory_arith.cpp that
are used only in assertions-enabled builds (and thus give warnings in
production builds). This was briefly discussed at the meeting this week.
|
|
\file tags corrected, copyright added to files that had it missing, etc.
I ensured that I didn't change any code with this commit, and even tested on the cluster to be doubly sure:
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4655&reference_id=4646&p=0
|
|
|
|
|
|
|
|
|
|
|
|
ArithPriorityQueue::reduce(), ::begin() and ::end().
|
|
|
|
|
|
superset of the basic variables that violate a bound to the exact set.
|
|
never made it to trunk. Do not know how. The fix to the bug is pending the hunt for bug 363.
|
|
|
|
|
|
result
|
|
|
|
|
|
|
|
|
|
other minor change is removing dependency of header file in
theory_engine.h
It fixes all known wrong answers in QF_BV and QF_AUFBV. It doesn't fix a
wrong answer for QF_AUFLIA -- it is currently unclear what is the cause
of this bug, could be sharing.
Performance impact (turns out) is none on QF_BV and QF_AUFBV (except, of
course, those for which the answer was wrong earlier; and also perhaps
one or two off-cases)
The issue was with how the infinite loop in justification stuff was prevented.
To keep it short, I skip what was wrong earlier, and this is what is done
now:
* whenever an atomic formula is seen, a list of pairs of <IteSkolemVariable,
AssertionCorrespondingToIteSkolem> is created for each skolem occuring in
the atom.
* we iterate over this list, doing the following: check if skolem is marked
as visited. if not, mark visited, recurse, when back unmark.
I lied, I will tell you what was being done earlier was -- 1. the check for
not being visited was being done in each recursive call, not just for atoms.
2. The AssertionCorrespondingToIteSkolem was being used to check if something
is visited and not IteSkolemVariable. I don't know if this makes any
difference, but anyhow, I think this is cleaner & clearer, so I keep this.
|
|
disabled in bitvectors due to non-stably infinite problems
the option to enable it is --theoryof-mode=term
|
|
whitespace issues in smt_engine.cpp.
|
|
|
|
|
|
could introduce additional assertions that were not beign processed by the
decision engine. Now these assertions are merged in with pre-ITE-removal
assertions, ensuring the decision engine sees them.
|
|
|
|
get bitblasted, it would restart to add the clauses, and loose propagation information.
|
|
|
|
|
|
|
|
simplification for some benchmarks
|
|
reenqueued so that the queue was a superset of the failing assertions. This adds a super expensive debug routine unenqueuedVariablesAreConsistent() that catches this bug. This is enabled when -d arith::consistency is turned on. make check passes with this flag enabled.
|
|
imporant: theories SHOULD NOT use getSatValue at all, otherwise they might create a conflict with a literal they didn't get()
|
|
|
|
|
|
non-SAT-solver) uses of std::cout to the Message stream, and all uses of std::cerr to the Warning stream.
|
|
|
|
|
|
* dramatically less terms to manage by doing reflexivity semantically
* fixes the problem clark had with not detecting inconsistencies with shared terms
i'm not sure what's the performance impact, but this is so much better and we'll deal with performance later
|
|
restricted-simplex.
|
|
* theories now get either an assertion from the SAT solver (normalized) or an (dis-)equality between two shared terms that is non-normalized
|
|
|
|
- Changes how CongruenceManager reports conflicts.
- ConstraintDatabase can now detect and raise conflicts when doing unate propagation.
|
|
|
|
|
|
|
|
|
