diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-07-06 23:42:04 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-07-06 23:42:04 +0000 |
commit | 684215b52755182678889f0df5c69e821da3e0c6 (patch) | |
tree | 24cccc678402f43b4956ee33f7d654236ac4bc4d /src/theory/arith | |
parent | 35a64b0ef46c8298b28358555c3b1175dc5fce5b (diff) |
Fixing two bugs:
1) arithmetic should check for subterms when solving equations, for instance x = if b then x + 1 else x -1 is not a valid substitution
2) a memory problem in minisat - explanations are constructed during conflict analysis, so the clause database might resize and relocate, which invalidates any references to clauses
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 34cb4d666..93c02942d 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -184,9 +184,12 @@ Theory::SolveStatus TheoryArith::solve(TNode in, SubstitutionMap& outSubstitutio } // x = (p - ax - c) * -1/a eliminateVar = NodeManager::currentNM()->mkNode(kind::MULT, eliminateVar, mkRationalNode(- minConstant.inverse())); - // Add the substitution - outSubstitutions.addSubstitution(minVar, Rewriter::rewrite(eliminateVar)); - return SOLVE_STATUS_SOLVED; + // Add the substitution if not recursive + Node rewritten = Rewriter::rewrite(eliminateVar); + if (!rewritten.hasSubterm(minVar)) { + outSubstitutions.addSubstitution(minVar, Rewriter::rewrite(eliminateVar)); + return SOLVE_STATUS_SOLVED; + } } } |