Fix bug in mbqi=fmc handling theory symbols. Fix mbqi=fmc models (Bug 557). Improve datatypes rewrite, make option for previous dt semantics.

6 files changed, 60 insertions, 42 deletions

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 8cb3fb4a2..99245ef69 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -138,26 +138,25 @@ public:
                                    << std::endl;
         return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]);
       }else{
-        if( options::dtRewriteErrorSel() ){
-          Node gt;
-          if( in.getType().isSort() ){
-            TypeEnumerator te(in.getType());
-            gt = *te;
-          }else{
-            gt = in.getType().mkGroundTerm();
-          }
-          TypeNode gtt = gt.getType();
-          //Assert( gtt.isDatatype() || gtt.isParametricDatatype() );
-          if( gtt.isDatatype() && !gtt.isInstantiatedDatatype() ){
-            gt = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
-                                                  NodeManager::currentNM()->mkConst(AscriptionType(in.getType().toType())), gt);
-          }
-          Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
-                                     << "Rewrite trivial selector " << in
-                                     << " to distinguished ground term "
-                                     << in.getType().mkGroundTerm() << std::endl;
-          return RewriteResponse(REWRITE_DONE,gt );
+        //typically should not be called
+        Node gt;
+        if( in.getType().isSort() ){
+          TypeEnumerator te(in.getType());
+          gt = *te;
+        }else{
+          gt = in.getType().mkGroundTerm();
         }
+        TypeNode gtt = gt.getType();
+        //Assert( gtt.isDatatype() || gtt.isParametricDatatype() );
+        if( gtt.isDatatype() && !gtt.isInstantiatedDatatype() ){
+          gt = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
+                                                NodeManager::currentNM()->mkConst(AscriptionType(in.getType().toType())), gt);
+        }
+        Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
+                                   << "Rewrite trivial selector " << in
+                                   << " to distinguished ground term "
+                                   << in.getType().mkGroundTerm() << std::endl;
+        return RewriteResponse(REWRITE_DONE,gt );
       }
     }
     if(in.getKind() == kind::TUPLE_SELECT &&
@@ -204,11 +203,18 @@ public:
       return RewriteResponse(REWRITE_DONE,
                              NodeManager::currentNM()->mkConst(true));
     }
-    if(in.getKind() == kind::EQUAL &&
-       checkClash(in[0], in[1])) {
-      Trace("datatypes-rewrite") << "Rewrite clashing equality " << in << " to false" << std::endl;
-      return RewriteResponse(REWRITE_DONE,
-                             NodeManager::currentNM()->mkConst(false));
+    if(in.getKind() == kind::EQUAL ) {
+      std::vector< Node > rew;
+      if( checkClash(in[0], in[1], rew) ){
+        Trace("datatypes-rewrite") << "Rewrite clashing equality " << in << " to false" << std::endl;
+        return RewriteResponse(REWRITE_DONE,
+                               NodeManager::currentNM()->mkConst(false));
+      }else if( rew.size()!=1 || rew[0]!=in ){
+        Node nn = rew.size()==0 ? NodeManager::currentNM()->mkConst( true ) :
+                    ( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) );
+        Trace("datatypes-rewrite") << "Rewrite equality to " << nn << std::endl;
+        return RewriteResponse(REWRITE_AGAIN_FULL, nn );
+      }
     }
 
     return RewriteResponse(REWRITE_DONE, in);
@@ -222,7 +228,7 @@ public:
   static inline void init() {}
   static inline void shutdown() {}
 
-  static bool checkClash( Node n1, Node n2 ) {
+  static bool checkClash( Node n1, Node n2, std::vector< Node >& rew ) {
     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) ) {
@@ -231,18 +237,14 @@ public:
       } else {
         Assert( n1.getNumChildren() == n2.getNumChildren() );
         for( int i=0; i<(int)n1.getNumChildren(); i++ ) {
-          if( checkClash( n1[i], n2[i] ) ) {
+          if( checkClash( n1[i], n2[i], rew ) ) {
             return true;
           }
         }
       }
-    }else if( !isTermDatatype( n1 ) ){
-      //also check for clashes between non-datatypes
+    }else{
       Node eq = NodeManager::currentNM()->mkNode( n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2 );
-      eq = Rewriter::rewrite( eq );
-      if( eq==NodeManager::currentNM()->mkConst(false) ){
-        return true;
-      }
+      rew.push_back( eq );
     }
     return false;
   }
