- Added a loop to internally assert constraints that are marked as true.

- Changes how CongruenceManager reports conflicts.
- ConstraintDatabase can now detect and raise conflicts when doing unate propagation.

1 files changed, 5 insertions, 4 deletions

diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 649e34134..14d2370ab 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -7,8 +7,9 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDatabase& cd, TNodeCallBack& setup, const ArithVarNodeMap& av2Node)
-  : d_conflict(c),
+ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDatabase& cd, TNodeCallBack& setup, const ArithVarNodeMap& av2Node, NodeCallBack& raiseConflict)
+  : d_inConflict(c),
+    d_raiseConflict(raiseConflict),
     d_notify(*this),
     d_keepAlive(c),
     d_propagatations(c),
@@ -112,7 +113,7 @@ bool ArithCongruenceManager::propagate(TNode x){
       ++(d_statistics.d_conflicts);
 
       Node conf = flattenAnd(explainInternal(x));
-      d_conflict.set(conf);
+      raiseConflict(conf);
       Debug("arith::congruenceManager") << "rewritten to false "<<x<<" with explanation "<< conf << std::endl;
       return false;
     }
@@ -141,7 +142,7 @@ bool ArithCongruenceManager::propagate(TNode x){
     Node final = flattenAnd(conf);
 
     ++(d_statistics.d_conflicts);
-    d_conflict.set(final);
+    raiseConflict(final);
     Debug("arith::congruenceManager") << "congruenceManager found a conflict " << final << std::endl;
     return false;
   }