Age | Commit message (Collapse) | Author | |
---|---|---|---|
2012-06-15 | Fixes some assertion failures | Clark Barrett | |
2012-06-15 | one bug fixed | Kshitij Bansal | |
2012-06-14 | fixing the problems with the bvminisat. there was a case when things would ↵ | Dejan Jovanović | |
get bitblasted, it would restart to add the clauses, and loose propagation information. | |||
2012-06-14 | add failing regression, move error up | Kshitij Bansal | |
2012-06-14 | bug fixes in justification heuristic | Kshitij Bansal | |
* remove assert iteSkolemMap gives ite-s (not true with repeatSimp) * handle a corner case in findSplitter triggered by repeatSimp | |||
2012-06-14 | enabling fixed bug345 case | Dejan Jovanović | |
2012-06-14 | fixes for the hasTerm issues in the shared database under the decision heuristic | Dejan Jovanović | |
2012-06-14 | Fixed arithmetic consistency issue. The simplex conflict variable had to be ↵ | Tim King | |
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. | |||
2012-06-14 | fix for clark's bug | Dejan Jovanović | |
imporant: theories SHOULD NOT use getSatValue at all, otherwise they might create a conflict with a literal they didn't get() | |||
2012-06-14 | don't run rewriterules regressions by default; fixes needed | Morgan Deters | |
2012-06-14 | fix quantifier non-bug | Kshitij Bansal | |
2012-06-14 | This commit: | Kshitij Bansal | |
* enables decision heuristic (justification) for QF_BV and QF_AUFBV * disables a failing regression in aufbv (because of equality engine assert failure trigerred by above change) * moves around the init procedure smt_engine * destruction time issues because of moving this -- still to be fixed, currently get around by not destucting stuff in driver | |||
2012-06-14 | failing quantifier | Kshitij Bansal | |
2012-06-14 | add passing regression | Kshitij Bansal | |
2012-06-14 | bug 346 resolved | Morgan Deters | |
2012-06-14 | * removing rewriteEquality from the rewriter | Dejan Jovanović | |
* theories now get either an assertion from the SAT solver (normalized) or an (dis-)equality between two shared terms that is non-normalized | |||
2012-06-13 | removing bug233 until morgan commits the actual file | Dejan Jovanović | |
2012-06-13 | adding some regressions to the usual regressions runs; several ↵ | Morgan Deters | |
recently-fixed incremental bugs are closed | |||
2012-06-13 | - Added a loop to internally assert constraints that are marked as true. | Tim King | |
- Changes how CongruenceManager reports conflicts. - ConstraintDatabase can now detect and raise conflicts when doing unate propagation. | |||
2012-06-13 | add passing regression | Kshitij Bansal | |
2012-06-13 | enabling regressions from last night, all fixed | Dejan Jovanović | |
2012-06-13 | enable some decision regressions | Kshitij Bansal | |
2012-06-13 | decision regressions, all but one fail | Kshitij Bansal | |
2012-06-13 | !(*child_it).isConst() assertion fail | Dejan Jovanović | |
this is delta minimal with the same assertion | |||
2012-06-13 | r2.node == response.node failure | Dejan Jovanović | |
2012-06-13 | r2.node == response.node failure | Dejan Jovanović | |
2012-06-13 | !current[0].isConst() failure | Dejan Jovanović | |
2012-06-13 | benchmark to show that we don't rewrite bvsmod correctly | Dejan Jovanović | |
the definition in smtlib was buggy and was changed on 2011-06-15 check http://goedel.cs.uiowa.edu/smtlib/logics/QF_BV.smt2 | |||
2012-06-12 | Fix to SMT-LIBv1 parser: QF_UF declares sort "U", but other *UF* logics do ↵ | Morgan Deters | |
not (e.g. QF_UFLIA). Also fix a syntax error in a regression test (CVC4 is too lenient to catch it though---CVC3 tripped over it). Also add additional parts for "make submission" in the top-level makefile | |||
2012-06-12 | missing problems | Dejan Jovanović | |
2012-06-12 | wrong answer for bv | Dejan Jovanović | |
2012-06-12 | Fix to yesterday's change in arithmetic. | Tim King | |
2012-06-12 | bv reduced with decision: sat instead of unsat | Kshitij Bansal | |
2012-06-12 | Assert fail equaility_engine.cpp: hasTerm(node) with --decision=justification | Kshitij Bansal | |
2012-06-12 | bufixes and the bugs | Dejan Jovanović | |
* array now only propagates thropugh the equality engine * assertions in the equality rewriting to ensure eq -> { eq, T, F } | |||
2012-06-12 | more breakage in aufbv | Dejan Jovanović | |
Assertion `value(l) == (lbool((uint8_t)0))' failed. and d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end() | |||
2012-06-12 | wrong answer benchmarks | Dejan Jovanović | |
these should be simple constant propagation problems | |||
2012-06-12 | wrong result benchmark | Dejan Jovanović | |
2012-06-12 | tests for the | Dejan Jovanović | |
!isEliminated(var(ps[i])) assert fails | |||
2012-06-12 | test cases for the | Dejan Jovanović | |
d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end() assertion fail | |||
2012-06-12 | Adding incorrect qf_lia result. | Tim King | |
2012-06-11 | Fix to term normalization of integer equalities. Adds a regression test that ↵ | Tim King | |
triggered it. | |||
2012-06-11 | another benchmark that used to fail | Dejan Jovanović | |
2012-06-11 | fixing bitvector bugs | Dejan Jovanović | |
* clauses shouldn't be erased when they could be a reason for outside propagation * propagation of p and !p is ignored as this must lead to a conflict in the subtheory internally | |||
2012-06-11 | distribute an .expect file. fixes a "make check" failure not for svn ↵ | Morgan Deters | |
working dirs but for distributed tarballs. | |||
2012-06-11 | Merge from quantifiers2-trunkmerge branch. | Morgan Deters | |
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure. Adds theory instantiators to many theories. Adds the UF strong solver. | |||
2012-06-11 | failing bv examples | Dejan Jovanović | |
2012-06-11 | some failing examples | Dejan Jovanović | |
2012-06-10 | adding an assertion to trigger the problem of bug349 and the testcase | Dejan Jovanović | |
bv rewriter apparently deosn't have a proper normal form for equalities | |||
2012-06-10 | fixes for bug347 | Dejan Jovanović | |
it was an issue with constants being merged, which influenced explanations of disequalities. when constants are attempted to be merged, equality engine now enters conflict mode immediately |