From: Clark Barrett <barrett@cs.nyu.edu>
Date: Tue, 23 Oct 2012 20:05:38 +0000 (+0000)
Subject: More debugging info, small changes to model builder
X-Git-Tag: cvc5-1.0.0~7683
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2f8226e01f37035fe4edefb1e47d47b48638f832;p=cvc5.git

More debugging info, small changes to model builder
---

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 3a3f706ac..aa2de656e 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -33,7 +33,7 @@ TheoryModel::TheoryModel( context::Context* c, std::string name, bool enableFunc
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::APPLY_UF);
   d_equalityEngine.addFunctionKind(kind::SELECT);
-  //  d_equalityEngine.addFunctionKind(kind::STORE);
+  // d_equalityEngine.addFunctionKind(kind::STORE);
   d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR);
   d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR);
   d_equalityEngine.addFunctionKind(kind::APPLY_TESTER);
@@ -222,18 +222,25 @@ void TheoryModel::addTerm( Node n ){
 
 /** assert equality */
 void TheoryModel::assertEquality( Node a, Node b, bool polarity ){
+  if (a == b && polarity) {
+    return;
+  }
   d_equalityEngine.assertEquality( a.eqNode(b), polarity, Node::null() );
-  Trace("model-builder-assertions") << "  Asserting " << (polarity ? "equality: " : "disequality: ") << a << " = " << b << endl;
+  Trace("model-builder-assertions") << "(assert " << (polarity ? "(= " : "(not (= ") << a << " " << b << (polarity ? "));" : ")));") << endl;
   Assert(d_equalityEngine.consistent());
 }
 
 /** assert predicate */
 void TheoryModel::assertPredicate( Node a, bool polarity ){
+  if ((a == d_true && polarity) ||
+      (a == d_false && (!polarity))) {
+    return;
+  }
   if( a.getKind()==EQUAL ){
     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;
+    Trace("model-builder-assertions") << "(assert " << (polarity ? "" : "(not ") << a << (polarity ? ");" : "));") << endl;
     Assert(d_equalityEngine.consistent());
   }
 }
@@ -260,8 +267,8 @@ void TheoryModel::assertEqualityEngine( const eq::EqualityEngine* ee ){
         else if (predFalse) {
           assertPredicate(*eqc_i, false);
         }
-        else {
-          Trace("model-builder-assertions") << "  Merging predicates: " << *eqc_i << " and " << eqc << endl;
+        else if (eqc != (*eqc_i)) {
+          Trace("model-builder-assertions") << "(assert (iff " << *eqc_i << " " << eqc << "));" << endl;
           d_equalityEngine.mergePredicates(*eqc_i, eqc, Node::null());
           Assert(d_equalityEngine.consistent());
         }
@@ -473,6 +480,12 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
                 constantReps[*i2] = normalized;
                 Trace("model-builder") << "  Eval: Setting constant rep of " << (*i2) << " to " << normalized << endl;
                 changed = true;
+                // if (t.isBoolean()) {
+                //   tm->assertPredicate(*i2, normalized == tm->d_true);
+                // }
+                // else {
+                //   tm->assertEquality(*i2, normalized, true);
+                // }
                 noRepSet.erase(i2);
                 break;
               }
@@ -494,6 +507,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
               constantReps[*i2] = n;
               Trace("model-builder") << "  New Const: Setting constant rep of " << (*i2) << " to " << n << endl;
               changed = true;
+              // tm->assertEquality(*i2, n, true);
               noRepSet.erase(i2);
             }
             else {
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 2b99f9c26..f24b11c41 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -550,6 +550,7 @@ void TheoryEngine::collectModelInfo( theory::TheoryModel* m, bool fullModel ){
   // concerning the model.
   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) {
     if(d_logicInfo.isTheoryEnabled(theoryId)) {
+      Trace("model-builder") << "  CollectModelInfo on theory: " << theoryId << endl;
       d_theoryTable[theoryId]->collectModelInfo( m, fullModel );
     }
   }