Merging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into master. See the CAV14 submission for an explanation of the changes to the integer solver's behavior. If compiled against the our custom extension of glpk, https://github.com/timothy-king/glpk-cut-log, this should have substantial differences in behavior. This should have moderate performance differences for linear real and integer arithmetic even if these features are disabled.

1 files changed, 28 insertions, 91 deletions

diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index b4e009169..8e369ff9a 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -57,43 +57,19 @@ private:
   private:
     ArithCongruenceManager& d_acm;
   public:
-    ArithCongruenceNotify(ArithCongruenceManager& acm): d_acm(acm) {}
-
-    bool eqNotifyTriggerEquality(TNode equality, bool value) {
-      Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false") << ")" << std::endl;
-      if (value) {
-        return d_acm.propagate(equality);
-      } else {
-        return d_acm.propagate(equality.notNode());
-      }
-    }
-
-    bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
-      Unreachable();
-    }
-
-    bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
-      Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ", " << (value ? "true" : "false") << ")" << std::endl;
-      if (value) {
-        return d_acm.propagate(t1.eqNode(t2));
-      } else {
-        return d_acm.propagate(t1.eqNode(t2).notNode());
-      }
-    }
-
-    void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
-      Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl;
-      if (t1.getKind() == kind::CONST_BOOLEAN) {
-        d_acm.propagate(t1.iffNode(t2));
-      } else {
-        d_acm.propagate(t1.eqNode(t2));
-      }
-    }
-
-    void eqNotifyNewClass(TNode t) { }
-    void eqNotifyPreMerge(TNode t1, TNode t2) { }
-    void eqNotifyPostMerge(TNode t1, TNode t2) { }
-    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { }
+    ArithCongruenceNotify(ArithCongruenceManager& acm);
+
+    bool eqNotifyTriggerEquality(TNode equality, bool value);
+
+    bool eqNotifyTriggerPredicate(TNode predicate, bool value);
+
+    bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value);
+
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2);
+    void eqNotifyNewClass(TNode t);
+    void eqNotifyPreMerge(TNode t1, TNode t2);
+    void eqNotifyPostMerge(TNode t1, TNode t2);
+    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
   };
   ArithCongruenceNotify d_notify;
 
@@ -117,66 +93,27 @@ private:
 
   eq::EqualityEngine d_ee;
 
-  void raiseConflict(Node conflict){
-    Assert(!inConflict());
-    Debug("arith::conflict") << "difference manager conflict   " << conflict << std::endl;
-    d_inConflict.raise();
-    d_raiseConflict(conflict);
-  }
+  void raiseConflict(Node conflict);
 public:
 
-  bool inConflict() const{
-    return d_inConflict.isRaised();
-  };
+  bool inConflict() const;
 
-  bool hasMorePropagations() const {
-    return !d_propagatations.empty();
-  }
+  bool hasMorePropagations() const;
 
-  const Node getNextPropagation() {
-    Assert(hasMorePropagations());
-    Node prop = d_propagatations.front();
-    d_propagatations.dequeue();
-    return prop;
-  }
+  const Node getNextPropagation();
 
-  bool canExplain(TNode n) const {
-    return d_explanationMap.find(n) != d_explanationMap.end();
-  }
+  bool canExplain(TNode n) const;
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);
 
 private:
-  Node externalToInternal(TNode n) const{
-    Assert(canExplain(n));
-    ExplainMap::const_iterator iter = d_explanationMap.find(n);
-    size_t pos = (*iter).second;
-    return d_propagatations[pos];
-  }
-
-  void pushBack(TNode n){
-    d_explanationMap.insert(n, d_propagatations.size());
-    d_propagatations.enqueue(n);
-
-    ++(d_statistics.d_propagations);
-  }
-
-  void pushBack(TNode n, TNode r){
-    d_explanationMap.insert(r, d_propagatations.size());
-    d_explanationMap.insert(n, d_propagatations.size());
-    d_propagatations.enqueue(n);
+  Node externalToInternal(TNode n) const;
 
-    ++(d_statistics.d_propagations);
-  }
+  void pushBack(TNode n);
 
-  void pushBack(TNode n, TNode r, TNode w){
-    d_explanationMap.insert(w, d_propagatations.size());
-    d_explanationMap.insert(r, d_propagatations.size());
-    d_explanationMap.insert(n, d_propagatations.size());
-    d_propagatations.enqueue(n);
+  void pushBack(TNode n, TNode r);
 
-    ++(d_statistics.d_propagations);
-  }
+  void pushBack(TNode n, TNode r, TNode w);
 
   bool propagate(TNode x);
   void explain(TNode literal, std::vector<TNode>& assumptions);
@@ -207,21 +144,21 @@ public:
   }
 
   /** Assert an equality. */
-  void watchedVariableIsZero(Constraint eq);
+  void watchedVariableIsZero(ConstraintCP eq);
 
   /** Assert a conjunction from lb and ub. */
-  void watchedVariableIsZero(Constraint lb, Constraint ub);
+  void watchedVariableIsZero(ConstraintCP lb, ConstraintCP ub);
 
   /** Assert that the value cannot be zero. */
-  void watchedVariableCannotBeZero(Constraint c);
+  void watchedVariableCannotBeZero(ConstraintCP c);
 
   /** Assert that the value cannot be zero. */
-  void watchedVariableCannotBeZero(Constraint c, Constraint d);
+  void watchedVariableCannotBeZero(ConstraintCP c, ConstraintCP d);
 
 
   /** Assert that the value is congruent to a constant. */
-  void equalsConstant(Constraint eq);
-  void equalsConstant(Constraint lb, Constraint ub);
+  void equalsConstant(ConstraintCP eq);
+  void equalsConstant(ConstraintCP lb, ConstraintCP ub);
 
 
   void addSharedTerm(Node x);