Minor fixes to model construction to take singleton equivalence classes into account (fixes sets+dt model bug). Minor fix for mixed int/real quantifier instantiation.

5 files changed, 39 insertions, 13 deletions

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index a2f995935..dc39183b5 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -865,6 +865,11 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
             }
             //d_consEqc[t1] = true;
           }
+          //AJR: do this?
+          //else if( cons2.isConst() ){
+          //  //prefer the constant
+          //  eqc1->d_constructor = cons2;
+          //}
           //d_consEqc[t2] = false;
         }
       }else{
diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index cd263e90c..0fe4b98c7 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -749,6 +749,7 @@ bool CegInstantiator::doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int
       Trace("cbqi-inst") << pv_coeff << " * ";
     }
     Trace("cbqi-inst") << pv << " -> " << n << std::endl;
+    Assert( n.getType().isSubtypeOf( pv.getType() ) );
   }
   //must ensure variables have been computed for n
   computeProgVars( n );
@@ -772,6 +773,7 @@ bool CegInstantiator::doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int
   std::vector< Node > new_has_coeff;
   Trace("cbqi-inst-debug2") << "Applying substitutions..." << std::endl;
   for( unsigned j=0; j<sf.d_subs.size(); j++ ){
+    Trace("cbqi-inst-debug2") << "  Apply for " << sf.d_subs[j]  << std::endl;
     Assert( d_prog_var.find( sf.d_subs[j] )!=d_prog_var.end() );
     if( d_prog_var[sf.d_subs[j]].find( pv )!=d_prog_var[sf.d_subs[j]].end() ){
       prev_subs[j] = sf.d_subs[j];
@@ -1629,10 +1631,11 @@ int CegInstantiator::solve_arith( Node pv, Node atom, Node& veq_c, Node& val, No
             real_part.push_back( msum[it->first].isNull() ? it->first : NodeManager::currentNM()->mkNode( MULT, msum[it->first], it->first ) );
           }
         }
-        for( unsigned t=0; t<2; t++ ){
-          if( !vts_coeff[t].isNull() ){
-            vts_coeff[t] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, rcoeff, vts_coeff[t] ) );
-          }
+        //remove delta  TODO: check this
+        vts_coeff[1] = Node::null();
+        //multiply inf
+        if( !vts_coeff[0].isNull() ){
+          vts_coeff[0] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, rcoeff, vts_coeff[0] ) );
         }
         realPart = real_part.empty() ? d_zero : ( real_part.size()==1 ? real_part[0] : NodeManager::currentNM()->mkNode( PLUS, real_part ) );
         Assert( d_out->isEligibleForInstantiation( realPart ) );
