From 96a0bc3b022b67b5ab79bf2ab087573c65a8d248 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 9 Oct 2017 21:56:40 -0500 Subject: [PATCH] Split term database (#1206) * Move equality query to own file, move equality inference to quantifiers engine. * Move quantifiers attributes out of TermDb and into QuantAttribute. * Move term database sygus to quantifiers engine, move some attributes to quantifiers attributes header. * Split term database into term util. * Partial fix for #1205 that eliminates need for dependency in node.cpp. * Add more references to github issues. --- src/Makefile.am | 4 + src/expr/node.cpp | 12 - src/parser/smt2/Smt2.g | 4 +- src/parser/smt2/smt2.cpp | 1 + src/printer/smt2/smt2_printer.cpp | 2 +- src/smt/smt_engine.cpp | 3 +- src/theory/datatypes/datatypes_sygus.cpp | 7 +- src/theory/quantifiers/alpha_equivalence.cpp | 10 +- src/theory/quantifiers/anti_skolem.cpp | 8 +- src/theory/quantifiers/bounded_integers.cpp | 8 +- src/theory/quantifiers/bv_inverter.cpp | 4 +- .../quantifiers/candidate_generator.cpp | 7 +- .../quantifiers/ce_guided_conjecture.cpp | 18 +- .../quantifiers/ce_guided_instantiation.cpp | 8 +- src/theory/quantifiers/ce_guided_pbe.cpp | 3 +- .../quantifiers/ce_guided_single_inv.cpp | 51 +- .../quantifiers/ce_guided_single_inv_sol.cpp | 23 +- src/theory/quantifiers/ceg_instantiator.cpp | 9 +- src/theory/quantifiers/ceg_t_instantiator.cpp | 33 +- .../quantifiers/conjecture_generator.cpp | 35 +- src/theory/quantifiers/equality_query.cpp | 336 ++++ src/theory/quantifiers/equality_query.h | 76 + src/theory/quantifiers/first_order_model.cpp | 5 +- src/theory/quantifiers/full_model_check.cpp | 3 +- src/theory/quantifiers/fun_def_process.cpp | 8 +- .../quantifiers/inst_match_generator.cpp | 29 +- src/theory/quantifiers/inst_strategy_cbqi.cpp | 54 +- .../quantifiers/inst_strategy_e_matching.cpp | 18 +- .../quantifiers/instantiation_engine.cpp | 3 +- src/theory/quantifiers/local_theory_ext.cpp | 1 + src/theory/quantifiers/macros.cpp | 5 +- src/theory/quantifiers/model_builder.cpp | 15 +- src/theory/quantifiers/model_engine.cpp | 3 +- .../quantifiers/quant_conflict_find.cpp | 11 +- .../quantifiers/quant_equality_engine.cpp | 6 +- src/theory/quantifiers/quant_util.cpp | 13 +- src/theory/quantifiers/quant_util.h | 2 + .../quantifiers/quantifiers_attributes.cpp | 308 +++- .../quantifiers/quantifiers_attributes.h | 130 +- .../quantifiers/quantifiers_rewriter.cpp | 18 +- src/theory/quantifiers/relevant_domain.cpp | 15 +- src/theory/quantifiers/rewrite_engine.cpp | 12 +- src/theory/quantifiers/sygus_grammar_cons.cpp | 3 +- src/theory/quantifiers/term_database.cpp | 1475 +---------------- src/theory/quantifiers/term_database.h | 409 +---- .../quantifiers/term_database_sygus.cpp | 13 +- src/theory/quantifiers/term_util.cpp | 1189 +++++++++++++ src/theory/quantifiers/term_util.h | 346 ++++ src/theory/quantifiers/theory_quantifiers.cpp | 9 +- src/theory/quantifiers/trigger.cpp | 43 +- src/theory/quantifiers_engine.cpp | 408 +---- src/theory/quantifiers_engine.h | 76 +- src/theory/rep_set.cpp | 8 +- src/theory/sep/theory_sep.cpp | 7 +- src/theory/uf/theory_uf_model.cpp | 2 +- src/theory/uf/theory_uf_rewriter.h | 2 +- 56 files changed, 2790 insertions(+), 2521 deletions(-) create mode 100644 src/theory/quantifiers/equality_query.cpp create mode 100644 src/theory/quantifiers/equality_query.h create mode 100644 src/theory/quantifiers/term_util.cpp create mode 100644 src/theory/quantifiers/term_util.h diff --git a/src/Makefile.am b/src/Makefile.am index cfb8e379d..9412e3433 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -368,6 +368,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/ceg_t_instantiator.h \ theory/quantifiers/conjecture_generator.cpp \ theory/quantifiers/conjecture_generator.h \ + theory/quantifiers/equality_query.cpp \ + theory/quantifiers/equality_query.h \ theory/quantifiers/equality_infer.cpp \ theory/quantifiers/equality_infer.h \ theory/quantifiers/first_order_model.cpp \ @@ -422,6 +424,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/term_database.h \ theory/quantifiers/term_database_sygus.cpp \ theory/quantifiers/term_database_sygus.h \ + theory/quantifiers/term_util.cpp \ + theory/quantifiers/term_util.h \ theory/quantifiers/theory_quantifiers.cpp \ theory/quantifiers/theory_quantifiers.h \ theory/quantifiers/theory_quantifiers_type_rules.h \ diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 0c844f92d..75e37151a 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -22,9 +22,6 @@ #include "base/output.h" #include "expr/attribute.h" -#include "theory/quantifiers/term_database.h" - - using namespace std; namespace CVC4 { @@ -113,15 +110,6 @@ bool NodeTemplate::hasBoundVar() { for(iterator i = begin(); i != end() && !hasBv; ++i) { hasBv = (*i).hasBoundVar(); } - if( !hasBv ){ - //FIXME : this is a hack to handle synthesis conjectures - // the issue is that we represent second-order quantification in synthesis conjectures via a Node: - // exists x forall y P[f,y], where x is a dummy variable that maps to f through attribute SygusSynthFunVarListAttributeId - // when asked whether a node has a bound variable, we want to treat f as if it were a bound (second-order) variable. -AJR - if( getKind()==kind::APPLY_UF && getOperator().hasAttribute(theory::SygusSynthFunVarListAttribute()) ){ - hasBv = true; - } - } } setAttribute(HasBoundVarAttr(), hasBv); setAttribute(HasBoundVarComputedAttr(), true); diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 29f507238..1b3d7b23f 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -624,8 +624,8 @@ sygusCommand [std::unique_ptr* cmd] }else{ synth_fun_type = range; } - // allow overloading for synth fun - synth_fun = PARSER_STATE->mkVar(fun, synth_fun_type, ExprManager::VAR_FLAG_NONE, true); + // we do not allow overloading for synth fun + synth_fun = PARSER_STATE->mkBoundVar(fun, synth_fun_type); // we add a declare function command here // this is the single unmuted command in the sequence generated by this smt2 command seq->addCommand(new DeclareFunctionCommand(fun, synth_fun, synth_fun_type)); diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index acfd886ce..a6830d95d 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1090,6 +1090,7 @@ const void Smt2::getSygusPrimedVars( std::vector& vars, bool isPrimed ) { } const void Smt2::addSygusFunSymbol( Type t, Expr synth_fun ){ + //FIXME #1205 : we should not create a proxy, instead quantify on synth_fun and set Type t as an attribute Expr sym = mkBoundVar("sfproxy", t); d_sygusFunSymbols.push_back(sym); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index c7d6b34ab..147fefa04 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -29,7 +29,7 @@ #include "smt_util/boolean_simplification.h" #include "smt_util/node_visitor.h" #include "theory/arrays/theory_arrays_rewriter.h" -#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/quantifiers_attributes.h" #include "theory/substitutions.h" #include "theory/theory_model.h" #include "util/smt2_quote_string.h" diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index db7c65291..bc335f2df 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -90,7 +90,7 @@ #include "theory/quantifiers/fun_def_process.h" #include "theory/quantifiers/macros.h" #include "theory/quantifiers/quantifiers_rewriter.h" -#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/sort_inference.h" #include "theory/strings/theory_strings.h" #include "theory/substitutions.h" @@ -4512,6 +4512,7 @@ Result SmtEngine::checkSynth(const Expr& e) throw(Exception) { quantifiers::SingleInvocationPartition sip; std::vector< Node > funcs; for( unsigned i=0; i deq_child[2]; if( children.size()==2 && children[0].getType()==tn ){ bool argDeq = false; - if( quantifiers::TermDb::isNonAdditive( nk ) ){ + if( quantifiers::TermUtil::isNonAdditive( nk ) ){ argDeq = true; }else{ //other cases of rewriting x k x -> x' @@ -617,7 +618,7 @@ Node SygusSymBreakNew::getSimpleSymBreakPred( TypeNode tn, int tindex, unsigned }else if( depth==2 ){ if( nk!=UNDEFINED_KIND ){ // commutative operators - if( quantifiers::TermDb::isComm( nk ) ){ + if( quantifiers::TermUtil::isComm( nk ) ){ if( children.size()==2 ){ if( children[0].getType()==children[1].getType() ){ //chainable diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index 6af5bd92f..ff32bbcb7 100644 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -14,7 +14,7 @@ **/ #include "theory/quantifiers/alpha_equivalence.h" -#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" using namespace CVC4; using namespace std; @@ -23,9 +23,9 @@ using namespace CVC4::theory::quantifiers; using namespace CVC4::kind; struct sortTypeOrder { - TermDb* d_tdb; + TermUtil* d_tu; bool operator() (TypeNode i, TypeNode j) { - return d_tdb->getIdForType( i )getIdForType( j ); + return d_tu->getIdForType( i )getIdForType( j ); } }; @@ -100,7 +100,7 @@ Node AlphaEquivalence::reduceQuantifier( Node q ) { Assert( q.getKind()==FORALL ); Trace("aeq") << "Alpha equivalence : register " << q << std::endl; //construct canonical quantified formula - Node t = d_qe->getTermDatabase()->getCanonicalTerm( q[1], true ); + Node t = d_qe->getTermUtil()->getCanonicalTerm( q[1], true ); Trace("aeq") << " canonical form: " << t << std::endl; //compute variable type counts std::map< TypeNode, int > typ_count; @@ -113,7 +113,7 @@ Node AlphaEquivalence::reduceQuantifier( Node q ) { } } sortTypeOrder sto; - sto.d_tdb = d_qe->getTermDatabase(); + sto.d_tu = d_qe->getTermUtil(); std::sort( typs.begin(), typs.end(), sto ); Trace("aeq-debug") << " "; Node ret = AlphaEquivalenceTypeNode::registerNode( &d_ae_typ_trie, d_qe, q, t, typs, typ_count ); diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp index e63dc6abb..e9c646f07 100644 --- a/src/theory/quantifiers/anti_skolem.cpp +++ b/src/theory/quantifiers/anti_skolem.cpp @@ -17,7 +17,7 @@ #include "options/quantifiers_options.h" #include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" using namespace std; @@ -29,9 +29,9 @@ namespace theory { namespace quantifiers { struct sortTypeOrder { - TermDb* d_tdb; + TermUtil* d_tu; bool operator() (TypeNode i, TypeNode j) { - return d_tdb->getIdForType( i )getIdForType( j ); + return d_tu->getIdForType( i )getIdForType( j ); } }; @@ -120,7 +120,7 @@ void QuantAntiSkolem::check( Theory::Effort e, unsigned quant_e ) { indices[d_ask_types[q][j]].push_back( j ); } sortTypeOrder sto; - sto.d_tdb = d_quantEngine->getTermDatabase(); + sto.d_tu = d_quantEngine->getTermUtil(); std::sort( d_ask_types[q].begin(), d_ask_types[q].end(), sto ); //increment j on inner loop for( unsigned j=0; jmayComplete( tn ) ){ + if( tn.isSort() || getTermUtil()->mayComplete( tn ) ){ success = true; setBoundedVar( f, f[0][i], BOUND_FINITE ); break; @@ -808,7 +808,7 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node Node tu = u; getBounds( q, v, rsi, tl, tu ); Assert( !tl.isNull() && !tu.isNull() ); - if( ra==d_quantEngine->getTermDatabase()->d_true ){ + if( ra==d_quantEngine->getTermUtil()->d_true ){ long rr = range.getConst().getNumerator().getLong()+1; Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl; for( unsigned k=0; k #include -#include "theory/quantifiers/term_database.h" +#include "theory/rewriter.h" +#include "theory/quantifiers/term_util.h" #include "theory/bv/theory_bv_utils.h" + using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::theory; diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 01e71be95..0a66109a0 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -16,6 +16,7 @@ #include "theory/quantifiers/candidate_generator.h" #include "theory/quantifiers/inst_match.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" #include "theory/uf/theory_uf.h" @@ -28,7 +29,7 @@ using namespace CVC4::theory; using namespace CVC4::theory::inst; bool CandidateGenerator::isLegalCandidate( Node n ){ - return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(n) ); + return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cbqi() || !quantifiers::TermUtil::hasInstConstAttr(n) ); } void CandidateGeneratorQueue::addCandidate( Node n ) { @@ -189,7 +190,7 @@ CandidateGeneratorQELitEq::CandidateGeneratorQELitEq( QuantifiersEngine* qe, Nod CandidateGenerator( qe ), d_match_pattern( mpat ){ Assert( mpat.getKind()==EQUAL ); for( unsigned i=0; i<2; i++ ){ - if( !quantifiers::TermDb::hasInstConstAttr(mpat[i]) ){ + if( !quantifiers::TermUtil::hasInstConstAttr(mpat[i]) ){ d_match_gterm = mpat[i]; } } @@ -262,7 +263,7 @@ CandidateGeneratorQEAll::CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mp CandidateGenerator( qe ), d_match_pattern( mpat ){ d_match_pattern_type = mpat.getType(); Assert( mpat.getKind()==INST_CONSTANT ); - d_f = quantifiers::TermDb::getInstConstAttr( mpat ); + d_f = quantifiers::TermUtil::getInstConstAttr( mpat ); d_index = mpat.getAttribute(InstVarNumAttribute()); d_firstTime = false; } diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp index 0fe246964..745c64b35 100644 --- a/src/theory/quantifiers/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/ce_guided_conjecture.cpp @@ -19,7 +19,9 @@ #include "prop/prop_engine.h" #include "smt/smt_statistics_registry.h" #include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database_sygus.h" +#include "theory/quantifiers/term_util.h" #include "theory/theory_engine.h" using namespace CVC4::kind; @@ -64,7 +66,7 @@ void CegConjecture::assign( Node q ) { std::map< Node, Node > templates; std::map< Node, Node > templates_arg; //register with single invocation if applicable - if( d_qe->getTermDatabase()->isQAttrSygus( d_quant ) ){ + if( d_qe->getQuantAttributes()->isSygus( d_quant ) ){ d_ceg_si->initialize( d_quant ); q = d_ceg_si->getSimplifiedConjecture(); // carry the templates @@ -84,7 +86,7 @@ void CegConjecture::assign( Node q ) { Trace("cegqi") << "CegConjecture : converted to embedding : " << d_embed_quant << std::endl; // we now finalize the single invocation module, based on the syntax restrictions - if( d_qe->getTermDatabase()->isQAttrSygus( d_quant ) ){ + if( d_qe->getQuantAttributes()->isSygus( d_quant ) ){ d_ceg_si->finishInit( d_ceg_gc->isSyntaxRestricted(), d_ceg_gc->hasSyntaxITE() ); } @@ -122,7 +124,7 @@ void CegConjecture::assign( Node q ) { } Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl; - if( d_qe->getTermDatabase()->isQAttrSygus( d_quant ) ){ + if( d_qe->getQuantAttributes()->isSygus( d_quant ) ){ collectDisjuncts( d_base_inst, d_base_disj ); Trace("cegqi") << "Conjecture has " << d_base_disj.size() << " disjuncts." << std::endl; //store the inner variables for each disjunct @@ -138,7 +140,7 @@ void CegConjecture::assign( Node q ) { } } d_syntax_guided = true; - }else if( d_qe->getTermDatabase()->isQAttrSynthesis( d_quant ) ){ + }else if( d_qe->getQuantAttributes()->isSynthesis( d_quant ) ){ d_syntax_guided = false; }else{ Assert( false ); @@ -292,7 +294,7 @@ void CegConjecture::doCheck(std::vector< Node >& lems, std::vector< Node >& mode Node dr = Rewriter::rewrite( d[i] ); if( dr.getKind()==NOT && dr[0].getKind()==FORALL ){ if( constructed_cand ){ - ic.push_back( d_qe->getTermDatabase()->getSkolemizedBody( dr[0] ).negate() ); + ic.push_back( d_qe->getTermUtil()->getSkolemizedBody( dr[0] ).negate() ); } if( sk_refine ){ Assert( !isGround() ); @@ -343,9 +345,9 @@ void CegConjecture::doRefine( std::vector< Node >& lems ){ Node ce_q = d_ce_sk[0][k]; if( !ce_q.isNull() ){ Assert( !d_inner_vars_disj[k].empty() ); - Assert( d_inner_vars_disj[k].size()==d_qe->getTermDatabase()->d_skolem_constants[ce_q].size() ); + Assert( d_inner_vars_disj[k].size()==d_qe->getTermUtil()->d_skolem_constants[ce_q].size() ); std::vector< Node > model_values; - getModelValues( d_qe->getTermDatabase()->d_skolem_constants[ce_q], model_values ); + getModelValues( d_qe->getTermUtil()->d_skolem_constants[ce_q], model_values ); sk_vars.insert( sk_vars.end(), d_inner_vars_disj[k].begin(), d_inner_vars_disj[k].end() ); sk_subs.insert( sk_subs.end(), model_values.begin(), model_values.end() ); }else{ @@ -577,7 +579,7 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation if( !options::sygusTemplEmbedGrammar() ){ TNode templa = d_ceg_si->getTemplateArg( sf ); // make the builtin version of the full solution - TermDbSygus* sygusDb = d_qe->getTermDatabase()->getTermDatabaseSygus(); + TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus(); sol = sygusDb->sygusToBuiltin( sol, sol.getType() ); Trace("cegqi-inv") << "Builtin version of solution is : " << sol << ", type : " << sol.getType() diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 2ad55bb07..a2a6e2bbe 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -18,7 +18,9 @@ #include "options/quantifiers_options.h" #include "smt/smt_statistics_registry.h" #include "theory/theory_engine.h" +#include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database_sygus.h" +#include "theory/quantifiers/term_util.h" //FIXME : remove this include (github issue #1156) #include "theory/bv/theory_bv_rewriter.h" @@ -253,7 +255,7 @@ void CegInstantiation::getCRefEvaluationLemmas( CegConjecture * conj, std::vecto lem_conj.push_back( lem ); } EvalSygusInvarianceTest vsit; - vsit.d_result = d_quantEngine->getTermDatabase()->d_false; + vsit.d_result = d_quantEngine->getTermUtil()->d_false; for( unsigned j=0; jgetTermDatabaseSygus()->evaluateWithUnfolding( lemcs, vsit.d_visited ); Trace("sygus-cref-eval2") << "...after unfolding is : " << lemcsu << std::endl; - if( lemcsu==d_quantEngine->getTermDatabase()->d_false ){ + if( lemcsu==d_quantEngine->getTermUtil()->d_false ){ std::vector< Node > msu; std::vector< Node > mexp; msu.insert( msu.end(), ms.begin(), ms.end() ); @@ -308,7 +310,7 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { void CegInstantiation::preregisterAssertion( Node n ) { //check if it sygus conjecture - if( TermDb::isSygusConjecture( n ) ){ + if( QuantAttributes::checkSygusConjecture( n ) ){ //this is a sygus conjecture Trace("cegqi") << "Preregister sygus conjecture : " << n << std::endl; d_conj->preregisterConjecture( n ); diff --git a/src/theory/quantifiers/ce_guided_pbe.cpp b/src/theory/quantifiers/ce_guided_pbe.cpp index 501e839db..9fa87c11d 100644 --- a/src/theory/quantifiers/ce_guided_pbe.cpp +++ b/src/theory/quantifiers/ce_guided_pbe.cpp @@ -17,6 +17,7 @@ #include "expr/datatype.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/term_database_sygus.h" +#include "theory/quantifiers/term_util.h" #include "theory/datatypes/datatypes_rewriter.h" using namespace CVC4; @@ -605,7 +606,7 @@ void CegConjecturePbe::staticLearnRedundantOps( Node c, Node e, std::map< Node, const Datatype& cdt = ((DatatypeType)ctn.toType()).getDatatype(); for( unsigned j=0; jgetConsNumKind( ctn, j ); - if( ck!=UNDEFINED_KIND && TermDb::isBoolConnective( ck ) ){ + if( ck!=UNDEFINED_KIND && TermUtil::isBoolConnective( ck ) ){ bool typeCorrect = true; for( unsigned k=0; kgetArgType( cdt[j], k )!=ctn ){ diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index edd9c4fa3..bf09c83f7 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -21,6 +21,7 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/term_database_sygus.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers/trigger.h" #include "theory/theory_engine.h" @@ -100,7 +101,7 @@ void CegConjectureSingleInv::getInitialSingleInvLemma( std::vector< Node >& lems }else{ inst = d_single_inv; } - inst = TermDb::simpleNegate( inst ); + inst = TermUtil::simpleNegate( inst ); Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl; //register with the instantiator @@ -139,7 +140,7 @@ void CegConjectureSingleInv::initialize( Node q ) { if( q[1].getKind()==NOT && q[1][0].getKind()==FORALL ){ qq = q[1][0][1]; }else{ - qq = TermDb::simpleNegate( q[1] ); + qq = TermUtil::simpleNegate( q[1] ); } //process the single invocation-ness of the property if( !d_sip->init( progs, qq ) ){ @@ -282,7 +283,7 @@ void CegConjectureSingleInv::finishInit( bool syntaxRestricted, bool hasItes ) { // we now have determined whether we will do single invocation techniques if( d_single_invocation ){ d_single_inv = d_sip->getSingleInvocation(); - d_single_inv = TermDb::simpleNegate( d_single_inv ); + d_single_inv = TermUtil::simpleNegate( d_single_inv ); if( !d_sip->d_func_vars.empty() ){ Node pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, d_sip->d_func_vars ); d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, d_single_inv ); @@ -349,9 +350,9 @@ bool CegConjectureSingleInv::doAddInstantiation( std::vector< Node >& subs ){ Trace("cegqi-engine") << siss.str() << std::endl; Assert( d_single_inv_var.size()==subs.size() ); lem = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), subs.begin(), subs.end() ); - if( d_qe->getTermDatabase()->containsVtsTerm( lem ) ){ + if( d_qe->getTermUtil()->containsVtsTerm( lem ) ){ Trace("cegqi-engine-debug") << "Rewrite based on vts symbols..." << std::endl; - lem = d_qe->getTermDatabase()->rewriteVtsSymbols( lem ); + lem = d_qe->getTermUtil()->rewriteVtsSymbols( lem ); } } } @@ -407,7 +408,7 @@ Node CegConjectureSingleInv::constructSolution( std::vector< unsigned >& indices if( itw!=weak_imp.end() ){ cond = itw->second; } - cond = TermDb::simpleNegate( cond ); + cond = TermUtil::simpleNegate( cond ); Node ite1 = d_inst[uindex][i]; Node ite2 = constructSolution( indices, i, index+1, weak_imp ); return NodeManager::currentNM()->mkNode( ITE, cond, ite1, ite2 ); @@ -473,7 +474,7 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& Node s; if( d_prog_to_sol_index.find( prog )==d_prog_to_sol_index.end() ){ Trace("csi-sol") << "Get solution for (unconstrained) " << prog << std::endl; - s = d_qe->getTermDatabase()->getEnumerateTerm( TypeNode::fromType( dt.getSygusType() ), 0 ); + s = d_qe->getTermUtil()->getEnumerateTerm( TypeNode::fromType( dt.getSygusType() ), 0 ); }else{ Trace("csi-sol") << "Get solution for " << prog << ", with skolems : "; sol_index = d_prog_to_sol_index[prog]; @@ -704,7 +705,7 @@ void SingleInvocationPartition::process( Node n ) { std::vector< Node > si_subs; Trace("si-prt") << "Process conjunct : " << conj[i] << std::endl; //do DER on conjunct - Node cr = TermDb::getQuantSimplify( conj[i] ); + Node cr = TermUtil::getQuantSimplify( conj[i] ); if( cr!=conj[i] ){ Trace("si-prt-debug") << "...rewritten to " << cr << std::endl; } @@ -751,11 +752,23 @@ void SingleInvocationPartition::process( Node n ) { Trace("si-prt-debug") << "...normalized invocations to " << cr << std::endl; //now must check if it has other bound variables std::vector< Node > bvs; - TermDb::getBoundVars( cr, bvs ); + TermUtil::getBoundVars( cr, bvs ); if( bvs.size()>d_si_vars.size() ){ - Trace("si-prt") << "...not ground single invocation." << std::endl; - ngroundSingleInvocation = true; - singleInvocation = false; + // getBoundVars also collects functions in the rare case that we are synthesizing a function with 0 arguments + // take these into account below. + unsigned n_const_synth_fun = 0; + for( unsigned j=0; jd_si_vars.size() ){ + Trace("si-prt") << "...not ground single invocation." << std::endl; + ngroundSingleInvocation = true; + singleInvocation = false; + }else{ + Trace("si-prt") << "...ground single invocation : success, after removing 0-arg synth functions." << std::endl; + } }else{ Trace("si-prt") << "...ground single invocation : success." << std::endl; } @@ -764,7 +777,7 @@ void SingleInvocationPartition::process( Node n ) { singleInvocation = false; //rename bound variables with maximal overlap with si_vars std::vector< Node > bvs; - TermDb::getBoundVars( cr, bvs ); + TermUtil::getBoundVars( cr, bvs ); std::vector< Node > terms; std::vector< Node > subs; for( unsigned j=0; j& return true; }else{ bool ret = true; - //if( TermDb::hasBoundVarAttr( n ) ){ + //if( TermUtil::hasBoundVarAttr( n ) ){ for( unsigned i=0; i& vars, st Node s; for( unsigned r=0; r<2; r++ ){ if( std::find( vars.begin(), vars.end(), slit[r] )!=vars.end() ){ - if( !TermDb::containsTerm( slit[1-r], slit[r] ) ){ + if( !TermUtil::containsTerm( slit[1-r], slit[r] ) ){ v = slit[r]; s = slit[1-r]; break; @@ -1122,7 +1135,7 @@ void TransitionInference::getConstantSubstitution( std::vector< Node >& vars, st Node veq_c; Node val; int ires = QuantArith::isolate( itm->first, msum, veq_c, val, EQUAL ); - if( ires!=0 && veq_c.isNull() && !TermDb::containsTerm( val, itm->first ) ){ + if( ires!=0 && veq_c.isNull() && !TermUtil::containsTerm( val, itm->first ) ){ v = itm->first; s = val; } @@ -1258,7 +1271,7 @@ void TransitionInference::process( Node n ) { } if( i==0 || i==1 ){ // pre-condition and transition are negated - ret = TermDb::simpleNegate( ret ); + ret = TermUtil::simpleNegate( ret ); } d_com[i].d_this = ret; } diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp index 1eafe1a93..9e69a31d3 100644 --- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp @@ -21,6 +21,7 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/term_database_sygus.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers/trigger.h" #include "theory/theory_engine.h" @@ -87,7 +88,7 @@ Node CegConjectureSingleInvSol::pullITEs( Node s ) { rem = pullITEs( rem ); Trace("csi-pull-ite") << "PI: Rewrite : " << s << std::endl; Node prev = s; - s = NodeManager::currentNM()->mkNode( ITE, TermDb::simpleNegate( cond ), t, rem ); + s = NodeManager::currentNM()->mkNode( ITE, TermUtil::simpleNegate( cond ), t, rem ); Trace("csi-pull-ite") << "PI: Rewrite Now : " << s << std::endl; Trace("csi-pull-ite") << "(= " << prev << " " << s << ")" << std::endl; success = true; @@ -109,7 +110,7 @@ bool CegConjectureSingleInvSol::pullITECondition( Node root, Node n_ite, std::ve Node cond = n_ite[0][i]; orig_conj.push_back( cond ); if( n_ite[0].getKind()==OR ){ - cond = TermDb::simpleNegate( cond ); + cond = TermUtil::simpleNegate( cond ); } curr_conj.push_back( cond ); } @@ -258,7 +259,7 @@ bool CegConjectureSingleInvSol::getAssign( bool pol, Node n, std::map< Node, boo Trace("csi-simp-debug") << "---already assigned, lookup " << pol << " " << ita->second << std::endl; return pol==ita->second; }else if( n.isConst() ){ - return pol==(n==d_qe->getTermDatabase()->d_true); + return pol==(n==d_qe->getTermUtil()->d_true); }else{ Trace("csi-simp-debug") << "---assign " << n << " " << pol << std::endl; assign[n] = pol; @@ -286,7 +287,7 @@ bool CegConjectureSingleInvSol::getAssignEquality( Node eq, std::vector< Node >& Assert( std::find( vars.begin(), vars.end(), eq[r] )==vars.end() ); if( std::find( new_vars.begin(), new_vars.end(), eq[r] )==new_vars.end() ){ Node eqro = eq[r==0 ? 1 : 0 ]; - if( !d_qe->getTermDatabase()->containsTerm( eqro, eq[r] ) ){ + if( !d_qe->getTermUtil()->containsTerm( eqro, eq[r] ) ){ Trace("csi-simp-debug") << "---equality " << eq[r] << " = " << eqro << std::endl; new_vars.push_back( eq[r] ); new_subs.push_back( eqro ); @@ -468,7 +469,7 @@ Node CegConjectureSingleInvSol::simplifySolutionNode( Node sol, TypeNode stn, st std::vector< Node > children; std::vector< Node > new_vars; std::vector< Node > new_subs; - Node bc = sol.getKind()==OR ? d_qe->getTermDatabase()->d_true : d_qe->getTermDatabase()->d_false; + Node bc = sol.getKind()==OR ? d_qe->getTermUtil()->d_true : d_qe->getTermUtil()->d_false; for( unsigned i=0; ii || std::find( final_children.begin(), final_children.end(), children[j] )!=final_children.end() ) ){ Node sj = children[j].substitute( tmp_vars.begin(), tmp_vars.end(), tmp_subs.begin(), tmp_subs.end() ); sj = Rewriter::rewrite( sj ); - if( sj==( sol.getKind()==AND ? d_qe->getTermDatabase()->d_false : d_qe->getTermDatabase()->d_true ) ){ + if( sj==( sol.getKind()==AND ? d_qe->getTermUtil()->d_false : d_qe->getTermUtil()->d_true ) ){ Trace("csi-simp") << "--- " << children[i].negate() << " is implied by " << children[j].negate() << std::endl; red = true; break; @@ -675,7 +676,7 @@ Node CegConjectureSingleInvSol::reconstructSolution( Node sol, TypeNode stn, int std::vector< TypeNode > to_erase; for( std::map< TypeNode, bool >::iterator it = active.begin(); it != active.end(); ++it ){ TypeNode stn = it->first; - Node ns = d_qe->getTermDatabase()->getEnumerateTerm( stn, index ); + Node ns = d_qe->getTermUtil()->getEnumerateTerm( stn, index ); if( ns.isNull() ){ to_erase.push_back( stn ); }else{ @@ -754,7 +755,7 @@ int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, in if( karg!=-1 ){ //collect the children of min_t std::vector< Node > tchildren; - if( min_t.getNumChildren()>dt[karg].getNumArgs() && quantifiers::TermDb::isAssoc( min_t.getKind() ) && dt[karg].getNumArgs()==2 ){ + if( min_t.getNumChildren()>dt[karg].getNumArgs() && quantifiers::TermUtil::isAssoc( min_t.getKind() ) && dt[karg].getNumArgs()==2 ){ tchildren.push_back( min_t[0] ); std::vector< Node > rem_children; for( unsigned i=1; imkNode( OR, NodeManager::currentNM()->mkNode( AND, curr[0], curr[1] ), NodeManager::currentNM()->mkNode( AND, curr[0].negate(), curr[2] ) ); }else if( curr.getKind()==OR || curr.getKind()==AND ){ - new_t = TermDb::simpleNegate( curr ).negate(); + new_t = TermUtil::simpleNegate( curr ).negate(); }else if( curr.getKind()==NOT ){ - new_t = TermDb::simpleNegate( curr[0] ); + new_t = TermUtil::simpleNegate( curr[0] ); }else{ new_t = NodeManager::currentNM()->mkNode( NOT, NodeManager::currentNM()->mkNode( NOT, curr ) ); } @@ -1096,7 +1097,7 @@ void CegConjectureSingleInvSol::getEquivalentTerms( Kind k, Node n, std::vector< } if( !eq.isNull() ){ eq = Rewriter::rewrite( eq ); - if( eq!=d_qe->getTermDatabase()->d_true ){ + if( eq!=d_qe->getTermUtil()->d_true ){ success = false; break; } diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 2fdc37134..b0a4da2af 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -19,6 +19,7 @@ #include "smt/term_formula_removal.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/trigger.h" #include "theory/theory_engine.h" @@ -605,7 +606,7 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node Node nretc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( PLUS, children ); nretc = Rewriter::rewrite( nretc ); //ensure that nret does not contain vars - if( !TermDb::containsTerms( nretc, vars ) ){ + if( !TermUtil::containsTerms( nretc, vars ) ){ //result is ( nret / pv_prop.d_coeff ) nret = nretc; }else{ @@ -647,7 +648,7 @@ Node CegInstantiator::applySubstitutionToLiteral( Node lit, std::vector< Node >& }else{ atom_lhs = NodeManager::currentNM()->mkNode( MINUS, atom[0], atom[1] ); atom_lhs = Rewriter::rewrite( atom_lhs ); - atom_rhs = getQuantifiersEngine()->getTermDatabase()->d_zero; + atom_rhs = getQuantifiersEngine()->getTermUtil()->d_zero; } //must be an eligible term if( isEligible( atom_lhs ) ){ @@ -968,7 +969,7 @@ void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited ) d_is_nested_quant = true; }else if( visited.find( n )==visited.end() ){ visited[n] = true; - if( TermDb::isBoolConnectiveTerm( n ) ){ + if( TermUtil::isBoolConnectiveTerm( n ) ){ for( unsigned i=0; i& lems, st Instantiator::Instantiator( QuantifiersEngine * qe, TypeNode tn ) : d_type( tn ){ - d_closed_enum_type = qe->getTermDatabase()->isClosedEnumerableType( tn ); + d_closed_enum_type = qe->getTermUtil()->isClosedEnumerableType( tn ); } diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp index 498d618d1..642ec8fcc 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/ceg_t_instantiator.cpp @@ -17,6 +17,7 @@ #include "options/quantifiers_options.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/trigger.h" @@ -86,7 +87,7 @@ Node ArithInstantiator::getModelBasedProjectionValue( CegInstantiator * ci, Node } if( !delta_coeff.isNull() ){ //create delta here if necessary - val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, delta_coeff, ci->getQuantifiersEngine()->getTermDatabase()->getVtsDelta() ) ); + val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, delta_coeff, ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta() ) ); val = Rewriter::rewrite( val ); } return val; @@ -148,7 +149,7 @@ int ArithInstantiator::solve_arith( CegInstantiator * ci, Node pv, Node atom, No } if( options::cbqiAll() ){ // when not pure LIA/LRA, we must check whether the lhs contains pv - if( TermDb::containsTerm( val, pv ) ){ + if( TermUtil::containsTerm( val, pv ) ){ Trace("cegqi-arith-debug") << "fail : contains bad term" << std::endl; return 0; } @@ -156,7 +157,7 @@ int ArithInstantiator::solve_arith( CegInstantiator * ci, Node pv, Node atom, No if( pvtn.isInteger() && ( ( !veq_c.isNull() && !veq_c.getType().isInteger() ) || !val.getType().isInteger() ) ){ //redo, split integer/non-integer parts bool useCoeff = false; - Integer coeff = ci->getQuantifiersEngine()->getTermDatabase()->d_one.getConst().getNumerator(); + Integer coeff = ci->getQuantifiersEngine()->getTermUtil()->d_one.getConst().getNumerator(); for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ if( it->first.isNull() || it->first.getType().isInteger() ){ if( !it->second.isNull() ){ @@ -186,7 +187,7 @@ int ArithInstantiator::solve_arith( CegInstantiator * ci, Node pv, Node atom, No if( !vts_coeff[0].isNull() ){ vts_coeff[0] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, rcoeff, vts_coeff[0] ) ); } - realPart = real_part.empty() ? ci->getQuantifiersEngine()->getTermDatabase()->d_zero : ( real_part.size()==1 ? real_part[0] : NodeManager::currentNM()->mkNode( PLUS, real_part ) ); + realPart = real_part.empty() ? ci->getQuantifiersEngine()->getTermUtil()->d_zero : ( real_part.size()==1 ? real_part[0] : NodeManager::currentNM()->mkNode( PLUS, real_part ) ); Assert( ci->getOutput()->isEligibleForInstantiation( realPart ) ); //re-isolate Trace("cegqi-arith-debug") << "Re-isolate..." << std::endl; @@ -213,8 +214,8 @@ int ArithInstantiator::solve_arith( CegInstantiator * ci, Node pv, Node atom, No } void ArithInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { - d_vts_sym[0] = ci->getQuantifiersEngine()->getTermDatabase()->getVtsInfinity( d_type, false, false ); - d_vts_sym[1] = ci->getQuantifiersEngine()->getTermDatabase()->getVtsDelta( false, false ); + d_vts_sym[0] = ci->getQuantifiersEngine()->getTermUtil()->getVtsInfinity( d_type, false, false ); + d_vts_sym[1] = ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta( false, false ); for( unsigned i=0; i<2; i++ ){ d_mbp_bounds[i].clear(); d_mbp_coeff[i].clear(); @@ -323,7 +324,7 @@ bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value ); cmp = Rewriter::rewrite( cmp ); Assert( cmp.isConst() ); - is_upper = ( cmp!=ci->getQuantifiersEngine()->getTermDatabase()->d_true ); + is_upper = ( cmp!=ci->getQuantifiersEngine()->getTermUtil()->d_true ); } }else{ is_upper = (r==0); @@ -354,7 +355,7 @@ bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, vts_coeff_delta = Rewriter::rewrite( vts_coeff_delta ); } }else{ - Node delta = ci->getQuantifiersEngine()->getTermDatabase()->getVtsDelta(); + Node delta = ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta(); uval = NodeManager::currentNM()->mkNode( uires==2 ? PLUS : MINUS, uval, delta ); uval = Rewriter::rewrite( uval ); } @@ -392,8 +393,8 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, } int best_used[2]; std::vector< Node > t_values[3]; - Node zero = ci->getQuantifiersEngine()->getTermDatabase()->d_zero; - Node one = ci->getQuantifiersEngine()->getTermDatabase()->d_one; + Node zero = ci->getQuantifiersEngine()->getTermUtil()->d_zero; + Node one = ci->getQuantifiersEngine()->getTermUtil()->d_one; Node pv_value = ci->getModelValue( pv ); //try optimal bounds for( unsigned r=0; r<2; r++ ){ @@ -403,7 +404,7 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, if( use_inf ){ Trace("cegqi-arith-bound") << "No " << ( rr==0 ? "lower" : "upper" ) << " bounds for " << pv << " (type=" << d_type << ")" << std::endl; //no bounds, we do +- infinity - Node val = ci->getQuantifiersEngine()->getTermDatabase()->getVtsInfinity( d_type ); + Node val = ci->getQuantifiersEngine()->getTermUtil()->getVtsInfinity( d_type ); //TODO : rho value for infinity? if( rr==0 ){ val = NodeManager::currentNM()->mkNode( UMINUS, val ); @@ -472,7 +473,7 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, Kind k = rr==0 ? GEQ : LEQ; Node cmp_bound = NodeManager::currentNM()->mkNode( k, value[t], best_bound_value[t] ); cmp_bound = Rewriter::rewrite( cmp_bound ); - if( cmp_bound!=ci->getQuantifiersEngine()->getTermDatabase()->d_true ){ + if( cmp_bound!=ci->getQuantifiersEngine()->getTermUtil()->d_true ){ new_best = false; break; } @@ -640,8 +641,8 @@ bool ArithInstantiator::postProcessInstantiationForVariable( CegInstantiator * c NodeManager::currentNM()->mkNode( ITE, NodeManager::currentNM()->mkNode( EQUAL, NodeManager::currentNM()->mkNode( INTS_MODULUS_TOTAL, veq[1], veq_c ), - ci->getQuantifiersEngine()->getTermDatabase()->d_zero ), - ci->getQuantifiersEngine()->getTermDatabase()->d_zero, ci->getQuantifiersEngine()->getTermDatabase()->d_one ) + ci->getQuantifiersEngine()->getTermUtil()->d_zero ), + ci->getQuantifiersEngine()->getTermUtil()->d_zero, ci->getQuantifiersEngine()->getTermUtil()->d_one ) ); } } @@ -695,7 +696,7 @@ Node DtInstantiator::solve_dt( Node v, Node a, Node b, Node sa, Node sb ) { } if( !ret.isNull() ){ //ensure does not contain - if( TermDb::containsTerm( ret, v ) ){ + if( TermUtil::containsTerm( ret, v ) ){ ret = Node::null(); } } @@ -784,7 +785,7 @@ void EprInstantiator::computeMatchScore( CegInstantiator * ci, Node pv, Node cat } void EprInstantiator::computeMatchScore( CegInstantiator * ci, Node pv, Node catom, Node eqc, std::map< Node, int >& match_score ) { - if( inst::Trigger::isAtomicTrigger( catom ) && TermDb::containsTerm( catom, pv ) ){ + if( inst::Trigger::isAtomicTrigger( catom ) && TermUtil::containsTerm( catom, pv ) ){ Trace("cegqi-epr") << "Find matches for " << catom << "..." << std::endl; std::vector< Node > arg_reps; for( unsigned j=0; jgetTermDatabase()->getCanonicalFreeVar( tn, i ); + return d_quantEngine->getTermUtil()->getCanonicalFreeVar( tn, i ); } bool ConjectureGenerator::isHandledTerm( TNode n ){ @@ -359,11 +360,11 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { Trace("sg-proc-debug") << "...eqc : " << r << std::endl; eqcs.push_back( r ); if( r.getType().isBoolean() ){ - if( areEqual( r, getTermDatabase()->d_true ) ){ - d_ground_eqc_map[r] = getTermDatabase()->d_true; + if( areEqual( r, getTermUtil()->d_true ) ){ + d_ground_eqc_map[r] = getTermUtil()->d_true; d_bool_eqc[0] = r; - }else if( areEqual( r, getTermDatabase()->d_false ) ){ - d_ground_eqc_map[r] = getTermDatabase()->d_false; + }else if( areEqual( r, getTermUtil()->d_false ) ){ + d_ground_eqc_map[r] = getTermUtil()->d_false; d_bool_eqc[1] = r; } } @@ -397,7 +398,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { std::vector< TNode > args; Trace("sg-pat-debug") << "******* Get ground term for " << r << std::endl; Node n; - if( getTermDatabase()->isInductionTerm( r ) ){ + if( getTermUtil()->isInductionTerm( r ) ){ n = d_op_arg_index[r].getGroundTerm( this, args ); }else{ n = r; @@ -427,7 +428,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { TNode r = eqcs[i]; //print out members bool firstTime = true; - bool isFalse = areEqual( r, getTermDatabase()->d_false ); + bool isFalse = areEqual( r, getTermUtil()->d_false ); eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); while( !eqc_i.isFinished() ){ TNode n = (*eqc_i); @@ -511,7 +512,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { if( d_tge.isRelevantTerm( eq ) ){ //make it canonical Trace("sg-proc-debug") << "get canonical " << eq << std::endl; - eq = d_quantEngine->getTermDatabase()->getCanonicalTerm( eq ); + eq = d_quantEngine->getTermUtil()->getCanonicalTerm( eq ); }else{ eq = Node::null(); } @@ -556,11 +557,11 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { //check each skolem variable bool disproven = true; //std::vector< Node > sk; - //getTermDatabase()->getSkolemConstants( q, sk, true ); + //getTermUtil()->getSkolemConstants( q, sk, true ); Trace("sg-conjecture") << " CONJECTURE : "; std::vector< Node > ce; - for( unsigned j=0; jd_skolem_constants[q].size(); j++ ){ - TNode k = getTermDatabase()->d_skolem_constants[q][j]; + for( unsigned j=0; jd_skolem_constants[q].size(); j++ ){ + TNode k = getTermUtil()->d_skolem_constants[q][j]; TNode rk = getRepresentative( k ); std::map< TNode, Node >::iterator git = d_ground_eqc_map.find( rk ); //check if it is a ground term @@ -568,7 +569,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { Trace("sg-conjecture") << "ACTIVE : " << q; if( Trace.isOn("sg-gen-eqc") ){ Trace("sg-conjecture") << " { "; - for( unsigned k=0; kd_skolem_constants[q].size(); k++ ){ Trace("sg-conjecture") << getTermDatabase()->d_skolem_constants[q][k] << ( j==k ? "*" : "" ) << " "; } + for( unsigned k=0; kd_skolem_constants[q].size(); k++ ){ Trace("sg-conjecture") << getTermUtil()->d_skolem_constants[q][k] << ( j==k ? "*" : "" ) << " "; } Trace("sg-conjecture") << "}"; } Trace("sg-conjecture") << std::endl; @@ -653,7 +654,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { typ_to_subs_index[it->first] = sum; sum += it->second; for( unsigned i=0; isecond; i++ ){ - gsubs_vars.push_back( d_quantEngine->getTermDatabase()->getCanonicalFreeVar( it->first, i ) ); + gsubs_vars.push_back( d_quantEngine->getTermUtil()->getCanonicalFreeVar( it->first, i ) ); } } } @@ -1055,7 +1056,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< for( unsigned i=0; iisClosedEnumerableType( tn ) ){ + if( getTermUtil()->isClosedEnumerableType( tn ) ){ types.push_back( tn ); }else{ return; @@ -1073,7 +1074,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< vec.push_back( size_limit ); }else{ //see if we can iterate current - if( vec_sumgetEnumerateTerm( types[index], vec[index]+1 ).isNull() ){ + if( vec_sumgetEnumerateTerm( types[index], vec[index]+1 ).isNull() ){ vec[index]++; vec_sum++; vec.push_back( size_limit - vec_sum ); @@ -1088,7 +1089,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< } if( success ){ if( vec.size()==n.getNumChildren() ){ - Node lc = getTermDatabase()->getEnumerateTerm( types[vec.size()-1], vec[vec.size()-1] ); + Node lc = getTermUtil()->getEnumerateTerm( types[vec.size()-1], vec[vec.size()-1] ); if( !lc.isNull() ){ for( unsigned i=0; i children; children.push_back( n.getOperator() ); for( unsigned i=0; i<(vec.size()-1); i++ ){ - Node nn = getTermDatabase()->getEnumerateTerm( types[i], vec[i] ); + Node nn = getTermUtil()->getEnumerateTerm( types[i], vec[i] ); Assert( !nn.isNull() ); Assert( nn.getType()==n[i].getType() ); children.push_back( nn ); diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp new file mode 100644 index 000000000..4acc3e6b8 --- /dev/null +++ b/src/theory/quantifiers/equality_query.cpp @@ -0,0 +1,336 @@ +/********************* */ +/*! \file equality_query.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Utilities used for querying about equality information + **/ + +#include "theory/quantifiers/equality_query.h" + +#include "options/quantifiers_options.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/equality_infer.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" +#include "theory/theory_engine.h" +#include "theory/uf/equality_engine.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; + +EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe ) : d_qe( qe ), d_eqi_counter( c ), d_reset_count( 0 ){ + +} + +EqualityQueryQuantifiersEngine::~EqualityQueryQuantifiersEngine(){ +} + +bool EqualityQueryQuantifiersEngine::reset( Theory::Effort e ){ + d_int_rep.clear(); + d_reset_count++; + return processInferences( e ); +} + +bool EqualityQueryQuantifiersEngine::processInferences( Theory::Effort e ) { + if( options::inferArithTriggerEq() ){ + eq::EqualityEngine* ee = getEngine(); + //updated implementation + EqualityInference * ei = d_qe->getEqualityInference(); + while( d_eqi_counter.get()getNumPendingMerges() ){ + Node eq = ei->getPendingMerge( d_eqi_counter.get() ); + Node eq_exp = ei->getPendingMergeExplanation( d_eqi_counter.get() ); + Trace("quant-engine-ee-proc") << "processInferences : Infer : " << eq << std::endl; + Trace("quant-engine-ee-proc") << " explanation : " << eq_exp << std::endl; + Assert( ee->hasTerm( eq[0] ) ); + Assert( ee->hasTerm( eq[1] ) ); + if( areDisequal( eq[0], eq[1] ) ){ + Trace("quant-engine-ee-proc") << "processInferences : Conflict : " << eq << std::endl; + if( Trace.isOn("term-db-lemma") ){ + Trace("term-db-lemma") << "Disequal terms, equal by normalization : " << eq[0] << " " << eq[1] << "!!!!" << std::endl; + if( !d_qe->getTheoryEngine()->needCheck() ){ + Trace("term-db-lemma") << " all theories passed with no lemmas." << std::endl; + //this should really never happen (implies arithmetic is incomplete when sharing is enabled) + Assert( false ); + } + Trace("term-db-lemma") << " add split on : " << eq << std::endl; + } + d_qe->addSplit( eq ); + return false; + }else{ + ee->assertEquality( eq, true, eq_exp ); + d_eqi_counter = d_eqi_counter.get() + 1; + } + } + Assert( ee->consistent() ); + } + return true; +} + +bool EqualityQueryQuantifiersEngine::hasTerm( Node a ){ + return getEngine()->hasTerm( a ); +} + +Node EqualityQueryQuantifiersEngine::getRepresentative( Node a ){ + eq::EqualityEngine* ee = getEngine(); + if( ee->hasTerm( a ) ){ + return ee->getRepresentative( a ); + }else{ + return a; + } +} + +bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){ + if( a==b ){ + return true; + }else{ + eq::EqualityEngine* ee = getEngine(); + if( ee->hasTerm( a ) && ee->hasTerm( b ) ){ + return ee->areEqual( a, b ); + }else{ + return false; + } + } +} + +bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){ + if( a==b ){ + return false; + }else{ + eq::EqualityEngine* ee = getEngine(); + if( ee->hasTerm( a ) && ee->hasTerm( b ) ){ + return ee->areDisequal( a, b, false ); + }else{ + return a.isConst() && b.isConst(); + } + } +} + +Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, int index ){ + Assert( f.isNull() || f.getKind()==FORALL ); + Node r = getRepresentative( a ); + if( options::finiteModelFind() ){ + if( r.isConst() && quantifiers::TermUtil::containsUninterpretedConstant( r ) ){ + //map back from values assigned by model, if any + if( d_qe->getModel() ){ + std::map< Node, Node >::iterator it = d_qe->getModel()->d_rep_set.d_values_to_terms.find( r ); + if( it!=d_qe->getModel()->d_rep_set.d_values_to_terms.end() ){ + r = it->second; + r = getRepresentative( r ); + }else{ + if( r.getType().isSort() ){ + Trace("internal-rep-warn") << "No representative for UF constant." << std::endl; + //should never happen : UF constants should never escape model + Assert( false ); + } + } + } + } + } + if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_EE ){ + return r; + }else{ + TypeNode v_tn = f.isNull() ? a.getType() : f[0][index].getType(); + std::map< Node, Node >::iterator itir = d_int_rep[v_tn].find( r ); + if( itir==d_int_rep[v_tn].end() ){ + //find best selection for representative + Node r_best; + //if( options::fmfRelevantDomain() && !f.isNull() ){ + // Trace("internal-rep-debug") << "Consult relevant domain to mkRep " << r << std::endl; + // r_best = d_qe->getRelevantDomain()->getRelevantTerm( f, index, r ); + // Trace("internal-rep-debug") << "Returned " << r_best << " " << r << std::endl; + //} + std::vector< Node > eqc; + getEquivalenceClass( r, eqc ); + Trace("internal-rep-select") << "Choose representative for equivalence class : { "; + for( unsigned i=0; i0 ) Trace("internal-rep-select") << ", "; + Trace("internal-rep-select") << eqc[i]; + } + Trace("internal-rep-select") << " }, type = " << v_tn << std::endl; + int r_best_score = -1; + for( size_t i=0; i=0 && ( r_best_score<0 || score cache; + r_best = getInstance( r_best, eqc, cache ); + //store that this representative was chosen at this point + if( d_rep_score.find( r_best )==d_rep_score.end() ){ + d_rep_score[ r_best ] = d_reset_count; + } + Trace("internal-rep-select") << "...Choose " << r_best << " with score " << r_best_score << std::endl; + Assert( r_best.getType().isSubtypeOf( v_tn ) ); + d_int_rep[v_tn][r] = r_best; + if( r_best!=a ){ + Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl; + Trace("internal-rep-debug") << "int_rep( " << a << " ) = " << r_best << ", " << std::endl; + } + return r_best; + }else{ + return itir->second; + } + } +} + +void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps ) { + //make sure internal representatives currently exist + for( std::map< TypeNode, std::vector< Node > >::iterator it = reps.begin(); it != reps.end(); ++it ){ + if( it->first.isSort() ){ + for( unsigned i=0; isecond.size(); i++ ){ + Node r = getInternalRepresentative( it->second[i], Node::null(), 0 ); + } + } + } + Trace("internal-rep-flatten") << "---Flattening representatives : " << std::endl; + for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){ + for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){ + Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl; + } + } + //store representatives for newly created terms + std::map< Node, Node > temp_rep_map; + + bool success; + do { + success = false; + for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){ + for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){ + if( it->second.getKind()==APPLY_UF && it->second.getType().isSort() ){ + Node ni = it->second; + std::vector< Node > cc; + cc.push_back( it->second.getOperator() ); + bool changed = false; + for( unsigned j=0; jsecond.find( r )==itt->second.end() ){ + Assert( temp_rep_map.find( r )!=temp_rep_map.end() ); + r = temp_rep_map[r]; + } + if( r==ni ){ + //found sub-term as instance + Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to subterm " << ni[j] << std::endl; + itt->second[it->first] = ni[j]; + changed = false; + success = true; + break; + }else{ + Node ir = itt->second[r]; + cc.push_back( ir ); + if( ni[j]!=ir ){ + changed = true; + } + } + }else{ + changed = false; + break; + } + } + if( changed ){ + Node n = NodeManager::currentNM()->mkNode( APPLY_UF, cc ); + Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to " << n << std::endl; + success = true; + itt->second[it->first] = n; + temp_rep_map[n] = it->first; + } + } + } + } + }while( success ); + Trace("internal-rep-flatten") << "---After flattening : " << std::endl; + for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){ + for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){ + Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl; + } + } +} + +eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){ + return d_qe->getActiveEqualityEngine(); +} + +void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< Node >& eqc ){ + eq::EqualityEngine* ee = getEngine(); + if( ee->hasTerm( a ) ){ + Node rep = ee->getRepresentative( a ); + eq::EqClassIterator eqc_iter( rep, ee ); + while( !eqc_iter.isFinished() ){ + eqc.push_back( *eqc_iter ); + eqc_iter++; + } + }else{ + eqc.push_back( a ); + } + //a should be in its equivalence class + Assert( std::find( eqc.begin(), eqc.end(), a )!=eqc.end() ); +} + +TNode EqualityQueryQuantifiersEngine::getCongruentTerm( Node f, std::vector< TNode >& args ) { + return d_qe->getTermDatabase()->getCongruentTerm( f, args ); +} + +//helper functions + +Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map& cache ){ + if(cache.find(n) != cache.end()) { + return cache[n]; + } + for( size_t i=0; igetTermDatabase()->isInstClosure( n ) || !d_qe->getTermDatabase()->hasTermCurrent( n, false ) ) ){ + return -1; + }else if( options::instMaxLevel()!=-1 ){ + //score prefer lowest instantiation level + if( n.hasAttribute(InstLevelAttribute()) ){ + return n.getAttribute(InstLevelAttribute()); + }else{ + return options::instLevelInputOnly() ? -1 : 0; + } + }else{ + if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_FIRST ){ + //score prefers earliest use of this term as a representative + return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n]; + }else{ + Assert( options::quantRepMode()==quantifiers::QUANT_REP_MODE_DEPTH ); + return quantifiers::TermUtil::getTermDepth( n ); + } + } +} diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h new file mode 100644 index 000000000..c3e0a8c5b --- /dev/null +++ b/src/theory/quantifiers/equality_query.h @@ -0,0 +1,76 @@ +/********************* */ +/*! \file equality_query.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Equality query class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H +#define __CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H + +#include "theory/quantifiers_engine.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +// TODO : (as part of #1171, #1214) further document and clean this class. +/** equality query object using theory engine */ +class EqualityQueryQuantifiersEngine : public EqualityQuery +{ +private: + /** pointer to theory engine */ + QuantifiersEngine* d_qe; + /** quantifiers equality inference */ + context::CDO< unsigned > d_eqi_counter; + /** internal representatives */ + std::map< TypeNode, std::map< Node, Node > > d_int_rep; + /** rep score */ + std::map< Node, int > d_rep_score; + /** reset count */ + int d_reset_count; + + /** processInferences : will merge equivalence classes in master equality engine, if possible */ + bool processInferences( Theory::Effort e ); + /** node contains */ + Node getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map& cache ); + /** get score */ + int getRepScore( Node n, Node f, int index, TypeNode v_tn ); + /** flatten representatives */ + void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps ); +public: + EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe ); + virtual ~EqualityQueryQuantifiersEngine(); + /** reset */ + bool reset( Theory::Effort e ); + /** identify */ + std::string identify() const { return "EqualityQueryQE"; } + /** general queries about equality */ + bool hasTerm( Node a ); + Node getRepresentative( Node a ); + bool areEqual( Node a, Node b ); + bool areDisequal( Node a, Node b ); + eq::EqualityEngine* getEngine(); + void getEquivalenceClass( Node a, std::vector< Node >& eqc ); + TNode getCongruentTerm( Node f, std::vector< TNode >& args ); + /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria. + If cbqi is active, this will return a term in the equivalence class of "a" that does + not contain instantiation constants, if such a term exists. + */ + Node getInternalRepresentative( Node a, Node f, int index ); +}; /* EqualityQueryQuantifiersEngine */ + +}/* CVC4::theory::quantifiers namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H */ diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 0ffa0c115..462dc23d0 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -19,6 +19,7 @@ #include "theory/quantifiers/model_engine.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #define USE_INDEX_ORDERING @@ -521,7 +522,7 @@ struct sortGetMaxVariableNum { int computeMaxVariableNum( Node n ){ if( n.getKind()==INST_CONSTANT ){ return n.getAttribute(InstVarNumAttribute()); - }else if( TermDb::hasInstConstAttr(n) ){ + }else if( TermUtil::hasInstConstAttr(n) ){ int maxVal = -1; for( int i=0; i<(int)n.getNumChildren(); i++ ){ int val = getMaxVariableNum( n[i] ); @@ -710,7 +711,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { }else{ //can happen for types not involved in quantified formulas Trace("fmc-model-func") << "No type rep for " << tn << std::endl; - v = d_qe->getTermDatabase()->getEnumerateTerm( tn, 0 ); + v = d_qe->getTermUtil()->getEnumerateTerm( tn, 0 ); } Trace("fmc-model-func") << "No term, assign " << v << std::endl; } diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 6f617db42..ddf7becf2 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -16,6 +16,7 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/full_model_check.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" using namespace std; using namespace CVC4; @@ -382,7 +383,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ Node r = fm->getRepresentative( it->second[a] ); if( Trace.isOn("fmc-model-debug") ){ std::vector< Node > eqc; - ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc ); + d_qe->getEqualityQuery()->getEquivalenceClass( r, eqc ); Trace("fmc-model-debug") << " " << (it->second[a]==r); Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : "; //Trace("fmc-model-debug") << r2 << " : " << ir << " : "; diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index 5bbd4c48e..356e95d1b 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -17,9 +17,9 @@ #include #include "theory/quantifiers/fun_def_process.h" -#include "theory/rewriter.h" +#include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/term_util.h" #include "proof/proof_manager.h" using namespace CVC4; @@ -34,7 +34,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions ) { std::map< int, Node > subs_head; //first pass : find defined functions, transform quantifiers for( unsigned i=0; i& assertions ) { exit( 0 ); } - Node bd = TermDb::getFunDefBody( assertions[i] ); + Node bd = QuantAttributes::getFunDefBody( assertions[i] ); Trace("fmf-fun-def-debug") << "Process function " << n << ", body = " << bd << std::endl; if( !bd.isNull() ){ d_funcs.push_back( f ); diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 79a412b3c..31bd1d517 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -19,6 +19,7 @@ #include "options/datatypes_options.h" #include "theory/quantifiers/candidate_generator.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers/trigger.h" #include "theory/quantifiers_engine.h" @@ -36,7 +37,7 @@ InstMatchGenerator::InstMatchGenerator( Node pat ){ d_cg = NULL; d_needsReset = true; d_active_add = false; - Assert( quantifiers::TermDb::hasInstConstAttr(pat) ); + Assert( quantifiers::TermUtil::hasInstConstAttr(pat) ); d_pattern = pat; d_match_pattern = pat; d_match_pattern_type = pat.getType(); @@ -99,7 +100,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< //make sure the matching portion of the equality is on the LHS of d_pattern // and record what d_match_pattern is for( unsigned i=0; i<2; i++ ){ - if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[i]) || d_match_pattern[i].getKind()==INST_CONSTANT ){ + if( !quantifiers::TermUtil::hasInstConstAttr(d_match_pattern[i]) || d_match_pattern[i].getKind()==INST_CONSTANT ){ Node mp = d_match_pattern[1-i]; Node mpo = d_match_pattern[i]; if( mp.getKind()!=INST_CONSTANT ){ @@ -127,7 +128,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< //now, collect children of d_match_pattern for( unsigned i=0; i prev; //if t is null Assert( !t.isNull() ); - Assert( !quantifiers::TermDb::hasInstConstAttr(t) ); + Assert( !quantifiers::TermUtil::hasInstConstAttr(t) ); Assert( d_match_pattern.getKind()==INST_CONSTANT || t.getKind()==d_match_pattern.getKind() ); Assert( !Trigger::isAtomicTrigger( d_match_pattern ) || t.getOperator()==d_match_pattern.getOperator() ); //first, check if ground arguments are not equal, or a match is in conflict @@ -253,20 +254,20 @@ int InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngin Node t_match; if( pol ){ if( pat.getKind()==GT ){ - t_match = NodeManager::currentNM()->mkNode(MINUS, t, qe->getTermDatabase()->d_one); + t_match = NodeManager::currentNM()->mkNode(MINUS, t, qe->getTermUtil()->d_one); }else{ t_match = t; } }else{ if( pat.getKind()==EQUAL ){ if( t.getType().isBoolean() ){ - t_match = NodeManager::currentNM()->mkConst( !q->areEqual( qe->getTermDatabase()->d_true, t ) ); + t_match = NodeManager::currentNM()->mkConst( !q->areEqual( qe->getTermUtil()->d_true, t ) ); }else{ Assert( t.getType().isReal() ); - t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermDatabase()->d_one); + t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermUtil()->d_one); } }else if( pat.getKind()==GEQ ){ - t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermDatabase()->d_one); + t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermUtil()->d_one); }else if( pat.getKind()==GT ){ t_match = t; } @@ -552,7 +553,7 @@ int VarMatchGeneratorTermSubs::getNextMatch( Node q, InstMatch& m, QuantifiersEn InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear( Node q, std::vector< Node >& pats, QuantifiersEngine* qe ) { //order patterns to maximize eager matching failures std::map< Node, std::vector< Node > > var_contains; - qe->getTermDatabase()->getVarContains( q, pats, var_contains ); + qe->getTermUtil()->getVarContains( q, pats, var_contains ); std::map< Node, std::vector< Node > > var_to_node; for( std::map< Node, std::vector< Node > >::iterator it = var_contains.begin(); it != var_contains.end(); ++it ){ for( unsigned i=0; isecond.size(); i++ ){ @@ -662,7 +663,7 @@ InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node q, std::vector< Node >& p d_f( q ){ Trace("multi-trigger-cache") << "Making smart multi-trigger for " << q << std::endl; std::map< Node, std::vector< Node > > var_contains; - qe->getTermDatabase()->getVarContains( q, pats, var_contains ); + qe->getTermUtil()->getVarContains( q, pats, var_contains ); //convert to indicies for( std::map< Node, std::vector< Node > >::iterator it = var_contains.begin(); it != var_contains.end(); ++it ){ Trace("multi-trigger-cache") << "Pattern " << it->first << " contains: "; @@ -793,7 +794,7 @@ void InstMatchGeneratorMulti::processNewInstantiations( QuantifiersEngine* qe, I processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, 0 ); }else if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){ int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex]; - //Node curr_ic = qe->getTermDatabase()->getInstantiationConstant( d_f, curr_index ); + //Node curr_ic = qe->getTermUtil()->getInstantiationConstant( d_f, curr_index ); Node n = m.get( curr_index ); if( n.isNull() ){ //if( d_var_to_node[ curr_index ].size()==1 ){ //FIXME @@ -861,7 +862,7 @@ void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe, } if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){ int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex]; - //Node curr_ic = qe->getTermDatabase()->getInstantiationConstant( d_f, curr_index ); + //Node curr_ic = qe->getTermUtil()->getInstantiationConstant( d_f, curr_index ); //unique non-set variable, add to InstMatch for( std::map< Node, InstMatchTrie >::iterator it = tr->d_data.begin(); it != tr->d_data.end(); ++it ){ InstMatch mn( &m ); @@ -893,12 +894,12 @@ InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node q, Node pat, Quantifier if( d_match_pattern.getKind()==EQUAL ){ d_eqc = d_match_pattern[1]; d_match_pattern = d_match_pattern[0]; - Assert( !quantifiers::TermDb::hasInstConstAttr( d_eqc ) ); + Assert( !quantifiers::TermUtil::hasInstConstAttr( d_eqc ) ); } Assert( Trigger::isSimpleTrigger( d_match_pattern ) ); for( unsigned i=0; igetTermDatabase()->getCounterexampleLiteral( q ); - Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( q ); + Node ceLit = d_quantEngine->getTermUtil()->getCounterexampleLiteral( q ); + Node ceBody = d_quantEngine->getTermUtil()->getInstConstantBody( q ); if( !ceBody.isNull() ){ //add counterexample lemma Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() ); @@ -90,7 +92,7 @@ bool InstStrategyCbqi::registerCbqiLemma( Node q ) { std::map< TypeNode, std::vector< Node > >::iterator itc = qepr->d_consts.find( tn ); if( itc!=qepr->d_consts.end() ){ Assert( !itc->second.empty() ); - Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i ); + Node ic = d_quantEngine->getTermUtil()->getInstantiationConstant( q, i ); std::vector< Node > disj; for( unsigned j=0; jsecond.size(); j++ ){ disj.push_back( ic.eqNode( itc->second[j] ) ); @@ -111,7 +113,7 @@ bool InstStrategyCbqi::registerCbqiLemma( Node q ) { //compute dependencies between quantified formulas if( options::cbqiLitDepend() || options::cbqiInnermost() ){ std::vector< Node > ics; - TermDb::computeVarContains( q, ics ); + TermUtil::computeVarContains( q, ics ); d_parent_quant[q].clear(); d_children_quant[q].clear(); std::vector< Node > dep; @@ -121,7 +123,7 @@ bool InstStrategyCbqi::registerCbqiLemma( Node q ) { d_parent_quant[q].push_back( qi ); d_children_quant[qi].push_back( q ); Assert( hasAddedCbqiLemma( qi ) ); - Node qicel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( qi ); + Node qicel = d_quantEngine->getTermUtil()->getCounterexampleLiteral( qi ); dep.push_back( qi ); dep.push_back( qicel ); } @@ -135,7 +137,7 @@ bool InstStrategyCbqi::registerCbqiLemma( Node q ) { //must register all sub-quantifiers of counterexample lemma, register their lemmas std::vector< Node > quants; - TermDb::computeQuantContains( lem, quants ); + TermUtil::computeQuantContains( lem, quants ); for( unsigned i=0; igetModel()->isQuantifierActive( q ) ){ d_active_quant[q] = true; Debug("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl; - Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q ); + Node cel = d_quantEngine->getTermUtil()->getCounterexampleLiteral( q ); bool value; if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){ Debug("cbqi-debug") << "...CE Literal has value " << value << std::endl; @@ -299,7 +301,7 @@ Node InstStrategyCbqi::getIdMarkedQuantNode( Node n, std::map< Node, Node >& vis Node ret = n; if( n.getKind()==FORALL ){ QAttributes qa; - TermDb::computeQuantAttributes( n, qa ); + QuantAttributes::computeQuantAttributes( n, qa ); if( qa.d_qid_num.isNull() ){ std::vector< Node > rc; rc.push_back( n[0] ); @@ -392,15 +394,15 @@ Node InstStrategyCbqi::doNestedQENode( Node q, Node ceq, Node n, std::vector< No //should not contain quantifiers Assert( !QuantifiersRewriter::containsQuantifiers( d_nested_qe[ceq] ) ); } - Assert( d_quantEngine->getTermDatabase()->d_inst_constants[q].size()==inst_terms.size() ); + Assert( d_quantEngine->getTermUtil()->d_inst_constants[q].size()==inst_terms.size() ); //replace inst constants with instantiation - Node ret = d_nested_qe[ceq].substitute( d_quantEngine->getTermDatabase()->d_inst_constants[q].begin(), - d_quantEngine->getTermDatabase()->d_inst_constants[q].end(), + Node ret = d_nested_qe[ceq].substitute( d_quantEngine->getTermUtil()->d_inst_constants[q].begin(), + d_quantEngine->getTermUtil()->d_inst_constants[q].end(), inst_terms.begin(), inst_terms.end() ); if( doVts ){ //do virtual term substitution ret = Rewriter::rewrite( ret ); - ret = d_quantEngine->getTermDatabase()->rewriteVtsSymbols( ret ); + ret = d_quantEngine->getTermUtil()->rewriteVtsSymbols( ret ); } Trace("cbqi-nqe") << "Nested quantifier elimination: " << std::endl; Trace("cbqi-nqe") << " " << n << std::endl; @@ -413,7 +415,7 @@ Node InstStrategyCbqi::doNestedQERec( Node q, Node n, std::map< Node, Node >& vi Node ret = n; if( n.getKind()==FORALL ){ QAttributes qa; - TermDb::computeQuantAttributes( n, qa ); + QuantAttributes::computeQuantAttributes( n, qa ); if( !qa.d_qid_num.isNull() ){ //if it has an id, check whether we have done quantifier elimination for this id std::map< Node, Node >::iterator it = d_id_to_ce_quant.find( qa.d_qid_num ); @@ -478,7 +480,7 @@ void InstStrategyCbqi::registerCounterexampleLemma( Node q, Node lem ){ bool InstStrategyCbqi::hasNonCbqiOperator( Node n, std::map< Node, bool >& visited ){ if( visited.find( n )==visited.end() ){ visited[n] = true; - if( n.getKind()!=BOUND_VARIABLE && TermDb::hasBoundVarAttr( n ) ){ + if( n.getKind()!=BOUND_VARIABLE && TermUtil::hasBoundVarAttr( n ) ){ if( !inst::Trigger::isCbqiKind( n.getKind() ) ){ Trace("cbqi-debug2") << "Non-cbqi kind : " << n.getKind() << " in " << n << std::endl; return true; @@ -554,8 +556,8 @@ bool InstStrategyCbqi::doCbqi( Node q ){ std::map< Node, int >::iterator it = d_do_cbqi.find( q ); if( it==d_do_cbqi.end() ){ int ret = 2; - if( !d_quantEngine->getTermDatabase()->isQAttrQuantElim( q ) ){ - Assert( !d_quantEngine->getTermDatabase()->isQAttrQuantElimPartial( q ) ); + if( !d_quantEngine->getQuantAttributes()->isQuantElim( q ) ){ + Assert( !d_quantEngine->getQuantAttributes()->isQuantElimPartial( q ) ); //if has an instantiation pattern, don't do it if( q.getNumChildren()==3 && options::eMatching() && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){ for( unsigned i=0; igetTermDatabase()->isQAttrSygus( q ) ){ + if( d_quantEngine->getQuantAttributes()->isSygus( q ) ){ ret = 0; } if( ret!=0 ){ @@ -616,7 +618,7 @@ Node InstStrategyCbqi::getNextDecisionRequestProc( Node q, std::map< Node, bool } //then check self if( hasAddedCbqiLemma( q ) ){ - Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q ); + Node cel = d_quantEngine->getTermUtil()->getCounterexampleLiteral( q ); bool value; if( !d_quantEngine->getValuation().hasSatValue( cel, value ) ){ Trace("cbqi-dec") << "CBQI: get next decision " << cel << std::endl; @@ -699,14 +701,14 @@ void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) { d_small_const = NodeManager::currentNM()->mkNode( MULT, d_small_const, d_small_const ); d_small_const = Rewriter::rewrite( d_small_const ); //heuristic for now, until we know how to do nested quantification - Node delta = d_quantEngine->getTermDatabase()->getVtsDelta( true, false ); + Node delta = d_quantEngine->getTermUtil()->getVtsDelta( true, false ); if( !delta.isNull() ){ Trace("quant-vts-debug") << "Delta lemma for " << d_small_const << std::endl; Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, delta, d_small_const ); d_quantEngine->getOutputChannel().lemma( delta_lem_ub ); } std::vector< Node > inf; - d_quantEngine->getTermDatabase()->getVtsTerms( inf, true, false, false ); + d_quantEngine->getTermUtil()->getVtsTerms( inf, true, false, false ); for( unsigned i=0; imkNode( GT, inf[i], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst() ) ); @@ -719,14 +721,14 @@ void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) { bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { Assert( !d_curr_quant.isNull() ); //if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma - if( d_quantEngine->getTermDatabase()->isQAttrQuantElimPartial( d_curr_quant ) ){ + if( d_quantEngine->getQuantAttributes()->isQuantElimPartial( d_curr_quant ) ){ d_cbqi_set_quant_inactive = true; d_incomplete_check = true; d_quantEngine->recordInstantiationInternal( d_curr_quant, subs, false, false ); return true; }else{ //check if we need virtual term substitution (if used delta or infinity) - bool used_vts = d_quantEngine->getTermDatabase()->containsVtsTerm( subs, false ); + bool used_vts = d_quantEngine->getTermUtil()->containsVtsTerm( subs, false ); if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, used_vts ) ){ ++(d_quantEngine->d_statistics.d_instantiations_cbqi); //d_added_inst.insert( d_curr_quant ); @@ -761,7 +763,7 @@ bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) { } } //only legal if current quantified formula contains n - return TermDb::containsTerm( d_curr_quant, n ); + return TermUtil::containsTerm( d_curr_quant, n ); } }else{ return true; @@ -796,8 +798,8 @@ void InstStrategyCegqi::registerCounterexampleLemma( Node q, Node lem ) { //must register with the instantiator //must explicitly remove ITEs so that we record dependencies std::vector< Node > ce_vars; - for( unsigned i=0; igetTermDatabase()->getNumInstantiationConstants( q ); i++ ){ - ce_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i ) ); + for( unsigned i=0; igetTermUtil()->getNumInstantiationConstants( q ); i++ ){ + ce_vars.push_back( d_quantEngine->getTermUtil()->getInstantiationConstant( q, i ) ); } std::vector< Node > lems; lems.push_back( lem ); diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 096e0933d..105f8f5e2 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -14,8 +14,10 @@ #include "theory/quantifiers/inst_strategy_e_matching.h" #include "theory/quantifiers/inst_match_generator.h" +#include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/relevant_domain.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/theory_engine.h" using namespace std; @@ -279,16 +281,16 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ std::map< Node, inst::TriggerTermInfo > tinfo; //well-defined function: can assume LHS is only trigger if( options::quantFunWellDefined() ){ - Node hd = TermDb::getFunDefHead( f ); + Node hd = QuantAttributes::getFunDefHead( f ); if( !hd.isNull() ){ - hd = d_quantEngine->getTermDatabase()->getInstConstantNode( hd, f ); + hd = d_quantEngine->getTermUtil()->getInstConstantNode( hd, f ); patTermsF.push_back( hd ); tinfo[hd].init( f, hd ); } } //otherwise, use algorithm for collecting pattern terms if( patTermsF.empty() ){ - Node bd = d_quantEngine->getTermDatabase()->getInstConstantBody( f ); + Node bd = d_quantEngine->getTermUtil()->getInstConstantBody( f ); Trigger::collectPatTerms( f, bd, patTermsF, d_tr_strategy, d_user_no_gen[f], tinfo, true ); if( ntrivTriggers ){ sortTriggers st; @@ -332,7 +334,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ if( options::partialTriggers() ){ std::vector< Node > vcs[2]; for( unsigned i=0; igetTermDatabase()->getInstantiationConstant( f, i ); + Node ic = d_quantEngine->getTermUtil()->getInstantiationConstant( f, i ); vcs[ vcMap.find( ic )==vcMap.end() ? 0 : 1 ].push_back( f[0][i] ); } for( unsigned i=0; i<2; i++ ){ @@ -506,7 +508,7 @@ void InstStrategyAutoGenTriggers::addTrigger( inst::Trigger * tr, Node q ) { if( tr ){ if( d_num_trigger_vars[q]mkNode( INST_PATTERN_LIST, d_quantEngine->getTermDatabase()->getVariableNode( tr->getInstPattern(), q ) ); + Node ipl = NodeManager::currentNM()->mkNode( INST_PATTERN_LIST, d_quantEngine->getTermUtil()->getVariableNode( tr->getInstPattern(), q ) ); Node qq = NodeManager::currentNM()->mkNode( FORALL, d_vc_partition[1][q], NodeManager::currentNM()->mkNode( FORALL, d_vc_partition[0][q], q[1] ), ipl ); Trace("auto-gen-trigger-partial") << "Make partially specified user pattern: " << std::endl; Trace("auto-gen-trigger-partial") << " " << qq << std::endl; @@ -567,7 +569,7 @@ bool InstStrategyLocalTheoryExt::isLocalTheoryExt( Node f ) { std::map< Node, bool >::iterator itq = d_quant.find( f ); if( itq==d_quant.end() ){ //generate triggers - Node bd = d_quantEngine->getTermDatabase()->getInstConstantBody( f ); + Node bd = d_quantEngine->getTermUtil()->getInstConstantBody( f ); std::vector< Node > vars; std::vector< Node > patTerms; bool ret = Trigger::isLocalTheoryExt( bd, vars, patTerms ); @@ -575,7 +577,7 @@ bool InstStrategyLocalTheoryExt::isLocalTheoryExt( Node f ) { d_quant[f] = ret; //add all variables to trigger that don't already occur for( unsigned i=0; igetTermDatabase()->getInstantiationConstant( f, i ); + Node x = d_quantEngine->getTermUtil()->getInstantiationConstant( f, i ); if( std::find( vars.begin(), vars.end(), x )==vars.end() ){ patTerms.push_back( x ); } @@ -698,7 +700,7 @@ bool FullSaturation::process( Node f, bool fullEffort ){ std::map< Node, Node > reps_found; for( unsigned j=0; jgetTermDatabase()->getTypeGroundTerm( ftypes[i], j ); - if( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr( gt ) ){ + if( !options::cbqi() || !quantifiers::TermUtil::hasInstConstAttr( gt ) ){ Node r = d_quantEngine->getEqualityQuery()->getRepresentative( gt ); if( reps_found.find( r )==reps_found.end() ){ reps_found[r] = gt; diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 1cdd224e7..1f3f56820 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -18,6 +18,7 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/inst_strategy_e_matching.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers/trigger.h" #include "theory/theory_engine.h" @@ -177,7 +178,7 @@ void InstantiationEngine::registerQuantifier( Node f ){ //} //take into account user patterns if( f.getNumChildren()==3 ){ - Node subsPat = d_quantEngine->getTermDatabase()->getInstConstantNode( f[2], f ); + Node subsPat = d_quantEngine->getTermUtil()->getInstConstantNode( f[2], f ); //add patterns for( int i=0; i<(int)subsPat.getNumChildren(); i++ ){ //Notice() << "Add pattern " << subsPat[i] << " for " << f << std::endl; diff --git a/src/theory/quantifiers/local_theory_ext.cpp b/src/theory/quantifiers/local_theory_ext.cpp index cf5fe3b50..e26c464e2 100644 --- a/src/theory/quantifiers/local_theory_ext.cpp +++ b/src/theory/quantifiers/local_theory_ext.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/local_theory_ext.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" #include "theory/quantifiers/first_order_model.h" diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp index a9fad80ae..57187b7ab 100644 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp @@ -24,6 +24,7 @@ #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers/trigger.h" #include "theory/rewriter.h" @@ -152,10 +153,10 @@ bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){ } bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) { - Node icn = d_qe->getTermDatabase()->getInstConstantNode( n, f ); + Node icn = d_qe->getTermUtil()->getInstConstantNode( n, f ); Trace("macros-debug2") << "Get free variables in " << icn << std::endl; std::vector< Node > var; - d_qe->getTermDatabase()->getVarContainsNode( f, icn, var ); + d_qe->getTermUtil()->getVarContainsNode( f, icn, var ); Trace("macros-debug2") << "Get trigger variables for " << icn << std::endl; std::vector< Node > trigger_var; inst::Trigger::getTriggerVariables( icn, f, trigger_var ); diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 2b7ba7ac9..ced62d8f5 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -19,6 +19,7 @@ #include "theory/quantifiers/model_engine.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers/trigger.h" #include "theory/theory_engine.h" #include "theory/uf/equality_engine.h" @@ -434,8 +435,8 @@ int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, in //if evaluate(...)==1, then the instantiation is already true in the model // depIndex is the index of the least significant variable that this evaluation relies upon depIndex = riter.getNumTerms()-1; - Debug("fmf-model-eval") << "We will evaluate " << d_qe->getTermDatabase()->getInstConstantBody( f ) << std::endl; - eval = fmig->evaluate( d_qe->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter ); + Debug("fmf-model-eval") << "We will evaluate " << d_qe->getTermUtil()->getInstConstantBody( f ) << std::endl; + eval = fmig->evaluate( d_qe->getTermUtil()->getInstConstantBody( f ), depIndex, &riter ); if( eval==1 ){ Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl; }else{ @@ -531,7 +532,7 @@ void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){ // - determine selection literals // - check which function/predicates have good and bad definitions for satisfying f if( d_phase_reqs.find( f )==d_phase_reqs.end() ){ - d_phase_reqs[f].initialize( d_qe->getTermDatabase()->getInstConstantBody( f ), true ); + d_phase_reqs[f].initialize( d_qe->getTermUtil()->getInstConstantBody( f ), true ); } int selectLitScore = -1; for( std::map< Node, bool >::iterator it = d_phase_reqs[f].d_phase_reqs.begin(); it != d_phase_reqs[f].d_phase_reqs.end(); ++it ){ @@ -547,7 +548,7 @@ void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){ // constant definitions. bool isConst = true; std::vector< Node > uf_terms; - if( TermDb::hasInstConstAttr(n) ){ + if( TermUtil::hasInstConstAttr(n) ){ isConst = false; if( gn.getKind()==APPLY_UF ){ uf_terms.push_back( gn ); @@ -555,7 +556,7 @@ void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){ }else if( gn.getKind()==EQUAL ){ isConst = true; for( int j=0; j<2; j++ ){ - if( TermDb::hasInstConstAttr(n[j]) ){ + if( TermUtil::hasInstConstAttr(n[j]) ){ if( n[j].getKind()==APPLY_UF && fmig->d_uf_model_tree.find( gn[j].getOperator() )!=fmig->d_uf_model_tree.end() ){ uf_terms.push_back( gn[j] ); @@ -663,7 +664,7 @@ int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){ for( size_t i=0; i tr_terms; if( lit.getKind()==APPLY_UF ){ //only match predicates that are contrary to this one, use literal matching @@ -672,7 +673,7 @@ int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){ }else if( lit.getKind()==EQUAL ){ //collect trigger terms for( int j=0; j<2; j++ ){ - if( TermDb::hasInstConstAttr(lit[j]) ){ + if( TermUtil::hasInstConstAttr(lit[j]) ){ if( lit[j].getKind()==APPLY_UF ){ tr_terms.push_back( lit[j] ); }else{ diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 24c2d1254..081d4e66a 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -20,6 +20,7 @@ #include "theory/quantifiers/full_model_check.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/theory_engine.h" #include "theory/uf/equality_engine.h" #include "theory/uf/theory_uf.h" @@ -265,7 +266,7 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ if( Trace.isOn("fmf-exh-inst-debug") ){ Trace("fmf-exh-inst-debug") << " Instantiation Constants: "; for( size_t i=0; igetTermDatabase()->getInstantiationConstant( f, i ) << " "; + Trace("fmf-exh-inst-debug") << d_quantEngine->getTermUtil()->getInstantiationConstant( f, i ) << " "; } Trace("fmf-exh-inst-debug") << std::endl; } diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 20d470de3..0094bc147 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -9,7 +9,7 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief quant conflict find class + ** \brief Implements conflict-based instantiation (Reynolds et al FMCAD 2014) ** **/ @@ -21,6 +21,7 @@ #include "smt/smt_statistics_registry.h" #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers/trigger.h" #include "theory/quantifiers/first_order_model.h" #include "theory/theory_engine.h" @@ -596,7 +597,7 @@ bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node } Trace("qcf-instance-check") << "...evaluates to " << inst_eval << std::endl; } - if( inst_eval.isNull() || inst_eval==p->getTermDatabase()->d_true || !isPropagatingInstance( p, inst_eval ) ){ + if( inst_eval.isNull() || inst_eval==p->getTermUtil()->d_true || !isPropagatingInstance( p, inst_eval ) ){ Trace("qcf-instance-check") << "...spurious." << std::endl; return true; }else{ @@ -608,7 +609,7 @@ bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node //check constraints for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){ //apply substitution to the tconstraint - Node cons = p->getTermDatabase()->getInstantiatedNode( it->first, d_q, terms ); + Node cons = p->getTermUtil()->getInstantiatedNode( it->first, d_q, terms ); cons = it->second ? cons : cons.negate(); if( !entailmentTest( p, cons, p->d_effort==QuantConflictFind::effort_conflict ) ){ return true; @@ -1863,7 +1864,7 @@ void MatchGen::setInvalid() { } bool MatchGen::isHandledBoolConnective( TNode n ) { - return TermDb::isBoolConnectiveTerm( n ) && n.getKind()!=SEP_STAR; + return TermUtil::isBoolConnectiveTerm( n ) && n.getKind()!=SEP_STAR; } bool MatchGen::isHandledUfTerm( TNode n ) { @@ -2185,7 +2186,7 @@ void QuantConflictFind::computeRelevantEqr() { Node r = (*eqcs_i); if( getTermDatabase()->hasTermCurrent( r ) ){ TypeNode rtn = r.getType(); - if( !options::cbqi() || !TermDb::hasInstConstAttr( r ) ){ + if( !options::cbqi() || !TermUtil::hasInstConstAttr( r ) ){ d_eqcs[rtn].push_back( r ); } } diff --git a/src/theory/quantifiers/quant_equality_engine.cpp b/src/theory/quantifiers/quant_equality_engine.cpp index b40212872..dab95f83b 100644 --- a/src/theory/quantifiers/quant_equality_engine.cpp +++ b/src/theory/quantifiers/quant_equality_engine.cpp @@ -16,7 +16,7 @@ #include "theory/quantifiers/quant_equality_engine.h" #include "theory/rewriter.h" -#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" using namespace CVC4; using namespace std; @@ -94,11 +94,11 @@ void QuantEqualityEngine::assertNode( Node n ) { Node t1; Node t2; if( lit.getKind()==APPLY_UF || lit.getKind()==EQUAL ){ - lit = getTermDatabase()->getCanonicalTerm( lit ); + lit = getTermUtil()->getCanonicalTerm( lit ); Trace("qee-debug") << "Canonical : " << lit << ", pol = " << pol << std::endl; if( lit.getKind()==APPLY_UF ){ t1 = getFunctionAppForPredicateApp( lit ); - t2 = pol ? getTermDatabase()->d_one : getTermDatabase()->d_zero; + t2 = pol ? getTermUtil()->d_one : getTermUtil()->d_zero; pol = true; lit = NodeManager::currentNM()->mkNode( EQUAL, t1, t2 ); }else if( lit.getKind()==EQUAL ){ diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index b34abba13..1e30914ef 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/inst_match.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" using namespace std; @@ -48,6 +49,10 @@ quantifiers::TermDb * QuantifiersModule::getTermDatabase() { return d_quantEngine->getTermDatabase(); } +quantifiers::TermUtil * QuantifiersModule::getTermUtil() { + return d_quantEngine->getTermUtil(); +} + bool QuantArith::getMonomial( Node n, Node& c, Node& v ){ if( n.getKind()==MULT && n.getNumChildren()==2 && n[0].isConst() ){ c = n[0]; @@ -218,7 +223,7 @@ Node QuantArith::solveEqualityFor( Node lit, Node v ) { } } if( tn.isReal() ){ - if( quantifiers::TermDb::containsTerm( lit, v ) ){ + if( quantifiers::TermUtil::containsTerm( lit, v ) ){ std::map< Node, Node > msum; if( QuantArith::getMonomialSumLit( lit, msum ) ){ Node val, veqc; @@ -338,13 +343,13 @@ void QuantPhaseReq::initialize( Node n, bool computeEq ){ for( std::map< Node, bool >::iterator it = d_phase_reqs.begin(); it != d_phase_reqs.end(); ++it ){ Debug("inst-engine-phase-req") << " " << it->first << " -> " << it->second << std::endl; if( it->first.getKind()==EQUAL ){ - if( quantifiers::TermDb::hasInstConstAttr(it->first[0]) ){ - if( !quantifiers::TermDb::hasInstConstAttr(it->first[1]) ){ + if( quantifiers::TermUtil::hasInstConstAttr(it->first[0]) ){ + if( !quantifiers::TermUtil::hasInstConstAttr(it->first[1]) ){ d_phase_reqs_equality_term[ it->first[0] ] = it->first[1]; d_phase_reqs_equality[ it->first[0] ] = it->second; Debug("inst-engine-phase-req") << " " << it->first[0] << ( it->second ? " == " : " != " ) << it->first[1] << std::endl; } - }else if( quantifiers::TermDb::hasInstConstAttr(it->first[1]) ){ + }else if( quantifiers::TermUtil::hasInstConstAttr(it->first[1]) ){ d_phase_reqs_equality_term[ it->first[1] ] = it->first[0]; d_phase_reqs_equality[ it->first[1] ] = it->second; Debug("inst-engine-phase-req") << " " << it->first[1] << ( it->second ? " == " : " != " ) << it->first[0] << std::endl; diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index f46b73b1c..27e517649 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -30,6 +30,7 @@ class QuantifiersEngine; namespace quantifiers { class TermDb; + class TermUtil; } class QuantifiersModule { @@ -69,6 +70,7 @@ public: bool areEqual( TNode n1, TNode n2 ); TNode getRepresentative( TNode n ); quantifiers::TermDb * getTermDatabase(); + quantifiers::TermUtil * getTermUtil(); };/* class QuantifiersModule */ class QuantifiersUtil { diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index a9b1470fd..ac3fb85d1 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -14,8 +14,12 @@ #include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers_engine.h" #include "options/quantifiers_options.h" -#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/ce_guided_instantiation.h" +#include "theory/quantifiers/fun_def_engine.h" +#include "theory/quantifiers/rewrite_engine.h" +#include "theory/quantifiers/term_util.h" using namespace std; using namespace CVC4; @@ -24,7 +28,12 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; -void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n, std::vector< Node >& node_values, std::string str_value ){ +QuantAttributes::QuantAttributes( QuantifiersEngine * qe ) : +d_quantEngine(qe) { + +} + +void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::vector< Node >& node_values, std::string str_value ){ Trace("quant-attr-debug") << "Set " << attr << " " << n << std::endl; if( attr=="axiom" ){ Trace("quant-attr-debug") << "Set axiom " << n << std::endl; @@ -78,3 +87,298 @@ void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n, s n.setAttribute( qepa, true ); } } + +bool QuantAttributes::checkRewriteRule( Node q ) { + return !getRewriteRule( q ).isNull(); +} + +Node QuantAttributes::getRewriteRule( Node q ) { + if( q.getKind()==FORALL && q.getNumChildren()==3 && q[2].getNumChildren()>0 && q[2][0][0].getKind()==REWRITE_RULE ){ + return q[2][0][0]; + }else{ + return Node::null(); + } +} + +bool QuantAttributes::checkFunDef( Node q ) { + return !getFunDefHead( q ).isNull(); +} + +bool QuantAttributes::checkFunDefAnnotation( Node ipl ) { + if( !ipl.isNull() ){ + for( unsigned i=0; imkConst( pol ); + } + } + } + return Node::null(); +} + +bool QuantAttributes::checkSygusConjecture( Node q ) { + return ( q.getKind()==FORALL && q.getNumChildren()==3 ) ? checkSygusConjectureAnnotation( q[2] ) : false; +} + +bool QuantAttributes::checkSygusConjectureAnnotation( Node ipl ){ + if( !ipl.isNull() ){ + for( unsigned i=0; igetRewriteEngine()==NULL ){ + Trace("quant-warn") << "WARNING : rewrite engine is null, and we have : " << q << std::endl; + } + //set rewrite engine as owner + d_quantEngine->setOwner( q, d_quantEngine->getRewriteEngine(), 2 ); + } + if( d_qattr[q].isFunDef() ){ + Node f = d_qattr[q].d_fundef_f; + if( d_fun_defs.find( f )!=d_fun_defs.end() ){ + Message() << "Cannot define function " << f << " more than once." << std::endl; + exit( 1 ); + } + d_fun_defs[f] = true; + d_quantEngine->setOwner( q, d_quantEngine->getFunDefEngine(), 2 ); + } + if( d_qattr[q].d_sygus ){ + if( d_quantEngine->getCegInstantiation()==NULL ){ + Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl; + } + d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation(), 2 ); + } + if( d_qattr[q].d_synthesis ){ + if( d_quantEngine->getCegInstantiation()==NULL ){ + Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl; + } + d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation(), 2 ); + } +} + +void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){ + Trace("quant-attr-debug") << "Compute attributes for " << q << std::endl; + if( q.getNumChildren()==3 ){ + qa.d_ipl = q[2]; + for( unsigned i=0; i::iterator it = d_qattr.find( q ); + if( it==d_qattr.end() ){ + return false; + }else{ + return it->second.d_conjecture; + } +} + +bool QuantAttributes::isAxiom( Node q ) { + std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); + if( it==d_qattr.end() ){ + return false; + }else{ + return it->second.d_axiom; + } +} + +bool QuantAttributes::isFunDef( Node q ) { + std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); + if( it==d_qattr.end() ){ + return false; + }else{ + return it->second.isFunDef(); + } +} + +bool QuantAttributes::isSygus( Node q ) { + std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); + if( it==d_qattr.end() ){ + return false; + }else{ + return it->second.d_sygus; + } +} + +bool QuantAttributes::isSynthesis( Node q ) { + std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); + if( it==d_qattr.end() ){ + return false; + }else{ + return it->second.d_synthesis; + } +} + +int QuantAttributes::getQuantInstLevel( Node q ) { + std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); + if( it==d_qattr.end() ){ + return -1; + }else{ + return it->second.d_qinstLevel; + } +} + +int QuantAttributes::getRewriteRulePriority( Node q ) { + std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); + if( it==d_qattr.end() ){ + return -1; + }else{ + return it->second.d_rr_priority; + } +} + +bool QuantAttributes::isQuantElim( Node q ) { + std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); + if( it==d_qattr.end() ){ + return false; + }else{ + return it->second.d_quant_elim; + } +} + +bool QuantAttributes::isQuantElimPartial( Node q ) { + std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); + if( it==d_qattr.end() ){ + return false; + }else{ + return it->second.d_quant_elim_partial; + } +} + +int QuantAttributes::getQuantIdNum( Node q ) { + std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); + if( it!=d_qattr.end() ){ + if( !it->second.d_qid_num.isNull() ){ + return it->second.d_qid_num.getAttribute(QuantIdNumAttribute()); + } + } + return -1; +} + +Node QuantAttributes::getQuantIdNumNode( Node q ) { + std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); + if( it==d_qattr.end() ){ + return Node::null(); + }else{ + return it->second.d_qid_num; + } +} + diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index 93a4ef408..1c35b646b 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -16,29 +16,147 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H -#define __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H +#ifndef __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H +#define __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H -#include "theory/rewriter.h" -#include "theory/quantifiers_engine.h" +#include "expr/attribute.h" +#include "expr/node.h" namespace CVC4 { namespace theory { + +class QuantifiersEngine; + +/** Attribute true for quantifiers that are axioms */ +struct AxiomAttributeId {}; +typedef expr::Attribute< AxiomAttributeId, bool > AxiomAttribute; + +/** Attribute true for quantifiers that are conjecture */ +struct ConjectureAttributeId {}; +typedef expr::Attribute< ConjectureAttributeId, bool > ConjectureAttribute; + +/** Attribute true for function definition quantifiers */ +struct FunDefAttributeId {}; +typedef expr::Attribute< FunDefAttributeId, bool > FunDefAttribute; + +/** Attribute true for quantifiers that we are doing quantifier elimination on */ +struct QuantElimAttributeId {}; +typedef expr::Attribute< QuantElimAttributeId, bool > QuantElimAttribute; + +/** Attribute true for quantifiers that we are doing partial quantifier elimination on */ +struct QuantElimPartialAttributeId {}; +typedef expr::Attribute< QuantElimPartialAttributeId, bool > QuantElimPartialAttribute; + +/** Attribute true for quantifiers that are SyGus conjectures */ +struct SygusAttributeId {}; +typedef expr::Attribute< SygusAttributeId, bool > SygusAttribute; + +/** Attribute true for quantifiers that are synthesis conjectures */ +struct SynthesisAttributeId {}; +typedef expr::Attribute< SynthesisAttributeId, bool > SynthesisAttribute; + namespace quantifiers { /** Attribute priority for rewrite rules */ //struct RrPriorityAttributeId {}; //typedef expr::Attribute< RrPriorityAttributeId, uint64_t > RrPriorityAttribute; -struct QuantifiersAttributes + +/** This class stores attributes for quantified formulas +* TODO : document (as part of #1171, #1215) +*/ +class QAttributes{ +public: + QAttributes() : d_hasPattern(false), d_conjecture(false), d_axiom(false), d_sygus(false), + d_synthesis(false), d_rr_priority(-1), d_qinstLevel(-1), d_quant_elim(false), d_quant_elim_partial(false){} + ~QAttributes(){} + bool d_hasPattern; + Node d_rr; + bool d_conjecture; + bool d_axiom; + Node d_fundef_f; + bool d_sygus; + bool d_synthesis; + int d_rr_priority; + int d_qinstLevel; + bool d_quant_elim; + bool d_quant_elim_partial; + Node d_ipl; + Node d_qid_num; + bool isRewriteRule() { return !d_rr.isNull(); } + bool isFunDef() { return !d_fundef_f.isNull(); } +}; + +/** This class caches information about attributes of quantified formulas +* It also has static utility functions used for determining attributes and information about +* quantified formulas. +*/ +class QuantAttributes { +public: + QuantAttributes( QuantifiersEngine * qe ); + ~QuantAttributes(){} + /** set user attribute * This function will apply a custom set of attributes to all top-level universal * quantifiers contained in n */ static void setUserAttribute( const std::string& attr, Node n, std::vector< Node >& node_values, std::string str_value ); -}; + + //general queries concerning quantified formulas wrt modules + /** is quantifier treated as a rewrite rule? */ + static bool checkRewriteRule( Node q ); + /** get the rewrite rule associated with the quanfied formula */ + static Node getRewriteRule( Node q ); + /** is fun def */ + static bool checkFunDef( Node q ); + /** is fun def */ + static bool checkFunDefAnnotation( Node ipl ); + /** is sygus conjecture */ + static bool checkSygusConjecture( Node q ); + /** is sygus conjecture */ + static bool checkSygusConjectureAnnotation( Node ipl ); + /** get fun def body */ + static Node getFunDefHead( Node q ); + /** get fun def body */ + static Node getFunDefBody( Node q ); + /** is quant elim annotation */ + static bool checkQuantElimAnnotation( Node ipl ); + /** is conjecture */ + bool isConjecture( Node q ); + /** is axiom */ + bool isAxiom( Node q ); + /** is function definition */ + bool isFunDef( Node q ); + /** is sygus conjecture */ + bool isSygus( Node q ); + /** is synthesis conjecture */ + bool isSynthesis( Node q ); + /** get instantiation level */ + int getQuantInstLevel( Node q ); + /** get rewrite rule priority */ + int getRewriteRulePriority( Node q ); + /** is quant elim */ + bool isQuantElim( Node q ); + /** is quant elim partial */ + bool isQuantElimPartial( Node q ); + /** get quant id num */ + int getQuantIdNum( Node q ); + /** get quant id num */ + Node getQuantIdNumNode( Node q ); + /** compute quantifier attributes */ + static void computeQuantAttributes( Node q, QAttributes& qa ); + /** compute the attributes for q */ + void computeAttributes( Node q ); +private: + /** pointer to quantifiers engine */ + QuantifiersEngine * d_quantEngine; + /** cache of attributes */ + std::map< Node, QAttributes > d_qattr; + /** function definitions */ + std::map< Node, bool > d_fun_defs; +}; } } diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 02f1b8509..9f6617d5a 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -15,7 +15,9 @@ #include "theory/quantifiers/quantifiers_rewriter.h" #include "options/quantifiers_options.h" +#include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers/trigger.h" using namespace std; @@ -196,7 +198,7 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { }else{ //compute attributes QAttributes qa; - TermDb::computeQuantAttributes( in, qa ); + QuantAttributes::computeQuantAttributes( in, qa ); if( !qa.isRewriteRule() ){ for( int op=0; op& n std::map< Node, Node > cache; std::map< Node, Node > icache; if( qa.isFunDef() ){ - Node h = TermDb::getFunDefHead( q ); + Node h = QuantAttributes::getFunDefHead( q ); Assert( !h.isNull() ); // if it is a function definition, rewrite the body independently - Node fbody = TermDb::getFunDefBody( q ); + Node fbody = QuantAttributes::getFunDefBody( q ); Assert( !body.isNull() ); Trace("quantifiers-rewrite-debug") << "Decompose " << h << " / " << fbody << " as function definition for " << q << "." << std::endl; Node r = computeProcessTerms2( fbody, true, true, curr_cond, 0, cache, icache, new_vars, new_conds, false ); @@ -745,7 +747,7 @@ bool QuantifiersRewriter::isConditionalVariableElim( Node n, int pol ){ }else if( n.getKind()==EQUAL ){ for( unsigned i=0; i<2; i++ ){ if( n[i].getKind()==BOUND_VARIABLE ){ - if( !TermDb::containsTerm( n[1-i], n[i] ) ){ + if( !TermUtil::containsTerm( n[1-i], n[i] ) ){ return true; } } @@ -843,7 +845,7 @@ Node QuantifiersRewriter::computeCondSplit( Node body, QAttributes& qa ){ } bool QuantifiersRewriter::isVariableElim( Node v, Node s ) { - if( TermDb::containsTerm( s, v ) || !s.getType().isSubtypeOf( v.getType() ) ){ + if( TermUtil::containsTerm( s, v ) || !s.getType().isSubtypeOf( v.getType() ) ){ return false; }else{ return true; @@ -973,7 +975,7 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto if( lit.getKind()==GEQ || lit.getKind()==GT ){ //compute variables in itm->first, these are not eligible for elimination std::vector< Node > bvs; - TermDb::getBoundVars( itm->first, bvs ); + TermUtil::getBoundVars( itm->first, bvs ); for( unsigned j=0; j& args, Node bo NodeBuilder<> tb(kind::OR); for( unsigned i=0; i sub_vars; //return skolemized body - return TermDb::mkSkolemizedBody( n, nn, fvTypes, fvs, sk, sub, sub_vars ); + return TermUtil::mkSkolemizedBody( n, nn, fvTypes, fvs, sk, sub, sub_vars ); } }else{ //check if it contains a quantifier as a subterm diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 9bc47a507..749026b66 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers_engine.h" #include "theory/quantifiers/relevant_domain.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers/first_order_model.h" using namespace std; @@ -54,7 +55,7 @@ void RelevantDomain::RDomain::removeRedundantTerms( QuantifiersEngine * qe ) { std::map< Node, Node > rterms; for( unsigned i=0; igetEqualityQuery()->getRepresentative( d_terms[i] ); } if( rterms.find( r )==rterms.end() ){ @@ -108,7 +109,7 @@ void RelevantDomain::compute(){ FirstOrderModel* fm = d_qe->getModel(); for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ Node q = fm->getAssertedQuantifier( i ); - Node icf = d_qe->getTermDatabase()->getInstConstantBody( q ); + Node icf = d_qe->getTermUtil()->getInstConstantBody( q ); Trace("rel-dom-debug") << "compute relevant domain for " << icf << std::endl; computeRelevantDomain( q, icf, true, true ); } @@ -173,7 +174,7 @@ void RelevantDomain::computeRelevantDomain( Node q, Node n, bool hasPol, bool po } } - if( ( ( n.getKind()==EQUAL && !n[0].getType().isBoolean() ) || n.getKind()==GEQ ) && TermDb::hasInstConstAttr( n ) ){ + if( ( ( n.getKind()==EQUAL && !n[0].getType().isBoolean() ) || n.getKind()==GEQ ) && TermUtil::hasInstConstAttr( n ) ){ //compute the information for what this literal does computeRelevantDomainLit( q, hasPol, pol, n ); if( d_rel_dom_lit[hasPol][pol][n].d_merge ){ @@ -197,16 +198,16 @@ void RelevantDomain::computeRelevantDomain( Node q, Node n, bool hasPol, bool po void RelevantDomain::computeRelevantDomainOpCh( RDomain * rf, Node n ) { if( n.getKind()==INST_CONSTANT ){ - Node q = d_qe->getTermDatabase()->getInstConstAttr( n ); + Node q = d_qe->getTermUtil()->getInstConstAttr( n ); //merge the RDomains unsigned id = n.getAttribute(InstVarNumAttribute()); Trace("rel-dom-debug") << n << " is variable # " << id << " for " << q; - Trace("rel-dom-debug") << " with body : " << d_qe->getTermDatabase()->getInstConstantBody( q ) << std::endl; + Trace("rel-dom-debug") << " with body : " << d_qe->getTermUtil()->getInstConstantBody( q ) << std::endl; RDomain * rq = getRDomain( q, id ); if( rf!=rq ){ rq->merge( rf ); } - }else if( !TermDb::hasInstConstAttr( n ) ){ + }else if( !TermUtil::hasInstConstAttr( n ) ){ Trace("rel-dom-debug") << "...add ground term to rel dom " << n << std::endl; //term to add rf->addTerm( n ); @@ -289,7 +290,7 @@ void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, No if( hasPol && !pol ){ d_rel_dom_lit[hasPol][pol][n].d_merge = false; } - }else if( !r_add.isNull() && !TermDb::hasInstConstAttr( r_add ) ){ + }else if( !r_add.isNull() && !TermUtil::hasInstConstAttr( r_add ) ){ Trace("rel-dom-debug") << "...add term " << r_add << ", pol = " << pol << ", kind = " << n.getKind() << std::endl; //the negative occurrence adds the term to the domain if( !hasPol || !pol ){ diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index f60d27cb9..d852667de 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -20,9 +20,11 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/inst_match_generator.h" #include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quant_conflict_find.h" #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/theory_engine.h" using namespace CVC4; @@ -44,7 +46,7 @@ RewriteEngine::RewriteEngine( context::Context* c, QuantifiersEngine* qe ) : Qua } double RewriteEngine::getPriority( Node f ) { - Node rr = TermDb::getRewriteRule( f ); + Node rr = QuantAttributes::getRewriteRule( f ); Node rrr = rr[2]; Trace("rr-priority") << "Get priority : " << rrr << " " << rrr.getKind() << std::endl; bool deterministic = rrr[1].getKind()!=OR; @@ -121,7 +123,7 @@ int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) { if( it!=d_qinfo.end() ){ QuantInfo * qi = &it->second; if( qi->matchGeneratorIsValid() ){ - Node rr = TermDb::getRewriteRule( f ); + Node rr = QuantAttributes::getRewriteRule( f ); Trace("rewrite-engine-inst-debug") << " Reset round..." << std::endl; qi->reset_round( qcf ); Trace("rewrite-engine-inst-debug") << " Get matches..." << std::endl; @@ -211,7 +213,7 @@ int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) { } void RewriteEngine::registerQuantifier( Node f ) { - Node rr = TermDb::getRewriteRule( f ); + Node rr = QuantAttributes::getRewriteRule( f ); if( !rr.isNull() ){ Trace("rr-register") << "Register quantifier " << f << std::endl; Trace("rr-register") << " rewrite rule is : " << rr << std::endl; @@ -262,7 +264,7 @@ void RewriteEngine::registerQuantifier( Node f ) { body_c.push_back( d_rr[f][1][j].negate() ); } } - }else if( d_rr[f][1]!=d_quantEngine->getTermDatabase()->d_true ){ + }else if( d_rr[f][1]!=d_quantEngine->getTermUtil()->d_true ){ if( MatchGen::isHandled( d_rr[f][1] ) ){ body_c.push_back( d_rr[f][1].negate() ); } @@ -291,7 +293,7 @@ bool RewriteEngine::checkCompleteFor( Node q ) { Node RewriteEngine::getInstConstNode( Node n, Node q ) { std::map< Node, Node >::iterator it = d_inst_const_node[q].find( n ); if( it==d_inst_const_node[q].end() ){ - Node nn = d_quantEngine->getTermDatabase()->getInstConstantNode( n, q ); + Node nn = d_quantEngine->getTermUtil()->getInstConstantNode( n, q ); d_inst_const_node[q][n] = nn; return nn; }else{ diff --git a/src/theory/quantifiers/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus_grammar_cons.cpp index 194e32b61..2eb541e66 100644 --- a/src/theory/quantifiers/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus_grammar_cons.cpp @@ -19,6 +19,7 @@ #include "expr/datatype.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/term_database_sygus.h" +#include "theory/quantifiers/term_util.h" using namespace CVC4::kind; using namespace std; @@ -559,7 +560,7 @@ TypeNode CegGrammarConstructor::mkSygusTemplateTypeRec( Node templ, Node templ_a Node op; std::vector< Type > argTypes; if( templ.getNumChildren()==0 ){ - // TODO : can short circuit to this case when !TermDb::containsTerm( templ, templ_arg ) + // TODO : can short circuit to this case when !TermUtil::containsTerm( templ, templ_arg ) op = templ; }else{ Assert( templ.hasOperator() ); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 79fdf8791..d4a71e43c 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -22,10 +22,12 @@ #include "theory/quantifiers/ce_guided_instantiation.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fun_def_engine.h" +#include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/rewrite_engine.h" #include "theory/quantifiers/theory_quantifiers.h" #include "theory/quantifiers/trigger.h" #include "theory/quantifiers/term_database_sygus.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" @@ -84,22 +86,21 @@ void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) { TermDb::TermDb(context::Context* c, context::UserContext* u, QuantifiersEngine* qe) : d_quantEngine(qe), - d_inactive_map(c), - d_op_id_count(0), - d_typ_id_count(0), - d_sygus_tdb(NULL) { + d_inactive_map(c) { d_consistent_ee = true; d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); - d_zero = NodeManager::currentNM()->mkConst(Rational(0)); - d_one = NodeManager::currentNM()->mkConst(Rational(1)); - if (options::ceGuidedInst()) { - d_sygus_tdb = new TermDbSygus(c, qe); - } } + TermDb::~TermDb(){ - if(d_sygus_tdb) { - delete d_sygus_tdb; + +} + +void TermDb::registerQuantifier( Node q ) { + Assert( q[0].getNumChildren()==d_quantEngine->getTermUtil()->getNumInstantiationConstants( q ) ); + for( unsigned i=0; igetTermUtil()->getInstantiationConstant( q, i ); + setTermInactive( ic ); } } @@ -165,7 +166,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi bool rec = false; if( d_processed.find( n )==d_processed.end() ){ d_processed.insert(n); - if( !TermDb::hasInstConstAttr(n) ){ + if( !TermUtil::hasInstConstAttr(n) ){ Trace("term-db-debug") << "register term : " << n << std::endl; d_type_map[ n.getType() ].push_back( n ); //if this is an atomic trigger, consider adding it @@ -180,8 +181,8 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi d_op_map[op].push_back( n ); added.insert( n ); - if( d_sygus_tdb ){ - d_sygus_tdb->registerEvalTerm( n ); + if( d_quantEngine->getTermDatabaseSygus() ){ + d_quantEngine->getTermDatabaseSygus()->registerEvalTerm( n ); } } }else{ @@ -660,7 +661,7 @@ bool TermDb::isTermEligibleForInstantiation( TNode n, TNode f, bool print ) { } if( options::instMaxLevel()!=-1 ){ if( n.hasAttribute(InstLevelAttribute()) ){ - int fml = f.isNull() ? -1 : getQAttrQuantInstLevel( f ); + int fml = f.isNull() ? -1 : d_quantEngine->getQuantAttributes()->getQuantInstLevel( f ); unsigned ml = fml>=0 ? fml : options::instMaxLevel(); if( n.getAttribute(InstLevelAttribute())>ml ){ @@ -882,12 +883,13 @@ TNode TermDb::getCongruentTerm( Node f, std::vector< TNode >& args ) { return d_func_map_trie[f].existsTerm( args ); } + Node TermDb::getModelBasisTerm( TypeNode tn, int i ){ if( d_model_basis_term.find( tn )==d_model_basis_term.end() ){ Node mbt; if( tn.isInteger() || tn.isReal() ){ - mbt = d_zero; - }else if( isClosedEnumerableType( tn ) ){ + mbt = NodeManager::currentNM()->mkConst(Rational(0)); + }else if( d_quantEngine->getTermUtil()->isClosedEnumerableType( tn ) ){ mbt = tn.mkGroundTerm(); }else{ if( options::fmfFreshDistConst() || d_type_map[ tn ].empty() ){ @@ -935,14 +937,15 @@ Node TermDb::getModelBasis( Node q, Node n ){ d_model_basis_terms[q].push_back( getModelBasisTerm( q[0][j].getType() ) ); } } - Node gn = n.substitute( d_inst_constants[q].begin(), d_inst_constants[q].end(), + Node gn = n.substitute( d_quantEngine->getTermUtil()->d_inst_constants[q].begin(), + d_quantEngine->getTermUtil()->d_inst_constants[q].end(), d_model_basis_terms[q].begin(), d_model_basis_terms[q].end() ); return gn; } Node TermDb::getModelBasisBody( Node q ){ if( d_model_basis_body.find( q )==d_model_basis_body.end() ){ - Node n = getInstConstantBody( q ); + Node n = d_quantEngine->getTermUtil()->getInstConstantBody( q ); d_model_basis_body[q] = getModelBasis( q, n ); } return d_model_basis_body[q]; @@ -966,1440 +969,6 @@ void TermDb::computeModelBasisArgAttribute( Node n ){ } } -void TermDb::makeInstantiationConstantsFor( Node q ){ - if( d_inst_constants.find( q )==d_inst_constants.end() ){ - Debug("quantifiers-engine") << "Instantiation constants for " << q << " : " << std::endl; - for( unsigned i=0; imkInstConstant( q[0][i].getType() ); - d_inst_constants_map[ic] = q; - d_inst_constants[ q ].push_back( ic ); - Debug("quantifiers-engine") << " " << ic << std::endl; - //set the var number attribute - InstVarNumAttribute ivna; - ic.setAttribute( ivna, i ); - InstConstantAttribute ica; - ic.setAttribute( ica, q ); - //also set the term inactive - setTermInactive( ic ); - } - } -} - -void TermDb::getBoundVars2( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited ) { - if( visited.find( n )==visited.end() ){ - visited[n] = true; - if( n.getKind()==BOUND_VARIABLE ){ - if( std::find( vars.begin(), vars.end(), n )==vars.end() ) { - vars.push_back( n ); - } - } - for( unsigned i=0; i& visited ) { - std::map< Node, Node >::iterator it = visited.find( n ); - if( it!=visited.end() ){ - return it->second; - }else{ - Node ret = n; - if( n.getKind()==FORALL ){ - ret = getRemoveQuantifiers2( n[1], visited ); - }else if( n.getNumChildren()>0 ){ - std::vector< Node > children; - bool childrenChanged = false; - for( unsigned i=0; imkNode( n.getKind(), children ); - } - } - visited[n] = ret; - return ret; - } -} - -Node TermDb::getInstConstAttr( Node n ) { - if (!n.hasAttribute(InstConstantAttribute()) ){ - Node q; - for( unsigned i=0; i& vars ) { - std::map< Node, bool > visited; - return getBoundVars2( n, vars, visited ); -} - -//remove quantifiers -Node TermDb::getRemoveQuantifiers( Node n ) { - std::map< Node, Node > visited; - return getRemoveQuantifiers2( n, visited ); -} - -//quantified simplify -Node TermDb::getQuantSimplify( Node n ) { - std::vector< Node > bvs; - getBoundVars( n, bvs ); - if( bvs.empty() ) { - return Rewriter::rewrite( n ); - }else{ - Node q = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs ), n ); - q = Rewriter::rewrite( q ); - return getRemoveQuantifiers( q ); - } -} - -/** get the i^th instantiation constant of q */ -Node TermDb::getInstantiationConstant( Node q, int i ) const { - std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q ); - if( it!=d_inst_constants.end() ){ - return it->second[i]; - }else{ - return Node::null(); - } -} - -/** get number of instantiation constants for q */ -unsigned TermDb::getNumInstantiationConstants( Node q ) const { - std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q ); - if( it!=d_inst_constants.end() ){ - return it->second.size(); - }else{ - return 0; - } -} - -Node TermDb::getInstConstantBody( Node q ){ - std::map< Node, Node >::iterator it = d_inst_const_body.find( q ); - if( it==d_inst_const_body.end() ){ - Node n = getInstConstantNode( q[1], q ); - d_inst_const_body[ q ] = n; - return n; - }else{ - return it->second; - } -} - -Node TermDb::getCounterexampleLiteral( Node q ){ - if( d_ce_lit.find( q )==d_ce_lit.end() ){ - /* - Node ceBody = getInstConstantBody( f ); - //check if any variable are of bad types, and fail if so - for( size_t i=0; imkSkolem( "g", NodeManager::currentNM()->booleanType() ); - //otherwise, ensure literal - Node ceLit = d_quantEngine->getValuation().ensureLiteral( g ); - d_ce_lit[ q ] = ceLit; - } - return d_ce_lit[ q ]; -} - -Node TermDb::getInstConstantNode( Node n, Node q ){ - makeInstantiationConstantsFor( q ); - return n.substitute( d_vars[q].begin(), d_vars[q].end(), d_inst_constants[q].begin(), d_inst_constants[q].end() ); -} - -Node TermDb::getVariableNode( Node n, Node q ) { - makeInstantiationConstantsFor( q ); - return n.substitute( d_inst_constants[q].begin(), d_inst_constants[q].end(), d_vars[q].begin(), d_vars[q].end() ); -} - -Node TermDb::getInstantiatedNode( Node n, Node q, std::vector< Node >& terms ) { - Assert( d_vars[q].size()==terms.size() ); - return n.substitute( d_vars[q].begin(), d_vars[q].end(), terms.begin(), terms.end() ); -} - - -void getSelfSel( const Datatype& dt, const DatatypeConstructor& dc, Node n, TypeNode ntn, std::vector< Node >& selfSel ){ - TypeNode tspec; - if( dt.isParametric() ){ - tspec = TypeNode::fromType( dc.getSpecializedConstructorType(n.getType().toType()) ); - Trace("sk-ind-debug") << "Specialized constructor type : " << tspec << std::endl; - Assert( tspec.getNumChildren()==dc.getNumArgs() ); - } - Trace("sk-ind-debug") << "Check self sel " << dc.getName() << " " << dt.getName() << std::endl; - for( unsigned j=0; j ssc; - if( dt.isParametric() ){ - Trace("sk-ind-debug") << "Compare " << tspec[j] << " " << ntn << std::endl; - if( tspec[j]==ntn ){ - ssc.push_back( n ); - } - }else{ - TypeNode tn = TypeNode::fromType( dc[j].getRangeType() ); - Trace("sk-ind-debug") << "Compare " << tn << " " << ntn << std::endl; - if( tn==ntn ){ - ssc.push_back( n ); - } - } - /* TODO: more than weak structural induction - else if( tn.isDatatype() && std::find( visited.begin(), visited.end(), tn )==visited.end() ){ - visited.push_back( tn ); - const Datatype& dt = ((DatatypeType)(subs[0].getType()).toType()).getDatatype(); - std::vector< Node > disj; - for( unsigned i=0; imkNode( APPLY_SELECTOR_TOTAL, dc.getSelectorInternal( n.getType().toType(), j ), n ); - if( std::find( selfSel.begin(), selfSel.end(), ss )==selfSel.end() ){ - selfSel.push_back( ss ); - } - } - } -} - - -Node TermDb::mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& argTypes, std::vector< TNode >& fvs, - std::vector< Node >& sk, Node& sub, std::vector< unsigned >& sub_vars ) { - Assert( sk.empty() || sk.size()==f[0].getNumChildren() ); - //calculate the variables and substitution - std::vector< TNode > ind_vars; - std::vector< unsigned > ind_var_indicies; - std::vector< TNode > vars; - std::vector< unsigned > var_indicies; - for( unsigned i=0; i=sk.size() ){ - if( argTypes.empty() ){ - s = NodeManager::currentNM()->mkSkolem( "skv", f[0][i].getType(), "created during skolemization" ); - }else{ - TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, f[0][i].getType() ); - Node op = NodeManager::currentNM()->mkSkolem( "skop", typ, "op created during pre-skolemization" ); - //DOTHIS: set attribute on op, marking that it should not be selected as trigger - std::vector< Node > funcArgs; - funcArgs.push_back( op ); - funcArgs.insert( funcArgs.end(), fvs.begin(), fvs.end() ); - s = NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs ); - } - sk.push_back( s ); - }else{ - Assert( sk[i].getType()==f[0][i].getType() ); - } - } - Node ret; - if( vars.empty() ){ - ret = n; - }else{ - std::vector< Node > var_sk; - for( unsigned i=0; i ~P( x ) ) - if( options::dtStcInduction() && tn.isDatatype() ){ - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - std::vector< Node > disj; - for( unsigned i=0; i selfSel; - getSelfSel( dt, dt[i], k, tn, selfSel ); - std::vector< Node > conj; - conj.push_back( NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), k ).negate() ); - for( unsigned j=0; jmkNode( OR, conj ) ); - } - Assert( !disj.empty() ); - n_str_ind = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( AND, disj ); - }else if( options::intWfInduction() && tn.isInteger() ){ - Node icond = NodeManager::currentNM()->mkNode( GEQ, k, NodeManager::currentNM()->mkConst( Rational(0) ) ); - Node iret = ret.substitute( ind_vars[0], NodeManager::currentNM()->mkNode( MINUS, k, NodeManager::currentNM()->mkConst( Rational(1) ) ) ).negate(); - n_str_ind = NodeManager::currentNM()->mkNode( OR, icond.negate(), iret ); - n_str_ind = NodeManager::currentNM()->mkNode( AND, icond, n_str_ind ); - }else{ - Trace("sk-ind") << "Unknown induction for term : " << ind_vars[0] << ", type = " << tn << std::endl; - Assert( false ); - } - Trace("sk-ind") << "Strengthening is : " << n_str_ind << std::endl; - - std::vector< Node > rem_ind_vars; - rem_ind_vars.insert( rem_ind_vars.end(), ind_vars.begin()+1, ind_vars.end() ); - if( !rem_ind_vars.empty() ){ - Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, rem_ind_vars ); - nret = NodeManager::currentNM()->mkNode( FORALL, bvl, nret ); - nret = Rewriter::rewrite( nret ); - sub = nret; - sub_vars.insert( sub_vars.end(), ind_var_indicies.begin()+1, ind_var_indicies.end() ); - n_str_ind = NodeManager::currentNM()->mkNode( FORALL, bvl, n_str_ind.negate() ).negate(); - } - ret = NodeManager::currentNM()->mkNode( OR, nret, n_str_ind ); - } - Trace("quantifiers-sk-debug") << "mkSkolem body for " << f << " returns : " << ret << std::endl; - //if it has an instantiation level, set the skolemized body to that level - if( f.hasAttribute(InstLevelAttribute()) ){ - theory::QuantifiersEngine::setInstantiationLevelAttr( ret, f.getAttribute(InstLevelAttribute()) ); - } - - if( Trace.isOn("quantifiers-sk") ){ - Trace("quantifiers-sk") << "Skolemize : "; - for( unsigned i=0; i fvTypes; - std::vector< TNode > fvs; - Node sub; - std::vector< unsigned > sub_vars; - d_skolem_body[ f ] = mkSkolemizedBody( f, f[1], fvTypes, fvs, d_skolem_constants[f], sub, sub_vars ); - //store sub quantifier information - if( !sub.isNull() ){ - //if we are skolemizing one at a time, we already know the skolem constants of the sub-quantified formula, store them - Assert( d_skolem_constants[sub].empty() ); - for( unsigned i=0; igetTheoryEngine()->getSortInference()->setSkolemVar( f, f[0][i], d_skolem_constants[f][i] ); - } - } - } - return d_skolem_body[ f ]; -} - -Node TermDb::getEnumerateTerm( TypeNode tn, unsigned index ) { - Trace("term-db-enum") << "Get enumerate term " << tn << " " << index << std::endl; - std::map< TypeNode, unsigned >::iterator it = d_typ_enum_map.find( tn ); - unsigned teIndex; - if( it==d_typ_enum_map.end() ){ - teIndex = (int)d_typ_enum.size(); - d_typ_enum_map[tn] = teIndex; - d_typ_enum.push_back( TypeEnumerator(tn) ); - }else{ - teIndex = it->second; - } - while( index>=d_enum_terms[tn].size() ){ - if( d_typ_enum[teIndex].isFinished() ){ - return Node::null(); - } - d_enum_terms[tn].push_back( *d_typ_enum[teIndex] ); - ++d_typ_enum[teIndex]; - } - return d_enum_terms[tn][index]; -} - -bool TermDb::isClosedEnumerableType( TypeNode tn ) { - std::map< TypeNode, bool >::iterator it = d_typ_closed_enum.find( tn ); - if( it==d_typ_closed_enum.end() ){ - d_typ_closed_enum[tn] = true; - bool ret = true; - if( tn.isArray() || tn.isSort() || tn.isCodatatype() || tn.isFunction() ){ - ret = false; - }else if( tn.isSet() ){ - ret = isClosedEnumerableType( tn.getSetElementType() ); - }else if( tn.isDatatype() ){ - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - for( unsigned i=0; isecond; - } -} - -//checks whether a type is not Array and is reasonably small enough (<1000) such that all of its domain elements can be enumerated -bool TermDb::mayComplete( TypeNode tn ) { - std::map< TypeNode, bool >::iterator it = d_may_complete.find( tn ); - if( it==d_may_complete.end() ){ - bool mc = false; - if( isClosedEnumerableType( tn ) && tn.getCardinality().isFinite() && !tn.getCardinality().isLargeFinite() ){ - Node card = NodeManager::currentNM()->mkConst( Rational(tn.getCardinality().getFiniteCardinality()) ); - Node oth = NodeManager::currentNM()->mkConst( Rational(1000) ); - Node eq = NodeManager::currentNM()->mkNode( LEQ, card, oth ); - eq = Rewriter::rewrite( eq ); - mc = eq==d_true; - } - d_may_complete[tn] = mc; - return mc; - }else{ - return it->second; - } -} - -void TermDb::computeVarContains( Node n, std::vector< Node >& varContains ) { - std::map< Node, bool > visited; - computeVarContains2( n, INST_CONSTANT, varContains, visited ); -} - -void TermDb::computeQuantContains( Node n, std::vector< Node >& quantContains ) { - std::map< Node, bool > visited; - computeVarContains2( n, FORALL, quantContains, visited ); -} - - -void TermDb::computeVarContains2( Node n, Kind k, std::vector< Node >& varContains, std::map< Node, bool >& visited ){ - if( visited.find( n )==visited.end() ){ - visited[n] = true; - if( n.getKind()==k ){ - if( std::find( varContains.begin(), varContains.end(), n )==varContains.end() ){ - varContains.push_back( n ); - } - }else{ - for( unsigned i=0; i& pats, std::map< Node, std::vector< Node > >& varContains ){ - for( unsigned i=0; i& varContains ){ - std::vector< Node > vars; - computeVarContains( n, vars ); - for( unsigned j=0; j& varContains1, std::vector< Node >& varContains2 ){ - if( n1==n2 ){ - return 1; - }else if( n1.getKind()==n2.getKind() ){ - if( n1.getKind()==APPLY_UF ){ - if( n1.getOperator()==n2.getOperator() ){ - int result = 0; - for( int i=0; i<(int)n1.getNumChildren(); i++ ){ - if( n1[i]!=n2[i] ){ - int cResult = isInstanceOf2( n1[i], n2[i], varContains1, varContains2 ); - if( cResult==0 ){ - return 0; - }else if( cResult!=result ){ - if( result!=0 ){ - return 0; - }else{ - result = cResult; - } - } - } - } - return result; - } - } - return 0; - }else if( n2.getKind()==INST_CONSTANT ){ - //if( std::find( d_var_contains[ n1 ].begin(), d_var_contains[ n1 ].end(), n2 )!=d_var_contains[ n1 ].end() ){ - // return 1; - //} - if( varContains1.size()==1 && varContains1[ 0 ]==n2 ){ - return 1; - } - }else if( n1.getKind()==INST_CONSTANT ){ - //if( std::find( d_var_contains[ n2 ].begin(), d_var_contains[ n2 ].end(), n1 )!=d_var_contains[ n2 ].end() ){ - // return -1; - //} - if( varContains2.size()==1 && varContains2[ 0 ]==n1 ){ - return 1; - } - } - return 0; -} - -int TermDb::isInstanceOf( Node n1, Node n2 ){ - std::vector< Node > varContains1; - std::vector< Node > varContains2; - computeVarContains( n1, varContains1 ); - computeVarContains( n1, varContains2 ); - return isInstanceOf2( n1, n2, varContains1, varContains2 ); -} - -bool TermDb::isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs ){ - if( n1==n2 ){ - return true; - }else if( n2.getKind()==INST_CONSTANT ){ - //if( !node_contains( n1, n2 ) ){ - // return false; - //} - if( subs.find( n2 )==subs.end() ){ - subs[n2] = n1; - }else if( subs[n2]!=n1 ){ - return false; - } - return true; - }else if( n1.getKind()==n2.getKind() && n1.getMetaKind()==kind::metakind::PARAMETERIZED ){ - if( n1.getOperator()!=n2.getOperator() ){ - return false; - } - for( int i=0; i<(int)n1.getNumChildren(); i++ ){ - if( !isUnifiableInstanceOf( n1[i], n2[i], subs ) ){ - return false; - } - } - return true; - }else{ - return false; - } -} - -void TermDb::filterInstances( std::vector< Node >& nodes ){ - std::vector< bool > active; - active.resize( nodes.size(), true ); - std::map< int, std::vector< Node > > varContains; - for( unsigned i=0; i temp; - for( unsigned i=0; i::iterator it = d_op_id.find( op ); - if( it==d_op_id.end() ){ - d_op_id[op] = d_op_id_count; - d_op_id_count++; - return d_op_id[op]; - }else{ - return it->second; - } -} - -int TermDb::getIdForType( TypeNode t ) { - std::map< TypeNode, int >::iterator it = d_typ_id.find( t ); - if( it==d_typ_id.end() ){ - d_typ_id[t] = d_typ_id_count; - d_typ_id_count++; - return d_typ_id[t]; - }else{ - return it->second; - } -} - -bool TermDb::getTermOrder( Node a, Node b ) { - if( a.getKind()==BOUND_VARIABLE ){ - if( b.getKind()==BOUND_VARIABLE ){ - return a.getAttribute(InstVarNumAttribute())mkBoundVar( os.str().c_str(), tn ); - InstVarNumAttribute ivna; - x.setAttribute(ivna,d_cn_free_var[tn].size()); - d_cn_free_var[tn].push_back( x ); - } - return d_cn_free_var[tn][i]; -} - -struct sortTermOrder { - TermDb* d_tdb; - //std::map< Node, std::map< Node, bool > > d_cache; - bool operator() (Node i, Node j) { - /* - //must consult cache since term order is partial? - std::map< Node, bool >::iterator it = d_cache[j].find( i ); - if( it!=d_cache[j].end() && it->second ){ - return false; - }else{ - bool ret = d_tdb->getTermOrder( i, j ); - d_cache[i][j] = ret; - return ret; - } - */ - return d_tdb->getTermOrder( i, j ); - } -}; - -//this function makes a canonical representation of a term ( -// - orders variables left to right -// - if apply_torder, then sort direct subterms of commutative operators -Node TermDb::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder, std::map< TNode, Node >& visited ) { - Trace("canon-term-debug") << "Get canonical term for " << n << std::endl; - if( n.getKind()==BOUND_VARIABLE ){ - std::map< TNode, TNode >::iterator it = subs.find( n ); - if( it==subs.end() ){ - TypeNode tn = n.getType(); - //allocate variable - unsigned vn = var_count[tn]; - var_count[tn]++; - subs[n] = getCanonicalFreeVar( tn, vn ); - Trace("canon-term-debug") << "...allocate variable." << std::endl; - return subs[n]; - }else{ - Trace("canon-term-debug") << "...return variable in subs." << std::endl; - return it->second; - } - }else if( n.getNumChildren()>0 ){ - std::map< TNode, Node >::iterator it = visited.find( n ); - if( it!=visited.end() ){ - return it->second; - }else{ - //collect children - Trace("canon-term-debug") << "Collect children" << std::endl; - std::vector< Node > cchildren; - for( unsigned i=0; imkNode( n.getKind(), cchildren ); - Trace("canon-term-debug") << "...constructed " << ret << " for " << n << "." << std::endl; - visited[n] = ret; - return ret; - } - }else{ - Trace("canon-term-debug") << "...return 0-child term." << std::endl; - return n; - } -} - -Node TermDb::getCanonicalTerm( TNode n, bool apply_torder ){ - std::map< TypeNode, unsigned > var_count; - std::map< TNode, TNode > subs; - std::map< TNode, Node > visited; - return getCanonicalTerm( n, var_count, subs, apply_torder, visited ); -} - -void TermDb::getVtsTerms( std::vector< Node >& t, bool isFree, bool create, bool inc_delta ) { - if( inc_delta ){ - Node delta = getVtsDelta( isFree, create ); - if( !delta.isNull() ){ - t.push_back( delta ); - } - } - for( unsigned r=0; r<2; r++ ){ - Node inf = getVtsInfinityIndex( r, isFree, create ); - if( !inf.isNull() ){ - t.push_back( inf ); - } - } -} - -Node TermDb::getVtsDelta( bool isFree, bool create ) { - if( create ){ - if( d_vts_delta_free.isNull() ){ - d_vts_delta_free = NodeManager::currentNM()->mkSkolem( "delta_free", NodeManager::currentNM()->realType(), "free delta for virtual term substitution" ); - Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_vts_delta_free, d_zero ); - d_quantEngine->getOutputChannel().lemma( delta_lem ); - } - if( d_vts_delta.isNull() ){ - d_vts_delta = NodeManager::currentNM()->mkSkolem( "delta", NodeManager::currentNM()->realType(), "delta for virtual term substitution" ); - //mark as a virtual term - VirtualTermSkolemAttribute vtsa; - d_vts_delta.setAttribute(vtsa,true); - } - } - return isFree ? d_vts_delta_free : d_vts_delta; -} - -Node TermDb::getVtsInfinity( TypeNode tn, bool isFree, bool create ) { - if( create ){ - if( d_vts_inf_free[tn].isNull() ){ - d_vts_inf_free[tn] = NodeManager::currentNM()->mkSkolem( "inf_free", tn, "free infinity for virtual term substitution" ); - } - if( d_vts_inf[tn].isNull() ){ - d_vts_inf[tn] = NodeManager::currentNM()->mkSkolem( "inf", tn, "infinity for virtual term substitution" ); - //mark as a virtual term - VirtualTermSkolemAttribute vtsa; - d_vts_inf[tn].setAttribute(vtsa,true); - } - } - return isFree ? d_vts_inf_free[tn] : d_vts_inf[tn]; -} - -Node TermDb::getVtsInfinityIndex( int i, bool isFree, bool create ) { - if( i==0 ){ - return getVtsInfinity( NodeManager::currentNM()->realType(), isFree, create ); - }else if( i==1 ){ - return getVtsInfinity( NodeManager::currentNM()->integerType(), isFree, create ); - }else{ - Assert( false ); - return Node::null(); - } -} - -Node TermDb::substituteVtsFreeTerms( Node n ) { - std::vector< Node > vars; - getVtsTerms( vars, false, false ); - std::vector< Node > vars_free; - getVtsTerms( vars_free, true, false ); - Assert( vars.size()==vars_free.size() ); - if( !vars.empty() ){ - return n.substitute( vars.begin(), vars.end(), vars_free.begin(), vars_free.end() ); - }else{ - return n; - } -} - -Node TermDb::rewriteVtsSymbols( Node n ) { - if( ( n.getKind()==EQUAL || n.getKind()==GEQ ) ){ - Trace("quant-vts-debug") << "VTS : process " << n << std::endl; - Node rew_vts_inf; - bool rew_delta = false; - //rewriting infinity always takes precedence over rewriting delta - for( unsigned r=0; r<2; r++ ){ - Node inf = getVtsInfinityIndex( r, false, false ); - if( !inf.isNull() && containsTerm( n, inf ) ){ - if( rew_vts_inf.isNull() ){ - rew_vts_inf = inf; - }else{ - //for mixed int/real with multiple infinities - Trace("quant-vts-debug") << "Multiple infinities...equate " << inf << " = " << rew_vts_inf << std::endl; - std::vector< Node > subs_lhs; - subs_lhs.push_back( inf ); - std::vector< Node > subs_rhs; - subs_lhs.push_back( rew_vts_inf ); - n = n.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() ); - n = Rewriter::rewrite( n ); - //may have cancelled - if( !containsTerm( n, rew_vts_inf ) ){ - rew_vts_inf = Node::null(); - } - } - } - } - if( rew_vts_inf.isNull() ){ - if( !d_vts_delta.isNull() && containsTerm( n, d_vts_delta ) ){ - rew_delta = true; - } - } - if( !rew_vts_inf.isNull() || rew_delta ){ - std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( n, msum ) ){ - if( Trace.isOn("quant-vts-debug") ){ - Trace("quant-vts-debug") << "VTS got monomial sum : " << std::endl; - QuantArith::debugPrintMonomialSum( msum, "quant-vts-debug" ); - } - Node vts_sym = !rew_vts_inf.isNull() ? rew_vts_inf : d_vts_delta; - Assert( !vts_sym.isNull() ); - Node iso_n; - Node nlit; - int res = QuantArith::isolate( vts_sym, msum, iso_n, n.getKind(), true ); - if( res!=0 ){ - Trace("quant-vts-debug") << "VTS isolated : -> " << iso_n << ", res = " << res << std::endl; - Node slv = iso_n[res==1 ? 1 : 0]; - //ensure the vts terms have been eliminated - if( containsVtsTerm( slv ) ){ - Trace("quant-vts-warn") << "Bad vts literal : " << n << ", contains " << vts_sym << " but bad solved form " << slv << "." << std::endl; - nlit = substituteVtsFreeTerms( n ); - Trace("quant-vts-debug") << "...return " << nlit << std::endl; - //Assert( false ); - //safe case: just convert to free symbols - return nlit; - }else{ - if( !rew_vts_inf.isNull() ){ - nlit = ( n.getKind()==GEQ && res==1 ) ? d_true : d_false; - }else{ - Assert( iso_n[res==1 ? 0 : 1]==d_vts_delta ); - if( n.getKind()==EQUAL ){ - nlit = d_false; - }else if( res==1 ){ - nlit = NodeManager::currentNM()->mkNode( GEQ, d_zero, slv ); - }else{ - nlit = NodeManager::currentNM()->mkNode( GT, slv, d_zero ); - } - } - } - Trace("quant-vts-debug") << "Return " << nlit << std::endl; - return nlit; - }else{ - Trace("quant-vts-warn") << "Bad vts literal : " << n << ", contains " << vts_sym << " but could not isolate." << std::endl; - //safe case: just convert to free symbols - nlit = substituteVtsFreeTerms( n ); - Trace("quant-vts-debug") << "...return " << nlit << std::endl; - //Assert( false ); - return nlit; - } - } - } - return n; - }else if( n.getKind()==FORALL ){ - //cannot traverse beneath quantifiers - return substituteVtsFreeTerms( n ); - }else{ - bool childChanged = false; - std::vector< Node > children; - for( unsigned i=0; imkNode( n.getKind(), children ); - Trace("quant-vts-debug") << "...make node " << ret << std::endl; - return ret; - }else{ - return n; - } - } -} - -bool TermDb::containsVtsTerm( Node n, bool isFree ) { - std::vector< Node > t; - getVtsTerms( t, isFree, false ); - return containsTerms( n, t ); -} - -bool TermDb::containsVtsTerm( std::vector< Node >& n, bool isFree ) { - std::vector< Node > t; - getVtsTerms( t, isFree, false ); - if( !t.empty() ){ - for( unsigned i=0; i t; - getVtsTerms( t, isFree, false, false ); - return containsTerms( n, t ); -} - -Node TermDb::ensureType( Node n, TypeNode tn ) { - TypeNode ntn = n.getType(); - Assert( ntn.isComparableTo( tn ) ); - if( ntn.isSubtypeOf( tn ) ){ - return n; - }else{ - if( tn.isInteger() ){ - return NodeManager::currentNM()->mkNode( TO_INTEGER, n ); - } - return Node::null(); - } -} - -void TermDb::getRelevancyCondition( Node n, std::vector< Node >& cond ) { - if( n.getKind()==APPLY_SELECTOR_TOTAL ){ - // don't worry about relevancy conditions if using shared selectors - if( !options::dtSharedSelectors() ){ - unsigned scindex = Datatype::cindexOf(n.getOperator().toExpr()); - const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype(); - Node rc = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[scindex].getTester() ), n[0] ).negate(); - if( std::find( cond.begin(), cond.end(), rc )==cond.end() ){ - cond.push_back( rc ); - } - getRelevancyCondition( n[0], cond ); - } - } -} - -bool TermDb::containsTerm2( Node n, Node t, std::map< Node, bool >& visited ) { - if( n==t ){ - return true; - }else{ - if( visited.find( n )==visited.end() ){ - visited[n] = true; - for( unsigned i=0; i& t, std::map< Node, bool >& visited ) { - if( visited.find( n )==visited.end() ){ - if( std::find( t.begin(), t.end(), n )!=t.end() ){ - return true; - }else{ - visited[n] = true; - for( unsigned i=0; i visited; - return containsTerm2( n, t, visited ); -} - -bool TermDb::containsTerms( Node n, std::vector< Node >& t ) { - if( t.empty() ){ - return false; - }else{ - std::map< Node, bool > visited; - return containsTerms2( n, t, visited ); - } -} - -int TermDb::getTermDepth( Node n ) { - if (!n.hasAttribute(TermDepthAttribute()) ){ - int maxDepth = -1; - for( unsigned i=0; imaxDepth ){ - maxDepth = depth; - } - } - TermDepthAttribute tda; - n.setAttribute(tda,1+maxDepth); - } - return n.getAttribute(TermDepthAttribute()); -} - -bool TermDb::containsUninterpretedConstant( Node n ) { - if (!n.hasAttribute(ContainsUConstAttribute()) ){ - bool ret = false; - if( n.getKind()==UNINTERPRETED_CONSTANT ){ - ret = true; - }else{ - for( unsigned i=0; i children; - for( unsigned i=0; imkNode( n.getKind()==OR ? AND : OR, children ); - }else{ - return n.negate(); - } -} - -bool TermDb::isAssoc( Kind k ) { - return k==PLUS || k==MULT || k==AND || k==OR || - k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT || - k==STRING_CONCAT; -} - -bool TermDb::isComm( Kind k ) { - return k==EQUAL || k==PLUS || k==MULT || k==AND || k==OR || k==XOR || - k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR; -} - -bool TermDb::isNonAdditive( Kind k ) { - return k==AND || k==OR || k==BITVECTOR_AND || k==BITVECTOR_OR; -} - -bool TermDb::isBoolConnective( Kind k ) { - return k==OR || k==AND || k==EQUAL || k==ITE || k==FORALL || k==NOT || k==SEP_STAR; -} - -bool TermDb::isBoolConnectiveTerm( TNode n ) { - return isBoolConnective( n.getKind() ) && - ( n.getKind()!=EQUAL || n[0].getType().isBoolean() ) && - ( n.getKind()!=ITE || n.getType().isBoolean() ); -} - -void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){ - if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){ - d_op_triggers[op].push_back( tr ); - } -} - -Node TermDb::getHoTypeMatchPredicate( TypeNode tn ) { - std::map< TypeNode, Node >::iterator ithp = d_ho_type_match_pred.find( tn ); - if( ithp==d_ho_type_match_pred.end() ){ - TypeNode ptn = NodeManager::currentNM()->mkFunctionType( tn, NodeManager::currentNM()->booleanType() ); - Node k = NodeManager::currentNM()->mkSkolem( "U", ptn, "predicate to force higher-order types" ); - d_ho_type_match_pred[tn] = k; - return k; - }else{ - return ithp->second; - } -} - -bool TermDb::isInductionTerm( Node n ) { - TypeNode tn = n.getType(); - if( options::dtStcInduction() && tn.isDatatype() ){ - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - return !dt.isCodatatype(); - } - if( options::intWfInduction() && n.getType().isInteger() ){ - return true; - } - return false; -} - -bool TermDb::isRewriteRule( Node q ) { - return !getRewriteRule( q ).isNull(); -} - -Node TermDb::getRewriteRule( Node q ) { - if( q.getKind()==FORALL && q.getNumChildren()==3 && q[2].getNumChildren()>0 && q[2][0][0].getKind()==REWRITE_RULE ){ - return q[2][0][0]; - }else{ - return Node::null(); - } -} - -bool TermDb::isFunDef( Node q ) { - return !getFunDefHead( q ).isNull(); -} - -bool TermDb::isFunDefAnnotation( Node ipl ) { - if( !ipl.isNull() ){ - for( unsigned i=0; imkConst( pol ); - } - } - } - return Node::null(); -} - -bool TermDb::isSygusConjecture( Node q ) { - return ( q.getKind()==FORALL && q.getNumChildren()==3 ) ? isSygusConjectureAnnotation( q[2] ) : false; -} - -bool TermDb::isSygusConjectureAnnotation( Node ipl ){ - if( !ipl.isNull() ){ - for( unsigned i=0; igetRewriteEngine()==NULL ){ - Trace("quant-warn") << "WARNING : rewrite engine is null, and we have : " << q << std::endl; - } - //set rewrite engine as owner - d_quantEngine->setOwner( q, d_quantEngine->getRewriteEngine(), 2 ); - } - if( d_qattr[q].isFunDef() ){ - Node f = d_qattr[q].d_fundef_f; - if( d_fun_defs.find( f )!=d_fun_defs.end() ){ - Message() << "Cannot define function " << f << " more than once." << std::endl; - exit( 1 ); - } - d_fun_defs[f] = true; - d_quantEngine->setOwner( q, d_quantEngine->getFunDefEngine(), 2 ); - } - if( d_qattr[q].d_sygus ){ - if( d_quantEngine->getCegInstantiation()==NULL ){ - Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl; - } - d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation(), 2 ); - } - if( d_qattr[q].d_synthesis ){ - if( d_quantEngine->getCegInstantiation()==NULL ){ - Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl; - } - d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation(), 2 ); - } -} - -void TermDb::computeQuantAttributes( Node q, QAttributes& qa ){ - Trace("quant-attr-debug") << "Compute attributes for " << q << std::endl; - if( q.getNumChildren()==3 ){ - qa.d_ipl = q[2]; - for( unsigned i=0; i::iterator it = d_qattr.find( q ); - if( it==d_qattr.end() ){ - return false; - }else{ - return it->second.d_conjecture; - } -} - -bool TermDb::isQAttrAxiom( Node q ) { - std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); - if( it==d_qattr.end() ){ - return false; - }else{ - return it->second.d_axiom; - } -} - -bool TermDb::isQAttrFunDef( Node q ) { - std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); - if( it==d_qattr.end() ){ - return false; - }else{ - return it->second.isFunDef(); - } -} - -bool TermDb::isQAttrSygus( Node q ) { - std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); - if( it==d_qattr.end() ){ - return false; - }else{ - return it->second.d_sygus; - } -} - -bool TermDb::isQAttrSynthesis( Node q ) { - std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); - if( it==d_qattr.end() ){ - return false; - }else{ - return it->second.d_synthesis; - } -} - -int TermDb::getQAttrQuantInstLevel( Node q ) { - std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); - if( it==d_qattr.end() ){ - return -1; - }else{ - return it->second.d_qinstLevel; - } -} - -int TermDb::getQAttrRewriteRulePriority( Node q ) { - std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); - if( it==d_qattr.end() ){ - return -1; - }else{ - return it->second.d_rr_priority; - } -} - -bool TermDb::isQAttrQuantElim( Node q ) { - std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); - if( it==d_qattr.end() ){ - return false; - }else{ - return it->second.d_quant_elim; - } -} - -bool TermDb::isQAttrQuantElimPartial( Node q ) { - std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); - if( it==d_qattr.end() ){ - return false; - }else{ - return it->second.d_quant_elim_partial; - } -} - -int TermDb::getQAttrQuantIdNum( Node q ) { - std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); - if( it!=d_qattr.end() ){ - if( !it->second.d_qid_num.isNull() ){ - return it->second.d_qid_num.getAttribute(QuantIdNumAttribute()); - } - } - return -1; -} - -Node TermDb::getQAttrQuantIdNumNode( Node q ) { - std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); - if( it==d_qattr.end() ){ - return Node::null(); - }else{ - return it->second.d_qid_num; - } -} - }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 852d94fde..f4c6c3877 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -25,109 +25,9 @@ #include "theory/type_enumerator.h" #include "theory/quantifiers/quant_util.h" - namespace CVC4 { namespace theory { -/** Attribute true for quantifiers that are axioms */ -struct AxiomAttributeId {}; -typedef expr::Attribute< AxiomAttributeId, bool > AxiomAttribute; - -/** Attribute true for quantifiers that are conjecture */ -struct ConjectureAttributeId {}; -typedef expr::Attribute< ConjectureAttributeId, bool > ConjectureAttribute; - -/** Attribute true for function definition quantifiers */ -struct FunDefAttributeId {}; -typedef expr::Attribute< FunDefAttributeId, bool > FunDefAttribute; - -/** Attribute true for quantifiers that are SyGus conjectures */ -struct SygusAttributeId {}; -typedef expr::Attribute< SygusAttributeId, bool > SygusAttribute; - -/** Attribute true for quantifiers that are synthesis conjectures */ -struct SynthesisAttributeId {}; -typedef expr::Attribute< SynthesisAttributeId, bool > SynthesisAttribute; - -// attribute for "contains instantiation constants from" -struct InstConstantAttributeId {}; -typedef expr::Attribute InstConstantAttribute; - -struct BoundVarAttributeId {}; -typedef expr::Attribute BoundVarAttribute; - -struct InstLevelAttributeId {}; -typedef expr::Attribute InstLevelAttribute; - -struct InstVarNumAttributeId {}; -typedef expr::Attribute InstVarNumAttribute; - -struct TermDepthAttributeId {}; -typedef expr::Attribute TermDepthAttribute; - -struct ContainsUConstAttributeId {}; -typedef expr::Attribute ContainsUConstAttribute; - -struct ModelBasisAttributeId {}; -typedef expr::Attribute ModelBasisAttribute; -//for APPLY_UF terms, 1 : term has direct child with model basis attribute, -// 0 : term has no direct child with model basis attribute. -struct ModelBasisArgAttributeId {}; -typedef expr::Attribute ModelBasisArgAttribute; - -//for bounded integers -struct BoundIntLitAttributeId {}; -typedef expr::Attribute BoundIntLitAttribute; - -//for quantifier instantiation level -struct QuantInstLevelAttributeId {}; -typedef expr::Attribute QuantInstLevelAttribute; - -//rewrite-rule priority -struct RrPriorityAttributeId {}; -typedef expr::Attribute RrPriorityAttribute; - -/** Attribute true for quantifiers that do not need to be partially instantiated */ -struct LtePartialInstAttributeId {}; -typedef expr::Attribute< LtePartialInstAttributeId, bool > LtePartialInstAttribute; - -// attribute for "contains instantiation constants from" -struct SygusProxyAttributeId {}; -typedef expr::Attribute SygusProxyAttribute; - -// attribute for associating a synthesis function with a first order variable -struct SygusSynthFunAttributeId {}; -typedef expr::Attribute SygusSynthFunAttribute; - -// attribute for associating a variable list with a synth fun -struct SygusSynthFunVarListAttributeId {}; -typedef expr::Attribute SygusSynthFunVarListAttribute; - -//attribute for fun-def abstraction type -struct AbsTypeFunDefAttributeId {}; -typedef expr::Attribute AbsTypeFunDefAttribute; - -/** Attribute true for quantifiers that we are doing quantifier elimination on */ -struct QuantElimAttributeId {}; -typedef expr::Attribute< QuantElimAttributeId, bool > QuantElimAttribute; - -/** Attribute true for quantifiers that we are doing partial quantifier elimination on */ -struct QuantElimPartialAttributeId {}; -typedef expr::Attribute< QuantElimPartialAttributeId, bool > QuantElimPartialAttribute; - -/** Attribute for id number */ -struct QuantIdNumAttributeId {}; -typedef expr::Attribute< QuantIdNumAttributeId, uint64_t > QuantIdNumAttribute; - -/** sygus var num */ -struct SygusVarNumAttributeId {}; -typedef expr::Attribute SygusVarNumAttribute; - -/** Attribute to mark Skolems as virtual terms */ -struct VirtualTermSkolemAttributeId {}; -typedef expr::Attribute< VirtualTermSkolemAttributeId, bool > VirtualTermSkolemAttribute; - - class QuantifiersEngine; namespace inst{ @@ -151,29 +51,6 @@ public: void clear() { d_data.clear(); } };/* class TermArgTrie */ - -class QAttributes{ -public: - QAttributes() : d_hasPattern(false), d_conjecture(false), d_axiom(false), d_sygus(false), - d_synthesis(false), d_rr_priority(-1), d_qinstLevel(-1), d_quant_elim(false), d_quant_elim_partial(false){} - ~QAttributes(){} - bool d_hasPattern; - Node d_rr; - bool d_conjecture; - bool d_axiom; - Node d_fundef_f; - bool d_sygus; - bool d_synthesis; - int d_rr_priority; - int d_qinstLevel; - bool d_quant_elim; - bool d_quant_elim_partial; - Node d_ipl; - Node d_qid_num; - bool isRewriteRule() { return !d_rr.isNull(); } - bool isFunDef() { return !d_fundef_f.isNull(); } -}; - namespace fmcheck { class FullModelChecker; } @@ -208,25 +85,23 @@ private: std::map< Node, std::map< TypeNode, Node > > d_par_op_map; /** whether master equality engine is UF-inconsistent */ bool d_consistent_ee; - - public: - TermDb(context::Context* c, context::UserContext* u, QuantifiersEngine* qe); - ~TermDb(); /** boolean terms */ Node d_true; Node d_false; - /** constants */ - Node d_zero; - Node d_one; - - public: +public: + TermDb(context::Context* c, context::UserContext* u, QuantifiersEngine* qe); + ~TermDb(); + + /** register quantified formula */ + void registerQuantifier( Node q ); +public: /** presolve (called once per user check-sat) */ void presolve(); /** reset (calculate which terms are active) */ bool reset( Theory::Effort effort ); /** identify */ std::string identify() const { return "TermDb"; } - private: +private: /** map from operators to ground terms for that operator */ std::map< Node, std::vector< Node > > d_op_map; /** map from type nodes to terms of that type */ @@ -330,275 +205,7 @@ public: Node getModelBasis( Node q, Node n ); //get model basis body Node getModelBasisBody( Node q ); - -//for inst constant -private: - /** map from universal quantifiers to the list of variables */ - std::map< Node, std::vector< Node > > d_vars; - std::map< Node, std::map< Node, unsigned > > d_var_num; - /** map from universal quantifiers to their inst constant body */ - std::map< Node, Node > d_inst_const_body; - /** map from universal quantifiers to their counterexample literals */ - std::map< Node, Node > d_ce_lit; - /** instantiation constants to universal quantifiers */ - std::map< Node, Node > d_inst_constants_map; - /** make instantiation constants for */ - void makeInstantiationConstantsFor( Node q ); -public: - /** map from universal quantifiers to the list of instantiation constants */ - std::map< Node, std::vector< Node > > d_inst_constants; - /** get variable number */ - unsigned getVariableNum( Node q, Node v ) { return d_var_num[q][v]; } - /** get the i^th instantiation constant of q */ - Node getInstantiationConstant( Node q, int i ) const; - /** get number of instantiation constants for q */ - unsigned getNumInstantiationConstants( Node q ) const; - /** get the ce body q[e/x] */ - Node getInstConstantBody( Node q ); - /** get counterexample literal (for cbqi) */ - Node getCounterexampleLiteral( Node q ); - /** returns node n with bound vars of q replaced by instantiation constants of q - node n : is the future pattern - node q : is the quantifier containing which bind the variable - return a pattern where the variable are replaced by variable for - instantiation. - */ - Node getInstConstantNode( Node n, Node q ); - Node getVariableNode( Node n, Node q ); - /** get substituted node */ - Node getInstantiatedNode( Node n, Node q, std::vector< Node >& terms ); - - static Node getInstConstAttr( Node n ); - static bool hasInstConstAttr( Node n ); - static Node getBoundVarAttr( Node n ); - static bool hasBoundVarAttr( Node n ); -private: - /** get bound vars */ - static void getBoundVars2( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited ); - /** get bound vars */ - static Node getRemoveQuantifiers2( Node n, std::map< Node, Node >& visited ); -public: - //get the bound variables in this node - static void getBoundVars( Node n, std::vector< Node >& vars ); - //remove quantifiers - static Node getRemoveQuantifiers( Node n ); - //quantified simplify (treat free variables in n as quantified and run rewriter) - static Node getQuantSimplify( Node n ); - -//for skolem -private: - /** map from universal quantifiers to their skolemized body */ - std::map< Node, Node > d_skolem_body; -public: - /** map from universal quantifiers to the list of skolem constants */ - std::map< Node, std::vector< Node > > d_skolem_constants; - /** make the skolemized body f[e/x] */ - static Node mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& fvTypes, std::vector< TNode >& fvs, - std::vector< Node >& sk, Node& sub, std::vector< unsigned >& sub_vars ); - /** get the skolemized body */ - Node getSkolemizedBody( Node f); - /** is induction variable */ - static bool isInductionTerm( Node n ); - -//for ground term enumeration -private: - /** ground terms enumerated for types */ - std::map< TypeNode, std::vector< Node > > d_enum_terms; - //type enumerators - std::map< TypeNode, unsigned > d_typ_enum_map; - std::vector< TypeEnumerator > d_typ_enum; - // closed enumerable type cache - std::map< TypeNode, bool > d_typ_closed_enum; - /** may complete */ - std::map< TypeNode, bool > d_may_complete; -public: - //get nth term for type - Node getEnumerateTerm( TypeNode tn, unsigned index ); - //does this type have an enumerator that produces constants that are handled by ground theory solvers - bool isClosedEnumerableType( TypeNode tn ); - // may complete - bool mayComplete( TypeNode tn ); - -//for triggers -private: - /** helper function for compute var contains */ - static void computeVarContains2( Node n, Kind k, std::vector< Node >& varContains, std::map< Node, bool >& visited ); - /** triggers for each operator */ - std::map< Node, std::vector< inst::Trigger* > > d_op_triggers; - /** helper for is instance of */ - static bool isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs ); - /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */ - static int isInstanceOf2( Node n1, Node n2, std::vector< Node >& varContains1, std::vector< Node >& varContains2 ); -public: - /** compute var contains */ - static void computeVarContains( Node n, std::vector< Node >& varContains ); - /** get var contains for each of the patterns in pats */ - static void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains ); - /** get var contains for node n */ - static void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ); - /** compute quant contains */ - static void computeQuantContains( Node n, std::vector< Node >& quantContains ); - /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */ - static int isInstanceOf( Node n1, Node n2 ); - /** filter all nodes that have instances */ - static void filterInstances( std::vector< Node >& nodes ); - /** register trigger (for eager quantifier instantiation) */ - void registerTrigger( inst::Trigger* tr, Node op ); - -//for term ordering -private: - /** operator id count */ - int d_op_id_count; - /** map from operators to id */ - std::map< Node, int > d_op_id; - /** type id count */ - int d_typ_id_count; - /** map from type to id */ - std::map< TypeNode, int > d_typ_id; - //free variables - std::map< TypeNode, std::vector< Node > > d_cn_free_var; - // get canonical term, return null if it contains a term apart from handled signature - Node getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder, - std::map< TNode, Node >& visited ); -public: - /** get id for operator */ - int getIdForOperator( Node op ); - /** get id for type */ - int getIdForType( TypeNode t ); - /** get term order */ - bool getTermOrder( Node a, Node b ); - /** get canonical free variable #i of type tn */ - Node getCanonicalFreeVar( TypeNode tn, unsigned i ); - /** get canonical term */ - Node getCanonicalTerm( TNode n, bool apply_torder = false ); - -//for virtual term substitution -private: - Node d_vts_delta; - std::map< TypeNode, Node > d_vts_inf; - Node d_vts_delta_free; - std::map< TypeNode, Node > d_vts_inf_free; - /** get vts infinity index */ - Node getVtsInfinityIndex( int i, bool isFree = false, bool create = true ); - /** substitute vts free terms */ - Node substituteVtsFreeTerms( Node n ); -public: - /** get vts delta */ - Node getVtsDelta( bool isFree = false, bool create = true ); - /** get vts infinity */ - Node getVtsInfinity( TypeNode tn, bool isFree = false, bool create = true ); - /** get all vts terms */ - void getVtsTerms( std::vector< Node >& t, bool isFree = false, bool create = true, bool inc_delta = true ); - /** rewrite delta */ - Node rewriteVtsSymbols( Node n ); - /** simple check for contains term */ - bool containsVtsTerm( Node n, bool isFree = false ); - /** simple check for contains term */ - bool containsVtsTerm( std::vector< Node >& n, bool isFree = false ); - /** simple check for contains term */ - bool containsVtsInfinity( Node n, bool isFree = false ); - /** ensure type */ - static Node ensureType( Node n, TypeNode tn ); - /** get relevancy condition */ - static void getRelevancyCondition( Node n, std::vector< Node >& cond ); -private: - //helper for contains term - static bool containsTerm2( Node n, Node t, std::map< Node, bool >& visited ); - static bool containsTerms2( Node n, std::vector< Node >& t, std::map< Node, bool >& visited ); -//general utilities -public: - /** simple check for whether n contains t as subterm */ - static bool containsTerm( Node n, Node t ); - /** simple check for contains term, true if contains at least one term in t */ - static bool containsTerms( Node n, std::vector< Node >& t ); - /** contains uninterpreted constant */ - static bool containsUninterpretedConstant( Node n ); - /** get the term depth of n */ - static int getTermDepth( Node n ); - /** simple negate */ - static Node simpleNegate( Node n ); - /** is assoc */ - static bool isAssoc( Kind k ); - /** is comm */ - static bool isComm( Kind k ); - /** ( x k ... ) k x = ( x k ... ) */ - static bool isNonAdditive( Kind k ); - /** is bool connective */ - static bool isBoolConnective( Kind k ); - /** is bool connective term */ - static bool isBoolConnectiveTerm( TNode n ); - -//for higher-order -private: - /** dummy predicate that states terms should be considered first-class members of equality engine */ - std::map< TypeNode, Node > d_ho_type_match_pred; -public: - /** get higher-order type match predicate - * This predicate is used to force certain functions f of type tn to appear as first-class representatives in the - * quantifier-free UF solver. For a typical use case, we call getHoTypeMatchPredicate which returns a fresh - * predicate P of type (tn -> Bool). Then, we add P( f ) as a lemma. - * TODO: we may eliminate this depending on how github issue #1115 is resolved. - */ - Node getHoTypeMatchPredicate( TypeNode tn ); - -//for sygus -private: - TermDbSygus * d_sygus_tdb; -public: - TermDbSygus * getTermDatabaseSygus() { return d_sygus_tdb; } - -private: - std::map< Node, bool > d_fun_defs; -public: //general queries concerning quantified formulas wrt modules - /** is quantifier treated as a rewrite rule? */ - static bool isRewriteRule( Node q ); - /** get the rewrite rule associated with the quanfied formula */ - static Node getRewriteRule( Node q ); - /** is fun def */ - static bool isFunDef( Node q ); - /** is fun def */ - static bool isFunDefAnnotation( Node ipl ); - /** is sygus conjecture */ - static bool isSygusConjecture( Node q ); - /** is sygus conjecture */ - static bool isSygusConjectureAnnotation( Node ipl ); - /** get fun def body */ - static Node getFunDefHead( Node q ); - /** get fun def body */ - static Node getFunDefBody( Node q ); - /** is quant elim annotation */ - static bool isQuantElimAnnotation( Node ipl ); -//attributes -private: - std::map< Node, QAttributes > d_qattr; - //record attributes - void computeAttributes( Node q ); -public: - /** is conjecture */ - bool isQAttrConjecture( Node q ); - /** is axiom */ - bool isQAttrAxiom( Node q ); - /** is function definition */ - bool isQAttrFunDef( Node q ); - /** is sygus conjecture */ - bool isQAttrSygus( Node q ); - /** is synthesis conjecture */ - bool isQAttrSynthesis( Node q ); - /** get instantiation level */ - int getQAttrQuantInstLevel( Node q ); - /** get rewrite rule priority */ - int getQAttrRewriteRulePriority( Node q ); - /** is quant elim */ - bool isQAttrQuantElim( Node q ); - /** is quant elim partial */ - bool isQAttrQuantElimPartial( Node q ); - /** get quant id num */ - int getQAttrQuantIdNum( Node q ); - /** get quant id num */ - Node getQAttrQuantIdNumNode( Node q ); - /** compute quantifier attributes */ - static void computeQuantAttributes( Node q, QAttributes& qa ); };/* class TermDb */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/term_database_sygus.cpp b/src/theory/quantifiers/term_database_sygus.cpp index 61bb20987..f5c04fced 100644 --- a/src/theory/quantifiers/term_database_sygus.cpp +++ b/src/theory/quantifiers/term_database_sygus.cpp @@ -19,12 +19,9 @@ #include "options/datatypes_options.h" #include "options/quantifiers_options.h" #include "smt/smt_engine.h" -#include "theory/quantifiers/ce_guided_instantiation.h" -#include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/fun_def_engine.h" -#include "theory/quantifiers/rewrite_engine.h" #include "theory/quantifiers/theory_quantifiers.h" -#include "theory/quantifiers/trigger.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" @@ -152,7 +149,7 @@ bool TermDbSygus::getMatch2( Node p, Node n, std::map< int, Node >& s, std::vect return p==n; }else if( n.getKind()==p.getKind() && n.getNumChildren()==p.getNumChildren() ){ //try both ways? - unsigned rmax = TermDb::isComm( n.getKind() ) && n.getNumChildren()==2 ? 2 : 1; + unsigned rmax = TermUtil::isComm( n.getKind() ) && n.getNumChildren()==2 ? 2 : 1; std::vector< int > new_tmp; for( unsigned r=0; r& terms Assert( dt.isSygus() ); Trace("sygus-eager") << "TermDbSygus::eager: Register model value : " << vn << " for " << n << std::endl; Trace("sygus-eager") << "...it has " << it->second.size() << " evaluations, already processed " << start << "." << std::endl; - Node bTerm = d_quantEngine->getTermDatabaseSygus()->sygusToBuiltin( vn, tn ); + Node bTerm = sygusToBuiltin( vn, tn ); Trace("sygus-eager") << "Built-in term : " << bTerm << std::endl; std::vector< Node > vars; Node var_list = Node::fromExpr( dt.getSygusVarList() ); diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp new file mode 100644 index 000000000..346745b1d --- /dev/null +++ b/src/theory/quantifiers/term_util.cpp @@ -0,0 +1,1189 @@ +/********************* */ +/*! \file term_util.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of term utilities class + **/ + +#include "theory/quantifiers/term_util.h" + +#include "expr/datatype.h" +#include "options/base_options.h" +#include "options/quantifiers_options.h" +#include "options/datatypes_options.h" +#include "options/uf_options.h" +#include "theory/theory_engine.h" +#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/term_database.h" + +using namespace std; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory::inst; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +TermUtil::TermUtil(QuantifiersEngine * qe) : +d_quantEngine(qe), +d_op_id_count(0), +d_typ_id_count(0){ + d_true = NodeManager::currentNM()->mkConst(true); + d_false = NodeManager::currentNM()->mkConst(false); + d_zero = NodeManager::currentNM()->mkConst(Rational(0)); + d_one = NodeManager::currentNM()->mkConst(Rational(1)); +} + +TermUtil::~TermUtil(){ + +} + +void TermUtil::registerQuantifier( Node q ){ + if( d_inst_constants.find( q )==d_inst_constants.end() ){ + Debug("quantifiers-engine") << "Instantiation constants for " << q << " : " << std::endl; + for( unsigned i=0; imkInstConstant( q[0][i].getType() ); + d_inst_constants_map[ic] = q; + d_inst_constants[ q ].push_back( ic ); + Debug("quantifiers-engine") << " " << ic << std::endl; + //set the var number attribute + InstVarNumAttribute ivna; + ic.setAttribute( ivna, i ); + InstConstantAttribute ica; + ic.setAttribute( ica, q ); + } + } +} + +void TermUtil::getBoundVars2( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited ) { + if( visited.find( n )==visited.end() ){ + visited[n] = true; + if( n.getKind()==BOUND_VARIABLE ){ + if( std::find( vars.begin(), vars.end(), n )==vars.end() ) { + vars.push_back( n ); + } + } + for( unsigned i=0; i& visited ) { + std::map< Node, Node >::iterator it = visited.find( n ); + if( it!=visited.end() ){ + return it->second; + }else{ + Node ret = n; + if( n.getKind()==FORALL ){ + ret = getRemoveQuantifiers2( n[1], visited ); + }else if( n.getNumChildren()>0 ){ + std::vector< Node > children; + bool childrenChanged = false; + for( unsigned i=0; imkNode( n.getKind(), children ); + } + } + visited[n] = ret; + return ret; + } +} + +Node TermUtil::getInstConstAttr( Node n ) { + if (!n.hasAttribute(InstConstantAttribute()) ){ + Node q; + for( unsigned i=0; i& vars ) { + std::map< Node, bool > visited; + return getBoundVars2( n, vars, visited ); +} + +//remove quantifiers +Node TermUtil::getRemoveQuantifiers( Node n ) { + std::map< Node, Node > visited; + return getRemoveQuantifiers2( n, visited ); +} + +//quantified simplify +Node TermUtil::getQuantSimplify( Node n ) { + std::vector< Node > bvs; + getBoundVars( n, bvs ); + if( bvs.empty() ) { + return Rewriter::rewrite( n ); + }else{ + Node q = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs ), n ); + q = Rewriter::rewrite( q ); + return getRemoveQuantifiers( q ); + } +} + +/** get the i^th instantiation constant of q */ +Node TermUtil::getInstantiationConstant( Node q, int i ) const { + std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q ); + if( it!=d_inst_constants.end() ){ + return it->second[i]; + }else{ + return Node::null(); + } +} + +/** get number of instantiation constants for q */ +unsigned TermUtil::getNumInstantiationConstants( Node q ) const { + std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q ); + if( it!=d_inst_constants.end() ){ + return it->second.size(); + }else{ + return 0; + } +} + +Node TermUtil::getInstConstantBody( Node q ){ + std::map< Node, Node >::iterator it = d_inst_const_body.find( q ); + if( it==d_inst_const_body.end() ){ + Node n = getInstConstantNode( q[1], q ); + d_inst_const_body[ q ] = n; + return n; + }else{ + return it->second; + } +} + +Node TermUtil::getCounterexampleLiteral( Node q ){ + if( d_ce_lit.find( q )==d_ce_lit.end() ){ + /* + Node ceBody = getInstConstantBody( f ); + //check if any variable are of bad types, and fail if so + for( size_t i=0; imkSkolem( "g", NodeManager::currentNM()->booleanType() ); + //otherwise, ensure literal + Node ceLit = d_quantEngine->getValuation().ensureLiteral( g ); + d_ce_lit[ q ] = ceLit; + } + return d_ce_lit[ q ]; +} + +Node TermUtil::getInstConstantNode( Node n, Node q ){ + registerQuantifier( q ); + return n.substitute( d_vars[q].begin(), d_vars[q].end(), d_inst_constants[q].begin(), d_inst_constants[q].end() ); +} + +Node TermUtil::getVariableNode( Node n, Node q ) { + registerQuantifier( q ); + return n.substitute( d_inst_constants[q].begin(), d_inst_constants[q].end(), d_vars[q].begin(), d_vars[q].end() ); +} + +Node TermUtil::getInstantiatedNode( Node n, Node q, std::vector< Node >& terms ) { + Assert( d_vars[q].size()==terms.size() ); + return n.substitute( d_vars[q].begin(), d_vars[q].end(), terms.begin(), terms.end() ); +} + + +void getSelfSel( const Datatype& dt, const DatatypeConstructor& dc, Node n, TypeNode ntn, std::vector< Node >& selfSel ){ + TypeNode tspec; + if( dt.isParametric() ){ + tspec = TypeNode::fromType( dc.getSpecializedConstructorType(n.getType().toType()) ); + Trace("sk-ind-debug") << "Specialized constructor type : " << tspec << std::endl; + Assert( tspec.getNumChildren()==dc.getNumArgs() ); + } + Trace("sk-ind-debug") << "Check self sel " << dc.getName() << " " << dt.getName() << std::endl; + for( unsigned j=0; j ssc; + if( dt.isParametric() ){ + Trace("sk-ind-debug") << "Compare " << tspec[j] << " " << ntn << std::endl; + if( tspec[j]==ntn ){ + ssc.push_back( n ); + } + }else{ + TypeNode tn = TypeNode::fromType( dc[j].getRangeType() ); + Trace("sk-ind-debug") << "Compare " << tn << " " << ntn << std::endl; + if( tn==ntn ){ + ssc.push_back( n ); + } + } + /* TODO: more than weak structural induction + else if( tn.isDatatype() && std::find( visited.begin(), visited.end(), tn )==visited.end() ){ + visited.push_back( tn ); + const Datatype& dt = ((DatatypeType)(subs[0].getType()).toType()).getDatatype(); + std::vector< Node > disj; + for( unsigned i=0; imkNode( APPLY_SELECTOR_TOTAL, dc.getSelectorInternal( n.getType().toType(), j ), n ); + if( std::find( selfSel.begin(), selfSel.end(), ss )==selfSel.end() ){ + selfSel.push_back( ss ); + } + } + } +} + + +Node TermUtil::mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& argTypes, std::vector< TNode >& fvs, + std::vector< Node >& sk, Node& sub, std::vector< unsigned >& sub_vars ) { + Assert( sk.empty() || sk.size()==f[0].getNumChildren() ); + //calculate the variables and substitution + std::vector< TNode > ind_vars; + std::vector< unsigned > ind_var_indicies; + std::vector< TNode > vars; + std::vector< unsigned > var_indicies; + for( unsigned i=0; i=sk.size() ){ + if( argTypes.empty() ){ + s = NodeManager::currentNM()->mkSkolem( "skv", f[0][i].getType(), "created during skolemization" ); + }else{ + TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, f[0][i].getType() ); + Node op = NodeManager::currentNM()->mkSkolem( "skop", typ, "op created during pre-skolemization" ); + //DOTHIS: set attribute on op, marking that it should not be selected as trigger + std::vector< Node > funcArgs; + funcArgs.push_back( op ); + funcArgs.insert( funcArgs.end(), fvs.begin(), fvs.end() ); + s = NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs ); + } + sk.push_back( s ); + }else{ + Assert( sk[i].getType()==f[0][i].getType() ); + } + } + Node ret; + if( vars.empty() ){ + ret = n; + }else{ + std::vector< Node > var_sk; + for( unsigned i=0; i ~P( x ) ) + if( options::dtStcInduction() && tn.isDatatype() ){ + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + std::vector< Node > disj; + for( unsigned i=0; i selfSel; + getSelfSel( dt, dt[i], k, tn, selfSel ); + std::vector< Node > conj; + conj.push_back( NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), k ).negate() ); + for( unsigned j=0; jmkNode( OR, conj ) ); + } + Assert( !disj.empty() ); + n_str_ind = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( AND, disj ); + }else if( options::intWfInduction() && tn.isInteger() ){ + Node icond = NodeManager::currentNM()->mkNode( GEQ, k, NodeManager::currentNM()->mkConst( Rational(0) ) ); + Node iret = ret.substitute( ind_vars[0], NodeManager::currentNM()->mkNode( MINUS, k, NodeManager::currentNM()->mkConst( Rational(1) ) ) ).negate(); + n_str_ind = NodeManager::currentNM()->mkNode( OR, icond.negate(), iret ); + n_str_ind = NodeManager::currentNM()->mkNode( AND, icond, n_str_ind ); + }else{ + Trace("sk-ind") << "Unknown induction for term : " << ind_vars[0] << ", type = " << tn << std::endl; + Assert( false ); + } + Trace("sk-ind") << "Strengthening is : " << n_str_ind << std::endl; + + std::vector< Node > rem_ind_vars; + rem_ind_vars.insert( rem_ind_vars.end(), ind_vars.begin()+1, ind_vars.end() ); + if( !rem_ind_vars.empty() ){ + Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, rem_ind_vars ); + nret = NodeManager::currentNM()->mkNode( FORALL, bvl, nret ); + nret = Rewriter::rewrite( nret ); + sub = nret; + sub_vars.insert( sub_vars.end(), ind_var_indicies.begin()+1, ind_var_indicies.end() ); + n_str_ind = NodeManager::currentNM()->mkNode( FORALL, bvl, n_str_ind.negate() ).negate(); + } + ret = NodeManager::currentNM()->mkNode( OR, nret, n_str_ind ); + } + Trace("quantifiers-sk-debug") << "mkSkolem body for " << f << " returns : " << ret << std::endl; + //if it has an instantiation level, set the skolemized body to that level + if( f.hasAttribute(InstLevelAttribute()) ){ + theory::QuantifiersEngine::setInstantiationLevelAttr( ret, f.getAttribute(InstLevelAttribute()) ); + } + + if( Trace.isOn("quantifiers-sk") ){ + Trace("quantifiers-sk") << "Skolemize : "; + for( unsigned i=0; i fvTypes; + std::vector< TNode > fvs; + Node sub; + std::vector< unsigned > sub_vars; + d_skolem_body[ f ] = mkSkolemizedBody( f, f[1], fvTypes, fvs, d_skolem_constants[f], sub, sub_vars ); + //store sub quantifier information + if( !sub.isNull() ){ + //if we are skolemizing one at a time, we already know the skolem constants of the sub-quantified formula, store them + Assert( d_skolem_constants[sub].empty() ); + for( unsigned i=0; igetTheoryEngine()->getSortInference()->setSkolemVar( f, f[0][i], d_skolem_constants[f][i] ); + } + } + } + return d_skolem_body[ f ]; +} + +Node TermUtil::getEnumerateTerm( TypeNode tn, unsigned index ) { + Trace("term-db-enum") << "Get enumerate term " << tn << " " << index << std::endl; + std::map< TypeNode, unsigned >::iterator it = d_typ_enum_map.find( tn ); + unsigned teIndex; + if( it==d_typ_enum_map.end() ){ + teIndex = (int)d_typ_enum.size(); + d_typ_enum_map[tn] = teIndex; + d_typ_enum.push_back( TypeEnumerator(tn) ); + }else{ + teIndex = it->second; + } + while( index>=d_enum_terms[tn].size() ){ + if( d_typ_enum[teIndex].isFinished() ){ + return Node::null(); + } + d_enum_terms[tn].push_back( *d_typ_enum[teIndex] ); + ++d_typ_enum[teIndex]; + } + return d_enum_terms[tn][index]; +} + +bool TermUtil::isClosedEnumerableType( TypeNode tn ) { + std::map< TypeNode, bool >::iterator it = d_typ_closed_enum.find( tn ); + if( it==d_typ_closed_enum.end() ){ + d_typ_closed_enum[tn] = true; + bool ret = true; + if( tn.isArray() || tn.isSort() || tn.isCodatatype() || tn.isFunction() ){ + ret = false; + }else if( tn.isSet() ){ + ret = isClosedEnumerableType( tn.getSetElementType() ); + }else if( tn.isDatatype() ){ + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + for( unsigned i=0; isecond; + } +} + +//checks whether a type is not Array and is reasonably small enough (<1000) such that all of its domain elements can be enumerated +bool TermUtil::mayComplete( TypeNode tn ) { + std::map< TypeNode, bool >::iterator it = d_may_complete.find( tn ); + if( it==d_may_complete.end() ){ + bool mc = false; + if( isClosedEnumerableType( tn ) && tn.getCardinality().isFinite() && !tn.getCardinality().isLargeFinite() ){ + Node card = NodeManager::currentNM()->mkConst( Rational(tn.getCardinality().getFiniteCardinality()) ); + Node oth = NodeManager::currentNM()->mkConst( Rational(1000) ); + Node eq = NodeManager::currentNM()->mkNode( LEQ, card, oth ); + eq = Rewriter::rewrite( eq ); + mc = eq==d_true; + } + d_may_complete[tn] = mc; + return mc; + }else{ + return it->second; + } +} + +void TermUtil::computeVarContains( Node n, std::vector< Node >& varContains ) { + std::map< Node, bool > visited; + computeVarContains2( n, INST_CONSTANT, varContains, visited ); +} + +void TermUtil::computeQuantContains( Node n, std::vector< Node >& quantContains ) { + std::map< Node, bool > visited; + computeVarContains2( n, FORALL, quantContains, visited ); +} + + +void TermUtil::computeVarContains2( Node n, Kind k, std::vector< Node >& varContains, std::map< Node, bool >& visited ){ + if( visited.find( n )==visited.end() ){ + visited[n] = true; + if( n.getKind()==k ){ + if( std::find( varContains.begin(), varContains.end(), n )==varContains.end() ){ + varContains.push_back( n ); + } + }else{ + for( unsigned i=0; i& pats, std::map< Node, std::vector< Node > >& varContains ){ + for( unsigned i=0; i& varContains ){ + std::vector< Node > vars; + computeVarContains( n, vars ); + for( unsigned j=0; j& varContains1, std::vector< Node >& varContains2 ){ + if( n1==n2 ){ + return 1; + }else if( n1.getKind()==n2.getKind() ){ + if( n1.getKind()==APPLY_UF ){ + if( n1.getOperator()==n2.getOperator() ){ + int result = 0; + for( int i=0; i<(int)n1.getNumChildren(); i++ ){ + if( n1[i]!=n2[i] ){ + int cResult = isInstanceOf2( n1[i], n2[i], varContains1, varContains2 ); + if( cResult==0 ){ + return 0; + }else if( cResult!=result ){ + if( result!=0 ){ + return 0; + }else{ + result = cResult; + } + } + } + } + return result; + } + } + return 0; + }else if( n2.getKind()==INST_CONSTANT ){ + //if( std::find( d_var_contains[ n1 ].begin(), d_var_contains[ n1 ].end(), n2 )!=d_var_contains[ n1 ].end() ){ + // return 1; + //} + if( varContains1.size()==1 && varContains1[ 0 ]==n2 ){ + return 1; + } + }else if( n1.getKind()==INST_CONSTANT ){ + //if( std::find( d_var_contains[ n2 ].begin(), d_var_contains[ n2 ].end(), n1 )!=d_var_contains[ n2 ].end() ){ + // return -1; + //} + if( varContains2.size()==1 && varContains2[ 0 ]==n1 ){ + return 1; + } + } + return 0; +} + +int TermUtil::isInstanceOf( Node n1, Node n2 ){ + std::vector< Node > varContains1; + std::vector< Node > varContains2; + computeVarContains( n1, varContains1 ); + computeVarContains( n1, varContains2 ); + return isInstanceOf2( n1, n2, varContains1, varContains2 ); +} + +bool TermUtil::isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs ){ + if( n1==n2 ){ + return true; + }else if( n2.getKind()==INST_CONSTANT ){ + //if( !node_contains( n1, n2 ) ){ + // return false; + //} + if( subs.find( n2 )==subs.end() ){ + subs[n2] = n1; + }else if( subs[n2]!=n1 ){ + return false; + } + return true; + }else if( n1.getKind()==n2.getKind() && n1.getMetaKind()==kind::metakind::PARAMETERIZED ){ + if( n1.getOperator()!=n2.getOperator() ){ + return false; + } + for( int i=0; i<(int)n1.getNumChildren(); i++ ){ + if( !isUnifiableInstanceOf( n1[i], n2[i], subs ) ){ + return false; + } + } + return true; + }else{ + return false; + } +} + +void TermUtil::filterInstances( std::vector< Node >& nodes ){ + std::vector< bool > active; + active.resize( nodes.size(), true ); + std::map< int, std::vector< Node > > varContains; + for( unsigned i=0; i temp; + for( unsigned i=0; i::iterator it = d_op_id.find( op ); + if( it==d_op_id.end() ){ + d_op_id[op] = d_op_id_count; + d_op_id_count++; + return d_op_id[op]; + }else{ + return it->second; + } +} + +int TermUtil::getIdForType( TypeNode t ) { + std::map< TypeNode, int >::iterator it = d_typ_id.find( t ); + if( it==d_typ_id.end() ){ + d_typ_id[t] = d_typ_id_count; + d_typ_id_count++; + return d_typ_id[t]; + }else{ + return it->second; + } +} + +bool TermUtil::getTermOrder( Node a, Node b ) { + if( a.getKind()==BOUND_VARIABLE ){ + if( b.getKind()==BOUND_VARIABLE ){ + return a.getAttribute(InstVarNumAttribute())mkBoundVar( os.str().c_str(), tn ); + InstVarNumAttribute ivna; + x.setAttribute(ivna,d_cn_free_var[tn].size()); + d_cn_free_var[tn].push_back( x ); + } + return d_cn_free_var[tn][i]; +} + +struct sortTermOrder { + TermUtil* d_tu; + //std::map< Node, std::map< Node, bool > > d_cache; + bool operator() (Node i, Node j) { + /* + //must consult cache since term order is partial? + std::map< Node, bool >::iterator it = d_cache[j].find( i ); + if( it!=d_cache[j].end() && it->second ){ + return false; + }else{ + bool ret = d_tdb->getTermOrder( i, j ); + d_cache[i][j] = ret; + return ret; + } + */ + return d_tu->getTermOrder( i, j ); + } +}; + +//this function makes a canonical representation of a term ( +// - orders variables left to right +// - if apply_torder, then sort direct subterms of commutative operators +Node TermUtil::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder, std::map< TNode, Node >& visited ) { + Trace("canon-term-debug") << "Get canonical term for " << n << std::endl; + if( n.getKind()==BOUND_VARIABLE ){ + std::map< TNode, TNode >::iterator it = subs.find( n ); + if( it==subs.end() ){ + TypeNode tn = n.getType(); + //allocate variable + unsigned vn = var_count[tn]; + var_count[tn]++; + subs[n] = getCanonicalFreeVar( tn, vn ); + Trace("canon-term-debug") << "...allocate variable." << std::endl; + return subs[n]; + }else{ + Trace("canon-term-debug") << "...return variable in subs." << std::endl; + return it->second; + } + }else if( n.getNumChildren()>0 ){ + std::map< TNode, Node >::iterator it = visited.find( n ); + if( it!=visited.end() ){ + return it->second; + }else{ + //collect children + Trace("canon-term-debug") << "Collect children" << std::endl; + std::vector< Node > cchildren; + for( unsigned i=0; imkNode( n.getKind(), cchildren ); + Trace("canon-term-debug") << "...constructed " << ret << " for " << n << "." << std::endl; + visited[n] = ret; + return ret; + } + }else{ + Trace("canon-term-debug") << "...return 0-child term." << std::endl; + return n; + } +} + +Node TermUtil::getCanonicalTerm( TNode n, bool apply_torder ){ + std::map< TypeNode, unsigned > var_count; + std::map< TNode, TNode > subs; + std::map< TNode, Node > visited; + return getCanonicalTerm( n, var_count, subs, apply_torder, visited ); +} + +void TermUtil::getVtsTerms( std::vector< Node >& t, bool isFree, bool create, bool inc_delta ) { + if( inc_delta ){ + Node delta = getVtsDelta( isFree, create ); + if( !delta.isNull() ){ + t.push_back( delta ); + } + } + for( unsigned r=0; r<2; r++ ){ + Node inf = getVtsInfinityIndex( r, isFree, create ); + if( !inf.isNull() ){ + t.push_back( inf ); + } + } +} + +Node TermUtil::getVtsDelta( bool isFree, bool create ) { + if( create ){ + if( d_vts_delta_free.isNull() ){ + d_vts_delta_free = NodeManager::currentNM()->mkSkolem( "delta_free", NodeManager::currentNM()->realType(), "free delta for virtual term substitution" ); + Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_vts_delta_free, d_zero ); + d_quantEngine->getOutputChannel().lemma( delta_lem ); + } + if( d_vts_delta.isNull() ){ + d_vts_delta = NodeManager::currentNM()->mkSkolem( "delta", NodeManager::currentNM()->realType(), "delta for virtual term substitution" ); + //mark as a virtual term + VirtualTermSkolemAttribute vtsa; + d_vts_delta.setAttribute(vtsa,true); + } + } + return isFree ? d_vts_delta_free : d_vts_delta; +} + +Node TermUtil::getVtsInfinity( TypeNode tn, bool isFree, bool create ) { + if( create ){ + if( d_vts_inf_free[tn].isNull() ){ + d_vts_inf_free[tn] = NodeManager::currentNM()->mkSkolem( "inf_free", tn, "free infinity for virtual term substitution" ); + } + if( d_vts_inf[tn].isNull() ){ + d_vts_inf[tn] = NodeManager::currentNM()->mkSkolem( "inf", tn, "infinity for virtual term substitution" ); + //mark as a virtual term + VirtualTermSkolemAttribute vtsa; + d_vts_inf[tn].setAttribute(vtsa,true); + } + } + return isFree ? d_vts_inf_free[tn] : d_vts_inf[tn]; +} + +Node TermUtil::getVtsInfinityIndex( int i, bool isFree, bool create ) { + if( i==0 ){ + return getVtsInfinity( NodeManager::currentNM()->realType(), isFree, create ); + }else if( i==1 ){ + return getVtsInfinity( NodeManager::currentNM()->integerType(), isFree, create ); + }else{ + Assert( false ); + return Node::null(); + } +} + +Node TermUtil::substituteVtsFreeTerms( Node n ) { + std::vector< Node > vars; + getVtsTerms( vars, false, false ); + std::vector< Node > vars_free; + getVtsTerms( vars_free, true, false ); + Assert( vars.size()==vars_free.size() ); + if( !vars.empty() ){ + return n.substitute( vars.begin(), vars.end(), vars_free.begin(), vars_free.end() ); + }else{ + return n; + } +} + +Node TermUtil::rewriteVtsSymbols( Node n ) { + if( ( n.getKind()==EQUAL || n.getKind()==GEQ ) ){ + Trace("quant-vts-debug") << "VTS : process " << n << std::endl; + Node rew_vts_inf; + bool rew_delta = false; + //rewriting infinity always takes precedence over rewriting delta + for( unsigned r=0; r<2; r++ ){ + Node inf = getVtsInfinityIndex( r, false, false ); + if( !inf.isNull() && containsTerm( n, inf ) ){ + if( rew_vts_inf.isNull() ){ + rew_vts_inf = inf; + }else{ + //for mixed int/real with multiple infinities + Trace("quant-vts-debug") << "Multiple infinities...equate " << inf << " = " << rew_vts_inf << std::endl; + std::vector< Node > subs_lhs; + subs_lhs.push_back( inf ); + std::vector< Node > subs_rhs; + subs_lhs.push_back( rew_vts_inf ); + n = n.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() ); + n = Rewriter::rewrite( n ); + //may have cancelled + if( !containsTerm( n, rew_vts_inf ) ){ + rew_vts_inf = Node::null(); + } + } + } + } + if( rew_vts_inf.isNull() ){ + if( !d_vts_delta.isNull() && containsTerm( n, d_vts_delta ) ){ + rew_delta = true; + } + } + if( !rew_vts_inf.isNull() || rew_delta ){ + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( n, msum ) ){ + if( Trace.isOn("quant-vts-debug") ){ + Trace("quant-vts-debug") << "VTS got monomial sum : " << std::endl; + QuantArith::debugPrintMonomialSum( msum, "quant-vts-debug" ); + } + Node vts_sym = !rew_vts_inf.isNull() ? rew_vts_inf : d_vts_delta; + Assert( !vts_sym.isNull() ); + Node iso_n; + Node nlit; + int res = QuantArith::isolate( vts_sym, msum, iso_n, n.getKind(), true ); + if( res!=0 ){ + Trace("quant-vts-debug") << "VTS isolated : -> " << iso_n << ", res = " << res << std::endl; + Node slv = iso_n[res==1 ? 1 : 0]; + //ensure the vts terms have been eliminated + if( containsVtsTerm( slv ) ){ + Trace("quant-vts-warn") << "Bad vts literal : " << n << ", contains " << vts_sym << " but bad solved form " << slv << "." << std::endl; + nlit = substituteVtsFreeTerms( n ); + Trace("quant-vts-debug") << "...return " << nlit << std::endl; + //Assert( false ); + //safe case: just convert to free symbols + return nlit; + }else{ + if( !rew_vts_inf.isNull() ){ + nlit = ( n.getKind()==GEQ && res==1 ) ? d_true : d_false; + }else{ + Assert( iso_n[res==1 ? 0 : 1]==d_vts_delta ); + if( n.getKind()==EQUAL ){ + nlit = d_false; + }else if( res==1 ){ + nlit = NodeManager::currentNM()->mkNode( GEQ, d_zero, slv ); + }else{ + nlit = NodeManager::currentNM()->mkNode( GT, slv, d_zero ); + } + } + } + Trace("quant-vts-debug") << "Return " << nlit << std::endl; + return nlit; + }else{ + Trace("quant-vts-warn") << "Bad vts literal : " << n << ", contains " << vts_sym << " but could not isolate." << std::endl; + //safe case: just convert to free symbols + nlit = substituteVtsFreeTerms( n ); + Trace("quant-vts-debug") << "...return " << nlit << std::endl; + //Assert( false ); + return nlit; + } + } + } + return n; + }else if( n.getKind()==FORALL ){ + //cannot traverse beneath quantifiers + return substituteVtsFreeTerms( n ); + }else{ + bool childChanged = false; + std::vector< Node > children; + for( unsigned i=0; imkNode( n.getKind(), children ); + Trace("quant-vts-debug") << "...make node " << ret << std::endl; + return ret; + }else{ + return n; + } + } +} + +bool TermUtil::containsVtsTerm( Node n, bool isFree ) { + std::vector< Node > t; + getVtsTerms( t, isFree, false ); + return containsTerms( n, t ); +} + +bool TermUtil::containsVtsTerm( std::vector< Node >& n, bool isFree ) { + std::vector< Node > t; + getVtsTerms( t, isFree, false ); + if( !t.empty() ){ + for( unsigned i=0; i t; + getVtsTerms( t, isFree, false, false ); + return containsTerms( n, t ); +} + +Node TermUtil::ensureType( Node n, TypeNode tn ) { + TypeNode ntn = n.getType(); + Assert( ntn.isComparableTo( tn ) ); + if( ntn.isSubtypeOf( tn ) ){ + return n; + }else{ + if( tn.isInteger() ){ + return NodeManager::currentNM()->mkNode( TO_INTEGER, n ); + } + return Node::null(); + } +} + +void TermUtil::getRelevancyCondition( Node n, std::vector< Node >& cond ) { + if( n.getKind()==APPLY_SELECTOR_TOTAL ){ + // don't worry about relevancy conditions if using shared selectors + if( !options::dtSharedSelectors() ){ + unsigned scindex = Datatype::cindexOf(n.getOperator().toExpr()); + const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype(); + Node rc = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[scindex].getTester() ), n[0] ).negate(); + if( std::find( cond.begin(), cond.end(), rc )==cond.end() ){ + cond.push_back( rc ); + } + getRelevancyCondition( n[0], cond ); + } + } +} + +bool TermUtil::containsTerm2( Node n, Node t, std::map< Node, bool >& visited ) { + if( n==t ){ + return true; + }else{ + if( visited.find( n )==visited.end() ){ + visited[n] = true; + for( unsigned i=0; i& t, std::map< Node, bool >& visited ) { + if( visited.find( n )==visited.end() ){ + if( std::find( t.begin(), t.end(), n )!=t.end() ){ + return true; + }else{ + visited[n] = true; + for( unsigned i=0; i visited; + return containsTerm2( n, t, visited ); +} + +bool TermUtil::containsTerms( Node n, std::vector< Node >& t ) { + if( t.empty() ){ + return false; + }else{ + std::map< Node, bool > visited; + return containsTerms2( n, t, visited ); + } +} + +int TermUtil::getTermDepth( Node n ) { + if (!n.hasAttribute(TermDepthAttribute()) ){ + int maxDepth = -1; + for( unsigned i=0; imaxDepth ){ + maxDepth = depth; + } + } + TermDepthAttribute tda; + n.setAttribute(tda,1+maxDepth); + } + return n.getAttribute(TermDepthAttribute()); +} + +bool TermUtil::containsUninterpretedConstant( Node n ) { + if (!n.hasAttribute(ContainsUConstAttribute()) ){ + bool ret = false; + if( n.getKind()==UNINTERPRETED_CONSTANT ){ + ret = true; + }else{ + for( unsigned i=0; i children; + for( unsigned i=0; imkNode( n.getKind()==OR ? AND : OR, children ); + }else{ + return n.negate(); + } +} + +bool TermUtil::isAssoc( Kind k ) { + return k==PLUS || k==MULT || k==AND || k==OR || + k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT || + k==STRING_CONCAT; +} + +bool TermUtil::isComm( Kind k ) { + return k==EQUAL || k==PLUS || k==MULT || k==AND || k==OR || k==XOR || + k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR; +} + +bool TermUtil::isNonAdditive( Kind k ) { + return k==AND || k==OR || k==BITVECTOR_AND || k==BITVECTOR_OR; +} + +bool TermUtil::isBoolConnective( Kind k ) { + return k==OR || k==AND || k==EQUAL || k==ITE || k==FORALL || k==NOT || k==SEP_STAR; +} + +bool TermUtil::isBoolConnectiveTerm( TNode n ) { + return isBoolConnective( n.getKind() ) && + ( n.getKind()!=EQUAL || n[0].getType().isBoolean() ) && + ( n.getKind()!=ITE || n.getType().isBoolean() ); +} + +void TermUtil::registerTrigger( theory::inst::Trigger* tr, Node op ){ + if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){ + d_op_triggers[op].push_back( tr ); + } +} + +Node TermUtil::getHoTypeMatchPredicate( TypeNode tn ) { + std::map< TypeNode, Node >::iterator ithp = d_ho_type_match_pred.find( tn ); + if( ithp==d_ho_type_match_pred.end() ){ + TypeNode ptn = NodeManager::currentNM()->mkFunctionType( tn, NodeManager::currentNM()->booleanType() ); + Node k = NodeManager::currentNM()->mkSkolem( "U", ptn, "predicate to force higher-order types" ); + d_ho_type_match_pred[tn] = k; + return k; + }else{ + return ithp->second; + } +} + +bool TermUtil::isInductionTerm( Node n ) { + TypeNode tn = n.getType(); + if( options::dtStcInduction() && tn.isDatatype() ){ + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + return !dt.isCodatatype(); + } + if( options::intWfInduction() && n.getType().isInteger() ){ + return true; + } + return false; +} + +}/* CVC4::theory::quantifiers namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h new file mode 100644 index 000000000..2360c5bfb --- /dev/null +++ b/src/theory/quantifiers/term_util.h @@ -0,0 +1,346 @@ +/********************* */ +/*! \file term_util.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief term utilities class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H +#define __CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H + +#include +#include + +#include "expr/attribute.h" +#include "theory/type_enumerator.h" + +namespace CVC4 { +namespace theory { + +// attribute for "contains instantiation constants from" +struct InstConstantAttributeId {}; +typedef expr::Attribute InstConstantAttribute; + +struct BoundVarAttributeId {}; +typedef expr::Attribute BoundVarAttribute; + +struct InstLevelAttributeId {}; +typedef expr::Attribute InstLevelAttribute; + +struct InstVarNumAttributeId {}; +typedef expr::Attribute InstVarNumAttribute; + +struct TermDepthAttributeId {}; +typedef expr::Attribute TermDepthAttribute; + +struct ContainsUConstAttributeId {}; +typedef expr::Attribute ContainsUConstAttribute; + +struct ModelBasisAttributeId {}; +typedef expr::Attribute ModelBasisAttribute; +//for APPLY_UF terms, 1 : term has direct child with model basis attribute, +// 0 : term has no direct child with model basis attribute. +struct ModelBasisArgAttributeId {}; +typedef expr::Attribute ModelBasisArgAttribute; + +//for bounded integers +struct BoundIntLitAttributeId {}; +typedef expr::Attribute BoundIntLitAttribute; + +//for quantifier instantiation level +struct QuantInstLevelAttributeId {}; +typedef expr::Attribute QuantInstLevelAttribute; + +//rewrite-rule priority +struct RrPriorityAttributeId {}; +typedef expr::Attribute RrPriorityAttribute; + +/** Attribute true for quantifiers that do not need to be partially instantiated */ +struct LtePartialInstAttributeId {}; +typedef expr::Attribute< LtePartialInstAttributeId, bool > LtePartialInstAttribute; + +// attribute for "contains instantiation constants from" +struct SygusProxyAttributeId {}; +typedef expr::Attribute SygusProxyAttribute; + +// attribute for associating a synthesis function with a first order variable +struct SygusSynthFunAttributeId {}; +typedef expr::Attribute SygusSynthFunAttribute; + +// attribute for associating a variable list with a synth fun +struct SygusSynthFunVarListAttributeId {}; +typedef expr::Attribute SygusSynthFunVarListAttribute; + +//attribute for fun-def abstraction type +struct AbsTypeFunDefAttributeId {}; +typedef expr::Attribute AbsTypeFunDefAttribute; + +/** Attribute for id number */ +struct QuantIdNumAttributeId {}; +typedef expr::Attribute< QuantIdNumAttributeId, uint64_t > QuantIdNumAttribute; + +/** sygus var num */ +struct SygusVarNumAttributeId {}; +typedef expr::Attribute SygusVarNumAttribute; + +/** Attribute to mark Skolems as virtual terms */ +struct VirtualTermSkolemAttributeId {}; +typedef expr::Attribute< VirtualTermSkolemAttributeId, bool > VirtualTermSkolemAttribute; + +class QuantifiersEngine; + +namespace inst{ + class Trigger; + class HigherOrderTrigger; +} + +namespace quantifiers { + +class TermDatabase; + +// TODO : #1216 split this class, most of the functions in this class should be dispersed to where they are used. +class TermUtil { + // TODO : remove these + friend class ::CVC4::theory::QuantifiersEngine; + friend class TermDatabase; +private: + /** reference to the quantifiers engine */ + QuantifiersEngine* d_quantEngine; +public: + TermUtil(QuantifiersEngine * qe); + ~TermUtil(); + /** boolean terms */ + Node d_true; + Node d_false; + /** constants */ + Node d_zero; + Node d_one; + + /** register quantifier */ + void registerQuantifier( Node q ); + +//for inst constant +private: + /** map from universal quantifiers to the list of variables */ + std::map< Node, std::vector< Node > > d_vars; + std::map< Node, std::map< Node, unsigned > > d_var_num; + /** map from universal quantifiers to their inst constant body */ + std::map< Node, Node > d_inst_const_body; + /** map from universal quantifiers to their counterexample literals */ + std::map< Node, Node > d_ce_lit; + /** instantiation constants to universal quantifiers */ + std::map< Node, Node > d_inst_constants_map; +public: + /** map from universal quantifiers to the list of instantiation constants */ + std::map< Node, std::vector< Node > > d_inst_constants; + /** get variable number */ + unsigned getVariableNum( Node q, Node v ) { return d_var_num[q][v]; } + /** get the i^th instantiation constant of q */ + Node getInstantiationConstant( Node q, int i ) const; + /** get number of instantiation constants for q */ + unsigned getNumInstantiationConstants( Node q ) const; + /** get the ce body q[e/x] */ + Node getInstConstantBody( Node q ); + /** get counterexample literal (for cbqi) */ + Node getCounterexampleLiteral( Node q ); + /** returns node n with bound vars of q replaced by instantiation constants of q + node n : is the future pattern + node q : is the quantifier containing which bind the variable + return a pattern where the variable are replaced by variable for + instantiation. + */ + Node getInstConstantNode( Node n, Node q ); + Node getVariableNode( Node n, Node q ); + /** get substituted node */ + Node getInstantiatedNode( Node n, Node q, std::vector< Node >& terms ); + + static Node getInstConstAttr( Node n ); + static bool hasInstConstAttr( Node n ); + static Node getBoundVarAttr( Node n ); + static bool hasBoundVarAttr( Node n ); + +private: + /** get bound vars */ + static void getBoundVars2( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited ); + /** get bound vars */ + static Node getRemoveQuantifiers2( Node n, std::map< Node, Node >& visited ); +public: + //get the bound variables in this node + static void getBoundVars( Node n, std::vector< Node >& vars ); + //remove quantifiers + static Node getRemoveQuantifiers( Node n ); + //quantified simplify (treat free variables in n as quantified and run rewriter) + static Node getQuantSimplify( Node n ); + +//for skolem +private: + /** map from universal quantifiers to their skolemized body */ + std::map< Node, Node > d_skolem_body; +public: + /** map from universal quantifiers to the list of skolem constants */ + std::map< Node, std::vector< Node > > d_skolem_constants; + /** make the skolemized body f[e/x] */ + static Node mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& fvTypes, std::vector< TNode >& fvs, + std::vector< Node >& sk, Node& sub, std::vector< unsigned >& sub_vars ); + /** get the skolemized body */ + Node getSkolemizedBody( Node f); + /** is induction variable */ + static bool isInductionTerm( Node n ); + +//for ground term enumeration +private: + /** ground terms enumerated for types */ + std::map< TypeNode, std::vector< Node > > d_enum_terms; + //type enumerators + std::map< TypeNode, unsigned > d_typ_enum_map; + std::vector< TypeEnumerator > d_typ_enum; + // closed enumerable type cache + std::map< TypeNode, bool > d_typ_closed_enum; + /** may complete */ + std::map< TypeNode, bool > d_may_complete; +public: + //get nth term for type + Node getEnumerateTerm( TypeNode tn, unsigned index ); + //does this type have an enumerator that produces constants that are handled by ground theory solvers + bool isClosedEnumerableType( TypeNode tn ); + // may complete + bool mayComplete( TypeNode tn ); + +//for triggers +private: + /** helper function for compute var contains */ + static void computeVarContains2( Node n, Kind k, std::vector< Node >& varContains, std::map< Node, bool >& visited ); + /** triggers for each operator */ + std::map< Node, std::vector< inst::Trigger* > > d_op_triggers; + /** helper for is instance of */ + static bool isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs ); + /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */ + static int isInstanceOf2( Node n1, Node n2, std::vector< Node >& varContains1, std::vector< Node >& varContains2 ); +public: + /** compute var contains */ + static void computeVarContains( Node n, std::vector< Node >& varContains ); + /** get var contains for each of the patterns in pats */ + static void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains ); + /** get var contains for node n */ + static void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ); + /** compute quant contains */ + static void computeQuantContains( Node n, std::vector< Node >& quantContains ); + /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */ + static int isInstanceOf( Node n1, Node n2 ); + /** filter all nodes that have instances */ + static void filterInstances( std::vector< Node >& nodes ); + /** register trigger (for eager quantifier instantiation) */ + void registerTrigger( inst::Trigger* tr, Node op ); + +//for term ordering +private: + /** operator id count */ + int d_op_id_count; + /** map from operators to id */ + std::map< Node, int > d_op_id; + /** type id count */ + int d_typ_id_count; + /** map from type to id */ + std::map< TypeNode, int > d_typ_id; + //free variables + std::map< TypeNode, std::vector< Node > > d_cn_free_var; + // get canonical term, return null if it contains a term apart from handled signature + Node getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder, + std::map< TNode, Node >& visited ); +public: + /** get id for operator */ + int getIdForOperator( Node op ); + /** get id for type */ + int getIdForType( TypeNode t ); + /** get term order */ + bool getTermOrder( Node a, Node b ); + /** get canonical free variable #i of type tn */ + Node getCanonicalFreeVar( TypeNode tn, unsigned i ); + /** get canonical term */ + Node getCanonicalTerm( TNode n, bool apply_torder = false ); + +//for virtual term substitution +private: + Node d_vts_delta; + std::map< TypeNode, Node > d_vts_inf; + Node d_vts_delta_free; + std::map< TypeNode, Node > d_vts_inf_free; + /** get vts infinity index */ + Node getVtsInfinityIndex( int i, bool isFree = false, bool create = true ); + /** substitute vts free terms */ + Node substituteVtsFreeTerms( Node n ); +public: + /** get vts delta */ + Node getVtsDelta( bool isFree = false, bool create = true ); + /** get vts infinity */ + Node getVtsInfinity( TypeNode tn, bool isFree = false, bool create = true ); + /** get all vts terms */ + void getVtsTerms( std::vector< Node >& t, bool isFree = false, bool create = true, bool inc_delta = true ); + /** rewrite delta */ + Node rewriteVtsSymbols( Node n ); + /** simple check for contains term */ + bool containsVtsTerm( Node n, bool isFree = false ); + /** simple check for contains term */ + bool containsVtsTerm( std::vector< Node >& n, bool isFree = false ); + /** simple check for contains term */ + bool containsVtsInfinity( Node n, bool isFree = false ); + /** ensure type */ + static Node ensureType( Node n, TypeNode tn ); + /** get relevancy condition */ + static void getRelevancyCondition( Node n, std::vector< Node >& cond ); + +//general utilities +private: + //helper for contains term + static bool containsTerm2( Node n, Node t, std::map< Node, bool >& visited ); + static bool containsTerms2( Node n, std::vector< Node >& t, std::map< Node, bool >& visited ); +public: + /** simple check for whether n contains t as subterm */ + static bool containsTerm( Node n, Node t ); + /** simple check for contains term, true if contains at least one term in t */ + static bool containsTerms( Node n, std::vector< Node >& t ); + /** contains uninterpreted constant */ + static bool containsUninterpretedConstant( Node n ); + /** get the term depth of n */ + static int getTermDepth( Node n ); + /** simple negate */ + static Node simpleNegate( Node n ); + /** is assoc */ + static bool isAssoc( Kind k ); + /** is comm */ + static bool isComm( Kind k ); + /** ( x k ... ) k x = ( x k ... ) */ + static bool isNonAdditive( Kind k ); + /** is bool connective */ + static bool isBoolConnective( Kind k ); + /** is bool connective term */ + static bool isBoolConnectiveTerm( TNode n ); + +//for higher-order +private: + /** dummy predicate that states terms should be considered first-class members of equality engine */ + std::map< TypeNode, Node > d_ho_type_match_pred; +public: + /** get higher-order type match predicate + * This predicate is used to force certain functions f of type tn to appear as first-class representatives in the + * quantifier-free UF solver. For a typical use case, we call getHoTypeMatchPredicate which returns a fresh + * predicate P of type (tn -> Bool). Then, we add P( f ) as a lemma. + * TODO: we may eliminate this depending on how github issue #1115 is resolved. + */ + Node getHoTypeMatchPredicate( TypeNode tn ); +};/* class TermUtil */ + +}/* CVC4::theory::quantifiers namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H */ diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 00a358e5f..855cdb911 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -24,6 +24,7 @@ #include "theory/quantifiers/model_engine.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" #include "theory/valuation.h" @@ -74,7 +75,7 @@ void TheoryQuantifiers::notifyEq(TNode lhs, TNode rhs) { void TheoryQuantifiers::preRegisterTerm(TNode n) { Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl; if( n.getKind()==FORALL ){ - if( !options::cbqi() || options::recurseCbqi() || !TermDb::hasInstConstAttr(n) ){ + if( !options::cbqi() || options::recurseCbqi() || !TermUtil::hasInstConstAttr(n) ){ getQuantifiersEngine()->registerQuantifier( n ); Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() done " << n << endl; } @@ -186,18 +187,18 @@ Node TheoryQuantifiers::getNextDecisionRequest( unsigned& priority ){ void TheoryQuantifiers::assertUniversal( Node n ){ Assert( n.getKind()==FORALL ); - if( !options::cbqi() || options::recurseCbqi() || !TermDb::hasInstConstAttr(n) ){ + if( !options::cbqi() || options::recurseCbqi() || !TermUtil::hasInstConstAttr(n) ){ getQuantifiersEngine()->assertQuantifier( n, true ); } } void TheoryQuantifiers::assertExistential( Node n ){ Assert( n.getKind()== NOT && n[0].getKind()==FORALL ); - if( !options::cbqi() || options::recurseCbqi() || !TermDb::hasInstConstAttr(n[0]) ){ + if( !options::cbqi() || options::recurseCbqi() || !TermUtil::hasInstConstAttr(n[0]) ){ getQuantifiersEngine()->assertQuantifier( n[0], false ); } } void TheoryQuantifiers::setUserAttribute(const std::string& attr, Node n, std::vector node_values, std::string str_value){ - QuantifiersAttributes::setUserAttribute( attr, n, node_values, str_value ); + QuantAttributes::setUserAttribute( attr, n, node_values, str_value ); } diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 20933c7f7..01cf655ac 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -16,6 +16,7 @@ #include "theory/quantifiers/candidate_generator.h" #include "theory/quantifiers/inst_match_generator.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" #include "theory/uf/equality_engine.h" @@ -32,7 +33,7 @@ namespace inst { void TriggerTermInfo::init( Node q, Node n, int reqPol, Node reqPolEq ){ if( d_fv.empty() ){ - quantifiers::TermDb::getVarContainsNode( q, n, d_fv ); + quantifiers::TermUtil::getVarContainsNode( q, n, d_fv ); } if( d_reqPol==0 ){ d_reqPol = reqPol; @@ -125,12 +126,12 @@ bool Trigger::mkTriggerTerms( Node q, std::vector< Node >& nodes, unsigned n_var std::map< Node, std::vector< Node > > patterns; size_t varCount = 0; std::map< Node, std::vector< Node > > varContains; - quantifiers::TermDb::getVarContains( q, temp, varContains ); + quantifiers::TermUtil::getVarContains( q, temp, varContains ); for( unsigned i=0; imkNode( n.getKind(), n[1], n[0] ); }else{ return n; @@ -268,16 +269,16 @@ Node Trigger::getIsUsableEq( Node q, Node n ) { bool Trigger::isUsableEqTerms( Node q, Node n1, Node n2 ) { if( n1.getKind()==INST_CONSTANT ){ if( options::relationalTriggers() ){ - if( !quantifiers::TermDb::hasInstConstAttr(n2) ){ + if( !quantifiers::TermUtil::hasInstConstAttr(n2) ){ return true; }else if( n2.getKind()==INST_CONSTANT ){ return true; } } }else if( isUsableAtomicTrigger( n1, q ) ){ - if( options::relationalTriggers() && n2.getKind()==INST_CONSTANT && !quantifiers::TermDb::containsTerm( n1, n2 ) ){ + if( options::relationalTriggers() && n2.getKind()==INST_CONSTANT && !quantifiers::TermUtil::containsTerm( n1, n2 ) ){ return true; - }else if( !quantifiers::TermDb::hasInstConstAttr(n2) ){ + }else if( !quantifiers::TermUtil::hasInstConstAttr(n2) ){ return true; } } @@ -329,7 +330,7 @@ Node Trigger::getIsUsableTrigger( Node n, Node q ) { return rtr2; } }else{ - Trace("trigger-debug") << n << " usable : " << ( quantifiers::TermDb::getInstConstAttr(n)==q ) << " " << isAtomicTrigger( n ) << " " << isUsable( n, q ) << std::endl; + Trace("trigger-debug") << n << " usable : " << ( quantifiers::TermUtil::getInstConstAttr(n)==q ) << " " << isAtomicTrigger( n ) << " " << isUsable( n, q ) << std::endl; if( isUsableAtomicTrigger( n, q ) ){ return pol ? n : NodeManager::currentNM()->mkNode( EQUAL, n, NodeManager::currentNM()->mkConst( true ) ).notNode(); } @@ -338,7 +339,7 @@ Node Trigger::getIsUsableTrigger( Node n, Node q ) { } bool Trigger::isUsableAtomicTrigger( Node n, Node q ) { - return quantifiers::TermDb::getInstConstAttr( n )==q && isAtomicTrigger( n ) && isUsable( n, q ); + return quantifiers::TermUtil::getInstConstAttr( n )==q && isAtomicTrigger( n ) && isUsable( n, q ); } bool Trigger::isUsableTrigger( Node n, Node q ){ @@ -366,7 +367,7 @@ bool Trigger::isRelationalTriggerKind( Kind k ) { } bool Trigger::isCbqiKind( Kind k ) { - if( quantifiers::TermDb::isBoolConnective( k ) || k==PLUS || k==GEQ || k==EQUAL || k==MULT ){ + if( quantifiers::TermUtil::isBoolConnective( k ) || k==PLUS || k==GEQ || k==EQUAL || k==MULT ){ return true; }else{ //CBQI typically works for satisfaction-complete theories @@ -378,13 +379,13 @@ bool Trigger::isCbqiKind( Kind k ) { bool Trigger::isSimpleTrigger( Node n ){ Node t = n.getKind()==NOT ? n[0] : n; if( t.getKind()==EQUAL ){ - if( !quantifiers::TermDb::hasInstConstAttr( t[1] ) ){ + if( !quantifiers::TermUtil::hasInstConstAttr( t[1] ) ){ t = t[0]; } } if( isAtomicTrigger( t ) ){ for( unsigned i=0; i& patTerms, qu collectPatTerms( q, n, patTerms2, quantifiers::TRIGGER_SEL_ALL, exclude, tinfo2, false ); std::vector< Node > temp; temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() ); - quantifiers::TermDb::filterInstances( temp ); + quantifiers::TermUtil::filterInstances( temp ); if( temp.size()!=patTerms2.size() ){ Trace("trigger-filter-instance") << "Filtered an instance: " << std::endl; Trace("trigger-filter-instance") << "Old: "; @@ -625,7 +626,7 @@ Node Trigger::getInversionVariable( Node n ) { }else if( n.getKind()==PLUS || n.getKind()==MULT ){ Node ret; for( unsigned i=0; imkNode( MINUS, x, n[i] ); }else if( n.getKind()==MULT ){ @@ -702,7 +703,7 @@ void Trigger::getTriggerVariables( Node icn, Node q, std::vector< Node >& t_vars collectPatTerms( q, icn, patTerms, quantifiers::TRIGGER_SEL_ALL, exclude, tinfo ); //collect all variables from all patterns in patTerms, add to t_vars for( unsigned i=0; id_true] = true; + d_lemmas_produced_c[d_term_util->d_true] = true; Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl; Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl; @@ -166,6 +186,9 @@ QuantifiersEngine::~QuantifiersEngine(){ delete d_model; delete d_tr_trie; delete d_term_db; + delete d_sygus_tdb; + delete d_term_util; + delete d_eq_inference; delete d_eq_query; delete d_sg_gen; delete d_ceg_inst; @@ -179,7 +202,7 @@ QuantifiersEngine::~QuantifiersEngine(){ delete d_inst_prop; } -EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() { +EqualityQuery* QuantifiersEngine::getEqualityQuery() { return d_eq_query; } @@ -337,7 +360,7 @@ bool QuantifiersEngine::isFiniteBound( Node q, Node v ) { TypeNode tn = v.getType(); if( tn.isSort() && options::finiteModelFind() ){ return true; - }else if( getTermDatabase()->mayComplete( tn ) ){ + }else if( getTermUtil()->mayComplete( tn ) ){ return true; } } @@ -717,9 +740,16 @@ bool QuantifiersEngine::registerQuantifier( Node f ){ d_quants[f] = false; return false; }else{ - //make instantiation constants for f - d_term_db->makeInstantiationConstantsFor( f ); - d_term_db->computeAttributes( f ); + // register with utilities : TODO (#1163) make this a standard call + + d_term_util->registerQuantifier( f ); + d_term_db->registerQuantifier( f ); + d_quant_attr->computeAttributes( f ); + //register with quantifier relevance + if( d_quant_rel ){ + d_quant_rel->registerQuantifier( f ); + } + for( unsigned i=0; iidentify() << "..." << std::endl; d_modules[i]->preRegisterQuantifier( f ); @@ -728,17 +758,13 @@ bool QuantifiersEngine::registerQuantifier( Node f ){ if( qm!=NULL ){ Trace("quant") << " Owner : " << qm->identify() << std::endl; } - //register with quantifier relevance - if( d_quant_rel ){ - d_quant_rel->registerQuantifier( f ); - } //register with each module for( unsigned i=0; iidentify() << "..." << std::endl; d_modules[i]->registerQuantifier( f ); } //TODO: remove this - Node ceBody = d_term_db->getInstConstantBody( f ); + Node ceBody = d_term_util->getInstConstantBody( f ); //also register it with the strong solver //if( options::finiteModelFind() ){ // ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f ); @@ -767,7 +793,7 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ if( !reduceQuantifier( f ) ){ //do skolemization if( d_skolemized.find( f )==d_skolemized.end() ){ - Node body = d_term_db->getSkolemizedBody( f ); + Node body = d_term_util->getSkolemizedBody( f ); NodeBuilder<> nb(kind::OR); nb << f << body.notNode(); Node lem = nb; @@ -787,7 +813,7 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ for( unsigned i=0; iassertNode( f ); } - addTermToDatabase( d_term_db->getInstConstantBody( f ), true ); + addTermToDatabase( d_term_util->getInstConstantBody( f ), true ); } } } @@ -813,10 +839,6 @@ Node QuantifiersEngine::getNextDecisionRequest( unsigned& priority ){ return dec; } -quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() { - return getTermDatabase()->getTermDatabaseSygus(); -} - void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool withinInstClosure ){ if( options::incrementalSolving() ){ if( d_presolve_in.find( n )==d_presolve_in.end() ){ @@ -844,14 +866,14 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool within void QuantifiersEngine::eqNotifyNewClass(TNode t) { addTermToDatabase( t ); - if( d_eq_query->getEqualityInference() ){ - d_eq_query->getEqualityInference()->eqNotifyNewClass( t ); + if( d_eq_inference ){ + d_eq_inference->eqNotifyNewClass( t ); } } void QuantifiersEngine::eqNotifyPreMerge(TNode t1, TNode t2) { - if( d_eq_query->getEqualityInference() ){ - d_eq_query->getEqualityInference()->eqNotifyMerge( t1, t2 ); + if( d_eq_inference ){ + d_eq_inference->eqNotifyMerge( t1, t2 ); } } @@ -947,7 +969,7 @@ Node QuantifiersEngine::getSubstitute( Node n, std::vector< Node >& terms, std:: Debug("check-inst") << "Substitute inst constant : " << n << std::endl; ret = terms[n.getAttribute(InstVarNumAttribute())]; }else{ - //if( !quantifiers::TermDb::hasInstConstAttr( n ) ){ + //if( !quantifiers::TermUtil::hasInstConstAttr( n ) ){ //Debug("check-inst") << "No inst const attr : " << n << std::endl; //return n; //}else{ @@ -998,7 +1020,7 @@ Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); }else{ //do optimized version - Node icb = d_term_db->getInstConstantBody( q ); + Node icb = d_term_util->getInstConstantBody( q ); std::map< Node, Node > visited; body = getSubstitute( icb, terms, visited ); if( Debug.isOn("check-inst") ){ @@ -1013,7 +1035,7 @@ Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std //do virtual term substitution body = Rewriter::rewrite( body ); Trace("quant-vts-debug") << "Rewrite vts symbols in " << body << std::endl; - Node body_r = d_term_db->rewriteVtsSymbols( body ); + Node body_r = d_term_util->rewriteVtsSymbols( body ); Trace("quant-vts-debug") << " ...result: " << body_r << std::endl; body = body_r; } @@ -1028,8 +1050,8 @@ Node QuantifiersEngine::getInstantiation( Node q, InstMatch& m, bool doVts ){ } Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& terms, bool doVts ) { - Assert( d_term_db->d_vars.find( q )!=d_term_db->d_vars.end() ); - return getInstantiation( q, d_term_db->d_vars[q], terms, doVts ); + Assert( d_term_util->d_vars.find( q )!=d_term_util->d_vars.end() ); + return getInstantiation( q, d_term_util->d_vars[q], terms, doVts ); } /* @@ -1114,7 +1136,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo terms[i] = getInternalRepresentative( terms[i], q, i ); }else{ //ensure the type is correct - terms[i] = quantifiers::TermDb::ensureType( terms[i], q[0][i].getType() ); + terms[i] = quantifiers::TermUtil::ensureType( terms[i], q[0][i].getType() ); } Trace("inst-add-debug") << " -> " << terms[i] << std::endl; if( terms[i].isNull() ){ @@ -1123,24 +1145,24 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo }else{ //get relevancy conditions if( options::instRelevantCond() ){ - quantifiers::TermDb::getRelevancyCondition( terms[i], rlv_cond ); + quantifiers::TermUtil::getRelevancyCondition( terms[i], rlv_cond ); } } #ifdef CVC4_ASSERTIONS bool bad_inst = false; - if( quantifiers::TermDb::containsUninterpretedConstant( terms[i] ) ){ + if( quantifiers::TermUtil::containsUninterpretedConstant( terms[i] ) ){ Trace("inst") << "***& inst contains uninterpreted constant : " << terms[i] << std::endl; bad_inst = true; }else if( !terms[i].getType().isSubtypeOf( q[0][i].getType() ) ){ Trace("inst") << "***& inst bad type : " << terms[i] << " " << terms[i].getType() << "/" << q[0][i].getType() << std::endl; bad_inst = true; }else if( options::cbqi() ){ - Node icf = quantifiers::TermDb::getInstConstAttr(terms[i]); + Node icf = quantifiers::TermUtil::getInstConstAttr(terms[i]); if( !icf.isNull() ){ if( icf==q ){ Trace("inst") << "***& inst contains inst constant attr : " << terms[i] << std::endl; bad_inst = true; - }else if( quantifiers::TermDb::containsTerms( terms[i], d_term_db->d_inst_constants[q] ) ){ + }else if( quantifiers::TermUtil::containsTerms( terms[i], d_term_util->d_inst_constants[q] ) ){ Trace("inst") << "***& inst contains inst constants : " << terms[i] << std::endl; bad_inst = true; } @@ -1193,8 +1215,8 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo //construct the instantiation Trace("inst-add-debug") << "Constructing instantiation..." << std::endl; - Assert( d_term_db->d_vars[q].size()==terms.size() ); - Node body = getInstantiation( q, d_term_db->d_vars[q], terms, doVts ); //do virtual term substitution + Assert( d_term_util->d_vars[q].size()==terms.size() ); + Node body = getInstantiation( q, d_term_util->d_vars[q], terms, doVts ); //do virtual term substitution Node orig_body = body; if( options::cbqiNestedQE() && d_i_cbqi ){ body = d_i_cbqi->doNestedQE( q, terms, body, doVts ); @@ -1208,7 +1230,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo if( d_useModelEe && options::instNoModelTrue() ){ Node val_body = d_model->getValue( body ); - if( val_body==d_term_db->d_true ){ + if( val_body==d_term_util->d_true ){ Trace("inst-add-debug") << " --> True in model." << std::endl; ++(d_statistics.d_inst_duplicate_model_true); return false; @@ -1495,9 +1517,9 @@ void QuantifiersEngine::printInstantiations( std::ostream& out ) { printed = true; out << "(skolem " << q << std::endl; out << " ( "; - for( unsigned i=0; id_skolem_constants[q].size(); i++ ){ + for( unsigned i=0; id_skolem_constants[q].size(); i++ ){ if( i>0 ){ out << " "; } - out << d_term_db->d_skolem_constants[q][i]; + out << d_term_util->d_skolem_constants[q][i]; } out << " )" << std::endl; out << ")" << std::endl; @@ -1595,7 +1617,7 @@ Node QuantifiersEngine::getInstantiatedConjunction( Node q ) { } //have to remove q, TODO: avoid this in a better way TNode tq = q; - TNode tt = d_term_db->d_true; + TNode tt = d_term_util->d_true; ret = ret.substitute( tq, tt ); return ret; } @@ -1739,313 +1761,3 @@ void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) { } } - -EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe ) : d_qe( qe ), d_eqi_counter( c ), d_reset_count( 0 ){ - if( options::inferArithTriggerEq() ){ - d_eq_inference = new quantifiers::EqualityInference( c, options::inferArithTriggerEqExp() ); - }else{ - d_eq_inference = NULL; - } -} - -EqualityQueryQuantifiersEngine::~EqualityQueryQuantifiersEngine(){ - delete d_eq_inference; -} - -bool EqualityQueryQuantifiersEngine::reset( Theory::Effort e ){ - d_int_rep.clear(); - d_reset_count++; - return processInferences( e ); -} - -bool EqualityQueryQuantifiersEngine::processInferences( Theory::Effort e ) { - if( options::inferArithTriggerEq() ){ - eq::EqualityEngine* ee = getEngine(); - //updated implementation - while( d_eqi_counter.get()getNumPendingMerges() ){ - Node eq = d_eq_inference->getPendingMerge( d_eqi_counter.get() ); - Node eq_exp = d_eq_inference->getPendingMergeExplanation( d_eqi_counter.get() ); - Trace("quant-engine-ee-proc") << "processInferences : Infer : " << eq << std::endl; - Trace("quant-engine-ee-proc") << " explanation : " << eq_exp << std::endl; - Assert( ee->hasTerm( eq[0] ) ); - Assert( ee->hasTerm( eq[1] ) ); - if( areDisequal( eq[0], eq[1] ) ){ - Trace("quant-engine-ee-proc") << "processInferences : Conflict : " << eq << std::endl; - if( Trace.isOn("term-db-lemma") ){ - Trace("term-db-lemma") << "Disequal terms, equal by normalization : " << eq[0] << " " << eq[1] << "!!!!" << std::endl; - if( !d_qe->getTheoryEngine()->needCheck() ){ - Trace("term-db-lemma") << " all theories passed with no lemmas." << std::endl; - //this should really never happen (implies arithmetic is incomplete when sharing is enabled) - Assert( false ); - } - Trace("term-db-lemma") << " add split on : " << eq << std::endl; - } - d_qe->addSplit( eq ); - return false; - }else{ - ee->assertEquality( eq, true, eq_exp ); - d_eqi_counter = d_eqi_counter.get() + 1; - } - } - Assert( ee->consistent() ); - } - return true; -} - -bool EqualityQueryQuantifiersEngine::hasTerm( Node a ){ - return getEngine()->hasTerm( a ); -} - -Node EqualityQueryQuantifiersEngine::getRepresentative( Node a ){ - eq::EqualityEngine* ee = getEngine(); - if( ee->hasTerm( a ) ){ - return ee->getRepresentative( a ); - }else{ - return a; - } -} - -bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){ - if( a==b ){ - return true; - }else{ - eq::EqualityEngine* ee = getEngine(); - if( ee->hasTerm( a ) && ee->hasTerm( b ) ){ - return ee->areEqual( a, b ); - }else{ - return false; - } - } -} - -bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){ - if( a==b ){ - return false; - }else{ - eq::EqualityEngine* ee = getEngine(); - if( ee->hasTerm( a ) && ee->hasTerm( b ) ){ - return ee->areDisequal( a, b, false ); - }else{ - return a.isConst() && b.isConst(); - } - } -} - -Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, int index ){ - Assert( f.isNull() || f.getKind()==FORALL ); - Node r = getRepresentative( a ); - if( options::finiteModelFind() ){ - if( r.isConst() && quantifiers::TermDb::containsUninterpretedConstant( r ) ){ - //map back from values assigned by model, if any - if( d_qe->getModel() ){ - std::map< Node, Node >::iterator it = d_qe->getModel()->d_rep_set.d_values_to_terms.find( r ); - if( it!=d_qe->getModel()->d_rep_set.d_values_to_terms.end() ){ - r = it->second; - r = getRepresentative( r ); - }else{ - if( r.getType().isSort() ){ - Trace("internal-rep-warn") << "No representative for UF constant." << std::endl; - //should never happen : UF constants should never escape model - Assert( false ); - } - } - } - } - } - if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_EE ){ - return r; - }else{ - TypeNode v_tn = f.isNull() ? a.getType() : f[0][index].getType(); - std::map< Node, Node >::iterator itir = d_int_rep[v_tn].find( r ); - if( itir==d_int_rep[v_tn].end() ){ - //find best selection for representative - Node r_best; - //if( options::fmfRelevantDomain() && !f.isNull() ){ - // Trace("internal-rep-debug") << "Consult relevant domain to mkRep " << r << std::endl; - // r_best = d_qe->getRelevantDomain()->getRelevantTerm( f, index, r ); - // Trace("internal-rep-debug") << "Returned " << r_best << " " << r << std::endl; - //} - std::vector< Node > eqc; - getEquivalenceClass( r, eqc ); - Trace("internal-rep-select") << "Choose representative for equivalence class : { "; - for( unsigned i=0; i0 ) Trace("internal-rep-select") << ", "; - Trace("internal-rep-select") << eqc[i]; - } - Trace("internal-rep-select") << " }, type = " << v_tn << std::endl; - int r_best_score = -1; - for( size_t i=0; i=0 && ( r_best_score<0 || score cache; - r_best = getInstance( r_best, eqc, cache ); - //store that this representative was chosen at this point - if( d_rep_score.find( r_best )==d_rep_score.end() ){ - d_rep_score[ r_best ] = d_reset_count; - } - Trace("internal-rep-select") << "...Choose " << r_best << " with score " << r_best_score << std::endl; - Assert( r_best.getType().isSubtypeOf( v_tn ) ); - d_int_rep[v_tn][r] = r_best; - if( r_best!=a ){ - Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl; - Trace("internal-rep-debug") << "int_rep( " << a << " ) = " << r_best << ", " << std::endl; - } - return r_best; - }else{ - return itir->second; - } - } -} - -void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps ) { - //make sure internal representatives currently exist - for( std::map< TypeNode, std::vector< Node > >::iterator it = reps.begin(); it != reps.end(); ++it ){ - if( it->first.isSort() ){ - for( unsigned i=0; isecond.size(); i++ ){ - Node r = getInternalRepresentative( it->second[i], Node::null(), 0 ); - } - } - } - Trace("internal-rep-flatten") << "---Flattening representatives : " << std::endl; - for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){ - for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){ - Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl; - } - } - //store representatives for newly created terms - std::map< Node, Node > temp_rep_map; - - bool success; - do { - success = false; - for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){ - for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){ - if( it->second.getKind()==APPLY_UF && it->second.getType().isSort() ){ - Node ni = it->second; - std::vector< Node > cc; - cc.push_back( it->second.getOperator() ); - bool changed = false; - for( unsigned j=0; jsecond.find( r )==itt->second.end() ){ - Assert( temp_rep_map.find( r )!=temp_rep_map.end() ); - r = temp_rep_map[r]; - } - if( r==ni ){ - //found sub-term as instance - Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to subterm " << ni[j] << std::endl; - itt->second[it->first] = ni[j]; - changed = false; - success = true; - break; - }else{ - Node ir = itt->second[r]; - cc.push_back( ir ); - if( ni[j]!=ir ){ - changed = true; - } - } - }else{ - changed = false; - break; - } - } - if( changed ){ - Node n = NodeManager::currentNM()->mkNode( APPLY_UF, cc ); - Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to " << n << std::endl; - success = true; - itt->second[it->first] = n; - temp_rep_map[n] = it->first; - } - } - } - } - }while( success ); - Trace("internal-rep-flatten") << "---After flattening : " << std::endl; - for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){ - for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){ - Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl; - } - } -} - -eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){ - return d_qe->getActiveEqualityEngine(); -} - -void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< Node >& eqc ){ - eq::EqualityEngine* ee = getEngine(); - if( ee->hasTerm( a ) ){ - Node rep = ee->getRepresentative( a ); - eq::EqClassIterator eqc_iter( rep, ee ); - while( !eqc_iter.isFinished() ){ - eqc.push_back( *eqc_iter ); - eqc_iter++; - } - }else{ - eqc.push_back( a ); - } - //a should be in its equivalence class - Assert( std::find( eqc.begin(), eqc.end(), a )!=eqc.end() ); -} - -TNode EqualityQueryQuantifiersEngine::getCongruentTerm( Node f, std::vector< TNode >& args ) { - return d_qe->getTermDatabase()->getCongruentTerm( f, args ); -} - -//helper functions - -Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map& cache ){ - if(cache.find(n) != cache.end()) { - return cache[n]; - } - for( size_t i=0; igetTermDatabase()->isInstClosure( n ) || !d_qe->getTermDatabase()->hasTermCurrent( n, false ) ) ){ - return -1; - }else if( options::instMaxLevel()!=-1 ){ - //score prefer lowest instantiation level - if( n.hasAttribute(InstLevelAttribute()) ){ - return n.getAttribute(InstLevelAttribute()); - }else{ - return options::instLevelInputOnly() ? -1 : 0; - } - }else{ - if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_FIRST ){ - //score prefers earliest use of this term as a representative - return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n]; - }else{ - Assert( options::quantRepMode()==quantifiers::QUANT_REP_MODE_DEPTH ); - return quantifiers::TermDb::getTermDepth( n ); - } - } -} diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 443bbd643..c72038659 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -52,10 +52,14 @@ namespace quantifiers { //utilities class TermDb; class TermDbSygus; + class TermUtil; class FirstOrderModel; + class QuantAttributes; class RelevantDomain; class BvInverter; class InstPropagator; + class EqualityInference; + class EqualityQueryQuantifiersEngine; //modules, these are "subsolvers" of the quantifiers theory. class InstantiationEngine; class ModelEngine; @@ -81,8 +85,6 @@ namespace inst { class TriggerTrie; }/* CVC4::theory::inst */ -//class EfficientEMatcher; -class EqualityQueryQuantifiersEngine; class QuantifiersEngine { friend class quantifiers::InstantiationEngine; @@ -106,7 +108,9 @@ private: /** instantiation notify */ std::vector< InstantiationNotify* > d_inst_notify; /** equality query class */ - EqualityQueryQuantifiersEngine* d_eq_query; + quantifiers::EqualityQueryQuantifiersEngine* d_eq_query; + /** equality inference class */ + quantifiers::EqualityInference* d_eq_inference; /** for computing relevance of quantifiers */ QuantRelevance * d_quant_rel; /** relevant domain */ @@ -191,6 +195,12 @@ private: BoolMap d_skolemized; /** term database */ quantifiers::TermDb* d_term_db; + /** term database */ + quantifiers::TermDbSygus* d_sygus_tdb; + /** term utilities */ + quantifiers::TermUtil* d_term_util; + /** quantifiers attributes */ + quantifiers::QuantAttributes* d_quant_attr; /** all triggers will be stored in this trie */ inst::TriggerTrie* d_tr_trie; /** extended model object */ @@ -219,7 +229,9 @@ public: /** get theory engine */ TheoryEngine* getTheoryEngine() { return d_te; } /** get equality query */ - EqualityQueryQuantifiersEngine* getEqualityQuery(); + EqualityQuery* getEqualityQuery(); + /** get the equality inference */ + quantifiers::EqualityInference* getEqualityInference() { return d_eq_inference; } /** get default sat context for quantifiers engine */ context::Context* getSatContext(); /** get default sat context for quantifiers engine */ @@ -363,7 +375,11 @@ public: /** get term database */ quantifiers::TermDb* getTermDatabase() { return d_term_db; } /** get term database sygus */ - quantifiers::TermDbSygus* getTermDatabaseSygus(); + quantifiers::TermDbSygus * getTermDatabaseSygus() { return d_sygus_tdb; } + /** get term utilities */ + quantifiers::TermUtil* getTermUtil() { return d_term_util; } + /** get quantifiers attributes */ + quantifiers::QuantAttributes* getQuantAttributes() { return d_quant_attr; } /** get trigger database */ inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; } /** add term to database */ @@ -435,56 +451,6 @@ public: Statistics d_statistics; };/* class QuantifiersEngine */ - - -/** equality query object using theory engine */ -class EqualityQueryQuantifiersEngine : public EqualityQuery -{ -private: - /** pointer to theory engine */ - QuantifiersEngine* d_qe; - /** quantifiers equality inference */ - quantifiers::EqualityInference * d_eq_inference; - context::CDO< unsigned > d_eqi_counter; - /** internal representatives */ - std::map< TypeNode, std::map< Node, Node > > d_int_rep; - /** rep score */ - std::map< Node, int > d_rep_score; - /** reset count */ - int d_reset_count; - - /** processInferences : will merge equivalence classes in master equality engine, if possible */ - bool processInferences( Theory::Effort e ); - /** node contains */ - Node getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map& cache ); - /** get score */ - int getRepScore( Node n, Node f, int index, TypeNode v_tn ); - /** flatten representatives */ - void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps ); -public: - EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe ); - virtual ~EqualityQueryQuantifiersEngine(); - /** reset */ - bool reset( Theory::Effort e ); - /** identify */ - std::string identify() const { return "EqualityQueryQE"; } - /** general queries about equality */ - bool hasTerm( Node a ); - Node getRepresentative( Node a ); - bool areEqual( Node a, Node b ); - bool areDisequal( Node a, Node b ); - eq::EqualityEngine* getEngine(); - void getEquivalenceClass( Node a, std::vector< Node >& eqc ); - TNode getCongruentTerm( Node f, std::vector< TNode >& args ); - /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria. - If cbqi is active, this will return a term in the equivalence class of "a" that does - not contain instantiation constants, if such a term exists. - */ - Node getInternalRepresentative( Node a, Node f, int index ); - /** get quantifiers equality inference */ - quantifiers::EqualityInference * getEqualityInference() { return d_eq_inference; } -}; /* EqualityQueryQuantifiersEngine */ - }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index cd1fac290..303e65eff 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -15,7 +15,7 @@ #include "theory/rep_set.h" #include "theory/type_enumerator.h" #include "theory/quantifiers/bounded_integers.h" -#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers/first_order_model.h" using namespace std; @@ -183,7 +183,7 @@ bool RepSetIterator::initialize( RepBoundExt* rext ){ // terms in rep_set are now constants which mapped to terms through TheoryModel // thus, should introduce a constant and a term. for now, just a term. - //Node c = d_qe->getTermDatabase()->getEnumerateTerm( tn, 0 ); + //Node c = d_qe->getTermUtil()->getEnumerateTerm( tn, 0 ); Node var = d_qe->getModel()->getSomeDomainElement( tn ); Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl; d_rep_set->add( tn, var ); @@ -208,7 +208,7 @@ bool RepSetIterator::initialize( RepBoundExt* rext ){ } if( !tn.isSort() ){ if( inc ){ - if( d_qe->getTermDatabase()->mayComplete( tn ) ){ + if( d_qe->getTermUtil()->mayComplete( tn ) ){ Trace("rsi") << " do complete, since cardinality is small (" << tn.getCardinality() << ")..." << std::endl; d_rep_set->complete( tn ); //must have succeeded @@ -242,7 +242,7 @@ bool RepSetIterator::initialize( RepBoundExt* rext ){ for( unsigned i=0; igetBoundedIntegers()->getNumBoundVars( d_owner ); i++ ){ Node v = d_qe->getBoundedIntegers()->getBoundVar( d_owner, i ); Trace("bound-int-rsi") << " bound var #" << i << " is " << v << std::endl; - varOrder.push_back( d_qe->getTermDatabase()->getVariableNum( d_owner, v ) ); + varOrder.push_back( d_qe->getTermUtil()->getVariableNum( d_owner, v ) ); } for( unsigned i=0; igetBoundedIntegers()->isBoundVar(d_owner, d_owner[0][i])) { diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 93d4124d9..92ecc0393 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -26,6 +26,7 @@ #include "smt/logic_exception.h" #include "theory/quantifiers_engine.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "options/quantifiers_options.h" using namespace std; @@ -816,10 +817,10 @@ Node TheorySep::getNextDecisionRequest( unsigned& priority ) { if( getLogicInfo().isQuantified() ){ Assert( d_guard_to_assertion.find( g )!= d_guard_to_assertion.end() ); Node a = d_guard_to_assertion[g]; - Node q = quantifiers::TermDb::getInstConstAttr( a ); + Node q = quantifiers::TermUtil::getInstConstAttr( a ); if( !q.isNull() ){ //must wait to decide on counterexample literal from quantified formula - Node cel = getQuantifiersEngine()->getTermDatabase()->getCounterexampleLiteral( q ); + Node cel = getQuantifiersEngine()->getTermUtil()->getCounterexampleLiteral( q ); bool value; if( d_valuation.hasSatValue( cel, value ) ){ Trace("sep-dec-debug") << "TheorySep::getNextDecisionRequest : dependent guard " << g << " depends on value for guard for quantified formula : " << value << std::endl; @@ -925,7 +926,7 @@ int TheorySep::processAssertion( Node n, std::map< int, std::map< Node, int > >& TypeNode tn1 = n[0].getType(); TypeNode tn2 = n[1].getType(); registerRefDataTypes( tn1, tn2, n ); - if( quantifiers::TermDb::hasBoundVarAttr( n[0] ) ){ + if( quantifiers::TermUtil::hasBoundVarAttr( n[0] ) ){ if( d_bound_kind[tn1]!=bound_strict && d_bound_kind[tn1]!=bound_invalid ){ if( options::quantEpr() && n[0].getKind()==kind::BOUND_VARIABLE ){ // still valid : bound on heap models will include Herbrand universe of n[0].getType() diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index b7572eaa1..1b7437a7e 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -19,7 +19,7 @@ #include "expr/attribute.h" #include "options/quantifiers_options.h" -#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/theory_engine.h" #include "theory/uf/equality_engine.h" #include "theory/uf/theory_uf.h" diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index db2f735c6..c45dd4833 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -170,7 +170,7 @@ public: //conversion between HO_APPLY AND APPLY_UF * Then, f and g can be used as APPLY_UF operators, but (ite C f g), (lambda x1. (f x1)) as well as the variable x above are not. */ static inline bool canUseAsApplyUfOperator(TNode n){ - return n.isVar() && n.getKind()!=kind::BOUND_VARIABLE; + return n.isVar(); } };/* class TheoryUfRewriter */ -- 2.30.2