Fix bugs 605 and 667.

8 files changed, 38 insertions, 12 deletions

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 4eb5dd680..dad21e90a 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -448,6 +448,9 @@ TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& bounds)
 TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) {
   Assert(t.isTuple() || t.isRecord());
 
+  //AJR: not sure why .getBaseType() was used in two cases below, 
+  //     disabling this, which is necessary to fix bug 605/667, 
+  //     which involves records of INT which were mapped to records of REAL below.
   TypeNode tOrig = t;
   if(t.isTuple()) {
     vector<TypeNode> v;
@@ -458,7 +461,7 @@ TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) {
       if(tn.isTuple() || tn.isRecord()) {
         base = getDatatypeForTupleRecord(tn);
       } else {
-        base = tn.getBaseType();
+        base = tn;//.getBaseType();
       }
       changed = changed || (tn != base);
       v.push_back(base);
@@ -476,7 +479,7 @@ TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) {
       if(tn.isTuple() || tn.isRecord()) {
         base = getDatatypeForTupleRecord(TypeNode::fromType(tn)).toType();
       } else {
-        base = tn.getBaseType();
+        base = tn;//.getBaseType();
       }
       changed = changed || (tn != base);
       v.push_back(std::make_pair((*i).first, base));
@@ -498,7 +501,7 @@ TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) {
       dt.addConstructor(c);
       dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt));
       Debug("tuprec") << "REWROTE " << t << " to " << dtt << std::endl;
-      dtt.setAttribute(DatatypeTupleAttr(), t);
+      dtt.setAttribute(DatatypeTupleAttr(), tOrig);
     } else {
       const Record& rec = t.getRecord();
       Datatype dt("__cvc4_record");
@@ -509,7 +512,7 @@ TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) {
       dt.addConstructor(c);
       dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt));
       Debug("tuprec") << "REWROTE " << t << " to " << dtt << std::endl;
-      dtt.setAttribute(DatatypeRecordAttr(), t);
+      dtt.setAttribute(DatatypeRecordAttr(), tOrig);
     }
   } else {
     Debug("tuprec") << "REUSING cached " << t << ": " << dtt << std::endl;
diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp
index 44b56fdd4..485b2c9a9 100644
--- a/src/smt/model_postprocessor.cpp
+++ b/src/smt/model_postprocessor.cpp
@@ -97,6 +97,15 @@ Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) {
     Node val = rewriteAs(asa.getExpr(), asType[1]);
     return NodeManager::currentNM()->mkConst(ArrayStoreAll(asType.toType(), val.toExpr()));
   }
