From 684215b52755182678889f0df5c69e821da3e0c6 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Wed, 6 Jul 2011 23:42:04 +0000 Subject: [PATCH] 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 --- src/prop/minisat/core/Solver.cc | 13 +++++++++---- src/theory/arith/theory_arith.cpp | 9 ++++++--- 2 files changed, 15 insertions(+), 7 deletions(-) diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index c2d53bef8..1ec9b0962 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -565,14 +565,19 @@ int Solver::litRedundant(Lit p, uint32_t abstract_levels) int top = analyze_toclear.size(); int max_level = 0; while (analyze_stack.size() > 0){ - assert(reason(var(analyze_stack.last())) != CRef_Undef); - Clause& c = ca[reason(var(analyze_stack.last()))]; analyze_stack.pop(); + CRef c_reason = reason(var(analyze_stack.last())); + assert(c_reason != CRef_Undef); + Clause& c = ca[c_reason]; + int c_size = c.size(); + analyze_stack.pop(); if (c.level() > max_level) { max_level = c.level(); } - for (int i = 1; i < c.size(); i++){ - Lit p = c[i]; + // Since calling reason might relocate to resize, c is not necesserily the right reference, we must + // use the allocator each time + for (int i = 1; i < c_size; i++){ + Lit p = ca[c_reason][i]; if (!seen[var(p)] && level(var(p)) > 0){ if (reason(var(p)) != CRef_Undef && (abstractLevel(var(p)) & abstract_levels) != 0){ seen[var(p)] = 1; 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; + } } } -- 2.30.2