From: ajreynol Date: Fri, 31 Jul 2015 23:31:07 +0000 (+0200) Subject: Make --fmf-fun and --macros-quant work in incremental mode. Add regressions. X-Git-Tag: cvc5-1.0.0~6262 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=91f40dee752910fca5d749656c0b6ee1bc1281aa;p=cvc5.git Make --fmf-fun and --macros-quant work in incremental mode. Add regressions. --- 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_mapfind(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; iinsert( f, fdf.d_sorts[f] ); + SmtEngine::NodeList* cl = new(true) SmtEngine::NodeList( d_smt.d_userContext ); + for( unsigned j=0; jpush_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 AssertionList; /** The type of our internal assignment set */ typedef context::CDHashSet AssignmentSet; + /** The types for the recursive function definitions */ + typedef context::CDHashMap< Node, TypeNode, NodeHashFunction > TypeNodeMap; + typedef context::CDList NodeList; + typedef context::CDHashMap 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; ifirst].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)