diff --git a/src/theory/datatypes/options b/src/theory/datatypes/options
index 1daa30981..fcf36648d 100644
--- a/src/theory/datatypes/options
+++ b/src/theory/datatypes/options
@@ -9,8 +9,8 @@ module DATATYPES "theory/datatypes/options.h" Datatypes theory
 # then we do not rewrite such a selector term to an arbitrary ground term.  
 # For example, by default cvc4 considers cdr( nil ) = nil.  If this option is set, then
 # cdr( nil ) has no set value.
-expert-option dtRewriteErrorSel /--disable-dt-rewrite-error-sel bool :default true
- disable rewriting incorrectly applied selectors to arbitrary ground term
+expert-option dtRewriteErrorSel --dt-rewrite-error-sel bool :default false
+ rewrite incorrectly applied selectors to arbitrary ground term
 option dtForceAssignment /--dt-force-assignment bool :default false :read-write
  force the datatypes solver to give specific values to all datatypes terms before answering sat
  
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index fc37c5417..4858d99db 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -327,15 +327,18 @@ void TheoryDatatypes::preRegisterTerm(TNode n) {
 Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) {
   switch( n.getKind() ){
   case kind::APPLY_SELECTOR: {
-      Node selector = n.getOperator();
-      Expr selectorExpr = selector.toExpr();
+    Node selector = n.getOperator();
+    Expr selectorExpr = selector.toExpr();
+    Node sel = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( selectorExpr ), n[0] );
+    if( options::dtRewriteErrorSel() ){
+      return sel;
+    }else{
       size_t selectorIndex = Datatype::cindexOf(selectorExpr);
       const Datatype& dt = Datatype::datatypeOf(selectorExpr);
       const DatatypeConstructor& c = dt[selectorIndex];
       Expr tester = c.getTester();
       Node tst = NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( tester ), n[0] );
       tst = Rewriter::rewrite( tst );
-      Node sel = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( selectorExpr ), n[0] );
       Node n_ret;
       if( tst==NodeManager::currentNM()->mkConst( true ) ){
         n_ret = sel;
@@ -357,6 +360,7 @@ Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) {
       Trace("dt-expand") << "Expand def : " << n << " to " << n_ret << std::endl;
       return n_ret;
     }
+  }
     break;
   default:
     return n;
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 54be11b44..d5c2b0e9d 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -648,7 +648,18 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
   Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars);
   Node curr;
   for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) {
-    Node v = getRepresentative( d_models[op]->d_value[i] );
+    Node v = d_models[op]->d_value[i];
+    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 );
+      }
+    }
+    v = getRepresentative( v );
     if( curr.isNull() ){
       curr = v;
     }else{
@@ -664,7 +675,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
           if( !isStar(cond[j][1]) ){
             children.push_back( NodeManager::currentNM()->mkNode( LT, vars[j], cond[j][1] ) );
           }
-        }else if ( !isStar(cond[j]) &&  //handle the case where there are 0 or 1 ground representatives of this type...
+        }else if ( !isStar(cond[j]) &&  //handle the case where there are 0 or 1 ground eqc of this type
                    d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && d_rep_set.d_type_reps[ tn ].size()>1 ){
           Node c = getUsedRepresentative( cond[j] );
           children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) );
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 6c889781d..126b30b81 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -937,7 +937,7 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
 void FullModelChecker::doNegate( Def & dc ) {
   for (unsigned i=0; i<dc.d_cond.size(); i++) {
     if (!dc.d_value[i].isNull()) {
-      dc.d_value[i] = dc.d_value[i]==d_true ? d_false : d_true;
+      dc.d_value[i] = dc.d_value[i]==d_true ? d_false : ( dc.d_value[i]==d_false ? d_true : dc.d_value[i] );
     }
   }
 }
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index 395054d67..e3bfd39b8 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -33,12 +33,13 @@ TESTS =	\
 	fc-simple.smt2 \
 	fc-unsat-tot-2.smt2 \
 	fc-unsat-pent.smt2 \
-	fc-pigeonhole19.smt2
+	fc-pigeonhole19.smt2 \
+	Hoare-z3.931718.smt
 
 EXTRA_DIST = $(TESTS)
 
 # disabled for now :
-# Hoare-z3.931718.smt bug0909.smt2
+#  bug0909.smt2
 
 #if CVC4_BUILD_PROFILE_COMPETITION
 #else