From 232782d690e1dc333ebc7bec1a9302f086c947b6 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Sun, 14 Jun 2015 15:03:15 +0200
Subject: [PATCH] Fixes for shared term normalization in replay for constraint
 construction.

---
 src/theory/arith/constraint.cpp           |  6 ++--
 src/theory/arith/constraint.h             | 10 +++++++
 src/theory/arith/theory_arith_private.cpp | 36 ++++++++++++++++++++---
 3 files changed, 45 insertions(+), 7 deletions(-)

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 94632e50e..822f0e578 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -34,7 +34,7 @@ namespace arith {
 
 /** Given a simplifiedKind this returns the corresponding ConstraintType. */
 //ConstraintType constraintTypeOfLiteral(Kind k);
-ConstraintType constraintTypeOfComparison(const Comparison& cmp){
+ConstraintType Constraint::constraintTypeOfComparison(const Comparison& cmp){
   Kind k = cmp.comparisonKind();
   switch(k){
   case LT:
@@ -989,7 +989,7 @@ ConstraintP ConstraintDatabase::addLiteral(TNode literal){
   Assert(!hasLiteral(negationNode));
   Comparison posCmp = Comparison::parseNormalForm(atomNode);
 
-  ConstraintType posType = constraintTypeOfComparison(posCmp);
+  ConstraintType posType = Constraint::constraintTypeOfComparison(posCmp);
 
   Polynomial nvp = posCmp.normalizedVariablePart();
   ArithVar v = d_avariables.asArithVar(nvp.getNode());
@@ -1024,7 +1024,7 @@ ConstraintP ConstraintDatabase::addLiteral(TNode literal){
   }else{
     Comparison negCmp = Comparison::parseNormalForm(negationNode);
     
-    ConstraintType negType = constraintTypeOfComparison(negCmp);
+    ConstraintType negType = Constraint::constraintTypeOfComparison(negCmp);
     DeltaRational negDR = negCmp.normalizedDeltaRational();
 
     ConstraintP negC = new Constraint(v, negType, negDR);
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 795798450..0e0b35020 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -93,6 +93,13 @@
 #include <set>
 #include <ext/hash_map>
 
+namespace CVC4 {
+namespace theory {
+namespace arith {
+class Comparison;
+}
+}
+}
 namespace CVC4 {
 namespace theory {
 namespace arith {
@@ -448,6 +455,7 @@ private:
   void initialize(ConstraintDatabase* db, SortedConstraintMapIterator v, ConstraintP negation);
 
 
+
   class ConstraintRuleCleanup {
   public:
     inline void operator()(ConstraintRule* crp){
@@ -517,6 +525,8 @@ private:
 
 public:
 
+  static ConstraintType constraintTypeOfComparison(const Comparison& cmp);
+
   inline ConstraintType getType() const {
     return d_type;
   }
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 616656408..a4825c1c4 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -2258,10 +2258,32 @@ std::pair<ConstraintP, ArithVar> TheoryArithPrivate::replayGetConstraint(const D
   Node sum = toSumNode(d_partialModel, lhs);
   if(sum.isNull()){ return make_pair(NullConstraint, added); }
 
-  Node norm = Rewriter::rewrite(sum);
-  DeltaRational dr(rhs);
+  Debug("approx::constraint") << "replayGetConstraint " << sum
+                              << " " << k
+                              << " " << rhs
+                              << endl;
 
-  ConstraintType t = (k == kind::LEQ) ? UpperBound : LowerBound;
+  Assert( k == kind::LEQ || k == kind::GEQ );
+
+  Node comparison = NodeManager::currentNM()->mkNode(k, sum, mkRationalNode(rhs));
+  Node rewritten = Rewriter::rewrite(comparison);
+  if(!(Comparison::isNormalAtom(rewritten))){
+    return make_pair(NullConstraint, added);
+  }
+
+  Comparison cmp = Comparison::parseNormalForm(rewritten);
+  if(cmp.isBoolean()){ return make_pair(NullConstraint, added); }
+
+  Polynomial nvp =  cmp.normalizedVariablePart();
+  if(nvp.isZero()){ return make_pair(NullConstraint, added); }
+
+  Node norm = nvp.getNode();
+
+  ConstraintType t = Constraint::constraintTypeOfComparison(cmp);
+  DeltaRational dr = cmp.normalizedDeltaRational();
+
+  Debug("approx::constraint") << "rewriting " << rewritten << endl
+                              << " |-> " << norm << " " << t << " " << dr << endl;
 
   Assert(!branch || d_partialModel.hasArithVar(norm));
   ArithVar v = ARITHVAR_SENTINEL;
@@ -2299,6 +2321,8 @@ std::pair<ConstraintP, ArithVar> TheoryArithPrivate::replayGetConstraint(const D
       return make_pair(imp, added);
     }
   }
+  
+
   ConstraintP newc = d_constraintDatabase.getConstraint(v, t, dr);
   d_replayConstraints.push_back(newc);
   return make_pair(newc, added);
@@ -2342,6 +2366,7 @@ std::pair<ConstraintP, ArithVar> TheoryArithPrivate::replayGetConstraint(const C
 // }
 
 Node toSumNode(const ArithVariables& vars, const DenseMap<Rational>& sum){
+  Debug("arith::toSumNode") << "toSumNode() begin" << endl;
   NodeBuilder<> nb(kind::PLUS);
   NodeManager* nm = NodeManager::currentNM();
   DenseMap<Rational>::const_iterator iter, end;
@@ -2351,8 +2376,11 @@ Node toSumNode(const ArithVariables& vars, const DenseMap<Rational>& sum){
     if(!vars.hasNode(x)){ return Node::null(); }
     Node xNode = vars.asNode(x);
     const Rational& q = sum[x];
-    nb << nm->mkNode(kind::MULT, mkRationalNode(q), xNode);
+    Node mult = nm->mkNode(kind::MULT, mkRationalNode(q), xNode);
+    Debug("arith::toSumNode") << "toSumNode() " << x << " " << mult << endl;
+    nb << mult;
   }
+  Debug("arith::toSumNode") << "toSumNode() end" << endl;
   return safeConstructNary(nb);
 }
 
-- 
2.30.2