Age | Commit message (Collapse) | Author | |
---|---|---|---|
2012-06-06 | Fixed problem causing crash at destruction time | Clark Barrett | |
2012-06-05 | More clean-up | Clark Barrett | |
2012-06-05 | Fixed a performance issue with unconstrained simplifier | Clark Barrett | |
2012-06-05 | Adding missing files... | Clark Barrett | |
2012-06-04 | Added preprocessing pass that propagates unconstrained values - solves all of | Clark Barrett | |
the unconstrained examples in QF_AUFBV/brummayerbiere3 - should also help generally on at least BV and maybe others. Off by default for now - results are mixed and it's hard to evaluate with so many existing assertion failures and segfaults - will re-evaluate once those are fixed | |||
2012-05-31 | Fixed bug in bv: one more case where non-shared equality was getting propagated | Clark Barrett | |
Added a global push and pop around solving - fixes an assertion failure when TNodes are still around in a CDHashMap at destruction time. | |||
2012-05-30 | Added BitwiseEq bitvector rewrite | Clark Barrett | |
Added option "--repeat-simp" which repeats nonclausal simplification: 4 times, twice before ite removal and twice after Enabled these options (plus ite-simp) on QF_AUFBV, obtaining significant speedup on dwp examples | |||
2012-05-30 | Fixed problem with array queue growing too large | Clark Barrett | |
2012-05-30 | remove unused/broken check build target | Morgan Deters | |
2012-05-29 | removing now-unused TheoryEngine::setLogic() interface function | Morgan Deters | |
2012-05-29 | Enabled SolveEq bv rewrite | Clark Barrett | |
2012-05-28 | Added some BV rewrites, fixed bugs in array theory, made ite simp work with BV | Clark Barrett | |
2012-05-27 | some reordering to keep invariants | Dejan Jovanović | |
2012-05-27 | Committing the work on equality engine, I need to see how it does on the ↵ | Dejan Jovanović | |
regressions. New additions: * areDisequal(x, y) -> areDisequal(x, y, needProof): when asking for a disequality you must say needProof if you will ask for an explanation later. * propagation of shared dis-equalities (not yet complete, once case missing) * changes to the theories that use it, authors should check up on the changes | |||
2012-05-27 | Another expensive function call in a Debug line | Clark Barrett | |
2012-05-25 | init bug fix | Kshitij Bansal | |
2012-05-25 | Checking in fix for bug 340 - somehow didn't get checked in earlier | Clark Barrett | |
2012-05-24 | Separating the subtheory implementations in the bitvector theory. | Dejan Jovanović | |
2012-05-24 | Significant changes to the internals of the equality engine. Equality is not ↵ | Dejan Jovanović | |
handled natively and not as a generic predicate. The changes also change the order of propagation, and can produce different conflicts. Since the engine is now used everywhere this means that so some crazy results are to be expected. | |||
2012-05-22 | This commit merges in the branch arithmetic/cprop. | Tim King | |
2012-05-21 | Updating equality manager to handle tagged trigger terms. Notifications are ↵ | Dejan Jovanović | |
pushed out for relationships between terms tagged with the same tag. No performance impact. | |||
2012-05-19 | - The array type rules were fixed to use isSubtypeOf. | Tim King | |
- The type of (kind::DIVISION x y) is RealType. - A reference to util/pseudoboolean.i was removed. - rec5.cvc is disabled for now. The type of 2 is Integer which is not a subtype of [0..11]. | |||
2012-05-18 | This commit adds TypeNode::leastCommonTypeNode(). The special case for ↵ | Tim King | |
arithmetic in TypeNode::operator==() has been removed. A number of faulty type checking checks were switched to use isSubtypeOf. The resolves bug #339 | |||
2012-05-18 | This commit removes the dead psuedoboolean code. | Tim King | |
2012-05-17 | This fixes a fascinating segfault. This is the sequence of events: | Tim King | |
1) A restart occurs 2) A shared term is registered to arithmetic. 3) Arithmetic sets this up. 4) No new linear relations are added to arithmetic. 5) Eventually a restart occurs. 6) Arithmetic resets the tableau as it has not had a row added since the last restart. 7) A new variable is added. 8) This exceeds the size of the column vector of the saved tableau by exactly one. 9) segfault | |||
2012-05-17 | Fixing an issue with LogicInfo::isPure() that turned off simplification in ↵ | Morgan Deters | |
QF_UF and maybe others | |||
2012-05-17 | Fixed bug 338: | Liana Hadarean | |
- fixed buggy rewrite rules assuming certain nodes only had 2 children - added support for bv-rewrite dump - fixed smt2_printer for bv constants | |||
2012-05-16 | adding simple-minded handling of (dis-)equalities where constants are involved | Dejan Jovanović | |
2012-05-16 | Changes to SAT solver: | Dejan Jovanović | |
* allowing propagation of false literals (handles conflict) * allowing lemmas during BCP (bug 337) * UF does direct propagation, without checking for literal value anymore | |||
2012-05-16 | equality status for bitvectors can now look into the sat solver to check for ↵ | Dejan Jovanović | |
IN_MODEL status | |||
2012-05-16 | refactored TheoryBV bitblaster and equality engine into subtheories (similar ↵ | Liana Hadarean | |
to TheoryEngine | |||
2012-05-15 | fixed QF_BV performance problem due to using CDList instead of CDQueue | Liana Hadarean | |
2012-05-15 | Fix to shared terms visitor. | Tim King | |
2012-05-15 | Fixed several bugs in shared terms database | Clark Barrett | |
2012-05-15 | This commit removes the CONST_INTEGER kind from nodes. This code comes from ↵ | Tim King | |
the branch arithmetic/remove_const_int. | |||
2012-05-15 | renamed bv_sat.h, bv_sat.cpp to bitblaster.h, bitblaster.cpp respectively | Liana Hadarean | |
2012-05-15 | fixing warnings, grr | Dejan Jovanović | |
2012-05-15 | several bug fixes: in TheoryBV::NotifyClass missing NOT in predicate notify ↵ | Liana Hadarean | |
and now term notify handles boolean constants; fixed bug 328 | |||
2012-05-14 | fixes for shared term registration. previously the type was not considered ↵ | Dejan Jovanović | |
when looking at theories of the term and for a term like read(a, f(x)) the term f(x) would not be registered to arithmetic in AUFLIA. this fixies the issue of bug 330 and moves it to some other assertion fail. | |||
2012-05-14 | Fixed assertion failures in array theory | Clark Barrett | |
This fixes bugs 335 and 333. | |||
2012-05-14 | fixing up preregistration again | Dejan Jovanović | |
2012-05-13 | fixing build warnings | Dejan Jovanović | |
2012-05-11 | Added some ITE rewrites, | Clark Barrett | |
Added ITE simplifier - on by default only for QF_LIA benchmarks Fixed one bug in arrays Added negate() to node.h - it returns kind == NOT ? kind[0] : kind.notNode() | |||
2012-05-11 | Partially fixes something-like-a-problem with TheoryArith::getDeltaValue(). | Tim King | |
2012-05-10 | Removing now unneeded (as of r3425) typenames from EqualityEngine. trunk now ↵ | Tim King | |
compiles on Debian. | |||
2012-05-09 | * simplifying equality engine interface | Dejan Jovanović | |
* notifications are now through the interface subclass instead of a template * notifications include constants being merged * changed contextNotifyObj::notify to contextNotifyObj::contextNotifyPop so it's more descriptive and doesn't clutter methods when subclassed * sat solver now has explicit methods to make true and false constants * 0-level literals are removed from explanations of propagations | |||
2012-05-09 | Merge from decision branch (ITE support) | Kshitij Bansal | |
Major changes from last merge * ITEs supported * Don't share theory lemmas to DE, only assertions Should probably be noted that 'make regress' doesn't quite pass with --decision=justification. Throws off search in couple of arith benchmarks. No serious performance changes expected. Keep an eye. | |||
2012-05-08 | Merging in bvprop branch, with proper bit-vector propagation. | Liana Hadarean | |
This should also fix bug 325. | |||
2012-05-07 | Fixing a bug with TheoryArith::ppAssert() and shared terms. | Tim King | |
2012-05-07 | Fixes a sign bug in the DioSolver. | Tim King | |