Minor fix for corner cases of fmf-fun, fix for --dt-rewrite-error-sel. Add competition scripts (in progress).

2 files changed, 42 insertions, 36 deletions

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 0c8d0fb62..371f27c95 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1205,9 +1205,11 @@ void TheoryDatatypes::computeCareGraph(){
     unsigned functionTerms = r==0 ? d_consTerms.size() : d_selTerms.size();
     for( unsigned i=0; i<functionTerms; i++ ){
       TNode f1 = r==0 ? d_consTerms[i] : d_selTerms[i];
+      Assert(d_equalityEngine.hasTerm(f1));
       for( unsigned j=i+1; j<functionTerms; j++ ){
         TNode f2 = r==0 ? d_consTerms[j] : d_selTerms[j];
-        Trace("dt-cg-debug") << "dt-cg: " << f1 << " and " << f2 << " " << (f1.getOperator()==f2.getOperator()) << " " << areEqual( f1, f2 ) << std::endl;
+        Trace("dt-cg-debug") << "dt-cg(" << r << "): " << f1 << " and " << f2 << " " << (f1.getOperator()==f2.getOperator()) << " " << areEqual( f1, f2 ) << std::endl;
+        Assert(d_equalityEngine.hasTerm(f2));
         if( f1.getOperator()==f2.getOperator() &&
             ( ( f1.getKind()!=DT_SIZE && f1.getKind()!=DT_HEIGHT_BOUND ) || f1[0].getType()==f2[0].getType() ) &&
             !areEqual( f1, f2 ) ){
@@ -1477,7 +1479,7 @@ Node TheoryDatatypes::getSingletonLemma( TypeNode tn, bool pol ) {
     return a;
   }else{
     return it->second;
-  } 
+  }
 }
 
 void TheoryDatatypes::collectTerms( Node n ) {
@@ -1583,6 +1585,7 @@ Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index
     //Assert( n_ic==Rewriter::rewrite( n_ic ) );
     n_ic = Rewriter::rewrite( n_ic );
     collectTerms( n_ic );
+    d_equalityEngine.addTerm(n_ic);
     Debug("dt-enum") << "Made instantiate cons " << n_ic << std::endl;
     d_inst_map[n][index] = n_ic;
     return n_ic;
diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp
index a46aca3c8..32097d3eb 100644
--- a/src/theory/quantifiers/fun_def_process.cpp
+++ b/src/theory/quantifiers/fun_def_process.cpp
@@ -47,44 +47,47 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
       
       Node bd = TermDb::getFunDefBody( assertions[i] );
       Trace("fmf-fun-def-debug") << "Process function " << n << ", body = " << bd << std::endl;
-      Assert( !bd.isNull() );
-      bd = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, n, bd );
+      if( !bd.isNull() ){
+        bd = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, n, bd );
 
-      //create a sort S that represents the inputs of the function
-      std::stringstream ss;
-      ss << "I_" << f;
-      TypeNode iType = NodeManager::currentNM()->mkSort( ss.str() );
-      d_sorts[f] = iType;
-
-      //create functions f1...fn mapping from this sort to concrete elements
-      for( unsigned j=0; j<n.getNumChildren(); j++ ){
-        TypeNode typ = NodeManager::currentNM()->mkFunctionType( iType, n[j].getType() );
+        //create a sort S that represents the inputs of the function
         std::stringstream ss;
-        ss << f << "_arg_" << j;
-        d_input_arg_inj[f].push_back( NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during fun def fmf" ) );
-      }
+        ss << "I_" << f;
+        TypeNode iType = NodeManager::currentNM()->mkSort( ss.str() );
+        d_sorts[f] = iType;
 
-      //construct new quantifier forall S. F[f1(S)/x1....fn(S)/xn]
-      std::vector< Node > children;
-      Node bv = NodeManager::currentNM()->mkBoundVar("?i", iType );
-      Node bvl = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, bv );
-      std::vector< Node > subs;
-      std::vector< Node > vars;
-      for( unsigned j=0; j<n.getNumChildren(); j++ ){
-        vars.push_back( n[j] );
-        subs.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, d_input_arg_inj[f][j], bv ) );
-      }
-      bd = bd.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
-      subs_head[i] = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+        //create functions f1...fn mapping from this sort to concrete elements
+        for( unsigned j=0; j<n.getNumChildren(); j++ ){
+          TypeNode typ = NodeManager::currentNM()->mkFunctionType( iType, n[j].getType() );
+          std::stringstream ss;
+          ss << f << "_arg_" << j;
+          d_input_arg_inj[f].push_back( NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during fun def fmf" ) );
+        }
 
-      Trace("fmf-fun-def") << "FMF fun def: FUNCTION : rewrite " << assertions[i] << std::endl;
-      Trace("fmf-fun-def") << "  to " << std::endl;
-      Node new_q = NodeManager::currentNM()->mkNode( FORALL, bvl, bd );
-      new_q = Rewriter::rewrite( new_q );
-      PROOF( ProofManager::currentPM()->addDependence(new_q, assertions[i]); );
-      assertions[i] = new_q;
-      Trace("fmf-fun-def") << "  " << assertions[i] << std::endl;
-      fd_assertions.push_back( i );
+        //construct new quantifier forall S. F[f1(S)/x1....fn(S)/xn]
+        std::vector< Node > children;
+        Node bv = NodeManager::currentNM()->mkBoundVar("?i", iType );
+        Node bvl = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, bv );
+        std::vector< Node > subs;
+        std::vector< Node > vars;
+        for( unsigned j=0; j<n.getNumChildren(); j++ ){
+          vars.push_back( n[j] );
+          subs.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, d_input_arg_inj[f][j], bv ) );
+        }
+        bd = bd.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+        subs_head[i] = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+
+        Trace("fmf-fun-def") << "FMF fun def: FUNCTION : rewrite " << assertions[i] << std::endl;
+        Trace("fmf-fun-def") << "  to " << std::endl;
+        Node new_q = NodeManager::currentNM()->mkNode( FORALL, bvl, bd );
+        new_q = Rewriter::rewrite( new_q );
+        PROOF( ProofManager::currentPM()->addDependence(new_q, assertions[i]); );
+        assertions[i] = new_q;
+        Trace("fmf-fun-def") << "  " << assertions[i] << std::endl;
+        fd_assertions.push_back( i );
+      }else{
+        //can be, e.g. in corner cases forall x. f(x)=f(x), forall x. f(x)=f(x)+1
+      }
     }
   }
   //second pass : rewrite assertions