+  if( n.getType().isSet() ){
+    if( n.getKind()==kind::UNION ){
+      std::vector< Node > children;
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        children.push_back( rewriteAs( n[i], asType ) );
+      }
+      return NodeManager::currentNM()->mkNode(kind::UNION,children);
+    }
+  }
   if(n.getType().isParametricDatatype() &&
      n.getType().isInstantiatedDatatype() &&
      asType.isParametricDatatype() &&
@@ -171,7 +180,7 @@ void ModelPostprocessor::visit(TNode current, TNode parent) {
     }
     Assert(t == expectType.end());
     d_nodes[current] = b;
-    Debug("tuprec") << "returning " << d_nodes[current] << endl;
+    Debug("tuprec") << "returning " << d_nodes[current] << ", operator = " << d_nodes[current].getOperator() << endl;
     // The assert below is too strong---we might be returning a model value but
     // expect a type that still uses datatypes for tuples/records.  If it's
     // really not the right type we should catch it in SmtEngine anyway.
@@ -205,7 +214,7 @@ void ModelPostprocessor::visit(TNode current, TNode parent) {
     }
     Assert(t == expectRec.end());
     d_nodes[current] = b;
-    Debug("tuprec") << "returning " << d_nodes[current] << endl;
+    Debug("tuprec") << "returning " << d_nodes[current] << ", operator = " << d_nodes[current].getOperator() << endl;
     Assert(d_nodes[current].getType() == expectType);
   } else if(current.getKind() == kind::APPLY_CONSTRUCTOR &&
             ( current.getOperator().hasAttribute(BooleanTermAttr()) ||
@@ -244,7 +253,9 @@ void ModelPostprocessor::visit(TNode current, TNode parent) {
     Debug("boolean-terms") << "model-post: " << current << endl
                            << "- returning " << n << endl;
     d_nodes[current] = n;
-  } else if(current.getKind() == kind::LAMBDA) {
+  //all kinds with children that can occur in nodes in a model go here
+  } else if(current.getKind() == kind::LAMBDA || current.getKind() == kind::SINGLETON || current.getKind() == kind::UNION || 
+            current.getKind()==kind::STORE || current.getKind()==kind::STORE_ALL || current.getKind()==kind::APPLY_CONSTRUCTOR ) {
     // rewrite based on children
     bool self = true;
     for(size_t i = 0; i < current.getNumChildren(); ++i) {
@@ -279,7 +290,7 @@ void ModelPostprocessor::visit(TNode current, TNode parent) {
         nb << rw;
       }
       d_nodes[current] = nb;
-      Debug("tuprec") << "rewrote children for kind " << current.getKind() << " got " << d_nodes[current] << endl;
+      Debug("tuprec") << "rewrote children for kind " << current.getKind() << " got " << d_nodes[current] << ", operator = " << d_nodes[current].getOperator() << endl;
     }
   } else {
     Debug("tuprec") << "returning self for kind " << current.getKind() << endl;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index be3df349a..5c6d028e5 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3835,6 +3835,8 @@ Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const {
   Debug("boolean-terms") << "postproc: got " << value << " expect type " << expectedType << endl;
   Node realValue = mpost.rewriteAs(value, expectedType);
   Debug("boolean-terms") << "postproc: realval " << realValue << " expect type " << expectedType << endl;
+  realValue = Rewriter::rewrite(realValue);
+  Debug("boolean-terms") << "postproc: after rewrite " << realValue << endl;
   return realValue;
 }
 
@@ -4287,6 +4289,7 @@ void SmtEngine::checkModel(bool hardFailure) {
       // In case it's a quantifier (or contains one), look up its value before
       // simplifying, or the quantifier might be irreparably altered.
       n = m->getValue(n);
+      Notice() << "SmtEngine::checkModel(): -- get value : " << n << std::endl;
     } else {
       // Note this "skip" is done here, rather than above.  This is
       // because (1) the quantifier could in principle simplify to false,
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index ec9318e99..6fafbca42 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -279,10 +279,13 @@ public:
   static inline void shutdown() {}
 
   static bool checkClash( Node n1, Node n2, std::vector< Node >& rew ) {
+    Trace("datatypes-rewrite-debug") << "Check clash : " << n1 << " " << n2 << std::endl;
     if( (n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR) ||
         (n1.getKind() == kind::TUPLE && n2.getKind() == kind::TUPLE) ||
         (n1.getKind() == kind::RECORD && n2.getKind() == kind::RECORD) ) {
+      //n1.getKind()==kind::APPLY_CONSTRUCTOR
       if( n1.getOperator() != n2.getOperator() ) {
+        Trace("datatypes-rewrite-debug") << "Clash operators : " << n1 << " " << n2 << " " << n1.getOperator() << " " << n2.getOperator() << std::endl;
         return true;
       } else {
         Assert( n1.getNumChildren() == n2.getNumChildren() );
@@ -294,6 +297,7 @@ public:
       }
     }else if( n1!=n2 ){
       if( n1.isConst() && n2.isConst() ){
+        Trace("datatypes-rewrite-debug") << "Clash constants : " << n1 << " " << n2 << std::endl;
         return true;
       }else{
         Node eq = NodeManager::currentNM()->mkNode( n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2 );
diff --git a/src/theory/quantifiers/quant_equality_engine.cpp b/src/theory/quantifiers/quant_equality_engine.cpp
index 8e683f660..54a931196 100755
--- a/src/theory/quantifiers/quant_equality_engine.cpp
+++ b/src/theory/quantifiers/quant_equality_engine.cpp
@@ -110,6 +110,8 @@ void QuantEqualityEngine::assertNode( Node n ) {
       d_quant_red.push_back( n );
       Trace("qee-debug") << "...add to redundant" << std::endl;
     }else{
+      Trace("qee-debug") << "...assert" << std::endl;
+      Trace("qee-assert") << "QEE : assert : " << lit << ", pol = " << pol << ", kind = " << lit.getKind() << std::endl;
       if( lit.getKind()==APPLY_UF ){
         d_uequalityEngine.assertPredicate(lit, pol, n);
       }else{
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 05d0c896a..cf0fbcbfe 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -185,7 +185,10 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
         Debug("model-getvalue-debug") << "  " << n << "[" << i << "] is " << ret << std::endl;
         children.push_back(ret);
       }
-      ret = Rewriter::rewrite(NodeManager::currentNM()->mkNode(n.getKind(), children));
+      ret = NodeManager::currentNM()->mkNode(n.getKind(), children);
+      Debug("model-getvalue-debug") << "ret (pre-rewrite): " << ret << std::endl;
+      ret = Rewriter::rewrite(ret);
+      Debug("model-getvalue-debug") << "ret (post-rewrite): " << ret << std::endl;
       if(ret.getKind() == kind::CARDINALITY_CONSTRAINT) {
         ret = NodeManager::currentNM()->mkConst(getCardinality(ret[0].getType().toType()).getFiniteCardinality() <= ret[1].getConst<Rational>().getNumerator());
       }
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index f716b8b11..7d7690d22 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -173,9 +173,9 @@ BUG_TESTS = \
 	bug593.smt2 \
 	bug595.cvc \
 	bug596.cvc \
-	bug596b.cvc
+	bug596b.cvc \
+	bug605.cvc
 #bug590.smt2
-#bug605.cvc  %% fixes 605, but disabling as it runs into a different assertion failure
 
 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 
diff --git a/test/regress/regress0/bug605.cvc b/test/regress/regress0/bug605.cvc
index 5217c2242..1ccf7fa9e 100644
--- a/test/regress/regress0/bug605.cvc
+++ b/test/regress/regress0/bug605.cvc
@@ -1,3 +1,4 @@
+% EXPECT: sat

 OPTION "produce-models";

 

 % GeoLocation

@@ -27,4 +28,3 @@ init: (A, INT, Facet) -> BOOLEAN
 ASSERT (init(a, 2, f0));

 

 CHECKSAT TRUE;

-COUNTERMODEL;
\ No newline at end of file