@@ -1645,7 +1648,7 @@ int CegInstantiator::solve_arith( Node pv, Node atom, Node& veq_c, Node& val, No
           int ires_use = ( msum[pv].isNull() || msum[pv].getConst<Rational>().sgn()==1 ) ? 1 : -1;
           val = Rewriter::rewrite( NodeManager::currentNM()->mkNode( ires_use==-1 ? PLUS : MINUS,
                                     NodeManager::currentNM()->mkNode( ires_use==-1 ? MINUS : PLUS, val, realPart ),
-                                    NodeManager::currentNM()->mkNode( TO_INTEGER, realPart ) ) );
+                                    NodeManager::currentNM()->mkNode( TO_INTEGER, realPart ) ) );  //TODO: round up for upper bounds?
           Trace("cbqi-inst-debug") << "result : " << val << std::endl;
           Assert( val.getType().isInteger() );
         }
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index cccd5c350..3cdaeb106 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -375,6 +375,11 @@ void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set<Node>*
       } else {
         if (first) {
           rep = (*eqc_i);
+          //add the term (this is specifically for the case of singleton equivalence classes)
+          if( !rep.getType().isRegExp() ){
+            d_equalityEngine->addTerm( rep );
+            Trace("model-builder-debug") << "Add term to ee within assertEqualityEngine: " << rep << std::endl;
+          }
           first = false;
         }
         else {
@@ -674,7 +679,8 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
     // Assign representative for this EC
     if (!const_rep.isNull()) {
       // Theories should not specify a rep if there is already a constant in the EC
-      Assert(rep.isNull() || rep == const_rep);
+      //AJR: I believe this assertion is too strict, eqc with asserted reps may merge with constant eqc
+      //Assert(rep.isNull() || rep == const_rep);
       assignConstantRep( tm, constantReps, eqc, const_rep, fullModel );
       typeConstSet.add(eqct.getBaseType(), const_rep);
     }
@@ -812,14 +818,16 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
       
       //get properties of this type
       bool isCorecursive = false;
-      bool isUSortFiniteRestricted = false;
       if( t.isDatatype() ){
         const Datatype& dt = ((DatatypeType)(t).toType()).getDatatype();
         isCorecursive = dt.isCodatatype() && ( !dt.isFinite() || dt.isRecursiveSingleton() );
       }
+#ifdef CVC4_ASSERTIONS
+      bool isUSortFiniteRestricted = false;
       if( options::finiteModelFind() ){
         isUSortFiniteRestricted = !t.isSort() && involvesUSort( t );
       }
+#endif
       
       set<Node>* repSet = typeRepSet.getSet(t);
       TypeNode tb = t.getBaseType();
@@ -864,8 +872,8 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
               Assert( !n.isNull() );
               success = true;
               Trace("model-builder-debug") << "Check if excluded : " << n << std::endl;
-              if( isUSortFiniteRestricted ){
 #ifdef CVC4_ASSERTIONS
+              if( isUSortFiniteRestricted ){
                 //must not involve uninterpreted constants beyond cardinality bound (which assumed to coincide with #eqc)
                 //this is just an assertion now, since TypeEnumeratorProperties should ensure that only legal values are enumerated wrt this constraint.
                 std::map< Node, bool > visited;
@@ -874,8 +882,8 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
                   Trace("model-builder") << "Excluded value for " << t << " : " << n << " due to out of range uninterpreted constant." << std::endl;
                 }
                 Assert( success );
-#endif
               }
+#endif
               if( success && isCorecursive ){
                 if (repSet != NULL && !repSet->empty()) {
                   // in the case of codatatypes, check if it is in the set of values that we cannot assign
@@ -960,9 +968,9 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
   //modelBuilder-specific initialization
   processBuildModel( tm, fullModel );
 
-  // Collect model comments from the theories
+  // Do post-processing of model from the theories (used for THEORY_SEP to construct heap model)
   if( fullModel ){
-    Trace("model-builder") << "TheoryEngineModelBuilder: Collect model comments..." << std::endl;
+    Trace("model-builder") << "TheoryEngineModelBuilder: Post-process model..." << std::endl;
     d_te->postProcessModel(tm);
   }
   
@@ -1044,7 +1052,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.getKind()==kind::REGEXP_RANGE || retNode.isConst());
+      Assert(retNode.getKind()==kind::APPLY_UF || retNode.getType().isRegExp() || retNode.isConst());
     }
   }
   d_normalizedCache[r] = retNode;
diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index 19f6313fb..98e7e744c 100644
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -62,7 +62,8 @@ TESTS =	\
 	union-1a.smt2 \
 	union-1b-flip.smt2 \
 	union-1b.smt2 \
-	union-2.smt2
+	union-2.smt2 \
+	dt-simp-mem.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/sets/dt-simp-mem.smt2 b/test/regress/regress0/sets/dt-simp-mem.smt2
new file mode 100644
index 000000000..a38544aa2
--- /dev/null
+++ b/test/regress/regress0/sets/dt-simp-mem.smt2
@@ -0,0 +1,9 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-datatypes () ((D (A (a Int)))))
+(declare-fun x1 () D)
+(declare-fun S () (Set D))
+(declare-fun P (D) Bool)
+(assert (member x1 S))
+(assert (=> (member (A 0) S) (P x1)))
+(check-sat)