diff options
author | lianah <lianahady@gmail.com> | 2013-10-09 18:48:07 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-10-09 18:48:07 -0400 |
commit | 5ffddfd87d690b915d46685cf07e8399fba028b9 (patch) | |
tree | 9c270a639274b2ab53712db7dfe72b34393331b6 | |
parent | 44485520fae92b34e4385d4d2c4774c9dd7d0dc0 (diff) |
fixed options::proof() segfault
-rw-r--r-- | src/smt/smt_engine.cpp | 15 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules.h | 3 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_normalization.h | 30 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 6 |
4 files changed, 44 insertions, 10 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 352db6789..2505294e4 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3105,14 +3105,13 @@ void SmtEngine::ensureBoolean(const Expr& e) throw(TypeCheckingException) { Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalException, LogicException) { Assert(ex.isNull() || ex.getExprManager() == d_exprManager); -#ifdef CVC4_PROOF - // if (options::proof()) { <-- SEGFAULT!! - ProofManager::currentPM()->addAssertion(ex); - //} -#endif SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); + + + PROOF( ProofManager::currentPM()->addAssertion(ex); ); + Trace("smt") << "SmtEngine::checkSat(" << ex << ")" << endl; if(d_queryMade && !options::incrementalSolving()) { @@ -3253,14 +3252,10 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, LogicException) { Assert(ex.getExprManager() == d_exprManager); -#ifdef CVC4_PROOF - // if (options::proof()) { <-- SEGFAULT!!! - ProofManager::currentPM()->addAssertion(ex); - // } -#endif SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); + PROOF( ProofManager::currentPM()->addAssertion(ex);); Trace("smt") << "SmtEngine::assertFormula(" << ex << ")" << endl; // Substitute out any abstract values in ex diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index 8426afb59..db48a1d05 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -152,6 +152,7 @@ enum RewriteRuleId { PlusCombineLikeTerms, MultSimplify, MultDistribConst, + MultDistribVariable, SolveEq, BitwiseEq, AndSimplify, @@ -265,6 +266,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case PlusCombineLikeTerms: out << "PlusCombineLikeTerms"; return out; case MultSimplify: out << "MultSimplify"; return out; case MultDistribConst: out << "MultDistribConst"; return out; + case MultDistribVariable: out << "MultDistribConst"; return out; case SolveEq : out << "SolveEq"; return out; case BitwiseEq : out << "BitwiseEq"; return out; case NegMult : out << "NegMult"; return out; @@ -498,6 +500,7 @@ struct AllRewriteRules { RewriteRule<SltZero> rule115; RewriteRule<BVToNatEliminate> rule116; RewriteRule<IntToBVEliminate> rule117; + RewriteRule<MultDistribVariable> rule118; }; template<> inline diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 2da4dfa6a..bb5c94b1e 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -432,6 +432,36 @@ Node RewriteRule<MultSimplify>::apply(TNode node) { } template<> inline +bool RewriteRule<MultDistribVariable>::applies(TNode node) { + if (node.getKind() != kind::BITVECTOR_MULT || + node.getNumChildren() != 2) { + return false; + } + Assert(!node[0].isConst()); + if (!node[1].getNumChildren() == 0) { + return false; + } + TNode factor = node[0]; + return (factor.getKind() == kind::BITVECTOR_PLUS || + factor.getKind() == kind::BITVECTOR_SUB); +} + +template<> inline +Node RewriteRule<MultDistribVariable>::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule<MultDistrib>(" << node << ")" << std::endl; + TNode var = node[1]; + TNode factor = node[0]; + + std::vector<Node> children; + for(unsigned i = 0; i < factor.getNumChildren(); ++i) { + children.push_back(utils::mkNode(kind::BITVECTOR_MULT, factor[i], var)); + } + + return utils::mkNode(factor.getKind(), children); +} + + +template<> inline bool RewriteRule<MultDistribConst>::applies(TNode node) { if (node.getKind() != kind::BITVECTOR_MULT || node.getNumChildren() != 2) { diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 2467ae3f1..76eb97b39 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -332,6 +332,12 @@ RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool prerewrite) { // creating new terms that might simplify further return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } + if(RewriteRule<MultDistribVariable>::applies(resultNode)) { + resultNode = RewriteRule<MultDistribVariable>::run<false>(resultNode); + // creating new terms that might simplify further + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } + } if(resultNode == node) { |