From 5ffddfd87d690b915d46685cf07e8399fba028b9 Mon Sep 17 00:00:00 2001
From: lianah <lianahady@gmail.com>
Date: Wed, 9 Oct 2013 18:48:07 -0400
Subject: [PATCH] fixed options::proof() segfault

---
 src/smt/smt_engine.cpp                        | 15 ++++------
 src/theory/bv/theory_bv_rewrite_rules.h       |  3 ++
 .../theory_bv_rewrite_rules_normalization.h   | 30 +++++++++++++++++++
 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
@@ -431,6 +431,36 @@ Node RewriteRule<MultSimplify>::apply(TNode node) {
   return utils::mkNode(kind::BITVECTOR_MULT, children); 
 }
 
+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 ||
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) {
-- 
2.30.2