From 4b580ea3876055f701b13e67e0e4e78abbe47674 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 1 Nov 2017 15:20:37 -0500 Subject: [PATCH] (Refactor) Split term util (#1303) * Fix some documentation. * Move model basis out of term db. * Moving * Finished moving. * Document Skolemize and term enumeration. * Minor * Model basis to first order model. * Change function name. * Minor * Clang format. * Minor * Format * Minor * Format * Address review. --- src/Makefile.am | 4 + src/theory/quantifiers/ambqi_builder.cpp | 18 +- src/theory/quantifiers/bounded_integers.cpp | 7 +- .../quantifiers/candidate_generator.cpp | 2 +- .../quantifiers/ce_guided_conjecture.cpp | 9 +- .../quantifiers/ce_guided_single_inv.cpp | 4 +- .../quantifiers/ce_guided_single_inv_sol.cpp | 3 +- src/theory/quantifiers/ceg_instantiator.cpp | 6 +- .../quantifiers/conjecture_generator.cpp | 35 +- src/theory/quantifiers/first_order_model.cpp | 126 +++++- src/theory/quantifiers/first_order_model.h | 102 +++-- src/theory/quantifiers/full_model_check.cpp | 7 +- .../quantifiers/inst_strategy_e_matching.cpp | 8 +- .../quantifiers/instantiation_engine.cpp | 4 +- src/theory/quantifiers/macros.cpp | 2 +- src/theory/quantifiers/model_builder.cpp | 28 +- src/theory/quantifiers/model_builder.h | 8 +- src/theory/quantifiers/model_engine.cpp | 2 +- .../quantifiers/quant_conflict_find.cpp | 3 +- .../quantifiers/quantifiers_rewriter.cpp | 4 +- src/theory/quantifiers/rewrite_engine.cpp | 4 +- src/theory/quantifiers/skolemize.cpp | 385 ++++++++++++++++++ src/theory/quantifiers/skolemize.h | 146 +++++++ src/theory/quantifiers/term_database.cpp | 182 ++++----- src/theory/quantifiers/term_database.h | 90 ++-- src/theory/quantifiers/term_enumeration.cpp | 133 ++++++ src/theory/quantifiers/term_enumeration.h | 83 ++++ src/theory/quantifiers/term_util.cpp | 298 +------------- src/theory/quantifiers/term_util.h | 68 +--- src/theory/quantifiers_engine.cpp | 53 ++- src/theory/quantifiers_engine.h | 30 +- src/theory/rep_set.cpp | 13 +- src/theory/uf/theory_uf_model.cpp | 2 +- src/theory/uf/theory_uf_model.h | 2 + 34 files changed, 1259 insertions(+), 612 deletions(-) create mode 100644 src/theory/quantifiers/skolemize.cpp create mode 100644 src/theory/quantifiers/skolemize.h create mode 100644 src/theory/quantifiers/term_enumeration.cpp create mode 100644 src/theory/quantifiers/term_enumeration.h diff --git a/src/Makefile.am b/src/Makefile.am index d370a73bc..e8910e182 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -424,6 +424,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/relevant_domain.h \ theory/quantifiers/rewrite_engine.cpp \ theory/quantifiers/rewrite_engine.h \ + theory/quantifiers/skolemize.cpp \ + theory/quantifiers/skolemize.h \ theory/quantifiers/sygus_grammar_cons.cpp \ theory/quantifiers/sygus_grammar_cons.h \ theory/quantifiers/sygus_process_conj.cpp \ @@ -434,6 +436,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/term_database.h \ theory/quantifiers/term_database_sygus.cpp \ theory/quantifiers/term_database_sygus.h \ + theory/quantifiers/term_enumeration.cpp \ + theory/quantifiers/term_enumeration.h \ theory/quantifiers/term_util.cpp \ theory/quantifiers/term_util.h \ theory/quantifiers/theory_quantifiers.cpp \ diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp index 29bbc6a2c..c418d0fb1 100644 --- a/src/theory/quantifiers/ambqi_builder.cpp +++ b/src/theory/quantifiers/ambqi_builder.cpp @@ -12,17 +12,19 @@ ** \brief Implementation of abstract MBQI builder **/ - -#include "options/quantifiers_options.h" #include "theory/quantifiers/ambqi_builder.h" +#include "options/quantifiers_options.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" using namespace std; -using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + void AbsDef::construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps, unsigned depth ) { d_def.clear(); @@ -807,7 +809,7 @@ bool AbsMbqiBuilder::processBuildModel(TheoryModel* m) { } if( fapps.empty() ){ //choose arbitrary value - Node mbt = d_qe->getTermDatabase()->getModelBasisOpTerm(f); + Node mbt = fm->getModelBasisOpTerm(f); Trace("ambqi-model-debug") << "Initial terms empty, add " << mbt << std::endl; fapps.push_back( mbt ); } @@ -958,3 +960,7 @@ bool AbsMbqiBuilder::doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNod return true; } } + +}/* namespace CVC4::theory::quantifiers */ +}/* namespace CVC4::theory */ +}/* namespace CVC4 */ diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index 2a2ba8d4f..f3244937d 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -14,11 +14,12 @@ ** This class manages integer bounds for quantifiers **/ -#include "options/quantifiers_options.h" #include "theory/quantifiers/bounded_integers.h" +#include "options/quantifiers_options.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/model_engine.h" #include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" #include "theory/theory_engine.h" @@ -455,7 +456,9 @@ void BoundedIntegers::preRegisterQuantifier( Node f ) { for( unsigned i=0; imayComplete( tn ) ){ + if (tn.isSort() + || d_quantEngine->getTermEnumeration()->mayComplete(tn)) + { success = true; setBoundedVar( f, f[0][i], BOUND_FINITE ); break; diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 0a66109a0..712112615 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -302,7 +302,7 @@ Node CandidateGeneratorQEAll::getNextCandidate() { if( d_firstTime ){ //must return something d_firstTime = false; - return d_qe->getTermDatabase()->getModelBasisTerm( d_match_pattern_type ); + return d_qe->getTermForType(d_match_pattern_type); } return Node::null(); } diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp index 7fcc3f2af..3af623f13 100644 --- a/src/theory/quantifiers/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/ce_guided_conjecture.cpp @@ -20,6 +20,7 @@ #include "smt/smt_statistics_registry.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/skolemize.h" #include "theory/quantifiers/term_database_sygus.h" #include "theory/quantifiers/term_util.h" #include "theory/theory_engine.h" @@ -296,7 +297,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->getTermUtil()->getSkolemizedBody( dr[0] ).negate() ); + ic.push_back(d_qe->getSkolemize()->getSkolemizedBody(dr[0]).negate()); } if( sk_refine ){ Assert( !isGround() ); @@ -347,9 +348,11 @@ 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->getTermUtil()->d_skolem_constants[ce_q].size() ); + std::vector skolems; + d_qe->getSkolemize()->getSkolemConstants(ce_q, skolems); + Assert(d_inner_vars_disj[k].size() == skolems.size()); std::vector< Node > model_values; - getModelValues( d_qe->getTermUtil()->d_skolem_constants[ce_q], model_values ); + getModelValues(skolems, 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{ diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 9d2d2fe98..c1b6c82ad 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -20,6 +20,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_enumeration.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers/trigger.h" #include "theory/theory_engine.h" @@ -472,7 +473,8 @@ 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->getTermUtil()->getEnumerateTerm( TypeNode::fromType( dt.getSygusType() ), 0 ); + s = d_qe->getTermEnumeration()->getEnumerateTerm( + TypeNode::fromType(dt.getSygusType()), 0); }else{ Trace("csi-sol") << "Get solution for " << prog << ", with skolems : "; sol_index = d_prog_to_sol_index[prog]; diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp index 9e69a31d3..a62b5f50b 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_enumeration.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers/trigger.h" #include "theory/theory_engine.h" @@ -676,7 +677,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->getTermUtil()->getEnumerateTerm( stn, index ); + Node ns = d_qe->getTermEnumeration()->getEnumerateTerm(stn, index); if( ns.isNull() ){ to_erase.push_back( stn ); }else{ diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index e7749cd92..36fac5e80 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -18,13 +18,13 @@ #include "options/quantifiers_options.h" #include "smt/term_formula_removal.h" #include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/trigger.h" #include "theory/theory_engine.h" - using namespace std; using namespace CVC4; using namespace CVC4::kind; @@ -1139,7 +1139,7 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st Instantiator::Instantiator( QuantifiersEngine * qe, TypeNode tn ) : d_type( tn ){ - d_closed_enum_type = qe->getTermUtil()->isClosedEnumerableType( tn ); + d_closed_enum_type = qe->getTermEnumeration()->isClosedEnumerableType(tn); } diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 508f58a07..e5a096c87 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -13,10 +13,12 @@ ** **/ -#include "options/quantifiers_options.h" #include "theory/quantifiers/conjecture_generator.h" +#include "options/quantifiers_options.h" #include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/skolemize.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers/trigger.h" #include "theory/theory_engine.h" @@ -398,7 +400,8 @@ 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( getTermUtil()->isInductionTerm( r ) ){ + if (Skolemize::isInductionTerm(r)) + { n = d_op_arg_index[r].getGroundTerm( this, args ); }else{ n = r; @@ -556,12 +559,13 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { if( std::find( provenConj.begin(), provenConj.end(), q )==provenConj.end() ){ //check each skolem variable bool disproven = true; - //std::vector< Node > sk; - //getTermUtil()->getSkolemConstants( q, sk, true ); + std::vector skolems; + d_quantEngine->getSkolemize()->getSkolemConstants(q, skolems); Trace("sg-conjecture") << " CONJECTURE : "; std::vector< Node > ce; - for( unsigned j=0; jd_skolem_constants[q].size(); j++ ){ - TNode k = getTermUtil()->d_skolem_constants[q][j]; + for (unsigned j = 0; j < skolems.size(); j++) + { + TNode k = skolems[j]; TNode rk = getRepresentative( k ); std::map< TNode, Node >::iterator git = d_ground_eqc_map.find( rk ); //check if it is a ground term @@ -569,7 +573,11 @@ 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") << getTermUtil()->d_skolem_constants[q][k] << ( j==k ? "*" : "" ) << " "; } + for (unsigned k = 0; k < skolems.size(); k++) + { + Trace("sg-conjecture") << skolems[k] << (j == k ? "*" : "") + << " "; + } Trace("sg-conjecture") << "}"; } Trace("sg-conjecture") << std::endl; @@ -1051,12 +1059,14 @@ Node ConjectureGenerator::getPredicateForType( TypeNode tn ) { void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< Node >& terms ) { if( n.getNumChildren()>0 ){ + TermEnumeration* te = d_quantEngine->getTermEnumeration(); std::vector< int > vec; std::vector< TypeNode > types; for( unsigned i=0; iisClosedEnumerableType( tn ) ){ + if (te->isClosedEnumerableType(tn)) + { types.push_back( tn ); }else{ return; @@ -1074,7 +1084,9 @@ 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_sum < size_limit + && !te->getEnumerateTerm(types[index], vec[index] + 1).isNull()) + { vec[index]++; vec_sum++; vec.push_back( size_limit - vec_sum ); @@ -1089,7 +1101,8 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< } if( success ){ if( vec.size()==n.getNumChildren() ){ - Node lc = getTermUtil()->getEnumerateTerm( types[vec.size()-1], vec[vec.size()-1] ); + Node lc = + te->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 = getTermUtil()->getEnumerateTerm( types[i], vec[i] ); + Node nn = te->getEnumerateTerm(types[i], vec[i]); Assert( !nn.isNull() ); Assert( nn.getType()==n[i].getType() ); children.push_back( nn ); diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 462dc23d0..f4cf1b32a 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -12,13 +12,15 @@ ** \brief Implementation of model engine model class **/ +#include "theory/quantifiers/first_order_model.h" +#include "options/base_options.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/ambqi_builder.h" -#include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/full_model_check.h" #include "theory/quantifiers/model_engine.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" #define USE_INDEX_ORDERING @@ -104,7 +106,7 @@ Node FirstOrderModel::getSomeDomainElement(TypeNode tn){ //check if there is even any domain elements at all if (!d_rep_set.hasType(tn)) { Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl; - Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn); + Node mbt = getModelBasisTerm(tn); Trace("fmc-model-debug") << "Add to representative set..." << std::endl; d_rep_set.add(tn, mbt); }else if( d_rep_set.d_type_reps[tn].size()==0 ){ @@ -200,6 +202,118 @@ bool FirstOrderModel::isQuantifierAsserted( TNode q ) { return std::find( d_forall_rlv_assert.begin(), d_forall_rlv_assert.end(), q )!=d_forall_rlv_assert.end(); } +Node FirstOrderModel::getModelBasisTerm(TypeNode tn) +{ + if (d_model_basis_term.find(tn) == d_model_basis_term.end()) + { + Node mbt; + if (d_qe->getTermEnumeration()->isClosedEnumerableType(tn)) + { + mbt = d_qe->getTermEnumeration()->getEnumerateTerm(tn, 0); + } + else + { + if (options::fmfFreshDistConst()) + { + mbt = d_qe->getTermDatabase()->getOrMakeTypeFreshVariable(tn); + } + else + { + mbt = d_qe->getTermDatabase()->getOrMakeTypeGroundTerm(tn); + } + } + ModelBasisAttribute mba; + mbt.setAttribute(mba, true); + d_model_basis_term[tn] = mbt; + Trace("model-basis-term") << "Choose " << mbt << " as model basis term for " + << tn << std::endl; + } + return d_model_basis_term[tn]; +} + +bool FirstOrderModel::isModelBasisTerm(Node n) +{ + return n == getModelBasisTerm(n.getType()); +} + +Node FirstOrderModel::getModelBasisOpTerm(Node op) +{ + if (d_model_basis_op_term.find(op) == d_model_basis_op_term.end()) + { + TypeNode t = op.getType(); + std::vector children; + children.push_back(op); + for (int i = 0; i < (int)(t.getNumChildren() - 1); i++) + { + children.push_back(getModelBasisTerm(t[i])); + } + if (children.size() == 1) + { + d_model_basis_op_term[op] = op; + } + else + { + d_model_basis_op_term[op] = + NodeManager::currentNM()->mkNode(APPLY_UF, children); + } + } + return d_model_basis_op_term[op]; +} + +Node FirstOrderModel::getModelBasis(Node q, Node n) +{ + // make model basis + if (d_model_basis_terms.find(q) == d_model_basis_terms.end()) + { + for (unsigned j = 0; j < q[0].getNumChildren(); j++) + { + d_model_basis_terms[q].push_back(getModelBasisTerm(q[0][j].getType())); + } + } + Node gn = d_qe->getTermUtil()->substituteInstConstants( + n, q, d_model_basis_terms[q]); + return gn; +} + +Node FirstOrderModel::getModelBasisBody(Node q) +{ + if (d_model_basis_body.find(q) == d_model_basis_body.end()) + { + Node n = d_qe->getTermUtil()->getInstConstantBody(q); + d_model_basis_body[q] = getModelBasis(q, n); + } + return d_model_basis_body[q]; +} + +void FirstOrderModel::computeModelBasisArgAttribute(Node n) +{ + if (!n.hasAttribute(ModelBasisArgAttribute())) + { + // ensure that the model basis terms have been defined + if (n.getKind() == APPLY_UF) + { + getModelBasisOpTerm(n.getOperator()); + } + uint64_t val = 0; + // determine if it has model basis attribute + for (unsigned j = 0; j < n.getNumChildren(); j++) + { + if (n[j].getAttribute(ModelBasisAttribute())) + { + val++; + } + } + ModelBasisArgAttribute mbaa; + n.setAttribute(mbaa, val); + } +} + +unsigned FirstOrderModel::getModelBasisArg(Node n) +{ + computeModelBasisArgAttribute(n); + return n.getAttribute(ModelBasisArgAttribute()); +} + FirstOrderModelIG::FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name) : FirstOrderModel(qe, c,name) { @@ -676,14 +790,6 @@ Node FirstOrderModelFmc::getStarElement(TypeNode tn) { return st; } -bool FirstOrderModelFmc::isModelBasisTerm(Node n) { - return n==getModelBasisTerm(n.getType()); -} - -Node FirstOrderModelFmc::getModelBasisTerm(TypeNode tn) { - return d_qe->getTermDatabase()->getModelBasisTerm(tn); -} - Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { Trace("fmc-model") << "Get function value for " << op << std::endl; TypeNode type = op.getType(); diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 8a00c70f6..6305a3807 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -26,6 +26,18 @@ namespace theory { class QuantifiersEngine; +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; + namespace quantifiers { class TermDb; @@ -42,24 +54,16 @@ class FirstOrderModelAbs; struct IsStarAttributeId {}; typedef expr::Attribute IsStarAttribute; +// TODO (#1301) : document and refactor this class class FirstOrderModel : public TheoryModel { -protected: - /** quant engine */ - QuantifiersEngine * d_qe; - /** list of quantifiers asserted in the current context */ - context::CDList d_forall_asserts; - /** quantified formulas marked as relevant */ - unsigned d_rlv_count; - std::map< Node, unsigned > d_forall_rlv; - std::vector< Node > d_forall_rlv_vec; - Node d_last_forall_rlv; - std::vector< Node > d_forall_rlv_assert; - /** get variable id */ - std::map< Node, std::map< Node, int > > d_quant_var_id; - /** get current model value (deprecated) */ - //virtual Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) = 0; -public: //for Theory Quantifiers: + public: + FirstOrderModel(QuantifiersEngine* qe, context::Context* c, std::string name); + virtual ~FirstOrderModel() throw() {} + virtual FirstOrderModelIG* asFirstOrderModelIG() { return nullptr; } + virtual fmcheck::FirstOrderModelFmc* asFirstOrderModelFmc() { return nullptr; } + virtual FirstOrderModelQInt* asFirstOrderModelQInt() { return nullptr; } + virtual FirstOrderModelAbs* asFirstOrderModelAbs() { return nullptr; } /** assert quantifier */ void assertQuantifier( Node n ); /** get number of asserted quantifiers */ @@ -68,30 +72,14 @@ public: //for Theory Quantifiers: Node getAssertedQuantifier( unsigned i, bool ordered = false ); /** initialize model for term */ void initializeModelForTerm( Node n, std::map< Node, bool >& visited ); - virtual void processInitializeModelForTerm( Node n ) = 0; - virtual void processInitializeQuantifier( Node q ) {} -public: - FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name ); - virtual ~FirstOrderModel() throw() {} - virtual FirstOrderModelIG * asFirstOrderModelIG() { return NULL; } - virtual fmcheck::FirstOrderModelFmc * asFirstOrderModelFmc() { return NULL; } - virtual FirstOrderModelQInt * asFirstOrderModelQInt() { return NULL; } - virtual FirstOrderModelAbs * asFirstOrderModelAbs() { return NULL; } // initialize the model void initialize(); - virtual void processInitialize( bool ispre ) = 0; /** get variable id */ int getVariableId(TNode q, TNode n) { return d_quant_var_id.find( q )!=d_quant_var_id.end() ? d_quant_var_id[q][n] : -1; } - /** get some domain element */ - Node getSomeDomainElement(TypeNode tn); /** do we need to do any work? */ bool checkNeeded(); -private: - //list of inactive quantified formulas - std::map< TNode, bool > d_quant_active; -public: /** reset round */ void reset_round(); /** mark quantified formula relevant */ @@ -107,6 +95,54 @@ public: bool isQuantifierActive( TNode q ); /** is quantified formula asserted */ bool isQuantifierAsserted( TNode q ); + /** get model basis term */ + Node getModelBasisTerm(TypeNode tn); + /** is model basis term */ + bool isModelBasisTerm(Node n); + /** get model basis term for op */ + Node getModelBasisOpTerm(Node op); + /** get model basis */ + Node getModelBasis(Node q, Node n); + /** get model basis body */ + Node getModelBasisBody(Node q); + /** get model basis arg */ + unsigned getModelBasisArg(Node n); + /** get some domain element */ + Node getSomeDomainElement(TypeNode tn); + + protected: + /** quant engine */ + QuantifiersEngine* d_qe; + /** list of quantifiers asserted in the current context */ + context::CDList d_forall_asserts; + /** quantified formulas marked as relevant */ + unsigned d_rlv_count; + std::map d_forall_rlv; + std::vector d_forall_rlv_vec; + Node d_last_forall_rlv; + std::vector d_forall_rlv_assert; + /** get variable id */ + std::map > d_quant_var_id; + /** process initialize model for term */ + virtual void processInitializeModelForTerm(Node n) = 0; + /** process intialize quantifier */ + virtual void processInitializeQuantifier(Node q) {} + /** process initialize */ + virtual void processInitialize(bool ispre) = 0; + + private: + // list of inactive quantified formulas + std::map d_quant_active; + /** map from types to model basis terms */ + std::map d_model_basis_term; + /** map from ops to model basis terms */ + std::map d_model_basis_op_term; + /** map from instantiation terms to their model basis equivalent */ + std::map d_model_basis_body; + /** map from universal quantifiers to model basis terms */ + std::map > d_model_basis_terms; + /** compute model basis arg */ + void computeModelBasisArgAttribute(Node n); };/* class FirstOrderModel */ @@ -180,8 +216,6 @@ public: bool isStar(Node n); Node getStar(TypeNode tn); Node getStarElement(TypeNode tn); - bool isModelBasisTerm(Node n); - Node getModelBasisTerm(TypeNode tn); bool isInterval(Node n); Node getInterval( Node lb, Node ub ); bool isInRange( Node v, Node i ); diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index b0f118ad5..5847449cf 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -433,7 +433,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ Trace("fmc-model-debug") << std::endl; //possibly get default if( needsDefault ){ - Node nmb = d_qe->getTermDatabase()->getModelBasisOpTerm(op); + Node nmb = fm->getModelBasisOpTerm(op); //add default value if necessary if( fm->hasTerm( nmb ) ){ Trace("fmc-model-debug") << "Add default " << nmb << std::endl; @@ -504,8 +504,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ ModelBasisArgSort mbas; for (int i=0; i<(int)conds.size(); i++) { mbas.d_terms.push_back(conds[i]); - mbas.d_mba_count[conds[i]] = - d_qe->getTermDatabase()->getModelBasisArg(conds[i]); + mbas.d_mba_count[conds[i]] = fm->getModelBasisArg(conds[i]); indices.push_back(i); } std::sort( indices.begin(), indices.end(), mbas ); @@ -556,7 +555,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ void FullModelChecker::preInitializeType( FirstOrderModelFmc * fm, TypeNode tn ){ if( d_preinitialized_types.find( tn )==d_preinitialized_types.end() ){ d_preinitialized_types[tn] = true; - Node mb = d_qe->getTermDatabase()->getModelBasisTerm(tn); + Node mb = fm->getModelBasisTerm(tn); if( !mb.isConst() ){ Trace("fmc") << "...add model basis term to EE of model " << mb << " " << tn << std::endl; fm->d_equalityEngine->addTerm( mb ); diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 0b248056c..dcc863f3e 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -287,7 +287,8 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ if( options::quantFunWellDefined() ){ Node hd = QuantAttributes::getFunDefHead( f ); if( !hd.isNull() ){ - hd = d_quantEngine->getTermUtil()->getInstConstantNode( hd, f ); + hd = d_quantEngine->getTermUtil() + ->substituteBoundVariablesToInstConstants(hd, f); patTermsF.push_back( hd ); tinfo[hd].init( f, hd ); } @@ -512,7 +513,10 @@ void InstStrategyAutoGenTriggers::addTrigger( inst::Trigger * tr, Node q ) { if( tr ){ if( d_num_trigger_vars[q]mkNode( INST_PATTERN_LIST, d_quantEngine->getTermUtil()->getVariableNode( tr->getInstPattern(), q ) ); + Node pat = + d_quantEngine->getTermUtil()->substituteInstConstantsToBoundVariables( + tr->getInstPattern(), q); + Node ipl = NodeManager::currentNM()->mkNode(INST_PATTERN_LIST, pat); 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; diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 1f3f56820..22af9dd00 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -178,7 +178,9 @@ void InstantiationEngine::registerQuantifier( Node f ){ //} //take into account user patterns if( f.getNumChildren()==3 ){ - Node subsPat = d_quantEngine->getTermUtil()->getInstConstantNode( f[2], f ); + Node subsPat = + d_quantEngine->getTermUtil()->substituteBoundVariablesToInstConstants( + 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/macros.cpp b/src/theory/quantifiers/macros.cpp index 57187b7ab..b84499ee4 100644 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp @@ -153,7 +153,7 @@ bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){ } bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) { - Node icn = d_qe->getTermUtil()->getInstConstantNode( n, f ); + Node icn = d_qe->getTermUtil()->substituteBoundVariablesToInstConstants(n, f); Trace("macros-debug2") << "Get free variables in " << icn << std::endl; std::vector< Node > var; d_qe->getTermUtil()->getVarContainsNode( f, icn, var ); diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 7c5259cb7..8fd659009 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -141,10 +141,10 @@ void QModelBuilder::debugModel( TheoryModel* m ){ } } - - -bool TermArgBasisTrie::addTerm2( FirstOrderModel* fm, Node n, int argIndex ){ - if( argIndex<(int)n.getNumChildren() ){ +bool TermArgBasisTrie::addTerm(FirstOrderModel* fm, Node n, unsigned argIndex) +{ + if (argIndex < n.getNumChildren()) + { Node r; if( n[ argIndex ].getAttribute(ModelBasisAttribute()) ){ r = n[ argIndex ]; @@ -153,10 +153,10 @@ bool TermArgBasisTrie::addTerm2( FirstOrderModel* fm, Node n, int argIndex ){ } std::map< Node, TermArgBasisTrie >::iterator it = d_data.find( r ); if( it==d_data.end() ){ - d_data[r].addTerm2( fm, n, argIndex+1 ); + d_data[r].addTerm(fm, n, argIndex + 1); return true; }else{ - return it->second.addTerm2( fm, n, argIndex+1 ); + return it->second.addTerm(fm, n, argIndex + 1); } }else{ return false; @@ -189,7 +189,7 @@ bool QModelBuilderIG::processBuildModel( TheoryModel* m ) { for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ Node q = fm->getAssertedQuantifier( i ); if( d_qe->getModel()->isQuantifierActive( q ) ){ - int lems = initializeQuantifier( q, q ); + int lems = initializeQuantifier(q, q, f); d_statistics.d_init_inst_gen_lemmas += lems; d_addedLemmas += lems; if( d_qe->inConflict() ){ @@ -285,7 +285,8 @@ bool QModelBuilderIG::processBuildModel( TheoryModel* m ) { return TheoryEngineModelBuilder::processBuildModel( m ); } -int QModelBuilderIG::initializeQuantifier( Node f, Node fp ){ +int QModelBuilderIG::initializeQuantifier(Node f, Node fp, FirstOrderModel* fm) +{ if( d_quant_basis_match_added.find( f )==d_quant_basis_match_added.end() ){ //create the basis match if necessary if( d_quant_basis_match.find( f )==d_quant_basis_match.end() ){ @@ -304,8 +305,9 @@ int QModelBuilderIG::initializeQuantifier( Node f, Node fp ){ // } //} d_quant_basis_match[f] = InstMatch( f ); - for( int j=0; j<(int)f[0].getNumChildren(); j++ ){ - Node t = d_qe->getTermDatabase()->getModelBasisTerm( f[0][j].getType() ); + for (unsigned j = 0; j < f[0].getNumChildren(); j++) + { + Node t = fm->getModelBasisTerm(f[0][j].getType()); //calculate the basis match for f d_quant_basis_match[f].setValue( j, t ); } @@ -540,7 +542,7 @@ void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){ 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 ){ //the literal n is phase-required for quantifier f Node n = it->first; - Node gn = d_qe->getTermDatabase()->getModelBasis( f, n ); + Node gn = fm->getModelBasis(f, n); Debug("fmf-model-req") << " Req: " << n << " -> " << it->second << std::endl; bool value; //if the corresponding ground abstraction literal has a SAT value @@ -727,7 +729,7 @@ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){ if( !d_uf_model_constructed[op] ){ //construct the model for the uninterpretted function/predicate bool setDefaultVal = true; - Node defaultTerm = d_qe->getTermDatabase()->getModelBasisOpTerm( op ); + Node defaultTerm = fmig->getModelBasisOpTerm(op); Trace("fmf-model-cons") << "Construct model for " << op << "..." << std::endl; //set the values in the model std::map< Node, std::vector< Node > >::iterator itut = fmig->d_uf_terms.find( op ); @@ -770,7 +772,7 @@ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){ if( defaultVal.isNull() ){ if (!fmig->getRepSet()->hasType(defaultTerm.getType())) { - Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(defaultTerm.getType()); + Node mbt = fmig->getModelBasisTerm(defaultTerm.getType()); fmig->getRepSetPtr()->d_type_reps[defaultTerm.getType()].push_back( mbt); } diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index 2dc561074..73e2937ab 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -60,13 +60,11 @@ public: class TermArgBasisTrie { -private: - bool addTerm2( FirstOrderModel* fm, Node n, int argIndex ); public: /** the data */ std::map< Node, TermArgBasisTrie > d_data; -public: - bool addTerm( FirstOrderModel* fm, Node n ) { return addTerm2( fm, n, 0 ); } + /** add term to the trie */ + bool addTerm(FirstOrderModel* fm, Node n, unsigned argIndex = 0); };/* class TermArgBasisTrie */ /** model builder class @@ -93,7 +91,7 @@ protected: //reset virtual void reset( FirstOrderModel* fm ) = 0; //initialize quantifiers, return number of lemmas produced - virtual int initializeQuantifier( Node f, Node fp ); + virtual int initializeQuantifier(Node f, Node fp, FirstOrderModel* fm); //analyze model virtual void analyzeModel( FirstOrderModel* fm ); //analyze quantifiers diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index b3acb408f..88b16bfd3 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -187,7 +187,7 @@ int ModelEngine::checkModel(){ Trace("model-engine-debug") << r << " "; } Trace("model-engine-debug") << std::endl; - Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first); + Node mbt = fm->getModelBasisTerm(it->first); Trace("model-engine-debug") << " Basis term : " << mbt << std::endl; } } diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 0094bc147..bd56b9d9b 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -609,7 +609,8 @@ 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->getTermUtil()->getInstantiatedNode( it->first, d_q, terms ); + Node cons = + p->getTermUtil()->substituteBoundVariables(it->first, d_q, terms); cons = it->second ? cons : cons.negate(); if( !entailmentTest( p, cons, p->d_effort==QuantConflictFind::effort_conflict ) ){ return true; diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 9f6617d5a..0ffed5243 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -16,6 +16,7 @@ #include "options/quantifiers_options.h" #include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/skolemize.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers/trigger.h" @@ -1793,7 +1794,8 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v Node sub; std::vector< unsigned > sub_vars; //return skolemized body - return TermUtil::mkSkolemizedBody( n, nn, fvTypes, fvs, sk, sub, sub_vars ); + return Skolemize::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/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index d852667de..b28dca1ed 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -293,7 +293,9 @@ 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->getTermUtil()->getInstConstantNode( n, q ); + Node nn = + d_quantEngine->getTermUtil()->substituteBoundVariablesToInstConstants( + n, q); d_inst_const_node[q][n] = nn; return nn; }else{ diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp new file mode 100644 index 000000000..2f210cc20 --- /dev/null +++ b/src/theory/quantifiers/skolemize.cpp @@ -0,0 +1,385 @@ +/********************* */ +/*! \file skolemize.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 skolemization utility + **/ + +#include "theory/quantifiers/skolemize.h" + +#include "options/quantifiers_options.h" +#include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" +#include "theory/sort_inference.h" +#include "theory/theory_engine.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +Skolemize::Skolemize(QuantifiersEngine* qe, context::UserContext* u) + : d_quantEngine(qe), d_skolemized(u) +{ +} + +Node Skolemize::process(Node q) +{ + // do skolemization + if (d_skolemized.find(q) == d_skolemized.end()) + { + Node body = getSkolemizedBody(q); + NodeBuilder<> nb(kind::OR); + nb << q << body.notNode(); + Node lem = nb; + d_skolemized[q] = lem; + return lem; + } + return Node::null(); +} + +bool Skolemize::getSkolemConstants(Node q, std::vector& skolems) +{ + std::unordered_map, NodeHashFunction>::iterator it = + d_skolem_constants.find(q); + if (it != d_skolem_constants.end()) + { + skolems.insert(skolems.end(), it->second.begin(), it->second.end()); + return true; + } + return false; +} + +Node Skolemize::getSkolemConstant(Node q, unsigned i) +{ + std::unordered_map, NodeHashFunction>::iterator it = + d_skolem_constants.find(q); + if (it != d_skolem_constants.end()) + { + if (i < it->second.size()) + { + return it->second[i]; + } + } + return Node::null(); +} + +void Skolemize::getSelfSel(const Datatype& dt, + const DatatypeConstructor& dc, + Node n, + TypeNode ntn, + std::vector& 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 < dc.getNumArgs(); j++) + { + std::vector 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 Skolemize::mkSkolemizedBody(Node f, + Node n, + std::vector& argTypes, + std::vector& fvs, + std::vector& sk, + Node& sub, + std::vector& sub_vars) +{ + Assert(sk.empty() || sk.size() == f[0].getNumChildren()); + // calculate the variables and substitution + std::vector ind_vars; + std::vector ind_var_indicies; + std::vector vars; + std::vector var_indicies; + for (unsigned i = 0; i < f[0].getNumChildren(); i++) + { + if (isInductionTerm(f[0][i])) + { + ind_vars.push_back(f[0][i]); + ind_var_indicies.push_back(i); + } + else + { + vars.push_back(f[0][i]); + var_indicies.push_back(i); + } + Node s; + // make the new function symbol or use existing + if (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 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 var_sk; + for (unsigned i = 0; i < var_indicies.size(); i++) + { + var_sk.push_back(sk[var_indicies[i]]); + } + Assert(vars.size() == var_sk.size()); + ret = n.substitute(vars.begin(), vars.end(), var_sk.begin(), var_sk.end()); + } + if (!ind_vars.empty()) + { + Trace("sk-ind") << "Ind strengthen : (not " << f << ")" << std::endl; + Trace("sk-ind") << "Skolemized is : " << ret << std::endl; + Node n_str_ind; + TypeNode tn = ind_vars[0].getType(); + Node k = sk[ind_var_indicies[0]]; + Node nret = ret.substitute(ind_vars[0], k); + // note : everything is under a negation + // the following constructs ~( R( x, k ) => ~P( x ) ) + if (options::dtStcInduction() && tn.isDatatype()) + { + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + std::vector disj; + for (unsigned i = 0; i < dt.getNumConstructors(); i++) + { + std::vector selfSel; + getSelfSel(dt, dt[i], k, tn, selfSel); + std::vector conj; + conj.push_back( + NodeManager::currentNM() + ->mkNode(APPLY_TESTER, Node::fromExpr(dt[i].getTester()), k) + .negate()); + for (unsigned j = 0; j < selfSel.size(); j++) + { + conj.push_back(ret.substitute(ind_vars[0], selfSel[j]).negate()); + } + disj.push_back(conj.size() == 1 + ? conj[0] + : NodeManager::currentNM()->mkNode(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 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 < sk.size(); i++) + { + Trace("quantifiers-sk") << sk[i] << " "; + } + Trace("quantifiers-sk") << "for " << std::endl; + Trace("quantifiers-sk") << " " << f << std::endl; + } + + return ret; +} + +Node Skolemize::getSkolemizedBody(Node f) +{ + Assert(f.getKind() == FORALL); + if (d_skolem_body.find(f) == d_skolem_body.end()) + { + std::vector fvTypes; + std::vector fvs; + Node sub; + std::vector 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; i < sub_vars.size(); i++) + { + d_skolem_constants[sub].push_back(d_skolem_constants[f][sub_vars[i]]); + } + } + Assert(d_skolem_constants[f].size() == f[0].getNumChildren()); + if (options::sortInference()) + { + for (unsigned i = 0; i < d_skolem_constants[f].size(); i++) + { + // carry information for sort inference + d_quantEngine->getTheoryEngine()->getSortInference()->setSkolemVar( + f, f[0][i], d_skolem_constants[f][i]); + } + } + } + return d_skolem_body[f]; +} + +bool Skolemize::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 Skolemize::printSkolemization(std::ostream& out) +{ + bool printed = false; + for (NodeNodeMap::iterator it = d_skolemized.begin(); + it != d_skolemized.end(); + ++it) + { + Node q = (*it).first; + printed = true; + out << "(skolem " << q << std::endl; + out << " ( "; + for (unsigned i = 0; i < d_skolem_constants[q].size(); i++) + { + if (i > 0) + { + out << " "; + } + out << d_skolem_constants[q][i]; + } + out << " )" << std::endl; + out << ")" << std::endl; + } + return printed; +} + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h new file mode 100644 index 000000000..c3fb1da29 --- /dev/null +++ b/src/theory/quantifiers/skolemize.h @@ -0,0 +1,146 @@ +/********************* */ +/*! \file skolemize.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 utilities for skolemization + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H +#define __CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H + +#include +#include + +#include "context/cdhashmap.h" +#include "expr/datatype.h" +#include "expr/node.h" +#include "expr/type_node.h" +#include "theory/quantifiers/quant_util.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** Skolemization utility + * + * This class constructs Skolemization lemmas. + * Given a quantified formula q = (forall x. P), + * its skolemization lemma is of the form: + * (~ forall x. P ) => ~P * { x -> d_skolem_constants[q] } + * + * This class also incorporates techniques for + * skolemization with "inductive strenghtening", see + * Section 2 of Reynolds et al., "Induction for SMT + * Solvers", VMCAI 2015. In the case that x is an inductive + * datatype or an integer, then we may strengthen the conclusion + * based on weak well-founded induction. For example, for + * quantification on lists, a skolemization with inductive + * strengthening is a lemma of this form: + * (~ forall x : List. P( x ) ) => + * ~P( k ) ^ ( is-cons( k ) => P( tail( k ) ) ) + * For the integers it is: + * (~ forall x : Int. P( x ) ) => + * ~P( k ) ^ ( x>0 => P( x-1 ) ) + * + * + * Inductive strenghtening is not enabled by + * default and can be enabled by option: + * --quant-ind + */ +class Skolemize +{ + typedef context::CDHashMap NodeNodeMap; + + public: + Skolemize(QuantifiersEngine* qe, context::UserContext* u); + ~Skolemize() {} + /** skolemize quantified formula q + * If the return value ret of this function + * is non-null, then ret is a new skolemization lemma + * we generated for q. These lemmas are constructed + * once per user-context. + */ + Node process(Node q); + /** get skolem constants for quantified formula q */ + bool getSkolemConstants(Node q, std::vector& skolems); + /** get the i^th skolem constant for quantified formula q */ + Node getSkolemConstant(Node q, unsigned i); + /** make skolemized body + * + * This returns the skolemized body n of a + * quantified formula q with inductive strenghtening, + * where typically n is q[1]. + * + * The skolem constants/functions we generate by this + * skolemization are added to sk. + * + * The arguments fvTypes and fvs are used if we are + * performing skolemization within a nested quantified + * formula. In this case, skolem constants we introduce + * must be parameterized based on fvTypes and must be + * applied to fvs. + * + * The last two arguments sub and sub_vars are used for + * to carry the body and indices of other induction + * variables if a quantified formula to skolemize + * has multiple induction variables. See page 5 + * of Reynolds et al., VMCAI 2015. + */ + static Node mkSkolemizedBody(Node q, + Node n, + std::vector& fvTypes, + std::vector& fvs, + std::vector& sk, + Node& sub, + std::vector& sub_vars); + /** get the skolemized body for quantified formula q */ + Node getSkolemizedBody(Node q); + /** is n a variable that we can apply inductive strenghtening to? */ + static bool isInductionTerm(Node n); + /** print all skolemizations + * This is used for the command line option + * --dump-instantiations + * which prints an informal justification + * of steps taken by the quantifiers module. + * Returns true if we printed at least one + * skolemization. + */ + bool printSkolemization(std::ostream& out); + + private: + /** get self selectors + * For datatype constructor dtc with type dt, + * this collects the set of datatype selector applications, + * applied to term n, whose return type in ntn, and stores + * them in the vector selfSel. + */ + static void getSelfSel(const Datatype& dt, + const DatatypeConstructor& dc, + Node n, + TypeNode ntn, + std::vector& selfSel); + /** quantifiers engine that owns this module */ + QuantifiersEngine* d_quantEngine; + /** quantified formulas that have been skolemized */ + NodeNodeMap d_skolemized; + /** map from quantified formulas to the list of skolem constants */ + std::unordered_map, NodeHashFunction> + d_skolem_constants; + /** map from quantified formulas to their skolemized body */ + std::unordered_map d_skolem_body; +}; + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H */ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 59405a5d5..a3225e404 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -112,8 +112,9 @@ Node TermDb::getOperator(unsigned i) } /** ground terms */ -unsigned TermDb::getNumGroundTerms( Node f ) { - std::map< Node, std::vector< Node > >::iterator it = d_op_map.find( f ); +unsigned TermDb::getNumGroundTerms(Node f) const +{ + std::map >::const_iterator it = d_op_map.find(f); if( it!=d_op_map.end() ){ return it->second.size(); }else{ @@ -121,13 +122,25 @@ unsigned TermDb::getNumGroundTerms( Node f ) { } } -Node TermDb::getGroundTerm( Node f, unsigned i ) { - Assert( i >::const_iterator it = d_op_map.find(f); + if (it != d_op_map.end()) + { + Assert(i < it->second.size()); + return it->second[i]; + } + else + { + Assert(false); + return Node::null(); + } } -unsigned TermDb::getNumTypeGroundTerms( TypeNode tn ) { - std::map< TypeNode, std::vector< Node > >::iterator it = d_type_map.find( tn ); +unsigned TermDb::getNumTypeGroundTerms(TypeNode tn) const +{ + std::map >::const_iterator it = + d_type_map.find(tn); if( it!=d_type_map.end() ){ return it->second.size(); }else{ @@ -135,9 +148,61 @@ unsigned TermDb::getNumTypeGroundTerms( TypeNode tn ) { } } -Node TermDb::getTypeGroundTerm( TypeNode tn, unsigned i ) { - Assert( i >::const_iterator it = + d_type_map.find(tn); + if (it != d_type_map.end()) + { + Assert(i < it->second.size()); + return it->second[i]; + } + else + { + Assert(false); + return Node::null(); + } +} + +Node TermDb::getOrMakeTypeGroundTerm(TypeNode tn) +{ + std::map >::const_iterator it = + d_type_map.find(tn); + if (it != d_type_map.end()) + { + Assert(!it->second.empty()); + return it->second[0]; + } + else + { + return getOrMakeTypeFreshVariable(tn); + } +} + +Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn) +{ + std::unordered_map::iterator it = + d_type_fv.find(tn); + if (it == d_type_fv.end()) + { + std::stringstream ss; + ss << language::SetLanguage(options::outputLanguage()); + ss << "e_" << tn; + Node k = NodeManager::currentNM()->mkSkolem( + ss.str(), tn, "is a termDb fresh variable"); + Trace("mkVar") << "TermDb:: Make variable " << k << " : " << tn + << std::endl; + if (options::instMaxLevel() != -1) + { + QuantifiersEngine::setInstantiationLevelAttr(k, 0); + } + d_type_fv[tn] = k; + return k; + } + else + { + return it->second; + } } Node TermDb::getMatchOperator( Node n ) { @@ -179,10 +244,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi //if this is an atomic trigger, consider adding it if( inst::Trigger::isAtomicTrigger( n ) ){ Trace("term-db") << "register term in db " << n << std::endl; - if( options::finiteModelFind() ){ - computeModelBasisArgAttribute( n ); - } - + Node op = getMatchOperator( n ); Trace("term-db-debug") << " match operator is : " << op << std::endl; d_ops.push_back(op); @@ -893,98 +955,6 @@ 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 = NodeManager::currentNM()->mkConst(Rational(0)); - }else if( d_quantEngine->getTermUtil()->isClosedEnumerableType( tn ) ){ - mbt = tn.mkGroundTerm(); - }else{ - if( options::fmfFreshDistConst() || d_type_map[ tn ].empty() ){ - std::stringstream ss; - ss << language::SetLanguage(options::outputLanguage()); - ss << "e_" << tn; - mbt = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "is a model basis term" ); - Trace("mkVar") << "ModelBasis:: Make variable " << mbt << " : " << tn << std::endl; - if( options::instMaxLevel()!=-1 ){ - QuantifiersEngine::setInstantiationLevelAttr( mbt, 0 ); - } - }else{ - mbt = d_type_map[ tn ][ 0 ]; - } - } - ModelBasisAttribute mba; - mbt.setAttribute(mba,true); - d_model_basis_term[tn] = mbt; - Trace("model-basis-term") << "Choose " << mbt << " as model basis term for " << tn << std::endl; - } - return d_model_basis_term[tn]; -} - -Node TermDb::getModelBasisOpTerm( Node op ){ - if( d_model_basis_op_term.find( op )==d_model_basis_op_term.end() ){ - TypeNode t = op.getType(); - std::vector< Node > children; - children.push_back( op ); - for( int i=0; i<(int)(t.getNumChildren()-1); i++ ){ - children.push_back( getModelBasisTerm( t[i] ) ); - } - if( children.size()==1 ){ - d_model_basis_op_term[op] = op; - }else{ - d_model_basis_op_term[op] = NodeManager::currentNM()->mkNode( APPLY_UF, children ); - } - } - return d_model_basis_op_term[op]; -} - -Node TermDb::getModelBasis( Node q, Node n ){ - //make model basis - if( d_model_basis_terms.find( q )==d_model_basis_terms.end() ){ - for( unsigned j=0; jgetTermUtil()->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 = d_quantEngine->getTermUtil()->getInstConstantBody( q ); - d_model_basis_body[q] = getModelBasis( q, n ); - } - return d_model_basis_body[q]; -} - -void TermDb::computeModelBasisArgAttribute( Node n ){ - if( !n.hasAttribute(ModelBasisArgAttribute()) ){ - //ensure that the model basis terms have been defined - if( n.getKind()==APPLY_UF ){ - getModelBasisOpTerm( n.getOperator() ); - } - uint64_t val = 0; - //determine if it has model basis attribute - for( unsigned j=0; j& args); /** in relevant domain * Returns true if there is at least one term t such that: * (1) t is a term that is currently indexed by this database, - * (2) t is of the form f( t1, ..., tk ) and ti is in the equivalence class of - * r. + * (2) t is of the form f( t1, ..., tk ) and ti is in the + * equivalence class of r. */ bool inRelevantDomain(TNode f, unsigned i, TNode r); /** evaluate term @@ -296,9 +318,13 @@ class TermDb : public QuantifiersUtil { bool hasTermCurrent(Node n, bool useMode = true); /** is term eligble for instantiation? */ bool isTermEligibleForInstantiation(TNode n, TNode f, bool print = false); - /** get eligible term in equivalence class */ + /** get eligible term in equivalence class of r */ Node getEligibleTermInEqc(TNode r); - /** is inst closure */ + /** is r a inst closure node? + * This terminology was used for specifying + * a particular status of nodes for + * Bansal et al., CAV 2015. + */ bool isInstClosure(Node r); private: @@ -321,6 +347,8 @@ class TermDb : public QuantifiersUtil { std::map< Node, std::vector< Node > > d_op_map; /** map from type nodes to terms of that type */ std::map< TypeNode, std::vector< Node > > d_type_map; + /** map from type nodes to a fresh variable we introduced */ + std::unordered_map d_type_fv; /** inactive map */ NodeBoolMap d_inactive_map; /** count of the number of non-redundant ground terms per operator */ @@ -364,32 +392,6 @@ class TermDb : public QuantifiersUtil { /** get operator representative */ Node getOperatorRepresentative( TNode op ) const; //------------------------------end higher-order term indexing - - // TODO : as part of #1171, these should be moved somewhere else - // for model basis - private: - /** map from types to model basis terms */ - std::map< TypeNode, Node > d_model_basis_term; - /** map from ops to model basis terms */ - std::map< Node, Node > d_model_basis_op_term; - /** map from instantiation terms to their model basis equivalent */ - std::map< Node, Node > d_model_basis_body; - /** map from universal quantifiers to model basis terms */ - std::map< Node, std::vector< Node > > d_model_basis_terms; - /** compute model basis arg */ - void computeModelBasisArgAttribute( Node n ); - public: - /** get model basis term */ - Node getModelBasisTerm(TypeNode tn, int i = 0); - /** get model basis term for op */ - Node getModelBasisOpTerm(Node op); - /** get model basis */ - Node getModelBasis(Node q, Node n); - /** get model basis body */ - Node getModelBasisBody(Node q); - /** get model basis arg */ - unsigned getModelBasisArg(Node n); - };/* class TermDb */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/term_enumeration.cpp b/src/theory/quantifiers/term_enumeration.cpp new file mode 100644 index 000000000..67ee88c07 --- /dev/null +++ b/src/theory/quantifiers/term_enumeration.cpp @@ -0,0 +1,133 @@ +/********************* */ +/*! \file term_enumeration.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 enumeration utility + **/ + +#include "theory/quantifiers/term_enumeration.h" + +#include "theory/quantifiers/term_util.h" +#include "theory/rewriter.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +Node TermEnumeration::getEnumerateTerm(TypeNode tn, unsigned index) +{ + Trace("term-db-enum") << "Get enumerate term " << tn << " " << index + << std::endl; + std::unordered_map::iterator it = + d_typ_enum_map.find(tn); + size_t teIndex; + if (it == d_typ_enum_map.end()) + { + teIndex = 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 TermEnumeration::isClosedEnumerableType(TypeNode tn) +{ + std::unordered_map::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; i < dt.getNumConstructors(); i++) + { + for (unsigned j = 0; j < dt[i].getNumArgs(); j++) + { + TypeNode ctn = TypeNode::fromType(dt[i][j].getRangeType()); + if (tn != ctn && !isClosedEnumerableType(ctn)) + { + ret = false; + break; + } + } + if (!ret) + { + break; + } + } + } + + // other parametric sorts go here + + d_typ_closed_enum[tn] = ret; + return ret; + } + else + { + return it->second; + } +} + +// checks whether a type is closed enumerable and is reasonably small enough (<1000) +// such that all of its domain elements can be enumerated +bool TermEnumeration::mayComplete(TypeNode tn) +{ + std::unordered_map::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.isConst() && eq.getConst(); + } + d_may_complete[tn] = mc; + return mc; + } + else + { + return it->second; + } +} + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ diff --git a/src/theory/quantifiers/term_enumeration.h b/src/theory/quantifiers/term_enumeration.h new file mode 100644 index 000000000..a96718800 --- /dev/null +++ b/src/theory/quantifiers/term_enumeration.h @@ -0,0 +1,83 @@ +/********************* */ +/*! \file term_enumeration.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 utilities for term enumeration + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H +#define __CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H + +#include +#include + +#include "expr/node.h" +#include "expr/type_node.h" +#include "theory/type_enumerator.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** Term enumeration + * + * This class has utilities for enumerating terms. It stores + * a cache of terms enumerated per each type. + * It also has various utility functions regarding type + * enumeration. + */ +class TermEnumeration +{ + public: + TermEnumeration() {} + ~TermEnumeration() {} + /** get i^th term for type tn */ + Node getEnumerateTerm(TypeNode tn, unsigned i); + /** is closed enumerable type + * + * This returns true if this type has an enumerator that produces + * constants that are handled by ground theory solvers. + * Examples of types that are not closed enumerable are: + * (1) uninterpreted sorts, + * (2) arrays, + * (3) codatatypes, + * (4) parametric sorts involving any of the above. + */ + bool isClosedEnumerableType(TypeNode tn); + /** may complete type + * + * Returns true if the type tn is closed + * enumerable, and is small enough + * for finite model finding to enumerate it, + * by some heuristic (current cardinality < 1000). + */ + bool mayComplete(TypeNode tn); + + private: + /** ground terms enumerated for types */ + std::unordered_map, TypeNodeHashFunction> + d_enum_terms; + /** map from type to the index of its type enumerator in d_typ_enum. */ + std::unordered_map d_typ_enum_map; + /** type enumerators */ + std::vector d_typ_enum; + /** closed enumerable type cache */ + std::unordered_map d_typ_closed_enum; + /** may complete */ + std::unordered_map d_may_complete; +}; + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H */ diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 346745b1d..471670515 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -16,12 +16,13 @@ #include "expr/datatype.h" #include "options/base_options.h" -#include "options/quantifiers_options.h" #include "options/datatypes_options.h" +#include "options/quantifiers_options.h" #include "options/uf_options.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers_engine.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_enumeration.h" +#include "theory/quantifiers_engine.h" +#include "theory/theory_engine.h" using namespace std; using namespace CVC4::kind; @@ -197,7 +198,7 @@ unsigned TermUtil::getNumInstantiationConstants( Node q ) const { 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 ); + Node n = substituteBoundVariablesToInstConstants(q[1], q); d_inst_const_body[ q ] = n; return n; }else{ @@ -225,273 +226,35 @@ Node TermUtil::getCounterexampleLiteral( Node q ){ return d_ce_lit[ q ]; } -Node TermUtil::getInstConstantNode( Node n, Node q ){ +Node TermUtil::substituteBoundVariablesToInstConstants(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 ) { +Node TermUtil::substituteInstConstantsToBoundVariables(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 ) { +Node TermUtil::substituteBoundVariables(Node n, + Node q, + std::vector& terms) +{ + registerQuantifier(q); 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; - } +Node TermUtil::substituteInstConstants(Node n, Node q, std::vector& terms) +{ + registerQuantifier(q); + Assert(d_inst_constants[q].size() == terms.size()); + return n.substitute(d_inst_constants[q].begin(), + d_inst_constants[q].end(), + terms.begin(), + terms.end()); } void TermUtil::computeVarContains( Node n, std::vector< Node >& varContains ) { @@ -1154,12 +917,6 @@ bool TermUtil::isBoolConnectiveTerm( TNode n ) { ( 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() ){ @@ -1172,17 +929,6 @@ Node TermUtil::getHoTypeMatchPredicate( TypeNode tn ) { } } -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 */ diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index f5cfd6df8..bcdf8a2ff 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -46,13 +46,6 @@ 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; @@ -69,7 +62,7 @@ typedef expr::Attribute RrPriorityAttribute; struct LtePartialInstAttributeId {}; typedef expr::Attribute< LtePartialInstAttributeId, bool > LtePartialInstAttribute; -// attribute for "contains instantiation constants from" +// attribute for sygus proxy variables struct SygusProxyAttributeId {}; typedef expr::Attribute SygusProxyAttribute; @@ -114,7 +107,6 @@ class TermUtil : public QuantifiersUtil { // TODO : remove these friend class ::CVC4::theory::QuantifiersEngine; - friend class TermDatabase; private: /** reference to the quantifiers engine */ QuantifiersEngine* d_quantEngine; @@ -164,10 +156,14 @@ public: 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 ); + Node substituteBoundVariablesToInstConstants(Node n, Node q); + /** substitute { instantiation constants of q -> bound variables of q } in n + */ + Node substituteInstConstantsToBoundVariables(Node n, Node q); + /** substitute { variables of q -> terms } in n */ + Node substituteBoundVariables(Node n, Node q, std::vector& terms); + /** substitute { instantiation constants of q -> terms } in n */ + Node substituteInstConstants(Node n, Node q, std::vector& terms); static Node getInstConstAttr( Node n ); static bool hasInstConstAttr( Node n ); @@ -187,51 +183,18 @@ public: //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: + /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */ + static int isInstanceOf(Node n1, Node n2); + + public: /** compute var contains */ static void computeVarContains( Node n, std::vector< Node >& varContains ); /** get var contains for each of the patterns in pats */ @@ -240,12 +203,9 @@ public: 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 ); + // TODO (#1216) : this should be in trigger.h /** 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: diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 2d5f48a5c..e742b8be9 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -45,8 +45,10 @@ #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/relevant_domain.h" #include "theory/quantifiers/rewrite_engine.h" +#include "theory/quantifiers/skolemize.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_database_sygus.h" +#include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers/trigger.h" #include "theory/sep/theory_sep.h" @@ -67,11 +69,12 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, TheoryEngine* te) : d_te(te), d_quant_attr(new quantifiers::QuantAttributes(this)), + d_skolemize(new quantifiers::Skolemize(this, u)), + d_term_enum(new quantifiers::TermEnumeration), d_conflict_c(c, false), // d_quants(u), d_quants_red(u), d_lemmas_produced_c(u), - d_skolemized(u), d_ierCounter_c(c), // d_ierCounter(c), // d_ierCounter_lc(c), @@ -366,7 +369,9 @@ bool QuantifiersEngine::isFiniteBound( Node q, Node v ) { TypeNode tn = v.getType(); if( tn.isSort() && options::finiteModelFind() ){ return true; - }else if( getTermUtil()->mayComplete( tn ) ){ + } + else if (d_term_enum->mayComplete(tn)) + { return true; } } @@ -792,17 +797,14 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ //if not reduced if( !reduceQuantifier( f ) ){ //do skolemization - if( d_skolemized.find( f )==d_skolemized.end() ){ - Node body = d_term_util->getSkolemizedBody( f ); - NodeBuilder<> nb(kind::OR); - nb << f << body.notNode(); - Node lem = nb; + Node lem = d_skolemize->process(f); + if (!lem.isNull()) + { if( Trace.isOn("quantifiers-sk-debug") ){ Node slem = Rewriter::rewrite( lem ); Trace("quantifiers-sk-debug") << "Skolemize lemma : " << slem << std::endl; } getOutputChannel().lemma( lem, false, true ); - d_skolemized[f] = true; } } }else{ @@ -848,8 +850,8 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool within //only wait if we are doing incremental solving if( !d_presolve || !options::incrementalSolving() ){ std::set< Node > added; - getTermDatabase()->addTerm( n, added, withinQuant, withinInstClosure ); - + d_term_db->addTerm(n, added, withinQuant, withinInstClosure); + //added contains also the Node that just have been asserted in this branch if( d_quant_rel ){ for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){ @@ -1125,15 +1127,16 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo for( unsigned i=0; i " << terms[i]; + TypeNode tn = q[0][i].getType(); if( terms[i].isNull() ){ - terms[i] = d_term_db->getModelBasisTerm( q[0][i].getType() ); + terms[i] = getTermForType(tn); } if( mkRep ){ //pick the best possible representative for instantiation, based on past use and simplicity of term terms[i] = getInternalRepresentative( terms[i], q, i ); }else{ //ensure the type is correct - terms[i] = quantifiers::TermUtil::ensureType( terms[i], q[0][i].getType() ); + terms[i] = quantifiers::TermUtil::ensureType(terms[i], tn); } Trace("inst-add-debug") << " -> " << terms[i] << std::endl; if( terms[i].isNull() ){ @@ -1509,18 +1512,12 @@ void QuantifiersEngine::printInstantiations( std::ostream& out ) { } bool printed = false; - for( BoolMap::iterator it = d_skolemized.begin(); it != d_skolemized.end(); ++it ){ - Node q = (*it).first; + // print the skolemizations + if (d_skolemize->printSkolemization(out)) + { printed = true; - out << "(skolem " << q << std::endl; - out << " ( "; - for( unsigned i=0; id_skolem_constants[q].size(); i++ ){ - if( i>0 ){ out << " "; } - out << d_term_util->d_skolem_constants[q][i]; - } - out << " )" << std::endl; - out << ")" << std::endl; } + // print the instantiations if( options::incrementalSolving() ){ for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){ bool firstTime = true; @@ -1722,6 +1719,18 @@ Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){ return ret; } +Node QuantifiersEngine::getTermForType(TypeNode tn) +{ + if (d_term_enum->isClosedEnumerableType(tn)) + { + return d_term_enum->getEnumerateTerm(tn, 0); + } + else + { + return d_term_db->getOrMakeTypeGroundTerm(tn); + } +} + void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) { eq::EqualityEngine* ee = getActiveEqualityEngine(); eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index be0c4cd43..9743588a7 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -50,10 +50,13 @@ public: namespace quantifiers { //TODO: organize this more/review this, github issue #1163 + //TODO: include these instead of doing forward declarations? #1307 //utilities class TermDb; class TermDbSygus; class TermUtil; + class Skolemize; + class TermEnumeration; class FirstOrderModel; class QuantAttributes; class RelevantDomain; @@ -132,6 +135,10 @@ private: quantifiers::TermUtil* d_term_util; /** quantifiers attributes */ std::unique_ptr d_quant_attr; + /** skolemize utility */ + std::unique_ptr d_skolemize; + /** term enumeration utility */ + std::unique_ptr d_term_enum; private: /** instantiation engine */ @@ -202,8 +209,6 @@ private: std::map< Node, inst::CDInstMatchTrie* > d_c_inst_match_trie; /** recorded instantiations */ std::vector< std::pair< Node, std::vector< Node > > > d_recorded_inst; - /** quantifiers that have been skolemized */ - BoolMap d_skolemized; /** all triggers will be stored in this trie */ inst::TriggerTrie* d_tr_trie; /** extended model object */ @@ -385,6 +390,13 @@ public: quantifiers::QuantAttributes* getQuantAttributes() { return d_quant_attr.get(); } + /** get skolemize utility */ + quantifiers::Skolemize* getSkolemize() { return d_skolemize.get(); } + /** get term enumeration utility */ + quantifiers::TermEnumeration* getTermEnumeration() + { + return d_term_enum.get(); + } /** get trigger database */ inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; } /** add term to database */ @@ -402,7 +414,19 @@ public: void debugPrintEqualityEngine( const char * c ); /** get internal representative */ Node getInternalRepresentative( Node a, Node q, int index ); -public: + /** get term for type + * + * This returns an arbitrary term for type tn. + * This term is chosen heuristically to be the best + * term for instantiation. Currently, this + * heuristic enumerates the first term of the + * type if the type is closed enumerable, otherwise + * an existing ground term from the term database if + * one exists, or otherwise a fresh variable. + */ + Node getTermForType(TypeNode tn); + + public: /** print instantiations */ void printInstantiations( std::ostream& out ); /** print solution for synthesis conjectures */ diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index dd139d5ec..5c02b631c 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -14,11 +14,12 @@ #include -#include "theory/rep_set.h" -#include "theory/type_enumerator.h" #include "theory/quantifiers/bounded_integers.h" -#include "theory/quantifiers/term_util.h" #include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/term_enumeration.h" +#include "theory/quantifiers/term_util.h" +#include "theory/rep_set.h" +#include "theory/type_enumerator.h" using namespace std; using namespace CVC4; @@ -216,6 +217,9 @@ bool RepSetIterator::setFunctionDomain( Node op, RepBoundExt* rext ){ return initialize( rext ); } +// TODO : as part of #1199, the portions of this +// function which modify d_rep_set should be +// moved to TheoryModel. bool RepSetIterator::initialize( RepBoundExt* rext ){ Trace("rsi") << "Initialize rep set iterator..." << std::endl; for( unsigned v=0; vgetTermUtil()->mayComplete( tn ) ){ + if (d_qe->getTermEnumeration()->mayComplete(tn)) + { Trace("rsi") << " do complete, since cardinality is small (" << tn.getCardinality() << ")..." << std::endl; d_rep_set->complete( tn ); //must have succeeded diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index 54e99cdba..b524f90c4 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_util.h" +#include "theory/quantifiers/first_order_model.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_model.h b/src/theory/uf/theory_uf_model.h index 0b55c926e..9cfffed16 100644 --- a/src/theory/uf/theory_uf_model.h +++ b/src/theory/uf/theory_uf_model.h @@ -23,6 +23,8 @@ namespace CVC4 { namespace theory { namespace uf { +// TODO (#1302) : some of these classes should be moved to +// src/theory/quantifiers/ class UfModelTreeNode { public: -- 2.30.2