Fix model bug in --mbqi=fmc. Minor cleanup in datatypes.

5 files changed, 38 insertions, 14 deletions

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 83d14149b..f3b8c1ec9 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -170,9 +170,9 @@ void TheoryDatatypes::check(Effort e) {
         TypeNode tn = n.getType();
         if( DatatypesRewriter::isTypeDatatype( tn ) ){
           Trace("datatypes-debug") << "Process equivalence class " << n << std::endl;
-          EqcInfo* eqc = getOrMakeEqcInfo( n, true );
+          EqcInfo* eqc = getOrMakeEqcInfo( n );
           //if there are more than 1 possible constructors for eqc
-          if( eqc->d_constructor.get().isNull() && !hasLabel( eqc, n ) ) {
+          if( !hasLabel( eqc, n ) ){
             Trace("datatypes-debug") << "No constructor..." << std::endl;
             const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
 
@@ -191,7 +191,7 @@ void TheoryDatatypes::check(Effort e) {
                 if( consIndex==-1 ){
                   consIndex = j;
                 }
-                if( !dt[ j ].isFinite() && !eqc->d_selectors ) {
+                if( !dt[ j ].isFinite() && ( !eqc || !eqc->d_selectors ) ) {
                   needSplit = false;
                 }
               }
@@ -832,7 +832,7 @@ d_inst( c, false ), d_constructor( c, Node::null() ), d_selectors( c, false ){
 }
 
 bool TheoryDatatypes::hasLabel( EqcInfo* eqc, Node n ){
-  return !eqc->d_constructor.get().isNull() || !getLabel( n ).isNull();
+  return ( eqc && !eqc->d_constructor.get().isNull() ) || !getLabel( n ).isNull();
 }
 
 Node TheoryDatatypes::getLabel( Node n ) {
@@ -847,7 +847,7 @@ Node TheoryDatatypes::getLabel( Node n ) {
 }
 
 int TheoryDatatypes::getLabelIndex( EqcInfo* eqc, Node n ){
-  if( !eqc->d_constructor.get().isNull() ){
+  if( eqc && !eqc->d_constructor.get().isNull() ){
     return Datatype::indexOf( eqc->d_constructor.get().getOperator().toExpr() );
   }else{
     return Datatype::indexOf( getLabel( n ).getOperator().toExpr() );
@@ -1118,7 +1118,7 @@ void TheoryDatatypes::computeCareGraph(){
             TNode x = f1[k];
             TNode y = f2[k];
             Assert(d_equalityEngine.hasTerm(x));
-            Assert(d_equalityEngine.hasTerm(y));            
+            Assert(d_equalityEngine.hasTerm(y));
             if( areDisequal(x, y) ){
               somePairIsDisequal = true;
               break;
@@ -1209,7 +1209,7 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
         cons.push_back( c );
         eqc_cons[ eqc ] = c;
       }else{
-        //if eqc contains a symbol known to datatypes (a selector), then we must assign 
+        //if eqc contains a symbol known to datatypes (a selector), then we must assign
         bool containsTSym = false;
         eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
         while( !eqc_i.isFinished() ){
@@ -1815,7 +1815,7 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){
         addLemma = true;
       }
     }
-    
+
     if( !addLemma ){
       TypeNode tn = n[0].getType();
       if( !DatatypesRewriter::isTypeDatatype( tn ) ){
@@ -1907,7 +1907,9 @@ void TheoryDatatypes::printModelDebug( const char* c ){
       //add terms to model
       eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
       while( !eqc_i.isFinished() ){
-        Trace( c ) << (*eqc_i) << " ";
+        if( (*eqc_i)!=eqc ){
+          Trace( c ) << (*eqc_i) << " ";
+        }
         ++eqc_i;
       }
       Trace( c ) << "}" << std::endl;
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 07fea3cca..1570ba306 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -677,18 +677,24 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
   Node curr;
   for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) {
     Node v = d_models[op]->d_value[i];
+    Trace("fmc-model-func") << "Value is : " << v << std::endl;
     if( !hasTerm( v ) ){
       //can happen when the model basis term does not exist in ground assignment
       TypeNode tn = v.getType();
-      if( d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && !d_rep_set.d_type_reps[ tn ].empty() ){
-        //see full_model_check.cpp line 366
-        v = d_rep_set.d_type_reps[tn][ d_rep_set.d_type_reps[tn].size()-1 ];
-      }else{
-        Assert( false );
+      //check if it is a constant introduced as a representative not existing in the model's equality engine
+      if( !d_rep_set.hasRep( tn, v ) ){
+        if( d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && !d_rep_set.d_type_reps[ tn ].empty() ){
+          //see full_model_check.cpp line 366
+          v = d_rep_set.d_type_reps[tn][ d_rep_set.d_type_reps[tn].size()-1 ];
+        }else{
+          Assert( false );
+        }
+        Trace("fmc-model-func") << "No term, assign " << v << std::endl;
       }
     }
     v = getRepresentative( v );
     if( curr.isNull() ){
+      Trace("fmc-model-func") << "base : " << v << std::endl;
       curr = v;
     }else{
       //make the condition
@@ -711,6 +717,8 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
       }
       Assert( !children.empty() );
       Node cc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children );
+
+      Trace("fmc-model-func") << "condition : " << cc << ", value : " << v << std::endl;
       curr = NodeManager::currentNM()->mkNode( ITE, cc, v, curr );
     }
   }
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index ee14d6fc1..db0524034 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -28,6 +28,15 @@ void RepSet::clear(){
   d_tmap.clear();
 }
 
+bool RepSet::hasRep( TypeNode tn, Node n ) {
+  std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.find( tn );
+  if( it==d_type_reps.end() ){
+    return false;
+  }else{
+    return std::find( it->second.begin(), it->second.end(), n )!=it->second.end();
+  }
+}
+
 int RepSet::getNumRepresentatives( TypeNode tn ) const{
   std::map< TypeNode, std::vector< Node > >::const_iterator it = d_type_reps.find( tn );
   if( it!=d_type_reps.end() ){
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index 23db36ead..19bb6d3d3 100644
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -37,6 +37,8 @@ public:
   void clear();
   /** has type */
   bool hasType( TypeNode tn ) const { return d_type_reps.find( tn )!=d_type_reps.end(); }
+  /** has rep */
+  bool hasRep( TypeNode tn, Node n );
   /** get cardinality for type */
   int getNumRepresentatives( TypeNode tn ) const;
   /** add representative for type */
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 54a647d89..7e1129e7b 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -169,9 +169,11 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
     if (n.getNumChildren() > 0 &&
         n.getKind() != kind::BITVECTOR_ACKERMANIZE_UDIV &&
         n.getKind() != kind::BITVECTOR_ACKERMANIZE_UREM) {
+      Debug("model-getvalue-debug") << "Get model value children " << n << std::endl;
       std::vector<Node> children;
       if (n.getKind() == APPLY_UF) {
         Node op = getModelValue(n.getOperator(), hasBoundVars);
+        Debug("model-getvalue-debug") << "  operator : " << op << std::endl;
         children.push_back(op);
       }
       else if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
@@ -180,6 +182,7 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
       //evaluate the children
       for (unsigned i = 0; i < n.getNumChildren(); ++i) {
         ret = getModelValue(n[i], hasBoundVars);
+        Debug("model-getvalue-debug") << "  " << n << "[" << i << "] is " << ret << std::endl;
         children.push_back(ret);
       }
       ret = Rewriter::rewrite(NodeManager::currentNM()->mkNode(n.getKind(), children));