summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Collapse)Author
2012-06-15Fixes some assertion failuresClark Barrett
2012-06-15one bug fixedKshitij Bansal
2012-06-14fixing 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-14add failing regression, move error upKshitij Bansal
2012-06-14bug fixes in justification heuristicKshitij Bansal
* remove assert iteSkolemMap gives ite-s (not true with repeatSimp) * handle a corner case in findSplitter triggered by repeatSimp
2012-06-14enabling fixed bug345 caseDejan Jovanović
2012-06-14fixes for the hasTerm issues in the shared database under the decision heuristicDejan Jovanović
2012-06-14Fixed 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-14fix for clark's bugDejan Jovanović
imporant: theories SHOULD NOT use getSatValue at all, otherwise they might create a conflict with a literal they didn't get()
2012-06-14don't run rewriterules regressions by default; fixes neededMorgan Deters
2012-06-14fix quantifier non-bugKshitij Bansal
2012-06-14This 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-14failing quantifierKshitij Bansal
2012-06-14add passing regressionKshitij Bansal
2012-06-14bug 346 resolvedMorgan Deters
2012-06-14* removing rewriteEquality from the rewriterDejan 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-13removing bug233 until morgan commits the actual fileDejan Jovanović
2012-06-13adding 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-13add passing regressionKshitij Bansal
2012-06-13enabling regressions from last night, all fixedDejan Jovanović
2012-06-13enable some decision regressionsKshitij Bansal
2012-06-13decision regressions, all but one failKshitij Bansal
2012-06-13!(*child_it).isConst() assertion failDejan Jovanović
this is delta minimal with the same assertion
2012-06-13r2.node == response.node failure Dejan Jovanović
2012-06-13r2.node == response.node failureDejan Jovanović
2012-06-13!current[0].isConst() failureDejan Jovanović
2012-06-13benchmark to show that we don't rewrite bvsmod correctlyDejan 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-12Fix 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-12missing problemsDejan Jovanović
2012-06-12wrong answer for bvDejan Jovanović
2012-06-12Fix to yesterday's change in arithmetic.Tim King
2012-06-12bv reduced with decision: sat instead of unsatKshitij Bansal
2012-06-12Assert fail equaility_engine.cpp: hasTerm(node) with --decision=justificationKshitij Bansal
2012-06-12bufixes and the bugsDejan Jovanović
* array now only propagates thropugh the equality engine * assertions in the equality rewriting to ensure eq -> { eq, T, F }
2012-06-12more breakage in aufbvDejan Jovanović
Assertion `value(l) == (lbool((uint8_t)0))' failed. and d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end()
2012-06-12wrong answer benchmarksDejan Jovanović
these should be simple constant propagation problems
2012-06-12wrong result benchmarkDejan Jovanović
2012-06-12tests for the Dejan Jovanović
!isEliminated(var(ps[i])) assert fails
2012-06-12test cases for the Dejan Jovanović
d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end() assertion fail
2012-06-12Adding incorrect qf_lia result.Tim King
2012-06-11Fix to term normalization of integer equalities. Adds a regression test that ↵Tim King
triggered it.
2012-06-11another benchmark that used to fail Dejan Jovanović
2012-06-11fixing bitvector bugsDejan 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-11distribute an .expect file. fixes a "make check" failure not for svn ↵Morgan Deters
working dirs but for distributed tarballs.
2012-06-11Merge 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-11failing bv examplesDejan Jovanović
2012-06-11some failing examplesDejan Jovanović
2012-06-10adding an assertion to trigger the problem of bug349 and the testcaseDejan Jovanović
bv rewriter apparently deosn't have a proper normal form for equalities
2012-06-10fixes for bug347Dejan 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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback