Make --fmf-fun and --macros-quant work in incremental mode. Add regressions.

2 files changed, 44 insertions, 2 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ce8f68c09..1e0c63ce8 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -693,6 +693,8 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_propEngine(NULL),
   d_proofManager(NULL),
   d_definedFunctions(NULL),
+  d_fmfRecFunctionsAbs(NULL),
+  d_fmfRecFunctionsConcrete(NULL),
   d_assertionList(NULL),
   d_assignments(NULL),
   d_modelGlobalCommands(),
@@ -736,6 +738,10 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_context->push();
 
   d_definedFunctions = new(true) DefinedFunctionMap(d_userContext);
+  if( options::fmfFunWellDefined() ){
+    d_fmfRecFunctionsAbs = new(true) TypeNodeMap(d_userContext);
+    d_fmfRecFunctionsConcrete = new(true) NodeListMap(d_userContext);
+  }
   d_modelCommands = new(true) smt::CommandList(d_userContext);
 }
 
@@ -1841,7 +1847,14 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
       }
 
       // otherwise expand it
-      if (k == kind::APPLY && n.getOperator().getKind() != kind::LAMBDA) {
+      bool doExpand = ( k == kind::APPLY && n.getOperator().getKind() != kind::LAMBDA );
+      if( !doExpand ){
+        if( options::macrosQuant() ){
+          //expand if we have inferred an operator corresponds to a defined function
+          doExpand = k==kind::APPLY_UF && d_smt.isDefinedFunction( n.getOperator().toExpr() );
+        }
+      }
+      if (doExpand) {
         // application of a user-defined symbol
         TNode func = n.getOperator();
         SmtEngine::DefinedFunctionMap::const_iterator i = d_smt.d_definedFunctions->find(func);
@@ -3285,7 +3298,7 @@ void SmtEnginePrivate::processAssertions() {
       }
     }
     dumpAssertions("post-skolem-quant", d_assertions);
-    if( options::macrosQuant() && !options::incrementalSolving() ){
+    if( options::macrosQuant() ){
       //quantifiers macro expansion
       bool success;
       do{
@@ -3297,7 +3310,29 @@ void SmtEnginePrivate::processAssertions() {
     //fmf-fun : assume admissible functions, applying preprocessing reduction to FMF
     if( options::fmfFunWellDefined() ){
       quantifiers::FunDefFmf fdf;
+      //must carry over current definitions (for incremental)
+      for( SmtEngine::TypeNodeMap::const_iterator fit = d_smt.d_fmfRecFunctionsAbs->begin(); fit != d_smt.d_fmfRecFunctionsAbs->end(); ++fit ){
+        Node f = (*fit).first;
+        TypeNode ft = (*fit).second;
+        fdf.d_sorts[f] = ft;
+        SmtEngine::NodeListMap::const_iterator fcit = d_smt.d_fmfRecFunctionsConcrete->find( f );
+        Assert( fcit!=d_smt.d_fmfRecFunctionsConcrete->end() );
+        SmtEngine::NodeList* cl = (*fcit).second;
+        for( SmtEngine::NodeList::const_iterator cit = cl->begin(); cit != cl->end(); ++cit ){
+          fdf.d_input_arg_inj[f].push_back( *cit );
+        }
+      }
       fdf.simplify( d_assertions.ref() );
+      //must store new definitions (for incremental)
+      for( unsigned i=0; i<fdf.d_funcs.size(); i++ ){
+        Node f = fdf.d_funcs[i];
+        d_smt.d_fmfRecFunctionsAbs->insert( f, fdf.d_sorts[f] );
+        SmtEngine::NodeList* cl = new(true) SmtEngine::NodeList( d_smt.d_userContext );
+        for( unsigned j=0; j<fdf.d_input_arg_inj[f].size(); j++ ){
+          cl->push_back( fdf.d_input_arg_inj[f][j] );
+        }
+        d_smt.d_fmfRecFunctionsConcrete->insert( f, cl );
+      }
     }
   }
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index db0809308..b4c293dff 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -128,6 +128,10 @@ class CVC4_PUBLIC SmtEngine {
   typedef context::CDList<Expr> AssertionList;
   /** The type of our internal assignment set */
   typedef context::CDHashSet<Node, NodeHashFunction> AssignmentSet;
+  /** The types for the recursive function definitions */
+  typedef context::CDHashMap< Node, TypeNode, NodeHashFunction > TypeNodeMap;
+  typedef context::CDList<Node> NodeList;
+  typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap;
 
   /** Expr manager context */
   context::Context* d_context;
@@ -151,6 +155,9 @@ class CVC4_PUBLIC SmtEngine {
   ProofManager* d_proofManager;
   /** An index of our defined functions */
   DefinedFunctionMap* d_definedFunctions;
+  /** recursive function definition abstractions for --fmf-fun */
+  TypeNodeMap* d_fmfRecFunctionsAbs;
+  NodeListMap* d_fmfRecFunctionsConcrete;
 
   /**
    * The assertion list (before any conversion) for supporting