Age | Commit message (Collapse) | Author | |
---|---|---|---|
2012-06-28 | Fixed bug in bv rewriter that caused wrong answer in SMT-COMPsmtcomp2012-resubmission-2 | Clark Barrett | |
2012-06-22 | TPTP: add parser for cnf and fof | François Bobot | |
- include directive works - no keyword : 'fof', 'cnf', ... can be used for symbols name - real -> unsorted -> real (for the one that appear, so no bijection bitween real and unsorted) - same thing for string But: - string not distinct by projection to real, not sure if the current state of string theory make them distinct - filtering in include is not done - the result is not printed in the TPTP way (currently SMT2 way) | |||
2012-06-17 | enabling theoryof=term for quantifiers with sharing | Dejan Jovanović | |
disableing one test case in equantifiers/decision that runs long | |||
2012-06-17 | fixing wrong assertion | Dejan Jovanović | |
2012-06-17 | fixing makefile error that brakes build | Dejan Jovanović | |
2012-06-17 | Fix array bug causing incorrect answers | Clark Barrett | |
2012-06-16 | Adding the failing QF_AUFLIA regression mentioned in last commit. | Kshitij Bansal | |
pp-regfile.delta02.smt is the one to look at with --decision=justificaiton, the delta minimized version of pp-regfile, which also gives wrong answer. due to various commits/fixes, delta01 gives correct answer currently. | |||
2012-06-16 | changing theoryOf in shared mode with arrays to move equalities to arrays | Dejan Jovanović | |
disabled in bitvectors due to non-stably infinite problems the option to enable it is --theoryof-mode=term | |||
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 | * 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ć | |