From: Clark Barrett <barrett@cs.nyu.edu>
Date: Tue, 9 Oct 2012 19:22:17 +0000 (+0000)
Subject: More fixes to model code
X-Git-Tag: cvc5-1.0.0~7717
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0db88552a98ce250db69746415b39bd7f7e9ea4f;p=cvc5.git

More fixes to model code
---

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index f218332ac..3d918277f 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -328,7 +328,7 @@ void TheoryModel::assertEqualityEngine( const eq::EqualityEngine* ee ){
           assertPredicate(*eqc_i, false);
         }
         else {
-          d_equalityEngine.addTerm(*eqc_i);
+          d_equalityEngine.mergePredicates(*eqc_i, eqc, Node::null());
         }
       } else {
         assertEquality(*eqc_i, eqc, true);
@@ -663,6 +663,7 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node
     retNode = NodeManager::currentNM()->mkNode( r.getKind(), children );
     if (childrenConst) {
       retNode = Rewriter::rewrite(retNode);
+      Assert(retNode.getKind() == kind::APPLY_UF || retNode.isConst());
     }
   }
   d_normalizedCache[r] = retNode;
diff --git a/src/theory/model.h b/src/theory/model.h
index a10d0a9ac..3c6d8e116 100644
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -207,10 +207,10 @@ private:
     }
     Node n = **te;
     while (s->find(n) != s->end()) {
+      ++(*te);
       if (te->isFinished()) {
         return Node();
       }
-      ++(*te);
       n = **te;
     }
     s->insert(n);
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 97dcbad86..5cf4a5f9f 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -355,8 +355,6 @@ void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason) {
 
 void EqualityEngine::mergePredicates(TNode p, TNode q, TNode reason) {
   Debug("equality") << d_name << "::eq::mergePredicats(" << p << "," << q << ")" << std::endl;
-  Assert(p.getKind() != kind::EQUAL, "Use assertEquality instead");
-  Assert(q.getKind() != kind::EQUAL, "Use assertEquality instead");
   assertEqualityInternal(p, q, reason);
   propagate();
 }