From a582fa3ea1de3b6419797bbebdcb415ff4d0c0d0 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 12 Aug 2015 07:33:16 +0200 Subject: [PATCH] Improvements to --macros-quant. Enable --clause-split by default. Bug fix for cbqi regarding instantiations with free skolems, extend to boolean quantification. Infrastructure for congruence closure with free variables. --- src/Makefile.am | 4 +- src/smt/smt_engine.cpp | 29 +- src/theory/quantifiers/inst_strategy_cbqi.cpp | 2 +- .../quantifiers/instantiation_engine.cpp | 10 +- src/theory/quantifiers/instantiation_engine.h | 1 + src/theory/quantifiers/macros.cpp | 274 +++++++++++++----- src/theory/quantifiers/macros.h | 15 +- src/theory/quantifiers/modes.h | 7 + src/theory/quantifiers/options | 27 +- src/theory/quantifiers/options_handlers.h | 24 ++ .../quantifiers/quant_equality_engine.cpp | 139 +++++++++ .../quantifiers/quant_equality_engine.h | 92 ++++++ .../quantifiers/quantifiers_rewriter.cpp | 21 +- src/theory/quantifiers/term_database.cpp | 2 +- src/theory/quantifiers_engine.cpp | 31 +- src/theory/quantifiers_engine.h | 5 + test/regress/regress0/quantifiers/Makefile.am | 6 +- .../regress0/quantifiers/nested-delta.smt2 | 6 + .../regress0/quantifiers/nested-inf.smt2 | 6 + 19 files changed, 595 insertions(+), 106 deletions(-) create mode 100755 src/theory/quantifiers/quant_equality_engine.cpp create mode 100755 src/theory/quantifiers/quant_equality_engine.h create mode 100644 test/regress/regress0/quantifiers/nested-delta.smt2 create mode 100644 test/regress/regress0/quantifiers/nested-inf.smt2 diff --git a/src/Makefile.am b/src/Makefile.am index b0d97754d..0cd4cff44 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -336,7 +336,9 @@ libcvc4_la_SOURCES = \ theory/quantifiers/fun_def_process.h \ theory/quantifiers/fun_def_process.cpp \ theory/quantifiers/fun_def_engine.h \ - theory/quantifiers/fun_def_engine.cpp \ + theory/quantifiers/fun_def_engine.cpp \ + theory/quantifiers/quant_equality_engine.h \ + theory/quantifiers/quant_equality_engine.cpp \ theory/quantifiers/options_handlers.h \ theory/arith/theory_arith_type_rules.h \ theory/arith/type_enumerator.h \ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 1e0c63ce8..87cd815e9 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3125,6 +3125,7 @@ void SmtEnginePrivate::processAssertions() { // Dump the assertions dumpAssertions("pre-everything", d_assertions); + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() begin" << endl; Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl; Debug("smt") << " d_assertions : " << d_assertions.size() << endl; @@ -3149,6 +3150,7 @@ void SmtEnginePrivate::processAssertions() { // Assertions are NOT guaranteed to be rewritten by this point + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-definition-expansion" << endl; dumpAssertions("pre-definition-expansion", d_assertions); { Chat() << "expanding definitions..." << endl; @@ -3159,6 +3161,7 @@ void SmtEnginePrivate::processAssertions() { d_assertions.replace(i, expandDefinitions(d_assertions[i], cache)); } } + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-definition-expansion" << endl; dumpAssertions("post-definition-expansion", d_assertions); Debug("smt") << " d_assertions : " << d_assertions.size() << endl; @@ -3212,12 +3215,14 @@ void SmtEnginePrivate::processAssertions() { // Unconstrained simplification if(options::unconstrainedSimp()) { + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-unconstrained-simp" << endl; dumpAssertions("pre-unconstrained-simp", d_assertions); Chat() << "...doing unconstrained simplification..." << endl; for (unsigned i = 0; i < d_assertions.size(); ++ i) { d_assertions.replace(i, Rewriter::rewrite(d_assertions[i])); } unconstrainedSimp(); + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-unconstrained-simp" << endl; dumpAssertions("post-unconstrained-simp", d_assertions); } @@ -3225,6 +3230,7 @@ void SmtEnginePrivate::processAssertions() { theory::bv::BVIntroducePow2::pow2Rewrite(d_assertions.ref()); } + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-substitution" << endl; dumpAssertions("pre-substitution", d_assertions); if(options::unsatCores()) { @@ -3240,13 +3246,13 @@ void SmtEnginePrivate::processAssertions() { << "applying substitutions" << endl; for (unsigned i = 0; i < d_assertions.size(); ++ i) { Trace("simplify") << "applying to " << d_assertions[i] << endl; - spendResource(options::preprocessStep()); + spendResource(options::preprocessStep()); d_assertions.replace(i, Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertions[i]))); Trace("simplify") << " got " << d_assertions[i] << endl; } } } - + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-substitution" << endl; dumpAssertions("post-substitution", d_assertions); // Assertions ARE guaranteed to be rewritten by this point @@ -3261,15 +3267,18 @@ void SmtEnginePrivate::processAssertions() { } if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) { + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-strings-preprocess" << endl; dumpAssertions("pre-strings-pp", d_assertions); CVC4::theory::strings::StringsPreprocess sp; sp.simplify( d_assertions.ref() ); //for (unsigned i = 0; i < d_assertions.size(); ++ i) { // d_assertions.replace( i, Rewriter::rewrite( d_assertions[i] ) ); //} + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-strings-preprocess" << endl; dumpAssertions("post-strings-pp", d_assertions); } if( d_smt.d_logic.isQuantified() ){ + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << endl; //remove rewrite rules for( unsigned i=0; i < d_assertions.size(); i++ ) { if( d_assertions[i].getKind() == kind::REWRITE_RULE ){ @@ -3300,11 +3309,13 @@ void SmtEnginePrivate::processAssertions() { dumpAssertions("post-skolem-quant", d_assertions); if( options::macrosQuant() ){ //quantifiers macro expansion + quantifiers::QuantifierMacros qm; bool success; do{ - quantifiers::QuantifierMacros qm; success = qm.simplify( d_assertions.ref(), true ); }while( success ); + //finalize the definitions + qm.finalizeDefinitions(); } //fmf-fun : assume admissible functions, applying preprocessing reduction to FMF @@ -3334,6 +3345,7 @@ void SmtEnginePrivate::processAssertions() { d_smt.d_fmfRecFunctionsConcrete->insert( f, cl ); } } + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-quant-preprocess" << endl; } if( options::sortInference() ){ @@ -3353,27 +3365,32 @@ void SmtEnginePrivate::processAssertions() { } } + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-simplify" << endl; dumpAssertions("pre-simplify", d_assertions); Chat() << "simplifying assertions..." << endl; noConflict = simplifyAssertions(); if(!noConflict){ ++(d_smt.d_stats->d_simplifiedToFalse); } + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-simplify" << endl; dumpAssertions("post-simplify", d_assertions); dumpAssertions("pre-static-learning", d_assertions); if(options::doStaticLearning()) { + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-static-learning" << endl; // Perform static learning Chat() << "doing static learning..." << endl; Trace("simplify") << "SmtEnginePrivate::simplify(): " << "performing static learning" << endl; staticLearning(); + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-static-learning" << endl; } dumpAssertions("post-static-learning", d_assertions); Debug("smt") << " d_assertions : " << d_assertions.size() << endl; + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-ite-removal" << endl; dumpAssertions("pre-ite-removal", d_assertions); { Chat() << "removing term ITEs..." << endl; @@ -3383,10 +3400,12 @@ void SmtEnginePrivate::processAssertions() { removeITEs(); d_smt.d_stats->d_numAssertionsPost += d_assertions.size(); } + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-ite-removal" << endl; dumpAssertions("post-ite-removal", d_assertions); dumpAssertions("pre-repeat-simplify", d_assertions); if(options::repeatSimp()) { + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-repeat-simplify" << endl; Chat() << "re-simplifying assertions..." << endl; ScopeCounter depth(d_simplifyAssertionsDepth); noConflict &= simplifyAssertions(); @@ -3452,6 +3471,7 @@ void SmtEnginePrivate::processAssertions() { removeITEs(); // Assert(iteRewriteAssertionsEnd == d_assertions.size()); } + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << endl; } dumpAssertions("post-repeat-simplify", d_assertions); @@ -3476,6 +3496,7 @@ void SmtEnginePrivate::processAssertions() { Debug("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl; Debug("smt") << " d_assertions : " << d_assertions.size() << endl; + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-theory-preprocessing" << endl; dumpAssertions("pre-theory-preprocessing", d_assertions); { Chat() << "theory preprocessing..." << endl; @@ -3486,6 +3507,7 @@ void SmtEnginePrivate::processAssertions() { d_assertions.replace(i, d_smt.d_theoryEngine->preprocess(d_assertions[i])); } } + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-theory-preprocessing" << endl; dumpAssertions("post-theory-preprocessing", d_assertions); // If we are using eager bit-blasting wrap assertions in fake atom so that @@ -3511,6 +3533,7 @@ void SmtEnginePrivate::processAssertions() { // end: INVARIANT to maintain: no reordering of assertions or // introducing new ones + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl; dumpAssertions("post-everything", d_assertions); //set instantiation level of everything to zero diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 20bd71b45..d9ac190dc 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -1130,7 +1130,7 @@ bool InstStrategyCegqi::addLemma( Node lem ) { } bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) { - if( n.getKind()==INST_CONSTANT ){ + if( n.getKind()==INST_CONSTANT || n.getKind()==SKOLEM ){ //only legal if current quantified formula contains n return TermDb::containsTerm( d_curr_quant, n ); }else{ diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 631216507..b686ddb3b 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -164,6 +164,14 @@ bool InstantiationEngine::needsCheck( Theory::Effort e ){ return d_quantEngine->getInstWhenNeedsCheck( e ); } +unsigned InstantiationEngine::needsModel( Theory::Effort e ) { + if( options::cbqiModel() && options::cbqi() ){ + return QuantifiersEngine::QEFFORT_STANDARD; + }else{ + return QuantifiersEngine::QEFFORT_NONE; + } +} + void InstantiationEngine::reset_round( Theory::Effort e ) { d_cbqi_set_quant_inactive = false; if( options::cbqi() ){ @@ -288,7 +296,7 @@ bool InstantiationEngine::hasApplyUf( Node f ){ bool InstantiationEngine::hasNonArithmeticVariable( Node f ){ for( int i=0; i<(int)f[0].getNumChildren(); i++ ){ TypeNode tn = f[0][i].getType(); - if( !tn.isInteger() && !tn.isReal() ){ + if( !tn.isInteger() && !tn.isReal() && !tn.isBoolean() ){ return true; } } diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index 5d46a9815..44612a85c 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -98,6 +98,7 @@ public: void finishInit(); bool needsCheck( Theory::Effort e ); + unsigned needsModel( Theory::Effort e ); void reset_round( Theory::Effort e ); void check( Theory::Effort e, unsigned quant_e ); bool checkComplete(); diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp index e46f115a4..c26aea465 100644 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp @@ -20,6 +20,8 @@ #include "theory/rewriter.h" #include "proof/proof_manager.h" #include "smt/smt_engine_scope.h" +#include "theory/quantifiers/modes.h" +#include "theory/quantifiers/options.h" using namespace CVC4; using namespace std; @@ -29,56 +31,84 @@ using namespace CVC4::kind; bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){ - Trace("macros") << "Find macros..." << std::endl; - //first, collect macro definitions - for( size_t i=0; i simp_assertions; + int last_macro = -1; + for( int i=0; i<(int)assertions.size(); i++ ){ + Trace("macros-debug") << " process assertion " << assertions[i] << std::endl; + Node curr = assertions[i]; + //do simplification before process + if( doRewrite && !d_macro_defs_new.empty() ){ + curr = simplify( assertions[i] ); curr = Rewriter::rewrite( curr ); - Trace("macros-rewrite") << "Rewrite " << assertions[i] << " to " << curr << std::endl; - PROOF( ProofManager::currentPM()->addDependence(curr, assertions[i]); ); - assertions[i] = curr; - retVal = true; + if( curr!=assertions[i] ){ + simp_assertions[i] = curr; + } + } + if( processAssertion( curr ) ){ + last_macro = i; + //process this assertion again + i--; } } - //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") << "...finished process, #new def = " << d_macro_defs_new.size() << std::endl; + if( doRewrite && !d_macro_defs_new.empty() ){ + bool retVal = false; + Trace("macros") << "Do simplifications..." << std::endl; + //now, rewrite based on macro definitions + for( unsigned i=0; i::iterator it = simp_assertions.find( i ); + if( it!=simp_assertions.end() ){ + curr = it->second; + } + //simplify again if before last macro + if( (int)iaddDependence(curr, assertions[i]); ); + assertions[i] = curr; + retVal = true; + } } - 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() ); + d_macro_defs_new.clear(); + if( retVal ){ + return true; + } + } + } + for( int i=0; i<(int)assertions.size(); i++ ){ + if( Trace.isOn("macros-warn") ){ + debugMacroDefinition( assertions[i], assertions[i] ); } } - return retVal; + return false; } -void QuantifierMacros::processAssertion( Node n ) { +bool QuantifierMacros::processAssertion( Node n ) { if( n.getKind()==AND ){ for( unsigned i=0; i args; for( size_t j=0; j& opc ){ if( n.getKind()==APPLY_UF ){ Node nop = n.getOperator(); if( nop==op || d_macro_defs.find( nop )!=d_macro_defs.end() ){ return true; } + if( std::find( opc.begin(), opc.end(), nop )==opc.end() ){ + opc.push_back( nop ); + } + }else if( d_ground_macros && n.getKind()==FORALL ){ + return true; } for( size_t i=0; i& candidat if( n.getNumChildren()==2 && n[0].isConst() ){ getMacroCandidates( n[1], candidates ); } + }else if( n.getKind()==NOT ){ + getMacroCandidates( n[0], candidates ); } } @@ -155,7 +192,9 @@ Node QuantifierMacros::solveInEquality( Node n, Node lit ){ //return the opposite side of the equality if defined that way for( int i=0; i<2; i++ ){ if( lit[i]==n ){ - return lit[ i==0 ? 1 : 0]; + return lit[i==0 ? 1 : 0]; + }else if( lit[i].getKind()==NOT && lit[i][0]==n ){ + return lit[i==0 ? 1 : 0].negate(); } } //must solve for term n in the literal lit @@ -235,9 +274,10 @@ bool QuantifierMacros::getSubstitution( std::vector< Node >& v_quant, std::map< return success; } -void QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Node f ){ +bool QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Node f ){ + Trace("macros-debug") << " process " << n << std::endl; if( n.getKind()==NOT ){ - process( n[0], !pol, args, f ); + return process( n[0], !pol, args, f ); }else if( n.getKind()==AND || n.getKind()==OR ){ //bool favorPol = (n.getKind()==AND)==pol; //conditional? @@ -246,10 +286,21 @@ void QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod }else if( n.getKind()==APPLY_UF ){ //predicate case if( isBoundVarApplyUf( n ) ){ - Node n_def = NodeManager::currentNM()->mkConst( pol ); - Trace("macros-quant") << "Macro found for " << f << std::endl; - Trace("macros") << "* " << n_def << " is a macro for " << n.getOperator() << std::endl; - d_macro_defs[ n.getOperator() ] = n_def; + Node op = n.getOperator(); + if( d_macro_defs.find( op )==d_macro_defs.end() ){ + Node n_def = NodeManager::currentNM()->mkConst( pol ); + for( unsigned i=0; imkSkolem( ss.str(), n[i].getType(), "created during macro definition recognition" ); + d_macro_basis[op].push_back( v ); + } + //contains no ops + std::vector< Node > op_contains; + //add the macro + addMacro( op, n_def, op_contains ); + return true; + } } }else{ //literal case @@ -266,8 +317,9 @@ void QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod getFreeVariables( m, args, fvs, false ); //get definition and condition Node n_def = solveInEquality( m, n ); //definition for the macro - //definition must exist and not contain any free variables apart from fvs - if( !n_def.isNull() && !getFreeVariables( n_def, args, fvs, true ) && !containsBadOp( n_def, op ) ){ + //definition must exist and not contain any free variables apart from fvs, opc is list of functions it contains + std::vector< Node > opc; + if( !n_def.isNull() && !getFreeVariables( n_def, args, fvs, true ) && !containsBadOp( n_def, op, opc ) ){ Node n_cond; //condition when this definition holds //conditional must not contain any free variables apart from fvs if( n_cond.isNull() || !getFreeVariables( n_cond, args, fvs, true ) ){ @@ -290,10 +342,8 @@ void QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod std::vector< Node > subs; if( getSubstitution( fvs, solved, vars, subs, true ) ){ n_def = n_def.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); - Trace("macros-quant") << "Macro found for " << f << std::endl; - Trace("macros") << "* " << n_def << " is a macro for " << op << std::endl; - d_macro_defs[op] = n_def; - return; + addMacro( op, n_def, opc ); + return true; } } } @@ -301,35 +351,123 @@ void QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod } } } + return false; } Node QuantifierMacros::simplify( Node n ){ - Trace("macros-debug") << "simplify " << n << std::endl; - std::vector< Node > children; - bool childChanged = false; - for( size_t i=0; i::iterator itn = d_simplify_cache.find( n ); + if( itn!=d_simplify_cache.end() ){ + return itn->second; + }else{ + Node ret = n; + Trace("macros-debug") << " simplify " << n << std::endl; + std::vector< Node > children; + bool childChanged = false; + for( size_t i=0; i::iterator it = d_macro_defs.find( op ); + if( it!=d_macro_defs.end() && !it->second.isNull() ){ + //do substitution if necessary + ret = it->second; + std::map< Node, std::vector< Node > >::iterator itb = d_macro_basis.find( op ); + if( itb!=d_macro_basis.end() ){ + ret = ret.substitute( itb->second.begin(), itb->second.end(), children.begin(), children.end() ); + } + retSet = true; + } + } + if( !retSet && childChanged ){ + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.insert( children.begin(), n.getOperator() ); + } + ret = NodeManager::currentNM()->mkNode( n.getKind(), children ); + } + d_simplify_cache[n] = ret; + return ret; + } } +} + +void QuantifierMacros::debugMacroDefinition( Node oo, Node n ) { + //for debugging, ensure that all previous definitions have been eliminated if( n.getKind()==APPLY_UF ){ Node op = n.getOperator(); - if( d_macro_defs.find( op )!=d_macro_defs.end() && !d_macro_defs[op].isNull() ){ - //do substitution if necessary - std::map< Node, std::vector< Node > >::iterator it = d_macro_basis.find( op ); - Node ret = d_macro_defs[op]; - if( it!=d_macro_basis.end() ){ - ret = ret.substitute( it->second.begin(), it->second.end(), children.begin(), children.end() ); + if( d_macro_defs.find( op )!=d_macro_defs.end() ){ + if( d_macro_defs.find( oo )!=d_macro_defs.end() ){ + Trace("macros-warn") << "BAD DEFINITION for macro " << oo << " : " << d_macro_defs[oo] << std::endl; + }else{ + Trace("macros-warn") << "BAD ASSERTION " << oo << std::endl; } - return ret; + Trace("macros-warn") << " contains defined function " << op << "!!!" << std::endl; } } - if( childChanged ){ - if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ - children.insert( children.begin(), n.getOperator() ); + for( unsigned i=0; i::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() ); + + if( Trace.isOn("macros-warn") ){ + debugMacroDefinition( it->first, sbody ); + } } - return NodeManager::currentNM()->mkNode( n.getKind(), children ); - }else{ - return n; + Trace("macros") << "done." << std::endl; } } + +void QuantifierMacros::addMacro( Node op, Node n, std::vector< Node >& opc ) { + Trace("macros") << "* " << n << " is a macro for " << op << ", #op contain = " << opc.size() << std::endl; + d_simplify_cache.clear(); + d_macro_defs[op] = n; + d_macro_defs_new[op] = n; + //substitute into all previous + std::vector< Node > dep_ops; + dep_ops.push_back( op ); + Trace("macros-debug") << "...substitute into " << d_macro_def_contains[op].size() << " previous definitions." << std::endl; + for( unsigned i=0; i& args, Node f ); + bool process( Node n, bool pol, std::vector< Node >& args, Node f ); bool contains( Node n, Node n_s ); - bool containsBadOp( Node n, Node op ); + bool containsBadOp( Node n, Node op, std::vector< Node >& opc ); bool isMacroLiteral( Node n, bool pol ); void getMacroCandidates( Node n, std::vector< Node >& candidates ); Node solveInEquality( Node n, Node lit ); @@ -45,13 +46,21 @@ private: std::map< Node, std::vector< Node > > d_macro_basis; //map from operators to macro definition std::map< Node, Node > d_macro_defs; + std::map< Node, Node > d_macro_defs_new; + //operators to macro ops that contain them + std::map< Node, std::vector< Node > > d_macro_def_contains; + //simplify cache + std::map< Node, Node > d_simplify_cache; private: Node simplify( Node n ); + void addMacro( Node op, Node n, std::vector< Node >& opc ); + void debugMacroDefinition( Node oo, Node n ); public: QuantifierMacros(){} ~QuantifierMacros(){} bool simplify( std::vector< Node >& assertions, bool doRewrite = false ); + void finalizeDefinitions(); }; } diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index af2d88e94..75e75637f 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -161,6 +161,13 @@ typedef enum { SYGUS_INV_TEMPL_MODE_POST, } SygusInvTemplMode; +typedef enum { + /** infer all definitions */ + MACROS_QUANT_MODE_ALL, + /** infer ground definitions */ + MACROS_QUANT_MODE_GROUND, +} MacrosQuantMode; + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 5cb9062e4..0edd3f1ea 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -40,7 +40,7 @@ option iteDtTesterSplitQuant --ite-dtt-split-quant bool :read-write :default fal # Whether to NNF quantifier bodies option nnfQuant --nnf-quant bool :default true apply NNF conversion to quantified formulas -option clauseSplit --clause-split bool :default false +option clauseSplit --clause-split bool :default true apply clause splitting to quantified formulas # Whether to pre-skolemize quantifier bodies. # For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to @@ -54,9 +54,6 @@ option preSkolemQuantAgg --pre-skolem-quant-agg bool :read-write :default true # Whether to perform agressive miniscoping option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false perform aggressive miniscoping for quantifiers -# Whether to perform quantifier macro expansion -option macrosQuant --macros-quant bool :default false - perform quantifiers macro expansions # Whether to CNF quantifier bodies option elimTautQuant --elim-taut-quant bool :default true eliminate tautological disjuncts of quantified formulas @@ -65,17 +62,14 @@ option elimTautQuant --elim-taut-quant bool :default true option eMatching --e-matching bool :read-write :default true whether to do heuristic E-matching - + option termDbMode --term-db-mode CVC4::theory::quantifiers::TermDbMode :default CVC4::theory::quantifiers::TERM_DB_ALL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToTermDbMode :handler-include "theory/quantifiers/options_handlers.h" which ground terms to consider for instantiation -# Whether to consider terms in the bodies of quantifiers for matching option registerQuantBodyTerms --register-quant-body-terms bool :default false consider ground terms within bodies of quantified formulas for matching -# Whether to use smart triggers option smartTriggers --smart-triggers bool :default true disable smart triggers -# Whether to use relevent triggers option relevantTriggers --relevant-triggers bool :default false prefer triggers that are more relevant based on SInE style analysis option relationalTriggers --relational-triggers bool :default false @@ -96,11 +90,12 @@ option triggerSelMode --trigger-sel CVC4::theory::quantifiers::TriggerSelMode :d selection mode for triggers option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_TRUST :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToUserPatMode :handler-include "theory/quantifiers/options_handlers.h" policy for handling user-provided patterns for quantifier instantiation +option incrementTriggers --increment-triggers bool :default true + generate additional triggers as needed during search option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h" when to apply instantiation - option instMaxLevel --inst-max-level=N int :read-write :default -1 maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default) option instLevelInputOnly --inst-level-input-only bool :default true @@ -108,8 +103,6 @@ option instLevelInputOnly --inst-level-input-only bool :default true option internalReps --quant-internal-reps bool :default true instantiate with representatives chosen by quantifiers engine -option incrementTriggers --increment-triggers bool :default true - generate additional triggers as needed during search option eagerInstQuant --eager-inst-quant bool :default false apply quantifier instantiation eagerly @@ -124,7 +117,6 @@ option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::Liter option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h" policy for instantiating axioms - ### finite model finding options option finiteModelFind finite-model-find --finite-model-find bool :default false :read-write @@ -252,6 +244,8 @@ option recurseCbqi --cbqi-recurse bool :default false turns on recursive counterexample-based quantifier instantiation option cbqiSat --cbqi-sat bool :read-write :default true answer sat when quantifiers are asserted with counterexample-based quantifier instantiation +option cbqiModel --cbqi-model bool :read-write :default true + guide instantiations by model values for counterexample-based quantifier instantiation ### local theory extensions options @@ -266,10 +260,19 @@ option lteRestrictInstClosure --lte-restrict-inst-closure bool :default false option quantAlphaEquiv --quant-alpha-equiv bool :default true infer alpha equivalence between quantified formulas +option macrosQuant --macros-quant bool :default false + perform quantifiers macro expansion +option macrosQuantMode --macros-quant-mode=MODE CVC4::theory::quantifiers::MacrosQuantMode :default CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMacrosQuantMode :handler-include "theory/quantifiers/options_handlers.h" + mode for quantifiers macro expansion ### recursive function options #option funDefs --fun-defs bool :default false # enable specialized techniques for recursive function definitions +### e-unification options + +option quantEqualityEngine --quant-ee bool :default false + maintain congrunce closure over universal equalities + endmodule diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index 4d2276621..699dd0296 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -230,6 +230,16 @@ post \n\ + Synthesize invariant based on strengthening of postcondition. \n\ \n\ "; +static const std::string macrosQuantHelp = "\ +Template modes for quantifiers macro expansion, supported by --macros-quant-mode:\n\ +\n\ +all \n\ ++ Infer definitions for functions, including those containing quantified formulas.\n\ +\n\ +ground (default) \n\ ++ Only infer ground definitions for functions.\n\ +\n\ +"; inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { if(optarg == "pre-full") { @@ -472,6 +482,20 @@ inline SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::stri } } +inline MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + if(optarg == "all" ) { + return MACROS_QUANT_MODE_ALL; + } else if(optarg == "ground") { + return MACROS_QUANT_MODE_GROUND; + } else if(optarg == "help") { + puts(macrosQuantHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --macros-quant-mode: `") + + optarg + "'. Try --macros-quant-mode help."); + } +} + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/quant_equality_engine.cpp b/src/theory/quantifiers/quant_equality_engine.cpp new file mode 100755 index 000000000..8e683f660 --- /dev/null +++ b/src/theory/quantifiers/quant_equality_engine.cpp @@ -0,0 +1,139 @@ +/********************* */ +/*! \file quant_equality_engine.cpp + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** Congruence closure with free variables + **/ + +#include + +#include "theory/quantifiers/quant_equality_engine.h" +#include "theory/rewriter.h" +#include "theory/quantifiers/term_database.h" + +using namespace CVC4; +using namespace std; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; +using namespace CVC4::kind; + +QuantEqualityEngine::QuantEqualityEngine( QuantifiersEngine * qe, context::Context* c ) : +QuantifiersModule( qe ), +d_notify( *this ), +d_uequalityEngine(d_notify, c, "theory::quantifiers::QuantEqualityEngine", true), +d_conflict(c, false), +d_quant_red(c), +d_quant_unproc(c){ + d_uequalityEngine.addFunctionKind( kind::APPLY_UF ); +} + +void QuantEqualityEngine::conflict(TNode t1, TNode t2) { + //report conflict through quantifiers engine output channel + std::vector assumptions; + d_uequalityEngine.explainEquality(t1, t2, true, assumptions, NULL); + Node conflict; + if( assumptions.size()==1 ){ + conflict = assumptions[0]; + }else{ + conflict = NodeManager::currentNM()->mkNode( AND, assumptions ); + } + d_conflict = true; + Trace("qee-conflict") << "Quantifier equality engine conflict : " << conflict << std::endl; + d_quantEngine->getOutputChannel().conflict( conflict ); +} + +void QuantEqualityEngine::eqNotifyNewClass(TNode t){ + +} +void QuantEqualityEngine::eqNotifyPreMerge(TNode t1, TNode t2){ + +} +void QuantEqualityEngine::eqNotifyPostMerge(TNode t1, TNode t2){ + +} +void QuantEqualityEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { + +} + +/* whether this module needs to check this round */ +bool QuantEqualityEngine::needsCheck( Theory::Effort e ) { + return e>=Theory::EFFORT_LAST_CALL; +} + +/* reset at a round */ +void QuantEqualityEngine::reset_round( Theory::Effort e ){ + //TODO +} + +/* Call during quantifier engine's check */ +void QuantEqualityEngine::check( Theory::Effort e, unsigned quant_e ) { + //TODO +} + +/* Called for new quantifiers */ +void QuantEqualityEngine::registerQuantifier( Node q ) { + //TODO +} + +/** called for everything that gets asserted */ +void QuantEqualityEngine::assertNode( Node n ) { + Assert( n.getKind()==FORALL ); + Trace("qee-debug") << "QEE assert : " << n << std::endl; + Node lit = n[1].getKind()==NOT ? n[1][0] : n[1]; + bool pol = n[1].getKind()!=NOT; + if( lit.getKind()==APPLY_UF || lit.getKind()==EQUAL ){ + lit = getTermDatabase()->getCanonicalTerm( lit ); + Trace("qee-debug") << "Canonical : " << lit << ", pol = " << pol << std::endl; + Node t1 = lit.getKind()==APPLY_UF ? lit : lit[0]; + Node t2; + if( lit.getKind()==APPLY_UF ){ + t2 = pol ? getTermDatabase()->d_true : getTermDatabase()->d_false; + pol = true; + }else{ + t2 = lit[1]; + } + bool alreadyHolds = false; + if( pol && areUnivEqual( t1, t2 ) ){ + alreadyHolds = true; + }else if( !pol && areUnivDisequal( t1, t2 ) ){ + alreadyHolds = true; + } + + if( alreadyHolds ){ + d_quant_red.push_back( n ); + Trace("qee-debug") << "...add to redundant" << std::endl; + }else{ + if( lit.getKind()==APPLY_UF ){ + d_uequalityEngine.assertPredicate(lit, pol, n); + }else{ + d_uequalityEngine.assertEquality(lit, pol, n); + } + } + }else{ + d_quant_unproc[n] = true; + Trace("qee-debug") << "...add to unprocessed (" << lit.getKind() << ")" << std::endl; + } +} + +bool QuantEqualityEngine::areUnivDisequal( TNode n1, TNode n2 ) { + return n1!=n2 && d_uequalityEngine.hasTerm( n1 ) && d_uequalityEngine.hasTerm( n2 ) && d_uequalityEngine.areDisequal( n1, n2, false ); +} + +bool QuantEqualityEngine::areUnivEqual( TNode n1, TNode n2 ) { + return n1==n2 || ( d_uequalityEngine.hasTerm( n1 ) && d_uequalityEngine.hasTerm( n2 ) && d_uequalityEngine.areEqual( n1, n2 ) ); +} + +TNode QuantEqualityEngine::getUnivRepresentative( TNode n ) { + if( d_uequalityEngine.hasTerm( n ) ){ + return d_uequalityEngine.getRepresentative( n ); + }else{ + return n; + } +} \ No newline at end of file diff --git a/src/theory/quantifiers/quant_equality_engine.h b/src/theory/quantifiers/quant_equality_engine.h new file mode 100755 index 000000000..0de6341cb --- /dev/null +++ b/src/theory/quantifiers/quant_equality_engine.h @@ -0,0 +1,92 @@ +/********************* */ +/*! \file quant_equality_engine.h + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Congruence closure with free variables + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__QUANTIFIERS_EQUALITY_ENGINE_H +#define __CVC4__QUANTIFIERS_EQUALITY_ENGINE_H + +#include +#include +#include +#include +#include "expr/node.h" +#include "expr/type_node.h" +#include "theory/quantifiers_engine.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class QuantEqualityEngine : public QuantifiersModule { + typedef context::CDHashMap NodeBoolMap; +private: + //notification class for equality engine + class NotifyClass : public eq::EqualityEngineNotify { + QuantEqualityEngine& d_qee; + public: + NotifyClass(QuantEqualityEngine& qee): d_qee(qee) {} + bool eqNotifyTriggerEquality(TNode equality, bool value) { return true; } + bool eqNotifyTriggerPredicate(TNode predicate, bool value) { return true; } + bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { return true; } + void eqNotifyConstantTermMerge(TNode t1, TNode t2) { d_qee.conflict(t1, t2); } + void eqNotifyNewClass(TNode t) { d_qee.eqNotifyNewClass(t); } + void eqNotifyPreMerge(TNode t1, TNode t2) { d_qee.eqNotifyPreMerge(t1, t2); } + void eqNotifyPostMerge(TNode t1, TNode t2) { d_qee.eqNotifyPostMerge(t1, t2); } + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {d_qee.eqNotifyDisequal(t1, t2, reason); } + };/* class ConjectureGenerator::NotifyClass */ + /** The notify class */ + NotifyClass d_notify; + /** (universal) equaltity engine */ + eq::EqualityEngine d_uequalityEngine; + /** Are we in conflict */ + context::CDO d_conflict; + /** list of redundant quantifiers in current context */ + context::CDList d_quant_red; + /** unprocessed quantifiers in current context */ + NodeBoolMap d_quant_unproc; +private: + void conflict(TNode t1, TNode t2); + void eqNotifyNewClass(TNode t); + void eqNotifyPreMerge(TNode t1, TNode t2); + void eqNotifyPostMerge(TNode t1, TNode t2); + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); +public: + QuantEqualityEngine( QuantifiersEngine * qe, context::Context* c ); + ~QuantEqualityEngine(){} + + /* whether this module needs to check this round */ + bool needsCheck( Theory::Effort e ); + /* reset at a round */ + void reset_round( Theory::Effort e ); + /* Call during quantifier engine's check */ + void check( Theory::Effort e, unsigned quant_e ); + /* Called for new quantifiers */ + void registerQuantifier( Node q ); + /** called for everything that gets asserted */ + void assertNode( Node n ); + /** Identify this module (for debugging, dynamic configuration, etc..) */ + std::string identify() const { return "QuantEqualityEngine"; } + /** queries */ + bool areUnivDisequal( TNode n1, TNode n2 ); + bool areUnivEqual( TNode n1, TNode n2 ); + TNode getUnivRepresentative( TNode n ); +}; + + +} +} +} + +#endif diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 6a95e243d..d6cbe386c 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -109,7 +109,7 @@ void QuantifiersRewriter::computeArgVec( std::vector< Node >& args, std::vector< std::map< Node, bool > activeMap; computeArgs( args, activeMap, n ); for( unsigned i=0; i& args, std::vector Assert( activeArgs.empty() ); std::map< Node, bool > activeMap; computeArgs( args, activeMap, n ); - computeArgs( args, activeMap, ipl ); - for( unsigned i=0; i& pcons, std::map< Node, std::map< int, Node > >& ncons, +void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj ){ if( n.getKind()==ITE && n[0].getKind()==APPLY_TESTER && n[1].getType().isBoolean() ){ Trace("quantifiers-rewrite-ite-debug") << "Split tester condition : " << n << std::endl; @@ -375,7 +378,7 @@ void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node std::vector< Node > children; children.push_back( n ); std::vector< Node > vars; - //add all positive testers + //add all positive testers for( std::map< Node, Node >::iterator it = pcons.begin(); it != pcons.end(); ++it ){ children.push_back( it->second.negate() ); vars.push_back( it->first ); @@ -797,7 +800,7 @@ Node QuantifiersRewriter::computeElimTaut( Node body ) { } return body; } - + Node QuantifiersRewriter::computeSplit( Node f, Node body, std::vector< Node >& vars ) { if( body.getKind()==OR ){ size_t var_found_count = 0; @@ -905,7 +908,7 @@ Node QuantifiersRewriter::computeSplit( Node f, Node body, std::vector< Node >& Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node ipl ){ std::vector< Node > activeArgs; - //if cegqi is on, may be synthesis conjecture, in which case we want to keep all variables + //if cegqi is on, may be synthesis conjecture, in which case we want to keep all variables if( options::ceGuidedInst() && !ipl.isNull() ){ for( unsigned i=0; i::iterator i = d_phase_reqs.begin(); i != d_phase_reqs.end(); ++i) { delete (*i).second; } @@ -378,7 +390,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ if( d_hasAddedLemma ){ break; //otherwise, complete the model generation if necessary - }else if( quant_e==QEFFORT_MODEL && needsModelE<=quant_e && options::produceModels() ){ + }else if( quant_e==QEFFORT_MODEL && needsModelE<=quant_e && options::produceModels() && e==Theory::EFFORT_LAST_CALL ){ Trace("quant-engine-debug") << "Build completed model..." << std::endl; d_builder->buildModel( d_model, true ); } @@ -441,10 +453,10 @@ bool QuantifiersEngine::reduceQuantifier( Node q ) { std::map< Node, bool >::iterator it = d_quants_red.find( q ); if( it==d_quants_red.end() ){ if( d_alpha_equiv ){ - Trace("quant-engine-debug") << "Alpha equivalence " << q << "?" << std::endl; + Trace("quant-engine-red") << "Alpha equivalence " << q << "?" << std::endl; //add equivalence with another quantified formula if( !d_alpha_equiv->registerQuantifier( q ) ){ - Trace("quant-engine-debug") << "...alpha equivalence success." << std::endl; + Trace("quant-engine-red") << "...alpha equivalence success." << std::endl; ++(d_statistics.d_red_alpha_equiv); d_quants_red[q] = true; return true; @@ -452,9 +464,9 @@ bool QuantifiersEngine::reduceQuantifier( Node q ) { } if( d_lte_part_inst && !q.getAttribute(LtePartialInstAttribute()) ){ //will partially instantiate - Trace("quant-engine-debug") << "LTE: Partially instantiate " << q << "?" << std::endl; + Trace("quant-engine-red") << "LTE: Partially instantiate " << q << "?" << std::endl; if( d_lte_part_inst->addQuantifier( q ) ){ - Trace("quant-engine-debug") << "...LTE partially instantiate success." << std::endl; + Trace("quant-engine-red") << "...LTE partially instantiate success." << std::endl; //delayed reduction : assert to model d_model->assertQuantifier( q, true ); ++(d_statistics.d_red_lte_partial_inst); @@ -795,7 +807,7 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache ){ //d_curr_out->lemma( lem, false, true ); d_lemmas_produced_c[ lem ] = true; d_lemmas_waiting.push_back( lem ); - Trace("inst-add-debug2") << "Added lemma : " << lem << std::endl; + Trace("inst-add-debug2") << "Added lemma" << std::endl; return true; }else{ Trace("inst-add-debug2") << "Duplicate." << std::endl; @@ -980,7 +992,9 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){ } void QuantifiersEngine::printInstantiations( std::ostream& out ) { + bool printed = false; for( std::map< Node, bool >::iterator it = d_skolemized.begin(); it != d_skolemized.end(); ++it ){ + printed = true; out << "Skolem constants of " << it->first << " : " << std::endl; out << " ( "; for( unsigned i=0; id_skolem_constants[it->first].size(); i++ ){ @@ -992,16 +1006,21 @@ void QuantifiersEngine::printInstantiations( std::ostream& out ) { } if( options::incrementalSolving() ){ for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){ + printed = true; out << "Instantiations of " << it->first << " : " << std::endl; it->second->print( out, it->first ); } }else{ for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){ + printed = true; out << "Instantiations of " << it->first << " : " << std::endl; it->second.print( out, it->first ); out << std::endl; } } + if( !printed ){ + out << "No instantiations." << std::endl; + } } void QuantifiersEngine::printSynthSolution( std::ostream& out ) { diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index c9a3a8027..101aa43cd 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -94,6 +94,7 @@ namespace quantifiers { class LtePartialInst; class AlphaEquivalence; class FunDefEngine; + class QuantEqualityEngine; }/* CVC4::theory::quantifiers */ namespace inst { @@ -145,6 +146,8 @@ private: quantifiers::LtePartialInst * d_lte_part_inst; /** function definitions engine */ quantifiers::FunDefEngine * d_fun_def_engine; + /** quantifiers equality engine */ + quantifiers::QuantEqualityEngine * d_uee; public: //effort levels enum { QEFFORT_CONFLICT, @@ -233,6 +236,8 @@ public: //modules quantifiers::LtePartialInst * getLtePartialInst() { return d_lte_part_inst; } /** function definition engine */ quantifiers::FunDefEngine * getFunDefEngine() { return d_fun_def_engine; } + /** quantifiers equality engine */ + quantifiers::QuantEqualityEngine * getQuantEqualityEngine() { return d_uee; } private: /** owner of quantified formulas */ std::map< Node, QuantifiersModule * > d_owner; diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 09ca6710d..eb004c184 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -49,7 +49,11 @@ TESTS = \ simp-len.smt2 \ is-even.smt2 \ is-even-pred.smt2 \ - delta-simp.smt2 + delta-simp.smt2 \ + nested-delta.smt2 \ + nested-inf.smt2 + + # regression can be solved with --finite-model-find --fmf-inst-engine # set3.smt2 diff --git a/test/regress/regress0/quantifiers/nested-delta.smt2 b/test/regress/regress0/quantifiers/nested-delta.smt2 new file mode 100644 index 000000000..9352f0410 --- /dev/null +++ b/test/regress/regress0/quantifiers/nested-delta.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --cbqi-recurse +; EXPECT: sat +(set-logic LRA) +(set-info :status sat) +(assert (forall ((x Real)) (or (exists ((y Real)) (and (< y 0) (< y x))) (<= x 0)))) +(check-sat) \ No newline at end of file diff --git a/test/regress/regress0/quantifiers/nested-inf.smt2 b/test/regress/regress0/quantifiers/nested-inf.smt2 new file mode 100644 index 000000000..f27a876db --- /dev/null +++ b/test/regress/regress0/quantifiers/nested-inf.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --cbqi-recurse +; EXPECT: sat +(set-logic LRA) +(set-info :status sat) +(assert (forall ((x Real)) (exists ((y Real)) (> y x)))) +(check-sat) \ No newline at end of file -- 2.30.2