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

9 files changed, 174 insertions, 11 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
diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp
index 32097d3eb..0197bda6b 100644
--- a/src/theory/quantifiers/fun_def_process.cpp
+++ b/src/theory/quantifiers/fun_def_process.cpp
@@ -44,10 +44,11 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
         Message() << "Cannot define function " << f << " more than once." << std::endl;
         exit( 0 );
       }
-      
+
       Node bd = TermDb::getFunDefBody( assertions[i] );
       Trace("fmf-fun-def-debug") << "Process function " << n << ", body = " << bd << std::endl;
       if( !bd.isNull() ){
+        d_funcs.push_back( f );
         bd = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, n, bd );
 
         //create a sort S that represents the inputs of the function
diff --git a/src/theory/quantifiers/fun_def_process.h b/src/theory/quantifiers/fun_def_process.h
index 54735d4d6..8cff6c952 100644
--- a/src/theory/quantifiers/fun_def_process.h
+++ b/src/theory/quantifiers/fun_def_process.h
@@ -31,10 +31,6 @@ namespace quantifiers {
 //find finite models for well-defined functions
 class FunDefFmf {
 private:
-  //defined functions to input sort
-  std::map< Node, TypeNode > d_sorts;
-  //defined functions to injections input -> argument elements
-  std::map< Node, std::vector< Node > > d_input_arg_inj;
   //simplify
   Node simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, Node hd, int is_fun_def = 0 );
   //simplify term
@@ -42,7 +38,13 @@ private:
 public:
   FunDefFmf(){}
   ~FunDefFmf(){}
-
+  //defined functions to input sort (alpha)
+  std::map< Node, TypeNode > d_sorts;
+  //defined functions to injections input -> argument elements (gamma)
+  std::map< Node, std::vector< Node > > d_input_arg_inj;
+  // (newly) defined functions
+  std::vector< Node > d_funcs;
+  //simplify
   void simplify( std::vector< Node >& assertions, bool doRewrite = false );
 };
 
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index d9a31f4b5..e46f115a4 100644
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -19,6 +19,7 @@
 #include "theory/quantifiers/macros.h"
 #include "theory/rewriter.h"
 #include "proof/proof_manager.h"
+#include "smt/smt_engine_scope.h"
 
 using namespace CVC4;
 using namespace std;
@@ -46,6 +47,22 @@ bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite
         retVal = true;
       }
     }
+    //also store as defined functions
+    for( std::map< Node, Node >::iterator it = d_macro_defs.begin(); it != d_macro_defs.end(); ++it ){
+      Trace("macros-def") << "Macro definition for " << it->first << " : " << it->second << std::endl;
+      Trace("macros-def") << "  basis is : ";
+      std::vector< Node > nargs;
+      std::vector< Expr > args;
+      for( unsigned i=0; i<d_macro_basis[it->first].size(); i++ ){
+        Node bv = NodeManager::currentNM()->mkBoundVar( d_macro_basis[it->first][i].getType() );
+        Trace("macros-def") << d_macro_basis[it->first][i] << " ";
+        nargs.push_back( bv );
+        args.push_back( bv.toExpr() );
+      }
+      Trace("macros-def") << std::endl;
+      Node sbody = it->second.substitute( d_macro_basis[it->first].begin(), d_macro_basis[it->first].end(), nargs.begin(), nargs.end() );
+      smt::currentSmtEngine()->defineFunction( it->first.toExpr(), args, sbody.toExpr() );
+    }
   }
   return retVal;
 }
@@ -167,7 +184,7 @@ Node QuantifierMacros::solveInEquality( Node n, Node lit ){
           }
         }
         if( !coeff.isNull() ){
-          term = NodeManager::currentNM()->mkNode( PLUS, plus_children );
+          term = plus_children.size()==1 ? plus_children[0] : NodeManager::currentNM()->mkNode( PLUS, plus_children );
           term = NodeManager::currentNM()->mkNode( MINUS, lit[0], term );
         }
       }
diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am
index 29ad34255..59531ce8a 100644
--- a/test/regress/regress0/push-pop/Makefile.am
+++ b/test/regress/regress0/push-pop/Makefile.am
@@ -29,14 +29,17 @@ CVC_TESTS = \
 	incremental-subst-bug.cvc
 
 SMT2_TESTS = \
