From: Clark Barrett <barrett@cs.nyu.edu>
Date: Fri, 12 Oct 2012 21:36:06 +0000 (+0000)
Subject: Added assertions and tracing code for collectModelInfo phase
X-Git-Tag: cvc5-1.0.0~7702
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=64d707c3a97a8bbc46d4f3cd07e3a4d3908130b1;p=cvc5.git

Added assertions and tracing code for collectModelInfo phase
---

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 07652918d..dad1b5fe6 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -223,6 +223,8 @@ void TheoryModel::addTerm( Node n ){
 /** assert equality */
 void TheoryModel::assertEquality( Node a, Node b, bool polarity ){
   d_equalityEngine.assertEquality( a.eqNode(b), polarity, Node::null() );
+  Trace("model-builder-assertions") << "  Asserting " << (polarity ? "equality: " : "disequality: ") << a << " = " << b << endl;
+  Assert(d_equalityEngine.consistent());
 }
 
 /** assert predicate */
@@ -231,6 +233,8 @@ void TheoryModel::assertPredicate( Node a, bool polarity ){
     d_equalityEngine.assertEquality( a, polarity, Node::null() );
   }else{
     d_equalityEngine.assertPredicate( a, polarity, Node::null() );
+    Trace("model-builder-assertions") << "  Asserting predicate " << (polarity ? "true" : "false") << ": " << a << endl;
+    Assert(d_equalityEngine.consistent());
   }
 }
 
@@ -257,7 +261,9 @@ void TheoryModel::assertEqualityEngine( const eq::EqualityEngine* ee ){
           assertPredicate(*eqc_i, false);
         }
         else {
+          Trace("model-builder-assertions") << "  Merging predicates: " << *eqc_i << " and " << eqc << endl;
           d_equalityEngine.mergePredicates(*eqc_i, eqc, Node::null());
+          Assert(d_equalityEngine.consistent());
         }
       } else {
         assertEquality(*eqc_i, eqc, true);