-	tiny_bug.smt2
+  tiny_bug.smt2
 
 BUG_TESTS = \
 	bug216.smt2 \
 	bug233.cvc \
 	bug326.smt2 \
 	arith_lra_01.smt2 \
-	arith_lra_02.smt2
+  arith_lra_02.smt2 \
+  quant-fun-proc.smt2 \
+  quant-fun-proc-unmacro.smt2 \
+  quant-fun-proc-unfd.smt2 
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 
diff --git a/test/regress/regress0/push-pop/quant-fun-proc-unfd.smt2 b/test/regress/regress0/push-pop/quant-fun-proc-unfd.smt2
new file mode 100644
index 000000000..f16c6fb90
--- /dev/null
+++ b/test/regress/regress0/push-pop/quant-fun-proc-unfd.smt2
@@ -0,0 +1,34 @@
+; COMMAND-LINE: --incremental --fmf-fun --macros-quant --no-check-models
+(set-logic UFLIA)
+
+
+(define-fun f ((x Int)) Int x)
+
+(declare-fun h (Int) Int)
+(assert (forall ((x Int)) (= (h x) 0)))
+
+; EXPECT: sat
+(push 1)
+(define-fun-rec g ((x Int)) Int (ite (<= x 0) 0 (+ (g x) x)))
+(check-sat)
+(pop 1)
+
+(declare-fun g (Int) Int)
+
+; EXPECT: unsat
+(push 1)
+(assert (= (f 1) 2))
+(check-sat)
+(pop 1)
+
+; EXPECT: sat
+(push 1)
+(assert (= (g 1) 5))
+(check-sat)
+(pop 1)
+
+; EXPECT: unsat
+(push 1)
+(assert (= (h 1) 5))
+(check-sat)
+(pop 1)
diff --git a/test/regress/regress0/push-pop/quant-fun-proc-unmacro.smt2 b/test/regress/regress0/push-pop/quant-fun-proc-unmacro.smt2
new file mode 100644
index 000000000..7cacfca98
--- /dev/null
+++ b/test/regress/regress0/push-pop/quant-fun-proc-unmacro.smt2
@@ -0,0 +1,34 @@
+; COMMAND-LINE: --incremental --fmf-fun --macros-quant --no-check-models
+(set-logic UFLIA)
+
+
+(define-fun f ((x Int)) Int x)
+
+(define-fun-rec g ((x Int)) Int (ite (<= x 0) 0 (+ (g x) x)))
+
+; EXPECT: sat
+(declare-fun h (Int) Int)
+(push 1)
+(assert (forall ((x Int)) (= (h x) 0)))
+(check-sat)
+(pop 1)
+
+
+; EXPECT: unsat
+(push 1)
+(assert (= (f 1) 2))
+(check-sat)
+(pop 1)
+
+; EXPECT: unsat
+(push 1)
+(assert (= (g 1) 5))
+(check-sat)
+(pop 1)
+
+; EXPECT: sat
+(push 1)
+(assert (= (h 1) 5))
+(check-sat)
+(pop 1)
+
diff --git a/test/regress/regress0/push-pop/quant-fun-proc.smt2 b/test/regress/regress0/push-pop/quant-fun-proc.smt2
new file mode 100644
index 000000000..8f4758df6
--- /dev/null
+++ b/test/regress/regress0/push-pop/quant-fun-proc.smt2
@@ -0,0 +1,30 @@
+; COMMAND-LINE: --incremental --fmf-fun --macros-quant --no-check-models
+(set-logic UFLIA)
+
+(define-fun f ((x Int)) Int x)
+
+(define-fun-rec g ((x Int)) Int (ite (<= x 0) 0 (+ (g x) x)))
+
+(declare-fun h (Int) Int)
+(assert (forall ((x Int)) (= (h x) (+ x 3))))
+
+; EXPECT: sat
+(check-sat)
+
+; EXPECT: unsat
+(push 1)
+(assert (= (f 1) 2))
+(check-sat)
+(pop 1)
+
+; EXPECT: unsat
+(push 1)
+(assert (= (g 1) 5))
+(check-sat)
+(pop 1)
+
+; EXPECT: unsat
+(push 1)
+(assert (= (h 1) 5))
+(check-sat)
+(pop 1)