diff options
author | Paul Meng <baolmeng@gmail.com> | 2016-10-11 13:54:20 -0500 |
---|---|---|
committer | Paul Meng <baolmeng@gmail.com> | 2016-10-11 13:54:20 -0500 |
commit | 3395c5c13cd61d98aec0d9806e3b9bc3d707968a (patch) | |
tree | 0eadad9799862ec77d29f7abe03a46c300d80de8 /src/theory/quantifiers | |
parent | 773e7d27d606b71ff0f78e84efe1deef2653f016 (diff) | |
parent | 5f415d4585134612bc24e9a823289fee35541a01 (diff) |
Merge branch 'origin' of https://github.com/CVC4/CVC4.git
Conflicts:
src/options/quantifiers_options
Diffstat (limited to 'src/theory/quantifiers')
48 files changed, 2622 insertions, 1906 deletions
diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp index 97116dee4..2ccc17e55 100755 --- a/src/theory/quantifiers/ambqi_builder.cpp +++ b/src/theory/quantifiers/ambqi_builder.cpp @@ -836,7 +836,7 @@ void AbsMbqiBuilder::processBuildModel(TheoryModel* m, bool fullModel) { //--------------------model checking--------------------------------------- //do exhaustive instantiation -bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ) { +int AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ) { Trace("ambqi-check") << "Exhaustive instantiation " << q << " " << effort << std::endl; if (effort==0) { FirstOrderModelAbs * fma = fm->asFirstOrderModelAbs(); @@ -868,9 +868,10 @@ bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, in d_addedLemmas += lem; Trace("ambqi-inst-debug") << "...Total : " << d_addedLemmas << std::endl; } - return quantValid; + return quantValid ? 1 : 0; + }else{ + return 1; } - return true; } bool AbsMbqiBuilder::doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n ) { diff --git a/src/theory/quantifiers/ambqi_builder.h b/src/theory/quantifiers/ambqi_builder.h index 3669d38b7..0adaef638 100755 --- a/src/theory/quantifiers/ambqi_builder.h +++ b/src/theory/quantifiers/ambqi_builder.h @@ -93,7 +93,7 @@ public: //process build model void processBuildModel(TheoryModel* m, bool fullModel); //do exhaustive instantiation - bool doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ); + int doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ); }; } diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp index c8d18aced..9ccba38cd 100755 --- a/src/theory/quantifiers/anti_skolem.cpp +++ b/src/theory/quantifiers/anti_skolem.cpp @@ -14,18 +14,19 @@ **/ #include "theory/quantifiers/anti_skolem.h" + +#include "options/quantifiers_options.h" +#include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers_engine.h" -#include "theory/quantifiers/first_order_model.h" -#include "options/quantifiers_options.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 { struct sortTypeOrder { TermDb* d_tdb; @@ -74,10 +75,13 @@ bool QuantAntiSkolem::CDSkQuantCache::add( context::Context* c, std::vector< Nod } } -QuantAntiSkolem::QuantAntiSkolem( QuantifiersEngine * qe ) : QuantifiersModule( qe ){ - d_sqc = new CDSkQuantCache( qe->getUserContext() ); +QuantAntiSkolem::QuantAntiSkolem(QuantifiersEngine* qe) + : QuantifiersModule(qe) { + d_sqc = new CDSkQuantCache(qe->getUserContext()); } +QuantAntiSkolem::~QuantAntiSkolem() { delete d_sqc; } + /* Call during quantifier engine's check */ void QuantAntiSkolem::check( Theory::Effort e, unsigned quant_e ) { if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){ @@ -267,3 +271,6 @@ bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool } } +}/* namespace CVC4::theory::quantifiers */ +}/* namespace CVC4::theory */ +}/* namespace CVC4 */ diff --git a/src/theory/quantifiers/anti_skolem.h b/src/theory/quantifiers/anti_skolem.h index 721371159..48205db9d 100755 --- a/src/theory/quantifiers/anti_skolem.h +++ b/src/theory/quantifiers/anti_skolem.h @@ -17,17 +17,39 @@ #ifndef __CVC4__THEORY__QUANT_ANTI_SKOLEM_H #define __CVC4__THEORY__QUANT_ANTI_SKOLEM_H -#include "theory/quantifiers_engine.h" +#include <map> +#include <vector> + +#include "expr/node.h" +#include "expr/type_node.h" +#include "context/cdhashset.h" #include "context/cdo.h" #include "theory/quantifiers/ce_guided_single_inv.h" +#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { namespace quantifiers { class QuantAntiSkolem : public QuantifiersModule { +public: + QuantAntiSkolem( QuantifiersEngine * qe ); + virtual ~QuantAntiSkolem(); + + bool sendAntiSkolemizeLemma( std::vector< Node >& quants, + bool pconnected = true ); + + /* Call during quantifier engine's check */ + void check( Theory::Effort e, unsigned quant_e ); + /* Called for new quantifiers */ + void registerQuantifier( Node q ) {} + void assertNode( Node n ) {} + /** Identify this module (for debugging, dynamic configuration, etc..) */ + std::string identify() const { return "QuantAntiSkolem"; } + + private: typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; -private: + std::map< Node, bool > d_quant_processed; std::map< Node, SingleInvocationPartition > d_quant_sip; std::map< Node, std::vector< TypeNode > > d_ask_types; @@ -54,22 +76,10 @@ private: bool add( context::Context* c, std::vector< Node >& quants, unsigned index = 0 ); }; CDSkQuantCache * d_sqc; -public: - bool sendAntiSkolemizeLemma( std::vector< Node >& quants, bool pconnected = true ); -public: - QuantAntiSkolem( QuantifiersEngine * qe ); - - /* Call during quantifier engine's check */ - void check( Theory::Effort e, unsigned quant_e ); - /* Called for new quantifiers */ - void registerQuantifier( Node q ) {} - void assertNode( Node n ) {} - /** Identify this module (for debugging, dynamic configuration, etc..) */ - std::string identify() const { return "QuantAntiSkolem"; } -}; +}; /* class QuantAntiSkolem */ -} -} -} +}/* namespace CVC4::theory::quantifiers */ +}/* namespace CVC4::theory */ +}/* namespace CVC4 */ #endif diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index a0d9bda0f..8e8f34cac 100755 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -264,6 +264,7 @@ CandidateGeneratorQEAll::CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mp Assert( mpat.getKind()==INST_CONSTANT ); d_f = quantifiers::TermDb::getInstConstAttr( mpat ); d_index = mpat.getAttribute(InstVarNumAttribute()); + d_firstTime = false; } void CandidateGeneratorQEAll::resetInstantiationRound() { diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 71bf7c426..54415d974 100755 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -767,7 +767,7 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { Assert( dt.isSygus() ); //get the solution Node sol; - int status; + int status = -1; if( d_last_inst_si ){ Assert( d_conj->getCegConjectureSingleInv() != NULL ); sol = d_conj->getSingleInvocationSolution( i, tn, status ); @@ -786,39 +786,45 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { for( unsigned j=0; j<svl.getNumChildren(); j++ ){ subs.push_back( Node::fromExpr( svl[j] ) ); } + bool templIsPost = false; + Node templ; if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){ - const CegConjectureSingleInv* ceg_si = - d_conj->getCegConjectureSingleInv(); + const CegConjectureSingleInv* ceg_si = d_conj->getCegConjectureSingleInv(); if(ceg_si->d_trans_pre.find( prog ) != ceg_si->d_trans_pre.end()){ - std::vector<Node>& templ_vars = d_conj->getProgTempVars(prog); - Assert(templ_vars.size() == subs.size()); - Node pre = ceg_si->getTransPre(prog); - pre = pre.substitute( templ_vars.begin(), templ_vars.end(), - subs.begin(), subs.end() ); - TermDbSygus* sygusDb = getTermDatabase()->getTermDatabaseSygus(); - sol = sygusDb->sygusToBuiltin( sol, sol.getType() ); - Trace("cegqi-inv") << "Builtin version of solution is : " - << sol << ", type : " << sol.getType() - << std::endl; - sol = NodeManager::currentNM()->mkNode( OR, sol, pre ); + templ = ceg_si->getTransPre(prog); + templIsPost = false; } }else if(options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST){ - const CegConjectureSingleInv* ceg_si = - d_conj->getCegConjectureSingleInv(); + const CegConjectureSingleInv* ceg_si = d_conj->getCegConjectureSingleInv(); if(ceg_si->d_trans_post.find(prog) != ceg_si->d_trans_post.end()){ - std::vector<Node>& templ_vars = d_conj->getProgTempVars(prog); - Assert( templ_vars.size()==subs.size() ); - Node post = ceg_si->getTransPost(prog); - post = post.substitute( templ_vars.begin(), templ_vars.end(), - subs.begin(), subs.end() ); - TermDbSygus* sygusDb = getTermDatabase()->getTermDatabaseSygus(); - sol = sygusDb->sygusToBuiltin( sol, sol.getType() ); - Trace("cegqi-inv") << "Builtin version of solution is : " - << sol << ", type : " << sol.getType() - << std::endl; - sol = NodeManager::currentNM()->mkNode( AND, sol, post ); + templ = ceg_si->getTransPost(prog); + templIsPost = true; } } + if( !templ.isNull() ){ + std::vector<Node>& templ_vars = d_conj->getProgTempVars(prog); + + //take into consideration Boolean term conversion (this step can be eliminated when boolean term conversion is eliminated) + std::vector< Node > vars; + vars.insert( vars.end(), templ_vars.begin(), templ_vars.end() ); + Node vl = Node::fromExpr( dt.getSygusVarList() ); + Assert(vars.size() == subs.size()); + for( unsigned j=0; j<templ_vars.size(); j++ ){ + if( vl[j].getType().isBoolean() ){ + Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u)); + vars[j] = vars[j].eqNode( c ); + } + Assert( vars[j].getType()==subs[j].getType() ); + } + + templ = templ.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + TermDbSygus* sygusDb = getTermDatabase()->getTermDatabaseSygus(); + sol = sygusDb->sygusToBuiltin( sol, sol.getType() ); + Trace("cegqi-inv") << "Builtin version of solution is : " + << sol << ", type : " << sol.getType() + << std::endl; + sol = NodeManager::currentNM()->mkNode( templIsPost ? AND : OR, sol, templ ); + } if( sol==sygus_sol ){ sol = sygus_sol; status = 1; diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 981abea94..e0bbbf8ac 100755 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -45,27 +45,41 @@ bool CegqiOutputSingleInv::addLemma( Node n ) { return d_out->addLemma( n ); } +CegConjectureSingleInv::CegConjectureSingleInv(QuantifiersEngine* qe, + CegConjecture* p) + : d_qe(qe), + d_parent(p), + d_sip(new SingleInvocationPartition), + d_sol(new CegConjectureSingleInvSol(qe)), + d_ei(NULL), + d_cosi(new CegqiOutputSingleInv(this)), + d_cinst(NULL), + d_c_inst_match_trie(NULL), + d_has_ites(true) { + // third and fourth arguments set to (false,false) until we have solution + // reconstruction for delta and infinity + d_cinst = new CegInstantiator(d_qe, d_cosi, false, false); -CegConjectureSingleInv::CegConjectureSingleInv( QuantifiersEngine * qe, CegConjecture * p ) : d_qe( qe ), d_parent( p ){ - d_has_ites = true; - if( options::incrementalSolving() ){ - d_c_inst_match_trie = new inst::CDInstMatchTrie( qe->getUserContext() ); - }else{ - d_c_inst_match_trie = NULL; + if (options::incrementalSolving()) { + d_c_inst_match_trie = new inst::CDInstMatchTrie(qe->getUserContext()); } - d_cosi = new CegqiOutputSingleInv( this ); - // third and fourth arguments set to (false,false) until we have solution reconstruction for delta and infinity - d_cinst = new CegInstantiator( d_qe, d_cosi, false, false ); - d_sol = new CegConjectureSingleInvSol( qe ); - - d_sip = new SingleInvocationPartition; + if (options::cegqiSingleInvPartial()) { + d_ei = new CegEntailmentInfer(qe, d_sip); + } +} - if( options::cegqiSingleInvPartial() ){ - d_ei = new CegEntailmentInfer( qe, d_sip ); - }else{ - d_ei = NULL; +CegConjectureSingleInv::~CegConjectureSingleInv() { + if (d_c_inst_match_trie) { + delete d_c_inst_match_trie; + } + delete d_cinst; + delete d_cosi; + if (d_ei) { + delete d_ei; } + delete d_sol; // (new CegConjectureSingleInvSol(qe)), + delete d_sip; // d_sip(new SingleInvocationPartition), } void CegConjectureSingleInv::getInitialSingleInvLemma( std::vector< Node >& lems ) { diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index feadeca39..449ab7189 100755 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -31,11 +31,10 @@ class CegConjecture; class CegConjectureSingleInv; class CegEntailmentInfer; -class CegqiOutputSingleInv : public CegqiOutput -{ +class CegqiOutputSingleInv : public CegqiOutput { public: CegqiOutputSingleInv( CegConjectureSingleInv * out ) : d_out( out ){} - ~CegqiOutputSingleInv() {} + virtual ~CegqiOutputSingleInv() {} CegConjectureSingleInv * d_out; bool doAddInstantiation( std::vector< Node >& subs ); bool isEligibleForInstantiation( Node n ); @@ -45,22 +44,13 @@ public: class SingleInvocationPartition; -class CegConjectureSingleInv -{ +class CegConjectureSingleInv { + private: friend class CegqiOutputSingleInv; -private: - SingleInvocationPartition * d_sip; - QuantifiersEngine * d_qe; - CegConjecture * d_parent; - CegConjectureSingleInvSol * d_sol; - CegEntailmentInfer * d_ei; - //the instantiator - CegqiOutputSingleInv * d_cosi; - CegInstantiator * d_cinst; - //for recognizing templates for invariant synthesis + // for recognizing templates for invariant synthesis Node substituteInvariantTemplates( - Node n, std::map< Node, Node >& prog_templ, - std::map< Node, std::vector< Node > >& prog_templ_vars ); + Node n, std::map<Node, Node>& prog_templ, + std::map<Node, std::vector<Node> >& prog_templ_vars); // partially single invocation Node removeDeepEmbedding( Node n, std::vector< Node >& progs, std::vector< TypeNode >& types, int& type_valid, @@ -73,42 +63,56 @@ private: std::vector< Node >& terms, std::map< Node, std::vector< Node > >& teq, Node n, std::vector< Node >& conj ); - //constructing solution - Node constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index, std::map< Node, Node >& weak_imp ); - Node postProcessSolution( Node n ); -private: - //list of skolems for each argument of programs - std::vector< Node > d_single_inv_arg_sk; - //list of variables/skolems for each program - std::vector< Node > d_single_inv_var; - std::vector< Node > d_single_inv_sk; - std::map< Node, int > d_single_inv_sk_index; - //program to solution index - std::map< Node, unsigned > d_prog_to_sol_index; - //lemmas produced + // constructing solution + Node constructSolution(std::vector<unsigned>& indices, unsigned i, + unsigned index, std::map<Node, Node>& weak_imp); + Node postProcessSolution(Node n); + + private: + QuantifiersEngine* d_qe; + CegConjecture* d_parent; + SingleInvocationPartition* d_sip; + CegConjectureSingleInvSol* d_sol; + CegEntailmentInfer* d_ei; + // the instantiator + CegqiOutputSingleInv* d_cosi; + CegInstantiator* d_cinst; + + // list of skolems for each argument of programs + std::vector<Node> d_single_inv_arg_sk; + // list of variables/skolems for each program + std::vector<Node> d_single_inv_var; + std::vector<Node> d_single_inv_sk; + std::map<Node, int> d_single_inv_sk_index; + // program to solution index + std::map<Node, unsigned> d_prog_to_sol_index; + // lemmas produced inst::InstMatchTrie d_inst_match_trie; - inst::CDInstMatchTrie * d_c_inst_match_trie; - //original conjecture + inst::CDInstMatchTrie* d_c_inst_match_trie; + // original conjecture Node d_orig_conjecture; // solution Node d_orig_solution; Node d_solution; Node d_sygus_solution; bool d_has_ites; -public: - //lemmas produced - std::vector< Node > d_lemmas_produced; - std::vector< std::vector< Node > > d_inst; -private: - std::vector< Node > d_curr_lemmas; - //add instantiation + + public: + // lemmas produced + std::vector<Node> d_lemmas_produced; + std::vector<std::vector<Node> > d_inst; + + private: + std::vector<Node> d_curr_lemmas; + // add instantiation bool doAddInstantiation( std::vector< Node >& subs ); //is eligible for instantiation bool isEligibleForInstantiation( Node n ); // add lemma bool addLemma( Node lem ); -public: + public: CegConjectureSingleInv( QuantifiersEngine * qe, CegConjecture * p ); + ~CegConjectureSingleInv(); // original conjecture Node d_quant; // single invocation portion of quantified formula @@ -130,7 +134,7 @@ public: std::map< Node, Node > d_nsi_op_map; std::map< Node, Node > d_nsi_op_map_to_prog; std::map< Node, Node > d_prog_to_eval_op; -public: + public: //get the single invocation lemma(s) void getInitialSingleInvLemma( std::vector< Node >& lems ); //initialize @@ -169,12 +173,12 @@ public: }; -// partitions any formulas given to it into single invocation/non-single invocation -// only processes functions having argument types exactly matching "d_arg_types", -// and all invocations are in the same order across all functions -class SingleInvocationPartition -{ -private: +// partitions any formulas given to it into single invocation/non-single +// invocation only processes functions having argument types exactly matching +// "d_arg_types", and all invocations are in the same order across all +// functions +class SingleInvocationPartition { + private: //options Kind d_checkKind; bool inferArgTypes( Node n, std::vector< TypeNode >& typs, std::map< Node, bool >& visited ); diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 0fe4b98c7..61a20ad42 100755 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -11,21 +11,18 @@ ** ** \brief Implementation of counterexample-guided quantifier instantiation **/ + #include "theory/quantifiers/ceg_instantiator.h" +#include "theory/quantifiers/ceg_t_instantiator.h" #include "options/quantifiers_options.h" #include "smt/ite_removal.h" -#include "theory/arith/partial_model.h" -#include "theory/arith/theory_arith.h" -#include "theory/arith/theory_arith_private.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/trigger.h" #include "theory/theory_engine.h" -#include "theory/bv/theory_bv_utils.h" -#include "util/bitvector.h" - -//#define MBP_STRICT_ASSERTIONS using namespace std; using namespace CVC4; @@ -36,12 +33,15 @@ using namespace CVC4::theory::quantifiers; CegInstantiator::CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta, bool use_vts_inf ) : d_qe( qe ), d_out( out ), d_use_vts_delta( use_vts_delta ), d_use_vts_inf( use_vts_inf ){ - d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); - d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); - d_true = NodeManager::currentNM()->mkConst( true ); d_is_nested_quant = false; } +CegInstantiator::~CegInstantiator() { + for( std::map< Node, Instantiator * >::iterator it = d_instantiator.begin(); it != d_instantiator.end(); ++it ){ + delete it->second; + } +} + void CegInstantiator::computeProgVars( Node n ){ if( d_prog_var.find( n )==d_prog_var.end() ){ d_prog_var[n].clear(); @@ -68,41 +68,108 @@ void CegInstantiator::computeProgVars( Node n ){ } } -bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, - std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, - std::map< Node, Node >& cons, std::vector< Node >& curr_var ){ +bool CegInstantiator::isEligible( Node n ) { + //compute d_subs_fv, which program variables are contained in n, and determines if eligible + computeProgVars( n ); + return d_inelig.find( n )==d_inelig.end(); +} + +bool CegInstantiator::hasVariable( Node n, Node pv ) { + computeProgVars( n ); + return d_prog_var[n].find( pv )!=d_prog_var[n].end(); +} + + +void CegInstantiator::registerInstantiationVariable( Node v, unsigned index ) { + if( d_instantiator.find( v )==d_instantiator.end() ){ + TypeNode tn = v.getType(); + Instantiator * vinst; + if( tn.isReal() ){ + vinst = new ArithInstantiator( d_qe, tn ); + }else if( tn.isSort() ){ + Assert( options::quantEpr() ); + vinst = new EprInstantiator( d_qe, tn ); + }else if( tn.isDatatype() ){ + vinst = new DtInstantiator( d_qe, tn ); + }else if( tn.isBitVector() ){ + vinst = new BvInstantiator( d_qe, tn ); + }else if( tn.isBoolean() ){ + vinst = new ModelValueInstantiator( d_qe, tn ); + }else{ + //default + vinst = new Instantiator( d_qe, tn ); + } + d_instantiator[v] = vinst; + } + d_curr_subs_proc[v].clear(); + d_curr_index[v] = index; +} + +void CegInstantiator::unregisterInstantiationVariable( Node v ) { + d_curr_subs_proc.erase( v ); + d_curr_index.erase( v ); +} + +bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned effort ){ if( i==d_vars.size() ){ //solved for all variables, now construct instantiation - if( !sf.d_has_coeff.empty() ){ - if( options::cbqiSymLia() ){ - //use symbolic solved forms - SolvedForm csf; - csf.copy( ssf ); - return doAddInstantiationCoeff( csf, vars, btyp, 0, cons ); + bool needsPostprocess = false; + std::map< Instantiator *, Node > pp_inst; + for( std::map< Node, Instantiator * >::iterator ita = d_active_instantiators.begin(); ita != d_active_instantiators.end(); ++ita ){ + if( ita->second->needsPostProcessInstantiation( this, sf, ita->first, effort ) ){ + needsPostprocess = true; + pp_inst[ ita->second ] = ita->first; + } + } + if( needsPostprocess ){ + //must make copy so that backtracking reverts sf + SolvedForm sf_tmp; + sf_tmp.copy( sf ); + bool postProcessSuccess = true; + for( std::map< Instantiator *, Node >::iterator itp = pp_inst.begin(); itp != pp_inst.end(); ++itp ){ + if( !itp->first->postProcessInstantiation( this, sf_tmp, itp->second, effort ) ){ + postProcessSuccess = false; + break; + } + } + if( postProcessSuccess ){ + return doAddInstantiation( sf_tmp.d_subs, sf_tmp.d_vars ); }else{ - return doAddInstantiationCoeff( sf, vars, btyp, 0, cons ); + return false; } }else{ - return doAddInstantiation( sf.d_subs, vars, cons ); + return doAddInstantiation( sf.d_subs, sf.d_vars ); } }else{ - std::map< Node, std::map< Node, bool > > subs_proc; //Node v = d_single_inv_map_to_prog[d_single_inv[0][i]]; bool is_cv = false; Node pv; - if( curr_var.empty() ){ + if( d_stack_vars.empty() ){ pv = d_vars[i]; }else{ - pv = curr_var.back(); + pv = d_stack_vars.back(); is_cv = true; + d_stack_vars.pop_back(); + } + registerInstantiationVariable( pv, i ); + + //get the instantiator object + Instantiator * vinst = NULL; + std::map< Node, Instantiator * >::iterator itin = d_instantiator.find( pv ); + if( itin!=d_instantiator.end() ){ + vinst = itin->second; } + Assert( vinst!=NULL ); + d_active_instantiators[pv] = vinst; + vinst->reset( this, sf, pv, effort ); + TypeNode pvtn = pv.getType(); TypeNode pvtnb = pvtn.getBaseType(); Node pvr = pv; if( d_qe->getMasterEqualityEngine()->hasTerm( pv ) ){ pvr = d_qe->getMasterEqualityEngine()->getRepresentative( pv ); } - Trace("cbqi-inst-debug") << "[Find instantiation for " << pv << "], rep=" << pvr << std::endl; + Trace("cbqi-inst-debug") << "[Find instantiation for " << pv << "], rep=" << pvr << ", instantiator is " << vinst->identify() << std::endl; Node pv_value; if( options::cbqiModel() ){ pv_value = getModelValue( pv ); @@ -116,72 +183,38 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std:: Trace("cbqi-inst-debug") << "[1] try based on equivalence class." << std::endl; std::map< Node, std::vector< Node > >::iterator it_eqc = d_curr_eqc.find( pvr ); if( it_eqc!=d_curr_eqc.end() ){ + //std::vector< Node > eq_candidates; Trace("cbqi-inst-debug2") << "...eqc has size " << it_eqc->second.size() << std::endl; for( unsigned k=0; k<it_eqc->second.size(); k++ ){ Node n = it_eqc->second[k]; if( n!=pv ){ Trace("cbqi-inst-debug") << "...try based on equal term " << n << std::endl; - //compute d_subs_fv, which program variables are contained in n - computeProgVars( n ); //must be an eligible term - if( d_inelig.find( n )==d_inelig.end() ){ + if( isEligible( n ) ){ Node ns; Node pv_coeff; //coefficient of pv in the equality we solve (null is 1) bool proc = false; if( !d_prog_var[n].empty() ){ - ns = applySubstitution( pvtn, n, sf, vars, pv_coeff, false ); + ns = applySubstitution( pvtn, n, sf, pv_coeff, false ); if( !ns.isNull() ){ computeProgVars( ns ); //substituted version must be new and cannot contain pv - proc = subs_proc[pv_coeff].find( ns )==subs_proc[pv_coeff].end() && d_prog_var[ns].find( pv )==d_prog_var[ns].end(); + proc = d_prog_var[ns].find( pv )==d_prog_var[ns].end(); } }else{ ns = n; proc = true; } if( proc ){ - //try the substitution - subs_proc[ns][pv_coeff] = true; - if( doAddInstantiationInc( ns, pv, pv_coeff, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + if( vinst->processEqualTerm( this, sf, pv, pv_coeff, ns, effort ) ){ return true; } } } } } - if( pvtn.isDatatype() ){ - Trace("cbqi-inst-debug") << "[2] try based on constructors in equivalence class." << std::endl; - //[2] look in equivalence class for a constructor - for( unsigned k=0; k<it_eqc->second.size(); k++ ){ - Node n = it_eqc->second[k]; - if( n.getKind()==APPLY_CONSTRUCTOR ){ - Trace("cbqi-inst-debug") << "... " << i << "...try based on constructor term " << n << std::endl; - cons[pv] = n.getOperator(); - const Datatype& dt = ((DatatypeType)(pvtn).toType()).getDatatype(); - unsigned cindex = Datatype::indexOf( n.getOperator().toExpr() ); - if( is_cv ){ - curr_var.pop_back(); - } - //now must solve for selectors applied to pv - for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){ - curr_var.push_back( NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][j].getSelector() ), pv ) ); - } - if( doAddInstantiation( sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ - return true; - }else{ - //cleanup - cons.erase( pv ); - Assert( curr_var.size()>=dt[cindex].getNumArgs() ); - for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){ - curr_var.pop_back(); - } - if( is_cv ){ - curr_var.push_back( pv ); - } - break; - } - } - } + if( vinst->processEqualTerms( this, sf, pv, it_eqc->second, effort ) ){ + return true; } }else{ Trace("cbqi-inst-debug2") << "...eqc not found." << std::endl; @@ -189,762 +222,246 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std:: //[3] : we can solve an equality for pv ///iterate over equivalence classes to find cases where we can solve for the variable - Trace("cbqi-inst-debug") << "[3] try based on solving equalities." << std::endl; - for( unsigned k=0; k<d_curr_type_eqc[pvtnb].size(); k++ ){ - Node r = d_curr_type_eqc[pvtnb][k]; - std::map< Node, std::vector< Node > >::iterator it_reqc = d_curr_eqc.find( r ); - std::vector< Node > lhs; - std::vector< bool > lhs_v; - std::vector< Node > lhs_coeff; - Assert( it_reqc!=d_curr_eqc.end() ); - for( unsigned kk=0; kk<it_reqc->second.size(); kk++ ){ - Node n = it_reqc->second[kk]; - Trace("cbqi-inst-debug2") << "...look at term " << n << std::endl; - //compute the variables in n - computeProgVars( n ); - //must be an eligible term - if( d_inelig.find( n )==d_inelig.end() ){ - Node ns; - Node pv_coeff; - if( !d_prog_var[n].empty() ){ - ns = applySubstitution( pvtn, n, sf, vars, pv_coeff ); - if( !ns.isNull() ){ - computeProgVars( ns ); + if( vinst->hasProcessEquality( this, sf, pv, effort ) ){ + Trace("cbqi-inst-debug") << "[3] try based on solving equalities." << std::endl; + for( unsigned k=0; k<d_curr_type_eqc[pvtnb].size(); k++ ){ + Node r = d_curr_type_eqc[pvtnb][k]; + std::map< Node, std::vector< Node > >::iterator it_reqc = d_curr_eqc.find( r ); + std::vector< Node > lhs; + std::vector< bool > lhs_v; + std::vector< Node > lhs_coeff; + Assert( it_reqc!=d_curr_eqc.end() ); + for( unsigned kk=0; kk<it_reqc->second.size(); kk++ ){ + Node n = it_reqc->second[kk]; + Trace("cbqi-inst-debug2") << "...look at term " << n << std::endl; + //must be an eligible term + if( isEligible( n ) ){ + Node ns; + Node pv_coeff; + if( !d_prog_var[n].empty() ){ + ns = applySubstitution( pvtn, n, sf, pv_coeff ); + if( !ns.isNull() ){ + computeProgVars( ns ); + } + }else{ + ns = n; } - }else{ - ns = n; - } - if( !ns.isNull() ){ - bool hasVar = d_prog_var[ns].find( pv )!=d_prog_var[ns].end(); - Trace("cbqi-inst-debug2") << "... " << ns << " has var " << pv << " : " << hasVar << std::endl; - for( unsigned j=0; j<lhs.size(); j++ ){ - //if this term or the another has pv in it, try to solve for it - if( hasVar || lhs_v[j] ){ - Trace("cbqi-inst-debug") << "... " << i << "...try based on equality " << lhs[j] << " = " << ns << std::endl; - Node val; - Node veq_c; - bool success = false; - if( pvtnb.isReal() ){ - Node eq_lhs = lhs[j]; - Node eq_rhs = ns; - //make the same coefficient - if( pv_coeff!=lhs_coeff[j] ){ - if( !pv_coeff.isNull() ){ - Trace("cbqi-inst-debug") << "...mult lhs by " << pv_coeff << std::endl; - eq_lhs = NodeManager::currentNM()->mkNode( MULT, pv_coeff, eq_lhs ); - eq_lhs = Rewriter::rewrite( eq_lhs ); - } - if( !lhs_coeff[j].isNull() ){ - Trace("cbqi-inst-debug") << "...mult rhs by " << lhs_coeff[j] << std::endl; - eq_rhs = NodeManager::currentNM()->mkNode( MULT, lhs_coeff[j], eq_rhs ); - eq_rhs = Rewriter::rewrite( eq_rhs ); - } - } - Node eq = eq_lhs.eqNode( eq_rhs ); - eq = Rewriter::rewrite( eq ); - Node vts_coeff_inf; - Node vts_coeff_delta; - //isolate pv in the equality - int ires = solve_arith( pv, eq, veq_c, val, vts_coeff_inf, vts_coeff_delta ); - if( ires!=0 ){ - success = true; - } - /* - //cannot contain infinity? - //if( !d_qe->getTermDatabase()->containsVtsInfinity( eq ) ){ - Trace("cbqi-inst-debug") << "...equality is " << eq << std::endl; - std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( eq, msum ) ){ - if( Trace.isOn("cbqi-inst-debug") ){ - Trace("cbqi-inst-debug") << "...got monomial sum: " << std::endl; - QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" ); - Trace("cbqi-inst-debug") << "isolate for " << pv << " : " << pv.getType() << "..." << std::endl; - } - Node veq; - if( QuantArith::isolate( pv, msum, veq, EQUAL, true )!=0 ){ - Trace("cbqi-inst-debug") << "...isolated equality " << veq << "." << std::endl; - Node veq_c; - if( veq[0]!=pv ){ - Node veq_v; - if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){ - Assert( veq_v==pv ); - } - } - Node val = veq[1]; - if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){ - subs_proc[val][veq_c] = true; - if( doAddInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ - return true; - } - } - } - } - */ - }else if( pvtnb.isDatatype() ){ - val = solve_dt( pv, lhs[j], ns, lhs[j], ns ); - if( !val.isNull() ){ - success = true; - } - } - if( success ){ - if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){ - subs_proc[val][veq_c] = true; - if( doAddInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ - return true; - } + if( !ns.isNull() ){ + bool hasVar = d_prog_var[ns].find( pv )!=d_prog_var[ns].end(); + Trace("cbqi-inst-debug2") << "... " << ns << " has var " << pv << " : " << hasVar << std::endl; + std::vector< Node > term_coeffs; + std::vector< Node > terms; + term_coeffs.push_back( pv_coeff ); + terms.push_back( ns ); + for( unsigned j=0; j<lhs.size(); j++ ){ + //if this term or the another has pv in it, try to solve for it + if( hasVar || lhs_v[j] ){ + Trace("cbqi-inst-debug") << "... " << i << "...try based on equality " << lhs[j] << " = " << ns << std::endl; + //processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) { return false; } + term_coeffs.push_back( lhs_coeff[j] ); + terms.push_back( lhs[j] ); + if( vinst->processEquality( this, sf, pv, term_coeffs, terms, effort ) ){ + return true; } + term_coeffs.pop_back(); + terms.pop_back(); } } + lhs.push_back( ns ); + lhs_v.push_back( hasVar ); + lhs_coeff.push_back( pv_coeff ); + }else{ + Trace("cbqi-inst-debug2") << "... term " << n << " is ineligible after substitution." << std::endl; } - lhs.push_back( ns ); - lhs_v.push_back( hasVar ); - lhs_coeff.push_back( pv_coeff ); }else{ - Trace("cbqi-inst-debug2") << "... term " << n << " is ineligible after substitution." << std::endl; + Trace("cbqi-inst-debug2") << "... term " << n << " is ineligible." << std::endl; } - }else{ - Trace("cbqi-inst-debug2") << "... term " << n << " is ineligible." << std::endl; } } } //[4] directly look at assertions - Trace("cbqi-inst-debug") << "[4] try based on assertions." << std::endl; - d_vts_sym[0] = d_qe->getTermDatabase()->getVtsInfinity( pvtn, false, false ); - d_vts_sym[1] = d_qe->getTermDatabase()->getVtsDelta( false, false ); - std::vector< Node > mbp_bounds[2]; - std::vector< Node > mbp_coeff[2]; - std::vector< Node > mbp_vts_coeff[2][2]; - std::vector< Node > mbp_lit[2]; - //std::vector< MbpBounds > mbp_bounds[2]; - //unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2; - for( unsigned r=0; r<2; r++ ){ - TheoryId tid = r==0 ? Theory::theoryOf( pvtn ) : THEORY_UF; - Trace("cbqi-inst-debug2") << " look at assertions of " << tid << std::endl; - std::map< TheoryId, std::vector< Node > >::iterator ita = d_curr_asserts.find( tid ); - if( ita!=d_curr_asserts.end() ){ - for (unsigned j = 0; j<ita->second.size(); j++) { - Node lit = ita->second[j]; - Trace("cbqi-inst-debug2") << " look at " << lit << std::endl; - Node atom = lit.getKind()==NOT ? lit[0] : lit; - bool pol = lit.getKind()!=NOT; - if( pvtn.isReal() ){ - //arithmetic inequalities and disequalities - if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && atom[0].getType().isReal() ) ){ - Assert( atom.getKind()!=GEQ || atom[1].isConst() ); - Node atom_lhs; - Node atom_rhs; - if( atom.getKind()==GEQ ){ - atom_lhs = atom[0]; - atom_rhs = atom[1]; - }else{ - atom_lhs = NodeManager::currentNM()->mkNode( MINUS, atom[0], atom[1] ); - atom_lhs = Rewriter::rewrite( atom_lhs ); - atom_rhs = d_zero; - } - - computeProgVars( atom_lhs ); - //must be an eligible term - if( d_inelig.find( atom_lhs )==d_inelig.end() ){ - //apply substitution to LHS of atom - if( !d_prog_var[atom_lhs].empty() ){ - Node atom_lhs_coeff; - atom_lhs = applySubstitution( pvtn, atom_lhs, sf, vars, atom_lhs_coeff ); - if( !atom_lhs.isNull() ){ - computeProgVars( atom_lhs ); - if( !atom_lhs_coeff.isNull() ){ - atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_coeff, atom_rhs ) ); - } - } - } - //if it contains pv, not infinity - if( !atom_lhs.isNull() && d_prog_var[atom_lhs].find( pv )!=d_prog_var[atom_lhs].end() ){ - Node satom = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs ); - //cannot contain infinity? - //if( !d_qe->getTermDatabase()->containsVtsInfinity( atom_lhs ) ){ - Trace("cbqi-inst-debug") << "..[3] From assertion : " << atom << ", pol = " << pol << std::endl; - Trace("cbqi-inst-debug") << " substituted : " << satom << ", pol = " << pol << std::endl; - Node vts_coeff_inf; - Node vts_coeff_delta; - Node val; - Node veq_c; - //isolate pv in the inequality - int ires = solve_arith( pv, satom, veq_c, val, vts_coeff_inf, vts_coeff_delta ); - if( ires!=0 ){ - //disequalities are either strict upper or lower bounds - unsigned rmax = ( atom.getKind()==GEQ && options::cbqiModel() ) ? 1 : 2; - for( unsigned r=0; r<rmax; r++ ){ - int uires = ires; - Node uval = val; - if( atom.getKind()==GEQ ){ - //push negation downwards - if( !pol ){ - uires = -ires; - if( pvtn.isInteger() ){ - uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); - uval = Rewriter::rewrite( uval ); - }else{ - Assert( pvtn.isReal() ); - //now is strict inequality - uires = uires*2; - } - } - }else{ - bool is_upper = ( r==0 ); - if( options::cbqiModel() ){ - // disequality is a disjunction : only consider the bound in the direction of the model - //first check if there is an infinity... - if( !vts_coeff_inf.isNull() ){ - //coefficient or val won't make a difference, just compare with zero - Trace("cbqi-inst-debug") << "Disequality : check infinity polarity " << vts_coeff_inf << std::endl; - Assert( vts_coeff_inf.isConst() ); - is_upper = ( vts_coeff_inf.getConst<Rational>().sgn()==1 ); - }else{ - Node rhs_value = getModelValue( val ); - Node lhs_value = pv_value; - if( !veq_c.isNull() ){ - lhs_value = NodeManager::currentNM()->mkNode( MULT, lhs_value, veq_c ); - lhs_value = Rewriter::rewrite( lhs_value ); - } - Trace("cbqi-inst-debug") << "Disequality : check model values " << lhs_value << " " << rhs_value << std::endl; - Assert( lhs_value!=rhs_value ); - Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value ); - cmp = Rewriter::rewrite( cmp ); - Assert( cmp.isConst() ); - is_upper = ( cmp!=d_true ); - } - } - Assert( atom.getKind()==EQUAL && !pol ); - if( pvtn.isInteger() ){ - uires = is_upper ? -1 : 1; - uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); - uval = Rewriter::rewrite( uval ); - }else{ - Assert( pvtn.isReal() ); - uires = is_upper ? -2 : 2; - } - } - Trace("cbqi-bound-inf") << "From " << lit << ", got : "; - if( !veq_c.isNull() ){ - Trace("cbqi-bound-inf") << veq_c << " * "; - } - Trace("cbqi-bound-inf") << pv << " -> " << uval << ", styp = " << uires << std::endl; - //take into account delta - if( d_use_vts_delta && ( uires==2 || uires==-2 ) ){ - if( options::cbqiModel() ){ - Node delta_coeff = NodeManager::currentNM()->mkConst( Rational( uires > 0 ? 1 : -1 ) ); - if( vts_coeff_delta.isNull() ){ - vts_coeff_delta = delta_coeff; - }else{ - vts_coeff_delta = NodeManager::currentNM()->mkNode( PLUS, vts_coeff_delta, delta_coeff ); - vts_coeff_delta = Rewriter::rewrite( vts_coeff_delta ); - } - }else{ - Node delta = d_qe->getTermDatabase()->getVtsDelta(); - uval = NodeManager::currentNM()->mkNode( uires==2 ? PLUS : MINUS, uval, delta ); - uval = Rewriter::rewrite( uval ); - } - } - if( options::cbqiModel() ){ - //just store bounds, will choose based on tighest bound - unsigned index = uires>0 ? 0 : 1; - mbp_bounds[index].push_back( uval ); - mbp_coeff[index].push_back( veq_c ); - for( unsigned t=0; t<2; t++ ){ - mbp_vts_coeff[index][t].push_back( t==0 ? vts_coeff_inf : vts_coeff_delta ); - } - mbp_lit[index].push_back( lit ); - }else{ - //try this bound - if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){ - subs_proc[uval][veq_c] = true; - if( doAddInstantiationInc( uval, pv, veq_c, uires>0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ - return true; - } - } - } - } - } - } - } - } - } - /* TODO: algebraic reasoning for bitvector instantiation - else if( pvtn.isBitVector() ){ - if( atom.getKind()==BITVECTOR_ULT || atom.getKind()==BITVECTOR_ULE ){ - for( unsigned t=0; t<2; t++ ){ - if( atom[t]==pv ){ - computeProgVars( atom[1-t] ); - if( d_inelig.find( atom[1-t] )==d_inelig.end() ){ - //only ground terms TODO: more - if( d_prog_var[atom[1-t]].empty() ){ - Node veq_c; - Node uval; - if( ( !pol && atom.getKind()==BITVECTOR_ULT ) || ( pol && atom.getKind()==BITVECTOR_ULE ) ){ - uval = atom[1-t]; - }else{ - uval = NodeManager::currentNM()->mkNode( (atom.getKind()==BITVECTOR_ULT)==(t==1) ? BITVECTOR_PLUS : BITVECTOR_SUB, atom[1-t], - bv::utils::mkConst(pvtn.getConst<BitVectorSize>(), 1) ); - } - if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){ - subs_proc[uval][veq_c] = true; - if( doAddInstantiationInc( uval, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ - return true; - } - } - } - } - } - } - } - } - */ - } - } - } - if( options::cbqiModel() ){ - if( pvtn.isInteger() || pvtn.isReal() ){ - bool use_inf = d_use_vts_inf && ( pvtn.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal() ) && !options::cbqiMidpoint(); - bool upper_first = false; - if( options::cbqiMinBounds() ){ - upper_first = mbp_bounds[1].size()<mbp_bounds[0].size(); - } - int best_used[2]; - std::vector< Node > t_values[3]; - //try optimal bounds - for( unsigned r=0; r<2; r++ ){ - int rr = upper_first ? (1-r) : r; - best_used[rr] = -1; - if( mbp_bounds[rr].empty() ){ - if( use_inf ){ - Trace("cbqi-bound") << "No " << ( rr==0 ? "lower" : "upper" ) << " bounds for " << pv << " (type=" << pvtn << ")" << std::endl; - //no bounds, we do +- infinity - Node val = d_qe->getTermDatabase()->getVtsInfinity( pvtn ); - //TODO : rho value for infinity? - if( rr==0 ){ - val = NodeManager::currentNM()->mkNode( UMINUS, val ); - val = Rewriter::rewrite( val ); - } - if( doAddInstantiationInc( val, pv, Node::null(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ - return true; - } - } - }else{ - Trace("cbqi-bound") << ( rr==0 ? "Lower" : "Upper" ) << " bounds for " << pv << " (type=" << pvtn << ") : " << std::endl; - int best = -1; - Node best_bound_value[3]; - for( unsigned j=0; j<mbp_bounds[rr].size(); j++ ){ - Node value[3]; - if( Trace.isOn("cbqi-bound") ){ - Assert( !mbp_bounds[rr][j].isNull() ); - Trace("cbqi-bound") << " " << j << ": " << mbp_bounds[rr][j]; - if( !mbp_vts_coeff[rr][0][j].isNull() ){ - Trace("cbqi-bound") << " (+ " << mbp_vts_coeff[rr][0][j] << " * INF)"; - } - if( !mbp_vts_coeff[rr][1][j].isNull() ){ - Trace("cbqi-bound") << " (+ " << mbp_vts_coeff[rr][1][j] << " * DELTA)"; - } - if( !mbp_coeff[rr][j].isNull() ){ - Trace("cbqi-bound") << " (div " << mbp_coeff[rr][j] << ")"; - } - Trace("cbqi-bound") << ", value = "; - } - t_values[rr].push_back( Node::null() ); - //check if it is better than the current best bound : lexicographic order infinite/finite/infinitesimal parts - bool new_best = true; - for( unsigned t=0; t<3; t++ ){ - //get the value - if( t==0 ){ - value[0] = mbp_vts_coeff[rr][0][j]; - if( !value[0].isNull() ){ - Trace("cbqi-bound") << "( " << value[0] << " * INF ) + "; - }else{ - value[0] = d_zero; - } - }else if( t==1 ){ - Node t_value = getModelValue( mbp_bounds[rr][j] ); - t_values[rr][j] = t_value; - value[1] = t_value; - Trace("cbqi-bound") << value[1]; - }else{ - value[2] = mbp_vts_coeff[rr][1][j]; - if( !value[2].isNull() ){ - Trace("cbqi-bound") << " + ( " << value[2] << " * DELTA )"; - }else{ - value[2] = d_zero; - } - } - //multiply by coefficient - if( value[t]!=d_zero && !mbp_coeff[rr][j].isNull() ){ - Assert( mbp_coeff[rr][j].isConst() ); - value[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(1) / mbp_coeff[rr][j].getConst<Rational>() ), value[t] ); - value[t] = Rewriter::rewrite( value[t] ); - } - //check if new best - if( best!=-1 ){ - Assert( !value[t].isNull() && !best_bound_value[t].isNull() ); - if( value[t]!=best_bound_value[t] ){ - Kind k = rr==0 ? GEQ : LEQ; - Node cmp_bound = NodeManager::currentNM()->mkNode( k, value[t], best_bound_value[t] ); - cmp_bound = Rewriter::rewrite( cmp_bound ); - if( cmp_bound!=d_true ){ - new_best = false; - break; - } - } - } - } - Trace("cbqi-bound") << std::endl; - if( new_best ){ - for( unsigned t=0; t<3; t++ ){ - best_bound_value[t] = value[t]; - } - best = j; - } - } - if( best!=-1 ){ - Trace("cbqi-bound") << "...best bound is " << best << " : "; - if( best_bound_value[0]!=d_zero ){ - Trace("cbqi-bound") << "( " << best_bound_value[0] << " * INF ) + "; - } - Trace("cbqi-bound") << best_bound_value[1]; - if( best_bound_value[2]!=d_zero ){ - Trace("cbqi-bound") << " + ( " << best_bound_value[2] << " * DELTA )"; - } - Trace("cbqi-bound") << std::endl; - best_used[rr] = best; - //if using cbqiMidpoint, only add the instance based on one bound if the bound is non-strict - if( !options::cbqiMidpoint() || pvtn.isInteger() || mbp_vts_coeff[rr][1][best].isNull() ){ - Node val = mbp_bounds[rr][best]; - val = getModelBasedProjectionValue( pv, val, rr==0, mbp_coeff[rr][best], pv_value, t_values[rr][best], theta, - mbp_vts_coeff[rr][0][best], mbp_vts_coeff[rr][1][best] ); - if( !val.isNull() ){ - if( subs_proc[val].find( mbp_coeff[rr][best] )==subs_proc[val].end() ){ - subs_proc[val][mbp_coeff[rr][best]] = true; - if( doAddInstantiationInc( val, pv, mbp_coeff[rr][best], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ - return true; - } - } - } - } - } - } - } - //if not using infinity, use model value of zero - if( !use_inf && mbp_bounds[0].empty() && mbp_bounds[1].empty() ){ - Node val = d_zero; - Node c; //null (one) coefficient - val = getModelBasedProjectionValue( pv, val, true, c, pv_value, d_zero, theta, Node::null(), Node::null() ); - if( !val.isNull() ){ - if( subs_proc[val].find( c )==subs_proc[val].end() ){ - subs_proc[val][c] = true; - if( doAddInstantiationInc( val, pv, c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ - return true; - } - } - } - } - if( options::cbqiMidpoint() && !pvtn.isInteger() ){ - Node vals[2]; - bool bothBounds = true; - Trace("cbqi-bound") << "Try midpoint of bounds..." << std::endl; - for( unsigned rr=0; rr<2; rr++ ){ - int best = best_used[rr]; - if( best==-1 ){ - bothBounds = false; - }else{ - vals[rr] = mbp_bounds[rr][best]; - vals[rr] = getModelBasedProjectionValue( pv, vals[rr], rr==0, Node::null(), pv_value, t_values[rr][best], theta, - mbp_vts_coeff[rr][0][best], Node::null() ); - } - Trace("cbqi-bound") << "Bound : " << vals[rr] << std::endl; - } - Node val; - if( bothBounds ){ - Assert( !vals[0].isNull() && !vals[1].isNull() ); - if( vals[0]==vals[1] ){ - val = vals[0]; - }else{ - val = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkNode( PLUS, vals[0], vals[1] ), - NodeManager::currentNM()->mkConst( Rational(1)/Rational(2) ) ); - val = Rewriter::rewrite( val ); - } - }else{ - if( !vals[0].isNull() ){ - val = NodeManager::currentNM()->mkNode( PLUS, vals[0], d_one ); - val = Rewriter::rewrite( val ); - }else if( !vals[1].isNull() ){ - val = NodeManager::currentNM()->mkNode( MINUS, vals[1], d_one ); - val = Rewriter::rewrite( val ); - } - } - Trace("cbqi-bound") << "Midpoint value : " << val << std::endl; - if( !val.isNull() ){ - if( subs_proc[val].find( Node::null() )==subs_proc[val].end() ){ - subs_proc[val][Node::null()] = true; - if( doAddInstantiationInc( val, pv, Node::null(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + if( vinst->hasProcessAssertion( this, sf, pv, effort ) ){ + Trace("cbqi-inst-debug") << "[4] try based on assertions." << std::endl; + std::vector< Node > lits; + //unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2; + for( unsigned r=0; r<2; r++ ){ + TheoryId tid = r==0 ? Theory::theoryOf( pvtn ) : THEORY_UF; + Trace("cbqi-inst-debug2") << " look at assertions of " << tid << std::endl; + std::map< TheoryId, std::vector< Node > >::iterator ita = d_curr_asserts.find( tid ); + if( ita!=d_curr_asserts.end() ){ + for (unsigned j = 0; j<ita->second.size(); j++) { + Node lit = ita->second[j]; + if( std::find( lits.begin(), lits.end(), lit )==lits.end() ){ + lits.push_back( lit ); + if( vinst->processAssertion( this, sf, pv, lit, effort ) ){ return true; } } } } -#ifdef MBP_STRICT_ASSERTIONS - Assert( false ); -#endif - if( options::cbqiNopt() ){ - //try non-optimal bounds (heuristic, may help when nested quantification) ? - Trace("cbqi-bound") << "Try non-optimal bounds..." << std::endl; - for( unsigned r=0; r<2; r++ ){ - int rr = upper_first ? (1-r) : r; - for( unsigned j=0; j<mbp_bounds[rr].size(); j++ ){ - if( (int)j!=best_used[rr] && ( !options::cbqiMidpoint() || mbp_vts_coeff[rr][1][j].isNull() ) ){ - Node val = getModelBasedProjectionValue( pv, mbp_bounds[rr][j], rr==0, mbp_coeff[rr][j], pv_value, t_values[rr][j], theta, - mbp_vts_coeff[rr][0][j], mbp_vts_coeff[rr][1][j] ); - if( !val.isNull() ){ - if( subs_proc[val].find( mbp_coeff[rr][j] )==subs_proc[val].end() ){ - subs_proc[val][mbp_coeff[rr][j]] = true; - if( doAddInstantiationInc( val, pv, mbp_coeff[rr][j], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ - return true; - } - } - } - } - } - } - } + } + if( vinst->processAssertions( this, sf, pv, lits, effort ) ){ + return true; } } } //[5] resort to using value in model // do so if we are in effort=1, or if the variable is boolean, or if we are solving for a subfield of a datatype - if( ( effort>0 || pvtn.isBoolean() || pvtn.isBitVector() || !curr_var.empty() ) && d_qe->getTermDatabase()->isClosedEnumerableType( pvtn ) ){ + bool use_model_value = vinst->useModelValue( this, sf, pv, effort ); + if( ( effort>0 || use_model_value || is_cv ) && vinst->allowModelValue( this, sf, pv, effort ) ){ +#ifdef CVC4_ASSERTIONS + if( pvtn.isReal() && options::cbqiNestedQE() && !options::cbqiAll() ){ + Trace("cbqi-warn") << "Had to resort to model value." << std::endl; + Assert( false ); + } +#endif Node mv = getModelValue( pv ); Node pv_coeff_m; Trace("cbqi-inst-debug") << "[5] " << i << "...try model value " << mv << std::endl; - int new_effort = pvtn.isBoolean() ? effort : 1; -#ifdef MBP_STRICT_ASSERTIONS - //we only resort to values in the case of booleans - Assert( ( pvtn.isInteger() ? !options::cbqiUseInfInt() : !options::cbqiUseInfReal() ) || pvtn.isBoolean() ); -#endif - if( doAddInstantiationInc( mv, pv, pv_coeff_m, 0, sf, ssf, vars, btyp, theta, i, new_effort, cons, curr_var ) ){ + int new_effort = use_model_value ? effort : 1; + if( doAddInstantiationInc( pv, mv, pv_coeff_m, 0, sf, new_effort ) ){ return true; } } Trace("cbqi-inst-debug") << "[No instantiation found for " << pv << "]" << std::endl; + if( is_cv ){ + d_stack_vars.push_back( pv ); + } + d_active_instantiators.erase( pv ); + unregisterInstantiationVariable( pv ); return false; } } +void CegInstantiator::pushStackVariable( Node v ) { + d_stack_vars.push_back( v ); +} -bool CegInstantiator::doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, - std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, - std::map< Node, Node >& cons, std::vector< Node >& curr_var ) { - if( Trace.isOn("cbqi-inst") ){ - for( unsigned j=0; j<sf.d_subs.size(); j++ ){ - Trace("cbqi-inst") << " "; - } - Trace("cbqi-inst") << sf.d_subs.size() << ": "; - if( !pv_coeff.isNull() ){ - Trace("cbqi-inst") << pv_coeff << " * "; - } - Trace("cbqi-inst") << pv << " -> " << n << std::endl; - Assert( n.getType().isSubtypeOf( pv.getType() ) ); - } - //must ensure variables have been computed for n - computeProgVars( n ); - Assert( d_inelig.find( n )==d_inelig.end() ); +void CegInstantiator::popStackVariable() { + Assert( !d_stack_vars.empty() ); + d_stack_vars.pop_back(); +} - //substitute into previous substitutions, when applicable - std::vector< Node > a_subs; - a_subs.push_back( n ); - std::vector< Node > a_var; - a_var.push_back( pv ); - std::vector< Node > a_coeff; - std::vector< Node > a_has_coeff; - if( !pv_coeff.isNull() ){ - a_coeff.push_back( pv_coeff ); - a_has_coeff.push_back( pv ); - } - bool success = true; - std::map< int, Node > prev_subs; - std::map< int, Node > prev_coeff; - std::map< int, Node > prev_sym_subs; - std::vector< Node > new_has_coeff; - Trace("cbqi-inst-debug2") << "Applying substitutions..." << std::endl; - for( unsigned j=0; j<sf.d_subs.size(); j++ ){ - Trace("cbqi-inst-debug2") << " Apply for " << sf.d_subs[j] << std::endl; - Assert( d_prog_var.find( sf.d_subs[j] )!=d_prog_var.end() ); - if( d_prog_var[sf.d_subs[j]].find( pv )!=d_prog_var[sf.d_subs[j]].end() ){ - prev_subs[j] = sf.d_subs[j]; - TNode tv = pv; - TNode ts = n; - Node a_pv_coeff; - Node new_subs = applySubstitution( vars[j].getType(), sf.d_subs[j], a_subs, a_coeff, a_has_coeff, a_var, a_pv_coeff, true ); - if( !new_subs.isNull() ){ - sf.d_subs[j] = new_subs; - if( !a_pv_coeff.isNull() ){ - prev_coeff[j] = sf.d_coeff[j]; - if( sf.d_coeff[j].isNull() ){ - Assert( std::find( sf.d_has_coeff.begin(), sf.d_has_coeff.end(), vars[j] )==sf.d_has_coeff.end() ); - //now has coefficient - new_has_coeff.push_back( vars[j] ); - sf.d_has_coeff.push_back( vars[j] ); - sf.d_coeff[j] = a_pv_coeff; - }else{ - sf.d_coeff[j] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[j], a_pv_coeff ) ); +bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, Node pv_coeff, int bt, SolvedForm& sf, unsigned effort ) { + if( d_curr_subs_proc[pv][n].find( pv_coeff )==d_curr_subs_proc[pv][n].end() ){ + d_curr_subs_proc[pv][n][pv_coeff] = true; + if( Trace.isOn("cbqi-inst") ){ + for( unsigned j=0; j<sf.d_subs.size(); j++ ){ + Trace("cbqi-inst") << " "; + } + Trace("cbqi-inst") << sf.d_subs.size() << ": "; + if( !pv_coeff.isNull() ){ + Trace("cbqi-inst") << pv_coeff << " * "; + } + Trace("cbqi-inst") << pv << " -> " << n << std::endl; + Assert( n.getType().isSubtypeOf( pv.getType() ) ); + } + //must ensure variables have been computed for n + computeProgVars( n ); + Assert( d_inelig.find( n )==d_inelig.end() ); + + //substitute into previous substitutions, when applicable + std::vector< Node > a_subs; + a_subs.push_back( n ); + std::vector< Node > a_var; + a_var.push_back( pv ); + std::vector< Node > a_coeff; + std::vector< Node > a_has_coeff; + if( !pv_coeff.isNull() ){ + a_coeff.push_back( pv_coeff ); + a_has_coeff.push_back( pv ); + } + bool success = true; + std::map< int, Node > prev_subs; + std::map< int, Node > prev_coeff; + std::map< int, Node > prev_sym_subs; + std::vector< Node > new_has_coeff; + Trace("cbqi-inst-debug2") << "Applying substitutions..." << std::endl; + for( unsigned j=0; j<sf.d_subs.size(); j++ ){ + Trace("cbqi-inst-debug2") << " Apply for " << sf.d_subs[j] << std::endl; + Assert( d_prog_var.find( sf.d_subs[j] )!=d_prog_var.end() ); + if( d_prog_var[sf.d_subs[j]].find( pv )!=d_prog_var[sf.d_subs[j]].end() ){ + prev_subs[j] = sf.d_subs[j]; + TNode tv = pv; + TNode ts = n; + Node a_pv_coeff; + Node new_subs = applySubstitution( sf.d_vars[j].getType(), sf.d_subs[j], a_subs, a_coeff, a_has_coeff, a_var, a_pv_coeff, true ); + if( !new_subs.isNull() ){ + sf.d_subs[j] = new_subs; + if( !a_pv_coeff.isNull() ){ + prev_coeff[j] = sf.d_coeff[j]; + if( sf.d_coeff[j].isNull() ){ + Assert( std::find( sf.d_has_coeff.begin(), sf.d_has_coeff.end(), sf.d_vars[j] )==sf.d_has_coeff.end() ); + //now has coefficient + new_has_coeff.push_back( sf.d_vars[j] ); + sf.d_has_coeff.push_back( sf.d_vars[j] ); + sf.d_coeff[j] = a_pv_coeff; + }else{ + sf.d_coeff[j] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[j], a_pv_coeff ) ); + } } + if( sf.d_subs[j]!=prev_subs[j] ){ + computeProgVars( sf.d_subs[j] ); + Assert( d_inelig.find( sf.d_subs[j] )==d_inelig.end() ); + } + Trace("cbqi-inst-debug2") << "Subs " << j << " " << sf.d_subs[j] << std::endl; + }else{ + Trace("cbqi-inst-debug2") << "...failed to apply substitution to " << sf.d_subs[j] << std::endl; + success = false; + break; } - if( sf.d_subs[j]!=prev_subs[j] ){ - computeProgVars( sf.d_subs[j] ); - Assert( d_inelig.find( sf.d_subs[j] )==d_inelig.end() ); - } - Trace("cbqi-inst-debug2") << "Subs " << j << " " << sf.d_subs[j] << std::endl; }else{ - Trace("cbqi-inst-debug2") << "...failed to apply substitution to " << sf.d_subs[j] << std::endl; - success = false; - break; + Trace("cbqi-inst-debug2") << "Skip " << j << " " << sf.d_subs[j] << std::endl; } - }else{ - Trace("cbqi-inst-debug2") << "Skip " << j << " " << sf.d_subs[j] << std::endl; - } - if( options::cbqiSymLia() && pv_coeff.isNull() ){ - //apply simple substitutions also to sym_subs - prev_sym_subs[j] = ssf.d_subs[j]; - ssf.d_subs[j] = ssf.d_subs[j].substitute( a_var.begin(), a_var.end(), a_subs.begin(), a_subs.end() ); - ssf.d_subs[j] = Rewriter::rewrite( ssf.d_subs[j] ); } - } - if( success ){ - Trace("cbqi-inst-debug2") << "Adding to vectors..." << std::endl; - vars.push_back( pv ); - btyp.push_back( bt ); - sf.push_back( pv, n, pv_coeff ); - ssf.push_back( pv, n, pv_coeff ); - Node new_theta = theta; - if( !pv_coeff.isNull() ){ - if( new_theta.isNull() ){ - new_theta = pv_coeff; - }else{ - new_theta = NodeManager::currentNM()->mkNode( MULT, new_theta, pv_coeff ); - new_theta = Rewriter::rewrite( new_theta ); + if( success ){ + Trace("cbqi-inst-debug2") << "Adding to vectors..." << std::endl; + sf.push_back( pv, n, pv_coeff, bt ); + Node prev_theta = sf.d_theta; + Node new_theta = sf.d_theta; + if( !pv_coeff.isNull() ){ + if( new_theta.isNull() ){ + new_theta = pv_coeff; + }else{ + new_theta = NodeManager::currentNM()->mkNode( MULT, new_theta, pv_coeff ); + new_theta = Rewriter::rewrite( new_theta ); + } } - } - bool is_cv = false; - if( !curr_var.empty() ){ - Assert( curr_var.back()==pv ); - curr_var.pop_back(); - is_cv = true; - } - Trace("cbqi-inst-debug2") << "Recurse..." << std::endl; - success = doAddInstantiation( sf, ssf, vars, btyp, new_theta, curr_var.empty() ? i+1 : i, effort, cons, curr_var ); - if( !success ){ - Trace("cbqi-inst-debug2") << "Removing from vectors..." << std::endl; - if( is_cv ){ - curr_var.push_back( pv ); + sf.d_theta = new_theta; + Trace("cbqi-inst-debug2") << "Recurse..." << std::endl; + unsigned i = d_curr_index[pv]; + success = doAddInstantiation( sf, d_stack_vars.empty() ? i+1 : i, effort ); + sf.d_theta = prev_theta; + if( !success ){ + Trace("cbqi-inst-debug2") << "Removing from vectors..." << std::endl; + sf.pop_back( pv, n, pv_coeff, bt ); } - sf.pop_back( pv, n, pv_coeff ); - ssf.pop_back( pv, n, pv_coeff ); - vars.pop_back(); - btyp.pop_back(); - } - } - if( success ){ - return true; - }else{ - Trace("cbqi-inst-debug2") << "Revert substitutions..." << std::endl; - //revert substitution information - for( std::map< int, Node >::iterator it = prev_subs.begin(); it != prev_subs.end(); it++ ){ - sf.d_subs[it->first] = it->second; - } - for( std::map< int, Node >::iterator it = prev_coeff.begin(); it != prev_coeff.end(); it++ ){ - sf.d_coeff[it->first] = it->second; - } - for( unsigned i=0; i<new_has_coeff.size(); i++ ){ - sf.d_has_coeff.pop_back(); - } - for( std::map< int, Node >::iterator it = prev_sym_subs.begin(); it != prev_sym_subs.end(); it++ ){ - ssf.d_subs[it->first] = it->second; } - return false; - } -} - -bool CegInstantiator::doAddInstantiationCoeff( SolvedForm& sf, std::vector< Node >& vars, std::vector< int >& btyp, - unsigned j, std::map< Node, Node >& cons ) { - - - if( j==sf.d_has_coeff.size() ){ - return doAddInstantiation( sf.d_subs, vars, cons ); - }else{ - Assert( std::find( vars.begin(), vars.end(), sf.d_has_coeff[j] )!=vars.end() ); - unsigned index = std::find( vars.begin(), vars.end(), sf.d_has_coeff[j] )-vars.begin(); - Node prev = sf.d_subs[index]; - Assert( !sf.d_coeff[index].isNull() ); - Trace("cbqi-inst-debug") << "Normalize substitution for " << sf.d_coeff[index] << " * " << vars[index] << " = " << sf.d_subs[index] << std::endl; - Assert( vars[index].getType().isInteger() ); - //must ensure that divisibility constraints are met - //solve updated rewritten equality for vars[index], if coefficient is one, then we are successful - Node eq_lhs = NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[index], vars[index] ); - Node eq_rhs = sf.d_subs[index]; - Node eq = eq_lhs.eqNode( eq_rhs ); - eq = Rewriter::rewrite( eq ); - Trace("cbqi-inst-debug") << "...equality is " << eq << std::endl; - std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( eq, msum ) ){ - Node veq; - if( QuantArith::isolate( vars[index], msum, veq, EQUAL, true )!=0 ){ - Node veq_c; - if( veq[0]!=vars[index] ){ - Node veq_v; - if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){ - Assert( veq_v==vars[index] ); - } - } - sf.d_subs[index] = veq[1]; - if( !veq_c.isNull() ){ - sf.d_subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION_TOTAL, veq[1], veq_c ); - Trace("cbqi-inst-debug") << "...bound type is : " << btyp[index] << std::endl; - //intger division rounding up if from a lower bound - if( btyp[index]==1 && options::cbqiRoundUpLowerLia() ){ - sf.d_subs[index] = NodeManager::currentNM()->mkNode( PLUS, sf.d_subs[index], - NodeManager::currentNM()->mkNode( ITE, - NodeManager::currentNM()->mkNode( EQUAL, - NodeManager::currentNM()->mkNode( INTS_MODULUS_TOTAL, veq[1], veq_c ), - d_zero ), - d_zero, d_one ) - ); - } - } - Trace("cbqi-inst-debug") << "...normalize integers : " << vars[index] << " -> " << sf.d_subs[index] << std::endl; - if( options::cbqiSymLia() ){ - //must apply substitution to previous subs - std::vector< Node > curr_var; - std::vector< Node > curr_subs; - curr_var.push_back( vars[index] ); - curr_subs.push_back( sf.d_subs[index] ); - for( unsigned k=0; k<index; k++ ){ - Node prevs = sf.d_subs[k]; - sf.d_subs[k] = sf.d_subs[k].substitute( curr_var.begin(), curr_var.end(), curr_subs.begin(), curr_subs.end() ); - if( prevs!=sf.d_subs[k] ){ - Trace("cbqi-inst-debug2") << " rewrite " << vars[k] << " -> " << prevs << " to "; - sf.d_subs[k] = Rewriter::rewrite( sf.d_subs[k] ); - Trace("cbqi-inst-debug2") << sf.d_subs[k] << std::endl; - } - } - } - if( doAddInstantiationCoeff( sf, vars, btyp, j+1, cons ) ){ - return true; - } + if( success ){ + return true; + }else{ + Trace("cbqi-inst-debug2") << "Revert substitutions..." << std::endl; + //revert substitution information + for( std::map< int, Node >::iterator it = prev_subs.begin(); it != prev_subs.end(); it++ ){ + sf.d_subs[it->first] = it->second; + } + for( std::map< int, Node >::iterator it = prev_coeff.begin(); it != prev_coeff.end(); it++ ){ + sf.d_coeff[it->first] = it->second; + } + for( unsigned i=0; i<new_has_coeff.size(); i++ ){ + sf.d_has_coeff.pop_back(); } + return false; } - sf.d_subs[index] = prev; - Trace("cbqi-inst-debug") << "...failed." << std::endl; + }else{ + //already tried this substitution return false; } } -bool CegInstantiator::doAddInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons ) { +bool CegInstantiator::doAddInstantiation( std::vector< Node >& subs, std::vector< Node >& vars ) { if( vars.size()>d_vars.size() ){ Trace("cbqi-inst-debug") << "Reconstructing instantiations...." << std::endl; std::map< Node, Node > subs_map; @@ -953,7 +470,9 @@ bool CegInstantiator::doAddInstantiation( std::vector< Node >& subs, std::vector } subs.clear(); for( unsigned i=0; i<d_vars.size(); i++ ){ - Node n = constructInstantiation( d_vars[i], subs_map, cons ); + std::map< Node, Node >::iterator it = subs_map.find( d_vars[i] ); + Assert( it!=subs_map.end() ); + Node n = it->second; Trace("cbqi-inst-debug") << " " << d_vars[i] << " -> " << n << std::endl; subs.push_back( n ); } @@ -967,32 +486,9 @@ bool CegInstantiator::doAddInstantiation( std::vector< Node >& subs, std::vector } } bool ret = d_out->doAddInstantiation( subs ); -#ifdef MBP_STRICT_ASSERTIONS - Assert( ret ); -#endif return ret; } -Node CegInstantiator::constructInstantiation( Node n, std::map< Node, Node >& subs_map, std::map< Node, Node >& cons ) { - std::map< Node, Node >::iterator it = subs_map.find( n ); - if( it!=subs_map.end() ){ - return it->second; - }else{ - it = cons.find( n ); - Assert( it!=cons.end() ); - std::vector< Node > children; - children.push_back( it->second ); - const Datatype& dt = Datatype::datatypeOf( it->second.toExpr() ); - unsigned cindex = Datatype::indexOf( it->second.toExpr() ); - for( unsigned i=0; i<dt[cindex].getNumArgs(); i++ ){ - Node nn = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][i].getSelector() ), n ); - Node nc = constructInstantiation( nn, subs_map, cons ); - children.push_back( nc ); - } - return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); - } -} - Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< Node >& vars, Node& pv_coeff, bool try_coeff ) { Assert( d_prog_var.find( n )!=d_prog_var.end() ); @@ -1097,66 +593,6 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node } } -Node CegInstantiator::getModelBasedProjectionValue( Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ) { - Node val = t; - Trace("cbqi-bound2") << "Value : " << val << std::endl; - Assert( !e.getType().isInteger() || t.getType().isInteger() ); - Assert( !e.getType().isInteger() || mt.getType().isInteger() ); - //add rho value - //get the value of c*e - Node ceValue = me; - Node new_theta = theta; - if( !c.isNull() ){ - Assert( c.getType().isInteger() ); - ceValue = NodeManager::currentNM()->mkNode( MULT, ceValue, c ); - ceValue = Rewriter::rewrite( ceValue ); - if( new_theta.isNull() ){ - new_theta = c; - }else{ - new_theta = NodeManager::currentNM()->mkNode( MULT, new_theta, c ); - new_theta = Rewriter::rewrite( new_theta ); - } - Trace("cbqi-bound2") << "...c*e = " << ceValue << std::endl; - Trace("cbqi-bound2") << "...theta = " << new_theta << std::endl; - } - if( !new_theta.isNull() && e.getType().isInteger() ){ - Node rho; - //if( !mt.getType().isInteger() ){ - //round up/down - //mt = NodeManager::currentNM()->mkNode( - //} - if( isLower ){ - rho = NodeManager::currentNM()->mkNode( MINUS, ceValue, mt ); - }else{ - rho = NodeManager::currentNM()->mkNode( MINUS, mt, ceValue ); - } - rho = Rewriter::rewrite( rho ); - Trace("cbqi-bound2") << "...rho = " << me << " - " << mt << " = " << rho << std::endl; - Trace("cbqi-bound2") << "..." << rho << " mod " << new_theta << " = "; - rho = NodeManager::currentNM()->mkNode( INTS_MODULUS_TOTAL, rho, new_theta ); - rho = Rewriter::rewrite( rho ); - Trace("cbqi-bound2") << rho << std::endl; - Kind rk = isLower ? PLUS : MINUS; - val = NodeManager::currentNM()->mkNode( rk, val, rho ); - val = Rewriter::rewrite( val ); - Trace("cbqi-bound2") << "(after rho) : " << val << std::endl; - } - if( !inf_coeff.isNull() ){ - Assert( !d_vts_sym[0].isNull() ); - val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, inf_coeff, d_vts_sym[0] ) ); - val = Rewriter::rewrite( val ); - } - if( !delta_coeff.isNull() ){ - //create delta here if necessary - if( d_vts_sym[1].isNull() ){ - d_vts_sym[1] = d_qe->getTermDatabase()->getVtsDelta(); - } - val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, delta_coeff, d_vts_sym[1] ) ); - val = Rewriter::rewrite( val ); - } - return val; -} - bool CegInstantiator::check() { if( d_qe->getTheoryEngine()->needCheck() ){ Trace("cbqi-engine") << " CEGQI instantiator : wait until all ground theories are finished." << std::endl; @@ -1165,14 +601,9 @@ bool CegInstantiator::check() { processAssertions(); for( unsigned r=0; r<2; r++ ){ SolvedForm sf; - SolvedForm ssf; - std::vector< Node > vars; - std::vector< int > btyp; - Node theta; - std::map< Node, Node > cons; - std::vector< Node > curr_var; + d_stack_vars.clear(); //try to add an instantiation - if( doAddInstantiation( sf, ssf, vars, btyp, theta, 0, r==0 ? 0 : 2, cons, curr_var ) ){ + if( doAddInstantiation( sf, 0, r==0 ? 0 : 2 ) ){ return true; } } @@ -1222,25 +653,27 @@ void getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& ter } void CegInstantiator::presolve( Node q ) { - Trace("cbqi-presolve") << "CBQI presolve " << q << std::endl; //at preregister time, add proxy of obvious instantiations up front, which helps learning during preprocessing - std::vector< Node > vars; - std::map< Node, std::vector< Node > > teq; - for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ - vars.push_back( q[0][i] ); - teq[q[0][i]].clear(); - } - collectPresolveEqTerms( q[1], teq ); - std::vector< Node > terms; - std::vector< Node > conj; - getPresolveEqConjuncts( vars, terms, teq, q, conj ); - - if( !conj.empty() ){ - Node lem = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ); - Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() ); - lem = NodeManager::currentNM()->mkNode( OR, g, lem ); - Trace("cbqi-presolve-debug") << "Presolve lemma : " << lem << std::endl; - d_qe->getOutputChannel().lemma( lem, false, true ); + //only if no nested quantifiers + if( !QuantifiersRewriter::containsQuantifiers( q[1] ) ){ + std::vector< Node > ps_vars; + std::map< Node, std::vector< Node > > teq; + for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ + ps_vars.push_back( q[0][i] ); + teq[q[0][i]].clear(); + } + collectPresolveEqTerms( q[1], teq ); + std::vector< Node > terms; + std::vector< Node > conj; + getPresolveEqConjuncts( ps_vars, terms, teq, q, conj ); + + if( !conj.empty() ){ + Node lem = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ); + Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() ); + lem = NodeManager::currentNM()->mkNode( OR, g, lem ); + Trace("cbqi-presolve-debug") << "Presolve lemma : " << lem << std::endl; + d_qe->getOutputChannel().lemma( lem, false, true ); + } } } @@ -1362,9 +795,7 @@ void CegInstantiator::processAssertions() { addToAuxVarSubstitution( subs_lhs, subs_rhs, r, it->second ); }else{ Trace("cbqi-proc") << "....no substitution found for auxiliary variable " << r << "!!!" << std::endl; -#ifdef MBP_STRICT_ASSERTIONS Assert( false ); -#endif } } @@ -1397,10 +828,8 @@ void CegInstantiator::processAssertions() { std::vector< Node > akeep; for( unsigned i=0; i<it->second.size(); i++ ){ Node n = it->second[i]; - //compute the variables in assertion - computeProgVars( n ); //must be an eligible term - if( d_inelig.find( n )==d_inelig.end() ){ + if( isEligible( n ) ){ //must contain at least one variable if( !d_prog_var[n].empty() ){ Trace("cbqi-proc") << "...literal[" << it->first << "] : " << n << std::endl; @@ -1453,17 +882,16 @@ Node CegInstantiator::getModelValue( Node n ) { void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited ) { if( n.getKind()==FORALL ){ d_is_nested_quant = true; - }else{ - if( visited.find( n )==visited.end() ){ - visited[n] = true; - if( TermDb::isBoolConnective( n.getKind() ) ){ - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - collectCeAtoms( n[i], visited ); - } - }else{ - if( std::find( d_ce_atoms.begin(), d_ce_atoms.end(), n )==d_ce_atoms.end() ){ - d_ce_atoms.push_back( n ); - } + }else if( visited.find( n )==visited.end() ){ + visited[n] = true; + if( TermDb::isBoolConnective( n.getKind() ) ){ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + collectCeAtoms( n[i], visited ); + } + }else{ + if( std::find( d_ce_atoms.begin(), d_ce_atoms.end(), n )==d_ce_atoms.end() ){ + Trace("cbqi-ce-atoms") << "CE atoms : " << n << std::endl; + d_ce_atoms.push_back( n ); } } } @@ -1479,7 +907,8 @@ struct sortCegVarOrder { void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) { - Assert( d_vars.empty() ); + //Assert( d_vars.empty() ); + d_vars.clear(); d_vars.insert( d_vars.end(), ce_vars.begin(), ce_vars.end() ); //determine variable order: must do Reals before Ints @@ -1512,7 +941,9 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st //remove ITEs IteSkolemMap iteSkolemMap; d_qe->getTheoryEngine()->getIteRemover()->run(lems, iteSkolemMap); - Assert( d_aux_vars.empty() ); + //Assert( d_aux_vars.empty() ); + d_aux_vars.clear(); + d_aux_eq.clear(); for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) { Trace("cbqi-debug") << " Auxiliary var (from ITE) : " << i->first << std::endl; d_aux_vars.push_back( i->first ); @@ -1544,159 +975,14 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st } } -//this isolates the atom into solved form -// veq_c * pv <> val + vts_coeff_delta * delta + vts_coeff_inf * inf -// ensures val is Int if pv is Int, and val does not contain vts symbols -int CegInstantiator::solve_arith( Node pv, Node atom, Node& veq_c, Node& val, Node& vts_coeff_inf, Node& vts_coeff_delta ) { - int ires = 0; - Trace("cbqi-inst-debug") << "isolate for " << pv << " in " << atom << std::endl; - std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( atom, msum ) ){ - Trace("cbqi-inst-debug") << "got monomial sum: " << std::endl; - if( Trace.isOn("cbqi-inst-debug") ){ - QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" ); - } - TypeNode pvtn = pv.getType(); - //remove vts symbols from polynomial - Node vts_coeff[2]; - for( unsigned t=0; t<2; t++ ){ - if( !d_vts_sym[t].isNull() ){ - std::map< Node, Node >::iterator itminf = msum.find( d_vts_sym[t] ); - if( itminf!=msum.end() ){ - vts_coeff[t] = itminf->second; - if( vts_coeff[t].isNull() ){ - vts_coeff[t] = NodeManager::currentNM()->mkConst( Rational( 1 ) ); - } - //negate if coefficient on variable is positive - std::map< Node, Node >::iterator itv = msum.find( pv ); - if( itv!=msum.end() ){ - //multiply by the coefficient we will isolate for - if( itv->second.isNull() ){ - vts_coeff[t] = QuantArith::negate(vts_coeff[t]); - }else{ - if( !pvtn.isInteger() ){ - vts_coeff[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) / itv->second.getConst<Rational>() ), vts_coeff[t] ); - vts_coeff[t] = Rewriter::rewrite( vts_coeff[t] ); - }else if( itv->second.getConst<Rational>().sgn()==1 ){ - vts_coeff[t] = QuantArith::negate(vts_coeff[t]); - } - } - } - Trace("cbqi-inst-debug") << "vts[" << t << "] coefficient is " << vts_coeff[t] << std::endl; - msum.erase( d_vts_sym[t] ); - } - } - } - ires = QuantArith::isolate( pv, msum, veq_c, val, atom.getKind() ); - if( ires!=0 ){ - Node realPart; - if( Trace.isOn("cbqi-inst-debug") ){ - Trace("cbqi-inst-debug") << "Isolate : "; - if( !veq_c.isNull() ){ - Trace("cbqi-inst-debug") << veq_c << " * "; - } - Trace("cbqi-inst-debug") << pv << " " << atom.getKind() << " " << val << std::endl; - } - if( options::cbqiAll() ){ - // when not pure LIA/LRA, we must check whether the lhs contains pv - if( TermDb::containsTerm( val, pv ) ){ - return 0; - } - } - if( pvtn.isInteger() && ( ( !veq_c.isNull() && !veq_c.getType().isInteger() ) || !val.getType().isInteger() ) ){ - //redo, split integer/non-integer parts - bool useCoeff = false; - Integer coeff = d_one.getConst<Rational>().getNumerator(); - for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ - if( it->first.isNull() || it->first.getType().isInteger() ){ - if( !it->second.isNull() ){ - coeff = coeff.lcm( it->second.getConst<Rational>().getDenominator() ); - useCoeff = true; - } - } - } - //multiply everything by this coefficient - Node rcoeff = NodeManager::currentNM()->mkConst( Rational( coeff ) ); - std::vector< Node > real_part; - for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ - if( useCoeff ){ - if( it->second.isNull() ){ - msum[it->first] = rcoeff; - }else{ - msum[it->first] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, it->second, rcoeff ) ); - } - } - if( !it->first.isNull() && !it->first.getType().isInteger() ){ - real_part.push_back( msum[it->first].isNull() ? it->first : NodeManager::currentNM()->mkNode( MULT, msum[it->first], it->first ) ); - } - } - //remove delta TODO: check this - vts_coeff[1] = Node::null(); - //multiply inf - if( !vts_coeff[0].isNull() ){ - vts_coeff[0] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, rcoeff, vts_coeff[0] ) ); - } - realPart = real_part.empty() ? d_zero : ( real_part.size()==1 ? real_part[0] : NodeManager::currentNM()->mkNode( PLUS, real_part ) ); - Assert( d_out->isEligibleForInstantiation( realPart ) ); - //re-isolate - Trace("cbqi-inst-debug") << "Re-isolate..." << std::endl; - ires = QuantArith::isolate( pv, msum, veq_c, val, atom.getKind() ); - Trace("cbqi-inst-debug") << "Isolate for mixed Int/Real : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl; - Trace("cbqi-inst-debug") << " real part : " << realPart << std::endl; - if( ires!=0 ){ - int ires_use = ( msum[pv].isNull() || msum[pv].getConst<Rational>().sgn()==1 ) ? 1 : -1; - val = Rewriter::rewrite( NodeManager::currentNM()->mkNode( ires_use==-1 ? PLUS : MINUS, - NodeManager::currentNM()->mkNode( ires_use==-1 ? MINUS : PLUS, val, realPart ), - NodeManager::currentNM()->mkNode( TO_INTEGER, realPart ) ) ); //TODO: round up for upper bounds? - Trace("cbqi-inst-debug") << "result : " << val << std::endl; - Assert( val.getType().isInteger() ); - } - } - } - vts_coeff_inf = vts_coeff[0]; - vts_coeff_delta = vts_coeff[1]; - } - return ires; +Instantiator::Instantiator( QuantifiersEngine * qe, TypeNode tn ) : d_type( tn ){ + d_closed_enum_type = qe->getTermDatabase()->isClosedEnumerableType( tn ); } -Node CegInstantiator::solve_dt( Node v, Node a, Node b, Node sa, Node sb ) { - Trace("cbqi-inst-debug2") << "Solve dt : " << v << " " << a << " " << b << " " << sa << " " << sb << std::endl; - Node ret; - if( !a.isNull() && a==v ){ - ret = sb; - }else if( !b.isNull() && b==v ){ - ret = sa; - }else if( !a.isNull() && a.getKind()==APPLY_CONSTRUCTOR ){ - if( !b.isNull() && b.getKind()==APPLY_CONSTRUCTOR ){ - if( a.getOperator()==b.getOperator() ){ - for( unsigned i=0; i<a.getNumChildren(); i++ ){ - Node s = solve_dt( v, a[i], b[i], sa[i], sb[i] ); - if( !s.isNull() ){ - return s; - } - } - } - }else{ - unsigned cindex = Datatype::indexOf( a.getOperator().toExpr() ); - TypeNode tn = a.getType(); - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - for( unsigned i=0; i<a.getNumChildren(); i++ ){ - Node nn = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][i].getSelector() ), sb ); - Node s = solve_dt( v, a[i], Node::null(), sa[i], nn ); - if( !s.isNull() ){ - return s; - } - } - } - }else if( !b.isNull() && b.getKind()==APPLY_CONSTRUCTOR ){ - return solve_dt( v, b, a, sb, sa ); - } - if( !ret.isNull() ){ - //ensure does not contain - if( TermDb::containsTerm( ret, v ) ){ - ret = Node::null(); - } - } - return ret; + +bool Instantiator::processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort ) { + return ci->doAddInstantiationInc( pv, n, pv_coeff, 0, sf, effort ); } + + diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index 3d7bbcb55..94d02de9b 100755 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -38,17 +38,52 @@ public: virtual bool addLemma( Node lem ) = 0; }; +class Instantiator; + + +//solved form, involves substitution with coefficients +class SolvedForm { +public: + std::vector< Node > d_vars; + std::vector< Node > d_subs; + std::vector< Node > d_coeff; + std::vector< int > d_btyp; + std::vector< Node > d_has_coeff; + Node d_theta; + void copy( SolvedForm& sf ){ + d_vars.insert( d_vars.end(), sf.d_vars.begin(), sf.d_vars.end() ); + d_subs.insert( d_subs.end(), sf.d_subs.begin(), sf.d_subs.end() ); + d_coeff.insert( d_coeff.end(), sf.d_coeff.begin(), sf.d_coeff.end() ); + d_btyp.insert( d_btyp.end(), sf.d_btyp.begin(), sf.d_btyp.end() ); + d_has_coeff.insert( d_has_coeff.end(), sf.d_has_coeff.begin(), sf.d_has_coeff.end() ); + d_theta = sf.d_theta; + } + void push_back( Node pv, Node n, Node pv_coeff, int bt ){ + d_vars.push_back( pv ); + d_subs.push_back( n ); + d_coeff.push_back( pv_coeff ); + d_btyp.push_back( bt ); + if( !pv_coeff.isNull() ){ + d_has_coeff.push_back( pv ); + } + } + void pop_back( Node pv, Node n, Node pv_coeff, int bt ){ + d_vars.pop_back(); + d_subs.pop_back(); + d_coeff.pop_back(); + d_btyp.pop_back(); + if( !pv_coeff.isNull() ){ + d_has_coeff.pop_back(); + } + } +}; + class CegInstantiator { private: QuantifiersEngine * d_qe; CegqiOutput * d_out; - //constants - Node d_zero; - Node d_one; - Node d_true; bool d_use_vts_delta; bool d_use_vts_inf; - Node d_vts_sym[2]; //program variable contains cache std::map< Node, std::map< Node, bool > > d_prog_var; std::map< Node, bool > d_inelig; @@ -67,81 +102,116 @@ private: //atoms of the CE lemma bool d_is_nested_quant; std::vector< Node > d_ce_atoms; -private: //collect atoms - void collectCeAtoms( Node n, std::map< Node, bool >& visited ); + void collectCeAtoms( Node n, std::map< Node, bool >& visited ); +private: + //map from variables to their instantiators + std::map< Node, Instantiator * > d_instantiator; + //cache of current substitutions tried between register/unregister + std::map< Node, std::map< Node, std::map< Node, bool > > > d_curr_subs_proc; + std::map< Node, unsigned > d_curr_index; + //stack of temporary variables we are solving (e.g. subfields of datatypes) + std::vector< Node > d_stack_vars; + //used instantiators + std::map< Node, Instantiator * > d_active_instantiators; + //register variable + void registerInstantiationVariable( Node v, unsigned index ); + void unregisterInstantiationVariable( Node v ); +private: //for adding instantiations during check void computeProgVars( Node n ); - //solved form, involves substitution with coefficients - class SolvedForm { - public: - std::vector< Node > d_subs; - std::vector< Node > d_coeff; - std::vector< Node > d_has_coeff; - void copy( SolvedForm& sf ){ - d_subs.insert( d_subs.end(), sf.d_subs.begin(), sf.d_subs.end() ); - d_coeff.insert( d_coeff.end(), sf.d_coeff.begin(), sf.d_coeff.end() ); - d_has_coeff.insert( d_has_coeff.end(), sf.d_has_coeff.begin(), sf.d_has_coeff.end() ); - } - void push_back( Node pv, Node n, Node pv_coeff ){ - d_subs.push_back( n ); - d_coeff.push_back( pv_coeff ); - if( !pv_coeff.isNull() ){ - d_has_coeff.push_back( pv ); - } - } - void pop_back( Node pv, Node n, Node pv_coeff ){ - d_subs.pop_back(); - d_coeff.pop_back(); - if( !pv_coeff.isNull() ){ - d_has_coeff.pop_back(); - } - } - }; - /* - class MbpBound { - public: - Node d_bound; - Node d_coeff; - Node d_vts_coeff[2]; - Node d_lit; - }; - */ // effort=0 : do not use model value, 1: use model value, 2: one must use model value - bool doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, - std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, - std::map< Node, Node >& cons, std::vector< Node >& curr_var ); - bool doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, - std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, - std::map< Node, Node >& cons, std::vector< Node >& curr_var ); - bool doAddInstantiationCoeff( SolvedForm& sf, - std::vector< Node >& vars, std::vector< int >& btyp, - unsigned j, std::map< Node, Node >& cons ); - bool doAddInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons ); - Node constructInstantiation( Node n, std::map< Node, Node >& subs_map, std::map< Node, Node >& cons ); - Node applySubstitution( TypeNode tn, Node n, SolvedForm& sf, std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ) { - return applySubstitution( tn, n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, vars, pv_coeff, try_coeff ); - } - Node applySubstitution( TypeNode tn, Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff, - std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ); - Node getModelBasedProjectionValue( Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ); + bool doAddInstantiation( SolvedForm& sf, unsigned i, unsigned effort ); + bool doAddInstantiation( std::vector< Node >& subs, std::vector< Node >& vars ); + //process void processAssertions(); void addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r ); - //get model value - Node getModelValue( Node n ); -private: - int solve_arith( Node v, Node atom, Node & veq_c, Node & val, Node& vts_coeff_inf, Node& vts_coeff_delta ); - Node solve_dt( Node v, Node a, Node b, Node sa, Node sb ); public: CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta = true, bool use_vts_inf = true ); + virtual ~CegInstantiator(); //check : add instantiations based on valuation of d_vars bool check(); //presolve for quantified formula void presolve( Node q ); //register the counterexample lemma (stored in lems), modify vector void registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ); + //output + CegqiOutput * getOutput() { return d_out; } + //get quantifiers engine + QuantifiersEngine* getQuantifiersEngine() { return d_qe; } + +//interface for instantiators +public: + void pushStackVariable( Node v ); + void popStackVariable(); + bool doAddInstantiationInc( Node pv, Node n, Node pv_coeff, int bt, SolvedForm& sf, unsigned effort ); + Node getModelValue( Node n ); + // TODO: move to solved form? + Node applySubstitution( TypeNode tn, Node n, SolvedForm& sf, Node& pv_coeff, bool try_coeff = true ) { + return applySubstitution( tn, n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, sf.d_vars, pv_coeff, try_coeff ); + } + Node applySubstitution( TypeNode tn, Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff, + std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ); +public: + unsigned getNumCEAtoms() { return d_ce_atoms.size(); } + Node getCEAtom( unsigned i ) { return d_ce_atoms[i]; } + // is eligible + bool isEligible( Node n ); + // has variable + bool hasVariable( Node n, Node pv ); + bool useVtsDelta() { return d_use_vts_delta; } + bool useVtsInfinity() { return d_use_vts_inf; } + bool hasNestedQuantification() { return d_is_nested_quant; } }; + + +// an instantiator for individual variables +// will make calls into CegInstantiator::doAddInstantiationInc +class Instantiator { +protected: + TypeNode d_type; + bool d_closed_enum_type; +public: + Instantiator( QuantifiersEngine * qe, TypeNode tn ); + virtual ~Instantiator(){} + virtual void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {} + + //called when pv_coeff * pv = n, and n is eligible for instantiation + virtual bool processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort ); + //eqc is the equivalence class of pv + virtual bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ) { return false; } + + //term_coeffs.size() = terms.size() = 2, called when term_coeff[0] * terms[0] = term_coeff[1] * terms[1], terms are eligible, and at least one of these terms contains pv + virtual bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; } + virtual bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) { return false; } + + //called when assertion lit holds. note that lit is unsubstituted, first must substitute/solve/check eligible + virtual bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; } + virtual bool processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { return false; } + virtual bool processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort ) { return false; } + + //do we allow instantiation for the model value of pv + virtual bool useModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; } + virtual bool allowModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return d_closed_enum_type; } + + //do we need to postprocess the solved form? did we successfully postprocess + virtual bool needsPostProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; } + virtual bool postProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } + + /** Identify this module (for debugging) */ + virtual std::string identify() const { return "Default"; } +}; + +class ModelValueInstantiator : public Instantiator { +public: + ModelValueInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} + virtual ~ModelValueInstantiator(){} + bool useModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } + std::string identify() const { return "ModelValue"; } +}; + + } } } diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp new file mode 100644 index 000000000..3282872d6 --- /dev/null +++ b/src/theory/quantifiers/ceg_t_instantiator.cpp @@ -0,0 +1,868 @@ +/********************* */ +/*! \file ceg_t_instantiator.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 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 theory-specific counterexample-guided quantifier instantiation + **/ + +#include "theory/quantifiers/ceg_t_instantiator.h" + +#include "options/quantifiers_options.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/trigger.h" + +#include "theory/arith/partial_model.h" +#include "theory/arith/theory_arith.h" +#include "theory/arith/theory_arith_private.h" +#include "theory/bv/theory_bv_utils.h" +#include "util/bitvector.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; + +Node ArithInstantiator::getModelBasedProjectionValue( CegInstantiator * ci, Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ) { + Node val = t; + Trace("cbqi-bound2") << "Value : " << val << std::endl; + Assert( !e.getType().isInteger() || t.getType().isInteger() ); + Assert( !e.getType().isInteger() || mt.getType().isInteger() ); + //add rho value + //get the value of c*e + Node ceValue = me; + Node new_theta = theta; + if( !c.isNull() ){ + Assert( c.getType().isInteger() ); + ceValue = NodeManager::currentNM()->mkNode( MULT, ceValue, c ); + ceValue = Rewriter::rewrite( ceValue ); + if( new_theta.isNull() ){ + new_theta = c; + }else{ + new_theta = NodeManager::currentNM()->mkNode( MULT, new_theta, c ); + new_theta = Rewriter::rewrite( new_theta ); + } + Trace("cbqi-bound2") << "...c*e = " << ceValue << std::endl; + Trace("cbqi-bound2") << "...theta = " << new_theta << std::endl; + } + if( !new_theta.isNull() && e.getType().isInteger() ){ + Node rho; + //if( !mt.getType().isInteger() ){ + //round up/down + //mt = NodeManager::currentNM()->mkNode( + //} + if( isLower ){ + rho = NodeManager::currentNM()->mkNode( MINUS, ceValue, mt ); + }else{ + rho = NodeManager::currentNM()->mkNode( MINUS, mt, ceValue ); + } + rho = Rewriter::rewrite( rho ); + Trace("cbqi-bound2") << "...rho = " << me << " - " << mt << " = " << rho << std::endl; + Trace("cbqi-bound2") << "..." << rho << " mod " << new_theta << " = "; + rho = NodeManager::currentNM()->mkNode( INTS_MODULUS_TOTAL, rho, new_theta ); + rho = Rewriter::rewrite( rho ); + Trace("cbqi-bound2") << rho << std::endl; + Kind rk = isLower ? PLUS : MINUS; + val = NodeManager::currentNM()->mkNode( rk, val, rho ); + val = Rewriter::rewrite( val ); + Trace("cbqi-bound2") << "(after rho) : " << val << std::endl; + } + if( !inf_coeff.isNull() ){ + Assert( !d_vts_sym[0].isNull() ); + val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, inf_coeff, d_vts_sym[0] ) ); + val = Rewriter::rewrite( val ); + } + if( !delta_coeff.isNull() ){ + //create delta here if necessary + val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, delta_coeff, ci->getQuantifiersEngine()->getTermDatabase()->getVtsDelta() ) ); + val = Rewriter::rewrite( val ); + } + return val; +} + +//this isolates the atom into solved form +// veq_c * pv <> val + vts_coeff_delta * delta + vts_coeff_inf * inf +// ensures val is Int if pv is Int, and val does not contain vts symbols +int ArithInstantiator::solve_arith( CegInstantiator * ci, Node pv, Node atom, Node& veq_c, Node& val, Node& vts_coeff_inf, Node& vts_coeff_delta ) { + int ires = 0; + Trace("cbqi-inst-debug") << "isolate for " << pv << " in " << atom << std::endl; + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( atom, msum ) ){ + Trace("cbqi-inst-debug") << "got monomial sum: " << std::endl; + if( Trace.isOn("cbqi-inst-debug") ){ + QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" ); + } + TypeNode pvtn = pv.getType(); + //remove vts symbols from polynomial + Node vts_coeff[2]; + for( unsigned t=0; t<2; t++ ){ + if( !d_vts_sym[t].isNull() ){ + std::map< Node, Node >::iterator itminf = msum.find( d_vts_sym[t] ); + if( itminf!=msum.end() ){ + vts_coeff[t] = itminf->second; + if( vts_coeff[t].isNull() ){ + vts_coeff[t] = NodeManager::currentNM()->mkConst( Rational( 1 ) ); + } + //negate if coefficient on variable is positive + std::map< Node, Node >::iterator itv = msum.find( pv ); + if( itv!=msum.end() ){ + //multiply by the coefficient we will isolate for + if( itv->second.isNull() ){ + vts_coeff[t] = QuantArith::negate(vts_coeff[t]); + }else{ + if( !pvtn.isInteger() ){ + vts_coeff[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) / itv->second.getConst<Rational>() ), vts_coeff[t] ); + vts_coeff[t] = Rewriter::rewrite( vts_coeff[t] ); + }else if( itv->second.getConst<Rational>().sgn()==1 ){ + vts_coeff[t] = QuantArith::negate(vts_coeff[t]); + } + } + } + Trace("cbqi-inst-debug") << "vts[" << t << "] coefficient is " << vts_coeff[t] << std::endl; + msum.erase( d_vts_sym[t] ); + } + } + } + + ires = QuantArith::isolate( pv, msum, veq_c, val, atom.getKind() ); + if( ires!=0 ){ + Node realPart; + if( Trace.isOn("cbqi-inst-debug") ){ + Trace("cbqi-inst-debug") << "Isolate : "; + if( !veq_c.isNull() ){ + Trace("cbqi-inst-debug") << veq_c << " * "; + } + Trace("cbqi-inst-debug") << pv << " " << atom.getKind() << " " << val << std::endl; + } + if( options::cbqiAll() ){ + // when not pure LIA/LRA, we must check whether the lhs contains pv + if( TermDb::containsTerm( val, pv ) ){ + Trace("cbqi-inst-debug") << "fail : contains bad term" << std::endl; + return 0; + } + } + if( pvtn.isInteger() && ( ( !veq_c.isNull() && !veq_c.getType().isInteger() ) || !val.getType().isInteger() ) ){ + //redo, split integer/non-integer parts + bool useCoeff = false; + Integer coeff = ci->getQuantifiersEngine()->getTermDatabase()->d_one.getConst<Rational>().getNumerator(); + for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ + if( it->first.isNull() || it->first.getType().isInteger() ){ + if( !it->second.isNull() ){ + coeff = coeff.lcm( it->second.getConst<Rational>().getDenominator() ); + useCoeff = true; + } + } + } + //multiply everything by this coefficient + Node rcoeff = NodeManager::currentNM()->mkConst( Rational( coeff ) ); + std::vector< Node > real_part; + for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ + if( useCoeff ){ + if( it->second.isNull() ){ + msum[it->first] = rcoeff; + }else{ + msum[it->first] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, it->second, rcoeff ) ); + } + } + if( !it->first.isNull() && !it->first.getType().isInteger() ){ + real_part.push_back( msum[it->first].isNull() ? it->first : NodeManager::currentNM()->mkNode( MULT, msum[it->first], it->first ) ); + } + } + //remove delta TODO: check this + vts_coeff[1] = Node::null(); + //multiply inf + if( !vts_coeff[0].isNull() ){ + vts_coeff[0] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, rcoeff, vts_coeff[0] ) ); + } + realPart = real_part.empty() ? ci->getQuantifiersEngine()->getTermDatabase()->d_zero : ( real_part.size()==1 ? real_part[0] : NodeManager::currentNM()->mkNode( PLUS, real_part ) ); + Assert( ci->getOutput()->isEligibleForInstantiation( realPart ) ); + //re-isolate + Trace("cbqi-inst-debug") << "Re-isolate..." << std::endl; + ires = QuantArith::isolate( pv, msum, veq_c, val, atom.getKind() ); + Trace("cbqi-inst-debug") << "Isolate for mixed Int/Real : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl; + Trace("cbqi-inst-debug") << " real part : " << realPart << std::endl; + if( ires!=0 ){ + int ires_use = ( msum[pv].isNull() || msum[pv].getConst<Rational>().sgn()==1 ) ? 1 : -1; + val = Rewriter::rewrite( NodeManager::currentNM()->mkNode( ires_use==-1 ? PLUS : MINUS, + NodeManager::currentNM()->mkNode( ires_use==-1 ? MINUS : PLUS, val, realPart ), + NodeManager::currentNM()->mkNode( TO_INTEGER, realPart ) ) ); //TODO: round up for upper bounds? + Trace("cbqi-inst-debug") << "result : " << val << std::endl; + Assert( val.getType().isInteger() ); + } + } + } + vts_coeff_inf = vts_coeff[0]; + vts_coeff_delta = vts_coeff[1]; + Trace("cbqi-inst-debug") << "Return " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << ", vts = (" << vts_coeff_inf << ", " << vts_coeff_delta << ")" << std::endl; + }else{ + Trace("cbqi-inst-debug") << "fail : could not get monomial sum" << std::endl; + } + return ires; +} + +void ArithInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { + d_vts_sym[0] = ci->getQuantifiersEngine()->getTermDatabase()->getVtsInfinity( d_type, false, false ); + d_vts_sym[1] = ci->getQuantifiersEngine()->getTermDatabase()->getVtsDelta( false, false ); + for( unsigned i=0; i<2; i++ ){ + d_mbp_bounds[i].clear(); + d_mbp_coeff[i].clear(); + for( unsigned j=0; j<2; j++ ){ + d_mbp_vts_coeff[i][j].clear(); + } + d_mbp_lit[i].clear(); + } +} + +bool ArithInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) { + Node eq_lhs = terms[0]; + Node eq_rhs = terms[1]; + Node lhs_coeff = term_coeffs[0]; + Node rhs_coeff = term_coeffs[1]; + //make the same coefficient + if( rhs_coeff!=lhs_coeff ){ + if( !rhs_coeff.isNull() ){ + Trace("cbqi-inst-debug") << "...mult lhs by " << rhs_coeff << std::endl; + eq_lhs = NodeManager::currentNM()->mkNode( MULT, rhs_coeff, eq_lhs ); + eq_lhs = Rewriter::rewrite( eq_lhs ); + } + if( !lhs_coeff.isNull() ){ + Trace("cbqi-inst-debug") << "...mult rhs by " << lhs_coeff << std::endl; + eq_rhs = NodeManager::currentNM()->mkNode( MULT, lhs_coeff, eq_rhs ); + eq_rhs = Rewriter::rewrite( eq_rhs ); + } + } + Node eq = eq_lhs.eqNode( eq_rhs ); + eq = Rewriter::rewrite( eq ); + Node val; + Node veq_c; + Node vts_coeff_inf; + Node vts_coeff_delta; + //isolate pv in the equality + int ires = solve_arith( ci, pv, eq, veq_c, val, vts_coeff_inf, vts_coeff_delta ); + if( ires!=0 ){ + if( ci->doAddInstantiationInc( pv, val, veq_c, 0, sf, effort ) ){ + return true; + } + } + + return false; +} + +bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { + Trace("cbqi-inst-debug2") << " look at " << lit << std::endl; + Node atom = lit.getKind()==NOT ? lit[0] : lit; + bool pol = lit.getKind()!=NOT; + //arithmetic inequalities and disequalities + if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && atom[0].getType().isReal() ) ){ + Assert( atom.getKind()!=GEQ || atom[1].isConst() ); + Node atom_lhs; + Node atom_rhs; + if( atom.getKind()==GEQ ){ + atom_lhs = atom[0]; + atom_rhs = atom[1]; + }else{ + atom_lhs = NodeManager::currentNM()->mkNode( MINUS, atom[0], atom[1] ); + atom_lhs = Rewriter::rewrite( atom_lhs ); + atom_rhs = ci->getQuantifiersEngine()->getTermDatabase()->d_zero; + } + //must be an eligible term + if( ci->isEligible( atom_lhs ) ){ + //apply substitution to LHS of atom + Node atom_lhs_coeff; + atom_lhs = ci->applySubstitution( d_type, atom_lhs, sf, atom_lhs_coeff ); + if( !atom_lhs.isNull() ){ + if( !atom_lhs_coeff.isNull() ){ + atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_coeff, atom_rhs ) ); + } + } + //if it contains pv, not infinity + if( !atom_lhs.isNull() && ci->hasVariable( atom_lhs, pv ) ){ + Node pv_value = ci->getModelValue( pv ); + Node satom = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs ); + //cannot contain infinity? + Trace("cbqi-inst-debug") << "..[3] From assertion : " << atom << ", pol = " << pol << std::endl; + Trace("cbqi-inst-debug") << " substituted : " << satom << ", pol = " << pol << std::endl; + Node vts_coeff_inf; + Node vts_coeff_delta; + Node val; + Node veq_c; + //isolate pv in the inequality + int ires = solve_arith( ci, pv, satom, veq_c, val, vts_coeff_inf, vts_coeff_delta ); + if( ires!=0 ){ + //disequalities are either strict upper or lower bounds + unsigned rmax = ( atom.getKind()==GEQ || options::cbqiModel() ) ? 1 : 2; + for( unsigned r=0; r<rmax; r++ ){ + int uires = ires; + Node uval = val; + if( atom.getKind()==GEQ ){ + //push negation downwards + if( !pol ){ + uires = -ires; + if( d_type.isInteger() ){ + uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); + uval = Rewriter::rewrite( uval ); + }else{ + Assert( d_type.isReal() ); + //now is strict inequality + uires = uires*2; + } + } + }else{ + bool is_upper; + if( options::cbqiModel() ){ + // disequality is a disjunction : only consider the bound in the direction of the model + //first check if there is an infinity... + if( !vts_coeff_inf.isNull() ){ + //coefficient or val won't make a difference, just compare with zero + Trace("cbqi-inst-debug") << "Disequality : check infinity polarity " << vts_coeff_inf << std::endl; + Assert( vts_coeff_inf.isConst() ); + is_upper = ( vts_coeff_inf.getConst<Rational>().sgn()==1 ); + }else{ + Node rhs_value = ci->getModelValue( val ); + Node lhs_value = pv_value; + if( !veq_c.isNull() ){ + lhs_value = NodeManager::currentNM()->mkNode( MULT, lhs_value, veq_c ); + lhs_value = Rewriter::rewrite( lhs_value ); + } + Trace("cbqi-inst-debug") << "Disequality : check model values " << lhs_value << " " << rhs_value << std::endl; + Assert( lhs_value!=rhs_value ); + Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value ); + cmp = Rewriter::rewrite( cmp ); + Assert( cmp.isConst() ); + is_upper = ( cmp!=ci->getQuantifiersEngine()->getTermDatabase()->d_true ); + } + }else{ + is_upper = (r==0); + } + Assert( atom.getKind()==EQUAL && !pol ); + if( d_type.isInteger() ){ + uires = is_upper ? -1 : 1; + uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); + uval = Rewriter::rewrite( uval ); + }else{ + Assert( d_type.isReal() ); + uires = is_upper ? -2 : 2; + } + } + Trace("cbqi-bound-inf") << "From " << lit << ", got : "; + if( !veq_c.isNull() ){ + Trace("cbqi-bound-inf") << veq_c << " * "; + } + Trace("cbqi-bound-inf") << pv << " -> " << uval << ", styp = " << uires << std::endl; + //take into account delta + if( ci->useVtsDelta() && ( uires==2 || uires==-2 ) ){ + if( options::cbqiModel() ){ + Node delta_coeff = NodeManager::currentNM()->mkConst( Rational( uires > 0 ? 1 : -1 ) ); + if( vts_coeff_delta.isNull() ){ + vts_coeff_delta = delta_coeff; + }else{ + vts_coeff_delta = NodeManager::currentNM()->mkNode( PLUS, vts_coeff_delta, delta_coeff ); + vts_coeff_delta = Rewriter::rewrite( vts_coeff_delta ); + } + }else{ + Node delta = ci->getQuantifiersEngine()->getTermDatabase()->getVtsDelta(); + uval = NodeManager::currentNM()->mkNode( uires==2 ? PLUS : MINUS, uval, delta ); + uval = Rewriter::rewrite( uval ); + } + } + if( options::cbqiModel() ){ + //just store bounds, will choose based on tighest bound + unsigned index = uires>0 ? 0 : 1; + d_mbp_bounds[index].push_back( uval ); + d_mbp_coeff[index].push_back( veq_c ); + Trace("cbqi-inst-debug") << "Store bound " << index << " " << uval << " " << veq_c << " " << vts_coeff_inf << " " << vts_coeff_delta << " " << lit << std::endl; + for( unsigned t=0; t<2; t++ ){ + d_mbp_vts_coeff[index][t].push_back( t==0 ? vts_coeff_inf : vts_coeff_delta ); + } + d_mbp_lit[index].push_back( lit ); + }else{ + //try this bound + if( ci->doAddInstantiationInc( pv, uval, veq_c, uires>0 ? 1 : -1, sf, effort ) ){ + return true; + } + } + } + } + } + } + } + + + return false; +} + +bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort ) { + if( options::cbqiModel() ){ + bool use_inf = ci->useVtsInfinity() && ( d_type.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal() ); + bool upper_first = false; + if( options::cbqiMinBounds() ){ + upper_first = d_mbp_bounds[1].size()<d_mbp_bounds[0].size(); + } + int best_used[2]; + std::vector< Node > t_values[3]; + Node zero = ci->getQuantifiersEngine()->getTermDatabase()->d_zero; + Node one = ci->getQuantifiersEngine()->getTermDatabase()->d_one; + Node pv_value = ci->getModelValue( pv ); + //try optimal bounds + for( unsigned r=0; r<2; r++ ){ + int rr = upper_first ? (1-r) : r; + best_used[rr] = -1; + if( d_mbp_bounds[rr].empty() ){ + if( use_inf ){ + Trace("cbqi-bound") << "No " << ( rr==0 ? "lower" : "upper" ) << " bounds for " << pv << " (type=" << d_type << ")" << std::endl; + //no bounds, we do +- infinity + Node val = ci->getQuantifiersEngine()->getTermDatabase()->getVtsInfinity( d_type ); + //TODO : rho value for infinity? + if( rr==0 ){ + val = NodeManager::currentNM()->mkNode( UMINUS, val ); + val = Rewriter::rewrite( val ); + } + if( ci->doAddInstantiationInc( pv, val, Node::null(), 0, sf, effort ) ){ + return true; + } + } + }else{ + Trace("cbqi-bound") << ( rr==0 ? "Lower" : "Upper" ) << " bounds for " << pv << " (type=" << d_type << ") : " << std::endl; + int best = -1; + Node best_bound_value[3]; + for( unsigned j=0; j<d_mbp_bounds[rr].size(); j++ ){ + Node value[3]; + if( Trace.isOn("cbqi-bound") ){ + Assert( !d_mbp_bounds[rr][j].isNull() ); + Trace("cbqi-bound") << " " << j << ": " << d_mbp_bounds[rr][j]; + if( !d_mbp_vts_coeff[rr][0][j].isNull() ){ + Trace("cbqi-bound") << " (+ " << d_mbp_vts_coeff[rr][0][j] << " * INF)"; + } + if( !d_mbp_vts_coeff[rr][1][j].isNull() ){ + Trace("cbqi-bound") << " (+ " << d_mbp_vts_coeff[rr][1][j] << " * DELTA)"; + } + if( !d_mbp_coeff[rr][j].isNull() ){ + Trace("cbqi-bound") << " (div " << d_mbp_coeff[rr][j] << ")"; + } + Trace("cbqi-bound") << ", value = "; + } + t_values[rr].push_back( Node::null() ); + //check if it is better than the current best bound : lexicographic order infinite/finite/infinitesimal parts + bool new_best = true; + for( unsigned t=0; t<3; t++ ){ + //get the value + if( t==0 ){ + value[0] = d_mbp_vts_coeff[rr][0][j]; + if( !value[0].isNull() ){ + Trace("cbqi-bound") << "( " << value[0] << " * INF ) + "; + }else{ + value[0] = zero; + } + }else if( t==1 ){ + Node t_value = ci->getModelValue( d_mbp_bounds[rr][j] ); + t_values[rr][j] = t_value; + value[1] = t_value; + Trace("cbqi-bound") << value[1]; + }else{ + value[2] = d_mbp_vts_coeff[rr][1][j]; + if( !value[2].isNull() ){ + Trace("cbqi-bound") << " + ( " << value[2] << " * DELTA )"; + }else{ + value[2] = zero; + } + } + //multiply by coefficient + if( value[t]!=zero && !d_mbp_coeff[rr][j].isNull() ){ + Assert( d_mbp_coeff[rr][j].isConst() ); + value[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(1) / d_mbp_coeff[rr][j].getConst<Rational>() ), value[t] ); + value[t] = Rewriter::rewrite( value[t] ); + } + //check if new best + if( best!=-1 ){ + Assert( !value[t].isNull() && !best_bound_value[t].isNull() ); + if( value[t]!=best_bound_value[t] ){ + Kind k = rr==0 ? GEQ : LEQ; + Node cmp_bound = NodeManager::currentNM()->mkNode( k, value[t], best_bound_value[t] ); + cmp_bound = Rewriter::rewrite( cmp_bound ); + if( cmp_bound!=ci->getQuantifiersEngine()->getTermDatabase()->d_true ){ + new_best = false; + break; + } + } + } + } + Trace("cbqi-bound") << std::endl; + if( new_best ){ + for( unsigned t=0; t<3; t++ ){ + best_bound_value[t] = value[t]; + } + best = j; + } + } + if( best!=-1 ){ + Trace("cbqi-bound") << "...best bound is " << best << " : "; + if( best_bound_value[0]!=zero ){ + Trace("cbqi-bound") << "( " << best_bound_value[0] << " * INF ) + "; + } + Trace("cbqi-bound") << best_bound_value[1]; + if( best_bound_value[2]!=zero ){ + Trace("cbqi-bound") << " + ( " << best_bound_value[2] << " * DELTA )"; + } + Trace("cbqi-bound") << std::endl; + best_used[rr] = best; + //if using cbqiMidpoint, only add the instance based on one bound if the bound is non-strict + if( !options::cbqiMidpoint() || d_type.isInteger() || d_mbp_vts_coeff[rr][1][best].isNull() ){ + Node val = d_mbp_bounds[rr][best]; + val = getModelBasedProjectionValue( ci, pv, val, rr==0, d_mbp_coeff[rr][best], pv_value, t_values[rr][best], sf.d_theta, + d_mbp_vts_coeff[rr][0][best], d_mbp_vts_coeff[rr][1][best] ); + if( !val.isNull() ){ + if( ci->doAddInstantiationInc( pv, val, d_mbp_coeff[rr][best], rr==0 ? 1 : -1, sf, effort ) ){ + return true; + } + } + } + } + } + } + //if not using infinity, use model value of zero + if( !use_inf && d_mbp_bounds[0].empty() && d_mbp_bounds[1].empty() ){ + Node val = zero; + Node c; //null (one) coefficient + val = getModelBasedProjectionValue( ci, pv, val, true, c, pv_value, zero, sf.d_theta, Node::null(), Node::null() ); + if( !val.isNull() ){ + if( ci->doAddInstantiationInc( pv, val, c, 0, sf, effort ) ){ + return true; + } + } + } + if( options::cbqiMidpoint() && !d_type.isInteger() ){ + Node vals[2]; + bool bothBounds = true; + Trace("cbqi-bound") << "Try midpoint of bounds..." << std::endl; + for( unsigned rr=0; rr<2; rr++ ){ + int best = best_used[rr]; + if( best==-1 ){ + bothBounds = false; + }else{ + vals[rr] = d_mbp_bounds[rr][best]; + vals[rr] = getModelBasedProjectionValue( ci, pv, vals[rr], rr==0, Node::null(), pv_value, t_values[rr][best], sf.d_theta, + d_mbp_vts_coeff[rr][0][best], Node::null() ); + } + Trace("cbqi-bound") << "Bound : " << vals[rr] << std::endl; + } + Node val; + if( bothBounds ){ + Assert( !vals[0].isNull() && !vals[1].isNull() ); + if( vals[0]==vals[1] ){ + val = vals[0]; + }else{ + val = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkNode( PLUS, vals[0], vals[1] ), + NodeManager::currentNM()->mkConst( Rational(1)/Rational(2) ) ); + val = Rewriter::rewrite( val ); + } + }else{ + if( !vals[0].isNull() ){ + val = NodeManager::currentNM()->mkNode( PLUS, vals[0], one ); + val = Rewriter::rewrite( val ); + }else if( !vals[1].isNull() ){ + val = NodeManager::currentNM()->mkNode( MINUS, vals[1], one ); + val = Rewriter::rewrite( val ); + } + } + Trace("cbqi-bound") << "Midpoint value : " << val << std::endl; + if( !val.isNull() ){ + if( ci->doAddInstantiationInc( pv, val, Node::null(), 0, sf, effort ) ){ + return true; + } + } + } + //generally should not make it to this point FIXME: write proper assertion + //Assert( ( ci->hasNestedQuantification() && !options::cbqiNestedQE() ) || options::cbqiAll() ); + + if( options::cbqiNopt() ){ + //try non-optimal bounds (heuristic, may help when nested quantification) ? + Trace("cbqi-bound") << "Try non-optimal bounds..." << std::endl; + for( unsigned r=0; r<2; r++ ){ + int rr = upper_first ? (1-r) : r; + for( unsigned j=0; j<d_mbp_bounds[rr].size(); j++ ){ + if( (int)j!=best_used[rr] && ( !options::cbqiMidpoint() || d_mbp_vts_coeff[rr][1][j].isNull() ) ){ + Node val = getModelBasedProjectionValue( ci, pv, d_mbp_bounds[rr][j], rr==0, d_mbp_coeff[rr][j], pv_value, t_values[rr][j], sf.d_theta, + d_mbp_vts_coeff[rr][0][j], d_mbp_vts_coeff[rr][1][j] ); + if( !val.isNull() ){ + if( ci->doAddInstantiationInc( pv, val, d_mbp_coeff[rr][j], rr==0 ? 1 : -1, sf, effort ) ){ + return true; + } + } + } + } + } + } + } + return false; +} + +bool ArithInstantiator::needsPostProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { + return std::find( sf.d_has_coeff.begin(), sf.d_has_coeff.end(), pv )!=sf.d_has_coeff.end(); +} + +bool ArithInstantiator::postProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { + Assert( std::find( sf.d_has_coeff.begin(), sf.d_has_coeff.end(), pv )!=sf.d_has_coeff.end() ); + Assert( std::find( sf.d_vars.begin(), sf.d_vars.end(), pv )!=sf.d_vars.end() ); + unsigned index = std::find( sf.d_vars.begin(), sf.d_vars.end(), pv )-sf.d_vars.begin(); + Assert( !sf.d_coeff[index].isNull() ); + Trace("cbqi-inst-debug") << "Normalize substitution for " << sf.d_coeff[index] << " * " << sf.d_vars[index] << " = " << sf.d_subs[index] << std::endl; + Assert( sf.d_vars[index].getType().isInteger() ); + //must ensure that divisibility constraints are met + //solve updated rewritten equality for vars[index], if coefficient is one, then we are successful + Node eq_lhs = NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[index], sf.d_vars[index] ); + Node eq_rhs = sf.d_subs[index]; + Node eq = eq_lhs.eqNode( eq_rhs ); + eq = Rewriter::rewrite( eq ); + Trace("cbqi-inst-debug") << "...equality is " << eq << std::endl; + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( eq, msum ) ){ + Node veq; + if( QuantArith::isolate( sf.d_vars[index], msum, veq, EQUAL, true )!=0 ){ + Node veq_c; + if( veq[0]!=sf.d_vars[index] ){ + Node veq_v; + if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){ + Assert( veq_v==sf.d_vars[index] ); + } + } + sf.d_subs[index] = veq[1]; + if( !veq_c.isNull() ){ + sf.d_subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION_TOTAL, veq[1], veq_c ); + Trace("cbqi-inst-debug") << "...bound type is : " << sf.d_btyp[index] << std::endl; + //intger division rounding up if from a lower bound + if( sf.d_btyp[index]==1 && options::cbqiRoundUpLowerLia() ){ + sf.d_subs[index] = NodeManager::currentNM()->mkNode( PLUS, sf.d_subs[index], + NodeManager::currentNM()->mkNode( ITE, + NodeManager::currentNM()->mkNode( EQUAL, + NodeManager::currentNM()->mkNode( INTS_MODULUS_TOTAL, veq[1], veq_c ), + ci->getQuantifiersEngine()->getTermDatabase()->d_zero ), + ci->getQuantifiersEngine()->getTermDatabase()->d_zero, ci->getQuantifiersEngine()->getTermDatabase()->d_one ) + ); + } + } + Trace("cbqi-inst-debug") << "...normalize integers : " << sf.d_vars[index] << " -> " << sf.d_subs[index] << std::endl; + }else{ + Trace("cbqi-inst-debug") << "...failed to isolate." << std::endl; + return false; + } + }else{ + Trace("cbqi-inst-debug") << "...failed to get monomial sum." << std::endl; + return false; + } + return true; +} + +void DtInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { + +} + +Node DtInstantiator::solve_dt( Node v, Node a, Node b, Node sa, Node sb ) { + Trace("cbqi-inst-debug2") << "Solve dt : " << v << " " << a << " " << b << " " << sa << " " << sb << std::endl; + Node ret; + if( !a.isNull() && a==v ){ + ret = sb; + }else if( !b.isNull() && b==v ){ + ret = sa; + }else if( !a.isNull() && a.getKind()==APPLY_CONSTRUCTOR ){ + if( !b.isNull() && b.getKind()==APPLY_CONSTRUCTOR ){ + if( a.getOperator()==b.getOperator() ){ + for( unsigned i=0; i<a.getNumChildren(); i++ ){ + Node s = solve_dt( v, a[i], b[i], sa[i], sb[i] ); + if( !s.isNull() ){ + return s; + } + } + } + }else{ + unsigned cindex = Datatype::indexOf( a.getOperator().toExpr() ); + TypeNode tn = a.getType(); + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + for( unsigned i=0; i<a.getNumChildren(); i++ ){ + Node nn = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][i].getSelector() ), sb ); + Node s = solve_dt( v, a[i], Node::null(), sa[i], nn ); + if( !s.isNull() ){ + return s; + } + } + } + }else if( !b.isNull() && b.getKind()==APPLY_CONSTRUCTOR ){ + return solve_dt( v, b, a, sb, sa ); + } + if( !ret.isNull() ){ + //ensure does not contain + if( TermDb::containsTerm( ret, v ) ){ + ret = Node::null(); + } + } + return ret; +} + +bool DtInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ) { + Trace("cbqi-inst-debug") << "[2] try based on constructors in equivalence class." << std::endl; + //[2] look in equivalence class for a constructor + for( unsigned k=0; k<eqc.size(); k++ ){ + Node n = eqc[k]; + if( n.getKind()==APPLY_CONSTRUCTOR ){ + Trace("cbqi-inst-debug") << "...try based on constructor term " << n << std::endl; + std::vector< Node > children; + children.push_back( n.getOperator() ); + const Datatype& dt = ((DatatypeType)(d_type).toType()).getDatatype(); + unsigned cindex = Datatype::indexOf( n.getOperator().toExpr() ); + //now must solve for selectors applied to pv + for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){ + Node c = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][j].getSelector() ), pv ); + ci->pushStackVariable( c ); + children.push_back( c ); + } + Node val = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children ); + if( ci->doAddInstantiationInc( pv, val, Node::null(), 0, sf, effort ) ){ + return true; + }else{ + //cleanup + for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){ + ci->popStackVariable(); + } + break; + } + } + } + return false; +} + +bool DtInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) { + Node val = solve_dt( pv, terms[0], terms[1], terms[0], terms[1] ); + if( !val.isNull() ){ + Node veq_c; + if( ci->doAddInstantiationInc( pv, val, veq_c, 0, sf, effort ) ){ + return true; + } + } + return false; +} + +void EprInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { + d_equal_terms.clear(); +} + +bool EprInstantiator::processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort ) { + if( options::quantEprMatching() ){ + Assert( pv_coeff.isNull() ); + d_equal_terms.push_back( n ); + return false; + }else{ + return ci->doAddInstantiationInc( pv, n, pv_coeff, 0, sf, effort ); + } +} + +void EprInstantiator::computeMatchScore( CegInstantiator * ci, Node pv, Node catom, std::vector< Node >& arg_reps, TermArgTrie * tat, unsigned index, std::map< Node, int >& match_score ) { + if( index==catom.getNumChildren() ){ + Assert( tat->hasNodeData() ); + Node gcatom = tat->getNodeData(); + Trace("epr-inst") << "Matched : " << catom << " and " << gcatom << std::endl; + for( unsigned i=0; i<catom.getNumChildren(); i++ ){ + if( catom[i]==pv ){ + Trace("epr-inst") << "...increment " << gcatom[i] << std::endl; + match_score[gcatom[i]]++; + }else{ + //recursive matching + computeMatchScore( ci, pv, catom[i], gcatom[i], match_score ); + } + } + }else{ + std::map< TNode, TermArgTrie >::iterator it = tat->d_data.find( arg_reps[index] ); + if( it!=tat->d_data.end() ){ + computeMatchScore( ci, pv, catom, arg_reps, &it->second, index+1, match_score ); + } + } +} + +void EprInstantiator::computeMatchScore( CegInstantiator * ci, Node pv, Node catom, Node eqc, std::map< Node, int >& match_score ) { + if( inst::Trigger::isAtomicTrigger( catom ) && TermDb::containsTerm( catom, pv ) ){ + Trace("epr-inst") << "Find matches for " << catom << "..." << std::endl; + std::vector< Node > arg_reps; + for( unsigned j=0; j<catom.getNumChildren(); j++ ){ + arg_reps.push_back( ci->getQuantifiersEngine()->getMasterEqualityEngine()->getRepresentative( catom[j] ) ); + } + if( ci->getQuantifiersEngine()->getMasterEqualityEngine()->hasTerm( eqc ) ){ + Node rep = ci->getQuantifiersEngine()->getMasterEqualityEngine()->getRepresentative( eqc ); + Node op = ci->getQuantifiersEngine()->getTermDatabase()->getMatchOperator( catom ); + TermArgTrie * tat = ci->getQuantifiersEngine()->getTermDatabase()->getTermArgTrie( rep, op ); + Trace("epr-inst") << "EPR instantiation match term : " << catom << ", check ground terms=" << (tat!=NULL) << std::endl; + if( tat ){ + computeMatchScore( ci, pv, catom, arg_reps, tat, 0, match_score ); + } + } + } +} + +struct sortEqTermsMatch { + std::map< Node, int > d_match_score; + bool operator() (Node i, Node j) { + int match_score_i = d_match_score[i]; + int match_score_j = d_match_score[j]; + return match_score_i>match_score_j || ( match_score_i==match_score_j && i<j ); + } +}; + + +bool EprInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ) { + if( options::quantEprMatching() ){ + //heuristic for best matching constant + sortEqTermsMatch setm; + for( unsigned i=0; i<ci->getNumCEAtoms(); i++ ){ + Node catom = ci->getCEAtom( i ); + computeMatchScore( ci, pv, catom, catom, setm.d_match_score ); + } + //sort by match score + std::sort( d_equal_terms.begin(), d_equal_terms.end(), setm ); + Node pv_coeff; + for( unsigned i=0; i<d_equal_terms.size(); i++ ){ + if( ci->doAddInstantiationInc( pv, d_equal_terms[i], pv_coeff, 0, sf, effort ) ){ + return true; + } + } + } + return false; +} + +bool BvInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { + /* TODO: algebraic reasoning for bitvector instantiation + if( atom.getKind()==BITVECTOR_ULT || atom.getKind()==BITVECTOR_ULE ){ + for( unsigned t=0; t<2; t++ ){ + if( atom[t]==pv ){ + computeProgVars( atom[1-t] ); + if( d_inelig.find( atom[1-t] )==d_inelig.end() ){ + //only ground terms TODO: more + if( d_prog_var[atom[1-t]].empty() ){ + Node veq_c; + Node uval; + if( ( !pol && atom.getKind()==BITVECTOR_ULT ) || ( pol && atom.getKind()==BITVECTOR_ULE ) ){ + uval = atom[1-t]; + }else{ + uval = NodeManager::currentNM()->mkNode( (atom.getKind()==BITVECTOR_ULT)==(t==1) ? BITVECTOR_PLUS : BITVECTOR_SUB, atom[1-t], + bv::utils::mkConst(pvtn.getConst<BitVectorSize>(), 1) ); + } + if( doAddInstantiationInc( pv, uval, veq_c, 0, sf, effort ) ){ + return true; + } + } + } + } + } + } + */ + + return false; +} + + diff --git a/src/theory/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/ceg_t_instantiator.h new file mode 100644 index 000000000..2df7946d5 --- /dev/null +++ b/src/theory/quantifiers/ceg_t_instantiator.h @@ -0,0 +1,93 @@ +/********************* */ +/*! \file ceg_t_instantiator.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 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 theory-specific counterexample-guided quantifier instantiation + **/ + + +#include "cvc4_private.h" + +#ifndef __CVC4__CEG_T_INSTANTIATOR_H +#define __CVC4__CEG_T_INSTANTIATOR_H + +#include "theory/quantifiers/ceg_instantiator.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class ArithInstantiator : public Instantiator { +private: + Node d_vts_sym[2]; + std::vector< Node > d_mbp_bounds[2]; + std::vector< Node > d_mbp_coeff[2]; + std::vector< Node > d_mbp_vts_coeff[2][2]; + std::vector< Node > d_mbp_lit[2]; + int solve_arith( CegInstantiator * ci, Node v, Node atom, Node & veq_c, Node & val, Node& vts_coeff_inf, Node& vts_coeff_delta ); + Node getModelBasedProjectionValue( CegInstantiator * ci, Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ); +public: + ArithInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} + virtual ~ArithInstantiator(){} + void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); + bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } + bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ); + bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } + bool processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ); + bool processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort ); + bool needsPostProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); + bool postProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); + std::string identify() const { return "Arith"; } +}; + +class DtInstantiator : public Instantiator { +private: + Node solve_dt( Node v, Node a, Node b, Node sa, Node sb ); +public: + DtInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} + virtual ~DtInstantiator(){} + void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); + bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ); + bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } + bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ); + std::string identify() const { return "Dt"; } +}; + +class TermArgTrie; + +class EprInstantiator : public Instantiator { +private: + std::vector< Node > d_equal_terms; + void computeMatchScore( CegInstantiator * ci, Node pv, Node catom, std::vector< Node >& arg_reps, TermArgTrie * tat, unsigned index, std::map< Node, int >& match_score ); + void computeMatchScore( CegInstantiator * ci, Node pv, Node catom, Node eqc, std::map< Node, int >& match_score ); +public: + EprInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} + virtual ~EprInstantiator(){} + void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); + bool processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort ); + bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ); + std::string identify() const { return "Epr"; } +}; + +class BvInstantiator : public Instantiator { +public: + BvInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} + virtual ~BvInstantiator(){} + bool processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ); + bool useModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } + std::string identify() const { return "Bv"; } +}; + + +} +} +} + +#endif diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index f4eb67d74..11adc61fd 100755 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -84,6 +84,9 @@ d_notify( *this ), d_uequalityEngine(d_notify, c, "ConjectureGenerator::ee", false), d_ee_conjectures( c ){ d_fullEffortCount = 0; + d_conj_count = 0; + d_subs_confirmCount = 0; + d_subs_unkCount = 0; d_uequalityEngine.addFunctionKind( kind::APPLY_UF ); d_uequalityEngine.addFunctionKind( kind::APPLY_CONSTRUCTOR ); diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index be608aeaa..72057e734 100755 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -589,7 +589,7 @@ void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) { } -bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { +int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl; Assert( !d_qe->inConflict() ); if( optUseModel() ){ @@ -723,15 +723,15 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, if( temp.addEntry(fmfmc, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){ if( !exhaustiveInstantiate(fmfmc, f, d_quant_models[f].d_cond[j], j ) ){ //something went wrong, resort to exhaustive instantiation - return false; + return 0; } } } } } - return true; + return 1; }else{ - return false; + return 0; } } diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h index 411b7a5eb..7d21b4185 100755 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/full_model_check.h @@ -139,7 +139,7 @@ public: void debugPrintCond(const char * tr, Node n, bool dispStar = false); void debugPrint(const char * tr, Node n, bool dispStar = false); - bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ); + int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ); Node getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix ); diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 7e5424d9c..12e15d353 100755 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -258,7 +258,11 @@ void InstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std:: } } }else{ - insts.push_back( qe->getInstantiation( q, terms, true ) ); + if( hasInstLemma() ){ + insts.push_back( getInstLemma() ); + }else{ + insts.push_back( qe->getInstantiation( q, terms, true ) ); + } } }else{ for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){ @@ -428,13 +432,17 @@ void CDInstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std if( terms.size()==q[0].getNumChildren() ){ if( useActive ){ if( hasInstLemma() ){ - Node lem; + Node lem = getInstLemma(); if( std::find( active.begin(), active.end(), lem )!=active.end() ){ insts.push_back( lem ); } } }else{ - insts.push_back( qe->getInstantiation( q, terms, true ) ); + if( hasInstLemma() ){ + insts.push_back( getInstLemma() ); + }else{ + insts.push_back( qe->getInstantiation( q, terms, true ) ); + } } }else{ for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){ diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index b3df9ca5d..2a940f1fd 100755 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -388,23 +388,6 @@ int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, Quantif return addedLemmas; } -int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){ - Assert( options::eagerInstQuant() ); - if( !d_match_pattern.isNull() ){ - InstMatch m( f ); - if( getMatch( f, t, m, qe ) ){ - if( qe->addInstantiation( f, m ) ){ - return 1; - } - } - }else{ - for( unsigned i=0; i<d_children.size(); i++ ){ - d_children[i]->addTerm( f, t, qe ); - } - } - return 0; -} - InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( Node q, Node pat, QuantifiersEngine* qe ) { std::vector< Node > pats; @@ -716,22 +699,6 @@ void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe, } } -int InstMatchGeneratorMulti::addTerm( Node q, Node t, QuantifiersEngine* qe ){ - Assert( options::eagerInstQuant() ); - int addedLemmas = 0; - for( int i=0; i<(int)d_children.size(); i++ ){ - Node t_op = qe->getTermDatabase()->getMatchOperator( t ); - if( ((InstMatchGenerator*)d_children[i])->d_match_pattern_op==t_op ){ - InstMatch m( q ); - //if it produces a match, then process it with the rest - if( ((InstMatchGenerator*)d_children[i])->getMatch( q, t, m, qe ) ){ - processNewMatch( qe, m, i, addedLemmas ); - } - } - } - return addedLemmas; -} - InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node q, Node pat, QuantifiersEngine* qe ) : d_f( q ), d_match_pattern( pat ) { if( d_match_pattern.getKind()==NOT ){ d_match_pattern = d_match_pattern[0]; @@ -774,17 +741,19 @@ int InstMatchGeneratorSimple::addInstantiations( Node q, InstMatch& baseMatch, Q Node r = qe->getEqualityQuery()->getRepresentative( d_eqc ); //iterate over all classes except r tat = qe->getTermDatabase()->getTermArgTrie( Node::null(), d_op ); - for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){ - if( it->first!=r ){ - InstMatch m( q ); - m.add( baseMatch ); - addInstantiations( m, qe, addedLemmas, 0, &(it->second) ); - if( qe->inConflict() ){ - break; + if( tat ){ + for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){ + if( it->first!=r ){ + InstMatch m( q ); + m.add( baseMatch ); + addInstantiations( m, qe, addedLemmas, 0, &(it->second) ); + if( qe->inConflict() ){ + break; + } } } + tat = NULL; } - tat = NULL; } } Debug("simple-trigger-debug") << "Adding instantiations based on " << tat << " from " << d_op << " " << d_eqc << std::endl; @@ -841,20 +810,6 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin } } -int InstMatchGeneratorSimple::addTerm( Node q, Node t, QuantifiersEngine* qe ){ - //for eager instantiation only - Assert( options::eagerInstQuant() ); - InstMatch m( q ); - for( unsigned i=0; i<t.getNumChildren(); i++ ){ - if( d_match_pattern[i].getKind()==INST_CONSTANT ){ - m.setValue(d_var_num[i], t[i]); - }else if( !qe->getEqualityQuery()->areEqual( d_match_pattern[i], t[i] ) ){ - return 0; - } - } - return qe->addInstantiation( q, m ) ? 1 : 0; -} - int InstMatchGeneratorSimple::getActiveScore( QuantifiersEngine * qe ) { Node f = qe->getTermDatabase()->getMatchOperator( d_match_pattern ); unsigned ngt = qe->getTermDatabase()->getNumGroundTerms( f ); diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h index 65c5a1427..c238e3c4e 100755 --- a/src/theory/quantifiers/inst_match_generator.h +++ b/src/theory/quantifiers/inst_match_generator.h @@ -42,8 +42,6 @@ public: virtual bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) = 0; /** add instantiations directly */ virtual int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0; - /** add ground term t, called when t is added to term db */ - virtual int addTerm( Node q, Node t, QuantifiersEngine* qe ) { return 0; } /** set active add */ virtual void setActiveAdd( bool val ) {} /** get active score */ @@ -113,8 +111,6 @@ public: bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ); /** add instantiations */ int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ); - /** add ground term t */ - int addTerm( Node q, Node t, QuantifiersEngine* qe ); bool d_active_add; void setActiveAdd( bool val ); @@ -205,8 +201,6 @@ public: bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) { return false; } /** add instantiations */ int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ); - /** add ground term t */ - int addTerm( Node q, Node t, QuantifiersEngine* qe ); };/* class InstMatchGeneratorMulti */ /** smart (single)-trigger implementation */ @@ -240,8 +234,6 @@ public: bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) { return false; } /** add instantiations */ int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ); - /** add ground term t, possibly add instantiations */ - int addTerm( Node q, Node t, QuantifiersEngine* qe ); /** get active score */ int getActiveScore( QuantifiersEngine * qe ); };/* class InstMatchGeneratorSimple */ diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp index 41c9c40c8..1f68fb787 100755 --- a/src/theory/quantifiers/inst_propagator.cpp +++ b/src/theory/quantifiers/inst_propagator.cpp @@ -597,6 +597,8 @@ void InstPropagator::InstInfo::init( Node q, Node lem, std::vector< Node >& term InstPropagator::InstPropagator( QuantifiersEngine* qe ) : d_qe( qe ), d_notify(*this), d_qy( qe ){ + d_icount = 1; + d_conflict = false; } bool InstPropagator::reset( Theory::Effort e ) { diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 523d868b5..ac6e1edbe 100755 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -21,6 +21,7 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/trigger.h" +#include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/theory_engine.h" using namespace std; @@ -34,9 +35,13 @@ using namespace CVC4::theory::arith; #define ARITH_INSTANTIATOR_USE_MINUS_DELTA InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe ) - : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ) + : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ), +d_elim_quants( qe->getSatContext() ), +d_nested_qe_waitlist_size( qe->getUserContext() ), +d_nested_qe_waitlist_proc( qe->getUserContext() ) //, d_added_inst( qe->getUserContext() ) { + d_qid_count = 0; } InstStrategyCbqi::~InstStrategyCbqi() throw(){} @@ -55,34 +60,117 @@ unsigned InstStrategyCbqi::needsModel( Theory::Effort e ) { return QuantifiersEngine::QEFFORT_NONE; } +bool InstStrategyCbqi::registerCbqiLemma( Node q ) { + if( !hasAddedCbqiLemma( q ) ){ + d_added_cbqi_lemma.insert( q ); + Trace("cbqi-debug") << "Do cbqi for " << q << std::endl; + //add cbqi lemma + //get the counterexample literal + Node ceLit = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q ); + Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( q ); + if( !ceBody.isNull() ){ + //add counterexample lemma + Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() ); + //require any decision on cel to be phase=true + d_quantEngine->addRequirePhase( ceLit, true ); + Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl; + //add counterexample lemma + lem = Rewriter::rewrite( lem ); + Trace("cbqi-lemma") << "Counterexample lemma : " << lem << std::endl; + registerCounterexampleLemma( q, lem ); + + //totality lemmas for EPR + QuantEPR * qepr = d_quantEngine->getQuantEPR(); + if( qepr!=NULL ){ + for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ + TypeNode tn = q[0][i].getType(); + if( tn.isSort() ){ + if( qepr->isEPR( tn ) ){ + //add totality lemma + std::map< TypeNode, std::vector< Node > >::iterator itc = qepr->d_consts.find( tn ); + if( itc!=qepr->d_consts.end() ){ + Assert( !itc->second.empty() ); + Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i ); + std::vector< Node > disj; + for( unsigned j=0; j<itc->second.size(); j++ ){ + disj.push_back( ic.eqNode( itc->second[j] ) ); + } + Node tlem = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj ); + Trace("cbqi-lemma") << "EPR totality lemma : " << tlem << std::endl; + d_quantEngine->getOutputChannel().lemma( tlem ); + }else{ + Assert( false ); + } + }else{ + Assert( !options::cbqiAll() ); + } + } + } + } + + //compute dependencies between quantified formulas + if( options::cbqiLitDepend() || options::cbqiInnermost() ){ + std::vector< Node > ics; + TermDb::computeVarContains( q, ics ); + d_parent_quant[q].clear(); + d_children_quant[q].clear(); + std::vector< Node > dep; + for( unsigned i=0; i<ics.size(); i++ ){ + Node qi = ics[i].getAttribute(InstConstantAttribute()); + if( std::find( d_parent_quant[q].begin(), d_parent_quant[q].end(), qi )==d_parent_quant[q].end() ){ + d_parent_quant[q].push_back( qi ); + d_children_quant[qi].push_back( q ); + Node qicel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( qi ); + dep.push_back( qi ); + dep.push_back( qicel ); + } + } + if( !dep.empty() ){ + Node dep_lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, ceLit, NodeManager::currentNM()->mkNode( kind::AND, dep ) ); + Trace("cbqi-lemma") << "Counterexample dependency lemma : " << dep_lemma << std::endl; + d_quantEngine->getOutputChannel().lemma( dep_lemma ); + } + } + + //must register all sub-quantifiers of counterexample lemma, register their lemmas + std::vector< Node > quants; + TermDb::computeQuantContains( lem, quants ); + for( unsigned i=0; i<quants.size(); i++ ){ + if( doCbqi( quants[i] ) ){ + registerCbqiLemma( quants[i] ); + } + if( options::cbqiNestedQE() ){ + //record these as counterexample quantifiers + QAttributes qa; + TermDb::computeQuantAttributes( quants[i], qa ); + if( !qa.d_qid_num.isNull() ){ + d_id_to_ce_quant[ qa.d_qid_num ] = quants[i]; + d_ce_quant_to_id[ quants[i] ] = qa.d_qid_num; + Trace("cbqi-nqe") << "CE quant id = " << qa.d_qid_num << " is " << quants[i] << std::endl; + } + } + } + } + return true; + }else{ + return false; + } +} + void InstStrategyCbqi::reset_round( Theory::Effort effort ) { d_cbqi_set_quant_inactive = false; d_incomplete_check = false; + d_active_quant.clear(); //check if any cbqi lemma has not been added yet for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine if( doCbqi( q ) ){ - if( !hasAddedCbqiLemma( q ) ){ - d_added_cbqi_lemma.insert( q ); - Trace("cbqi") << "Do cbqi for " << q << std::endl; - //add cbqi lemma - //get the counterexample literal - Node ceLit = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q ); - Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( q ); - if( !ceBody.isNull() ){ - //add counterexample lemma - Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() ); - //require any decision on cel to be phase=true - d_quantEngine->addRequirePhase( ceLit, true ); - Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl; - //add counterexample lemma - lem = Rewriter::rewrite( lem ); - Trace("cbqi") << "Counterexample lemma : " << lem << std::endl; - registerCounterexampleLemma( q, lem ); - } + if( registerCbqiLemma( q ) ){ + Debug("cbqi-debug") << "Registered cbqi lemma." << std::endl; //set inactive the quantified formulas whose CE literals are asserted false }else if( d_quantEngine->getModel()->isQuantifierActive( q ) ){ + d_active_quant[q] = true; Debug("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl; Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q ); bool value; @@ -92,8 +180,24 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) { if( d_quantEngine->getValuation().isDecision( cel ) ){ Trace("cbqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl; }else{ + Trace("cbqi") << "Inactive : " << q << std::endl; d_quantEngine->getModel()->setQuantifierActive( q, false ); d_cbqi_set_quant_inactive = true; + d_active_quant.erase( q ); + d_elim_quants.insert( q ); + Trace("cbqi-nqe") << "Inactive, waitlist proc/size = " << d_nested_qe_waitlist_proc[q].get() << "/" << d_nested_qe_waitlist_size[q].get() << std::endl; + //process from waitlist + while( d_nested_qe_waitlist_proc[q]<d_nested_qe_waitlist_size[q] ){ + int index = d_nested_qe_waitlist_proc[q]; + Assert( index>=0 ); + Assert( index<(int)d_nested_qe_waitlist[q].size() ); + Node nq = d_nested_qe_waitlist[q][index]; + Node nqeqn = doNestedQENode( d_nested_qe_info[nq].d_q, q, nq, d_nested_qe_info[nq].d_inst_terms, d_nested_qe_info[nq].d_doVts ); + Node dqelem = nq.iffNode( nqeqn ); + Trace("cbqi-lemma") << "Delayed nested quantifier elimination lemma : " << dqelem << std::endl; + d_quantEngine->getOutputChannel().lemma( dqelem ); + d_nested_qe_waitlist_proc[q] = index + 1; + } } } }else{ @@ -102,6 +206,34 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) { } } } + + //refinement: only consider innermost active quantified formulas + if( options::cbqiInnermost() ){ + if( !d_children_quant.empty() && !d_active_quant.empty() ){ + Trace("cbqi-debug") << "Find non-innermost quantifiers..." << std::endl; + std::vector< Node > ninner; + for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){ + std::map< Node, std::vector< Node > >::iterator itc = d_children_quant.find( it->first ); + if( itc!=d_children_quant.end() ){ + for( unsigned j=0; j<itc->second.size(); j++ ){ + if( d_active_quant.find( itc->second[j] )!=d_active_quant.end() ){ + Trace("cbqi-debug") << "Do not consider " << it->first << " since it is not innermost (" << itc->second[j] << std::endl; + ninner.push_back( it->first ); + break; + } + } + } + } + Trace("cbqi-debug") << "Found " << ninner.size() << " non-innermost." << std::endl; + for( unsigned i=0; i<ninner.size(); i++ ){ + Assert( d_active_quant.find( ninner[i] )!=d_active_quant.end() ); + d_active_quant.erase( ninner[i] ); + } + Assert( !d_active_quant.empty() ); + Trace("cbqi-debug") << "...done removing." << std::endl; + } + } + processResetInstantiationRound( effort ); } @@ -115,13 +247,20 @@ void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) { } unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting(); for( int ee=0; ee<=1; ee++ ){ - for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ - Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); - if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ + //for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ + // Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); + // if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ + for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){ + Node q = it->first; + Trace("cbqi") << "CBQI : Process quantifier " << q[0] << " at effort " << ee << std::endl; + if( d_nested_qe.find( q )==d_nested_qe.end() ){ process( q, e, ee ); if( d_quantEngine->inConflict() ){ break; } + }else{ + Trace("cbqi-warn") << "CBQI : Cannot process already eliminated quantified formula " << q << std::endl; + Assert( false ); } } if( d_quantEngine->inConflict() || d_quantEngine->getNumLemmasWaiting()>lastWaiting ){ @@ -146,11 +285,88 @@ bool InstStrategyCbqi::checkComplete() { } } +bool InstStrategyCbqi::checkCompleteFor( Node q ) { + std::map< Node, int >::iterator it = d_do_cbqi.find( q ); + if( it!=d_do_cbqi.end() ){ + return it->second>0; + }else{ + return false; + } +} + +Node InstStrategyCbqi::getIdMarkedQuantNode( Node n, std::map< Node, Node >& visited ){ + std::map< Node, Node >::iterator it = visited.find( n ); + if( it==visited.end() ){ + Node ret = n; + if( n.getKind()==FORALL ){ + QAttributes qa; + TermDb::computeQuantAttributes( n, qa ); + if( qa.d_qid_num.isNull() ){ + std::vector< Node > rc; + rc.push_back( n[0] ); + rc.push_back( getIdMarkedQuantNode( n[1], visited ) ); + Node avar = NodeManager::currentNM()->mkSkolem( "id", NodeManager::currentNM()->booleanType() ); + QuantIdNumAttribute ida; + avar.setAttribute(ida,d_qid_count); + d_qid_count++; + std::vector< Node > iplc; + iplc.push_back( NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, avar ) ); + if( n.getNumChildren()==3 ){ + for( unsigned i=0; i<n[2].getNumChildren(); i++ ){ + iplc.push_back( n[2][i] ); + } + } + rc.push_back( NodeManager::currentNM()->mkNode( INST_PATTERN_LIST, iplc ) ); + ret = NodeManager::currentNM()->mkNode( FORALL, rc ); + } + }else if( n.getNumChildren()>0 ){ + std::vector< Node > children; + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.push_back( n.getOperator() ); + } + bool childChanged = false; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + Node nc = getIdMarkedQuantNode( n[i], visited ); + childChanged = childChanged || nc!=n[i]; + children.push_back( nc ); + } + if( childChanged ){ + ret = NodeManager::currentNM()->mkNode( n.getKind(), children ); + } + } + visited[n] = ret; + return ret; + }else{ + return it->second; + } +} + void InstStrategyCbqi::preRegisterQuantifier( Node q ) { if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){ - if( !options::cbqiAll() && !options::cbqiSplx() ){ + if( d_do_cbqi[q]==2 ){ //take full ownership of the quantified formula d_quantEngine->setOwner( q, this ); + + //mark all nested quantifiers with id + if( options::cbqiNestedQE() ){ + std::map< Node, Node > visited; + Node mq = getIdMarkedQuantNode( q[1], visited ); + if( mq!=q[1] ){ + //do not do cbqi + d_do_cbqi[q] = false; + //instead do reduction + std::vector< Node > qqc; + qqc.push_back( q[0] ); + qqc.push_back( mq ); + if( q.getNumChildren()==3 ){ + qqc.push_back( q[2] ); + } + Node qq = NodeManager::currentNM()->mkNode( FORALL, qqc ); + Node mlem = NodeManager::currentNM()->mkNode( IMPLIES, q, qq ); + Trace("cbqi-lemma") << "Mark quant id lemma : " << mlem << std::endl; + d_quantEngine->getOutputChannel().lemma( mlem ); + } + } } } } @@ -159,6 +375,98 @@ void InstStrategyCbqi::registerQuantifier( Node q ) { } +Node InstStrategyCbqi::doNestedQENode( Node q, Node ceq, Node n, std::vector< Node >& inst_terms, bool doVts ) { + // there is a nested quantified formula (forall y. nq[y,x]) such that + // q is (forall y. nq[y,t]) for ground terms t, + // ceq is (forall y. nq[y,e]) for CE variables e. + // we call this function when we know (forall y. nq[y,e]) is equivalent to quantifier-free formula C[e]. + // in this case, q is equivalent to the quantifier-free formula C[t]. + if( d_nested_qe.find( ceq )==d_nested_qe.end() ){ + d_nested_qe[ceq] = d_quantEngine->getInstantiatedConjunction( ceq ); + Trace("cbqi-nqe") << "CE quantifier elimination : " << std::endl; + Trace("cbqi-nqe") << " " << ceq << std::endl; + Trace("cbqi-nqe") << " " << d_nested_qe[ceq] << std::endl; + //should not contain quantifiers + Assert( !QuantifiersRewriter::containsQuantifiers( d_nested_qe[ceq] ) ); + } + Assert( d_quantEngine->getTermDatabase()->d_inst_constants[q].size()==inst_terms.size() ); + //replace inst constants with instantiation + Node ret = d_nested_qe[ceq].substitute( d_quantEngine->getTermDatabase()->d_inst_constants[q].begin(), + d_quantEngine->getTermDatabase()->d_inst_constants[q].end(), + inst_terms.begin(), inst_terms.end() ); + if( doVts ){ + //do virtual term substitution + ret = Rewriter::rewrite( ret ); + ret = d_quantEngine->getTermDatabase()->rewriteVtsSymbols( ret ); + } + Trace("cbqi-nqe") << "Nested quantifier elimination: " << std::endl; + Trace("cbqi-nqe") << " " << n << std::endl; + Trace("cbqi-nqe") << " " << ret << std::endl; + return ret; +} + +Node InstStrategyCbqi::doNestedQERec( Node q, Node n, std::map< Node, Node >& visited, std::vector< Node >& inst_terms, bool doVts ) { + if( visited.find( n )==visited.end() ){ + Node ret = n; + if( n.getKind()==FORALL ){ + QAttributes qa; + TermDb::computeQuantAttributes( n, qa ); + if( !qa.d_qid_num.isNull() ){ + //if it has an id, check whether we have done quantifier elimination for this id + std::map< Node, Node >::iterator it = d_id_to_ce_quant.find( qa.d_qid_num ); + if( it!=d_id_to_ce_quant.end() ){ + Node ceq = it->second; + bool doNestedQe = d_elim_quants.contains( ceq ); + if( doNestedQe ){ + ret = doNestedQENode( q, ceq, n, inst_terms, doVts ); + }else{ + Trace("cbqi-nqe") << "Add to nested qe waitlist : " << std::endl; + Node nr = Rewriter::rewrite( n ); + Trace("cbqi-nqe") << " " << ceq << std::endl; + Trace("cbqi-nqe") << " " << nr << std::endl; + int wlsize = d_nested_qe_waitlist_size[ceq] + 1; + d_nested_qe_waitlist_size[ceq] = wlsize; + if( wlsize<(int)d_nested_qe_waitlist[ceq].size() ){ + d_nested_qe_waitlist[ceq][wlsize] = nr; + }else{ + d_nested_qe_waitlist[ceq].push_back( nr ); + } + d_nested_qe_info[nr].d_q = q; + d_nested_qe_info[nr].d_inst_terms.clear(); + d_nested_qe_info[nr].d_inst_terms.insert( d_nested_qe_info[nr].d_inst_terms.end(), inst_terms.begin(), inst_terms.end() ); + d_nested_qe_info[nr].d_doVts = doVts; + //TODO: ensure this holds by restricting prenex when cbqiNestedQe is true. + Assert( !options::cbqiInnermost() ); + } + } + } + }else if( n.getNumChildren()>0 ){ + std::vector< Node > children; + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.push_back( n.getOperator() ); + } + bool childChanged = false; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + Node nc = doNestedQERec( q, n[i], visited, inst_terms, doVts ); + childChanged = childChanged || nc!=n[i]; + children.push_back( nc ); + } + if( childChanged ){ + ret = NodeManager::currentNM()->mkNode( n.getKind(), children ); + } + } + visited[n] = ret; + return ret; + }else{ + return n; + } +} + +Node InstStrategyCbqi::doNestedQE( Node q, std::vector< Node >& inst_terms, Node lem, bool doVts ) { + std::map< Node, Node > visited; + return doNestedQERec( q, lem, visited, inst_terms, doVts ); +} + void InstStrategyCbqi::registerCounterexampleLemma( Node q, Node lem ){ Trace("cbqi-debug") << "Counterexample lemma : " << lem << std::endl; d_quantEngine->addLemma( lem, false ); @@ -187,57 +495,91 @@ bool InstStrategyCbqi::hasNonCbqiOperator( Node n, std::map< Node, bool >& visit } return false; } -bool InstStrategyCbqi::hasNonCbqiVariable( Node q ){ +int InstStrategyCbqi::hasNonCbqiVariable( Node q ){ + int hmin = 1; for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ TypeNode tn = q[0][i].getType(); - if( !tn.isInteger() && !tn.isReal() && !tn.isBoolean() && !tn.isBitVector() ){ - if( options::cbqiSplx() ){ - return true; - }else{ - //datatypes supported in new implementation - if( !tn.isDatatype() ){ - return true; - } + int handled = -1; + if( tn.isInteger() || tn.isReal() || tn.isBoolean() || tn.isBitVector() ){ + handled = 0; + }else if( tn.isDatatype() ){ + handled = 0; + }else if( tn.isSort() ){ + QuantEPR * qepr = d_quantEngine->getQuantEPR(); + if( qepr!=NULL ){ + handled = qepr->isEPR( tn ) ? 1 : -1; } } + if( handled==-1 ){ + return -1; + }else if( handled<hmin ){ + hmin = handled; + } } - return false; + return hmin; } bool InstStrategyCbqi::doCbqi( Node q ){ - std::map< Node, bool >::iterator it = d_do_cbqi.find( q ); + std::map< Node, int >::iterator it = d_do_cbqi.find( q ); if( it==d_do_cbqi.end() ){ - bool ret = false; - if( d_quantEngine->getTermDatabase()->isQAttrQuantElim( q ) ){ - ret = true; - }else{ + int ret = 2; + if( !d_quantEngine->getTermDatabase()->isQAttrQuantElim( q ) ){ //if has an instantiation pattern, don't do it if( q.getNumChildren()==3 && options::eMatching() && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){ - ret = false; - }else{ - if( options::cbqiAll() ){ - ret = true; - }else{ - //if quantifier has a non-arithmetic variable, then do not use cbqi - //if quantifier has an APPLY_UF term, then do not use cbqi - //Node cb = d_quantEngine->getTermDatabase()->getInstConstantBody( q ); + for( unsigned i=0; i<q[2].getNumChildren(); i++ ){ + if( q[2][i].getKind()==INST_PATTERN ){ + ret = 0; + } + } + } + if( ret!=0 ){ + //if quantifier has a non-handled variable, then do not use cbqi + //if quantifier has an APPLY_UF term, then do not use cbqi unless EPR + int ncbqiv = hasNonCbqiVariable( q ); + if( ncbqiv==0 || ncbqiv==1 ){ std::map< Node, bool > visited; - ret = !hasNonCbqiVariable( q ) && !hasNonCbqiOperator( q[1], visited ); + if( hasNonCbqiOperator( q[1], visited ) ){ + if( ncbqiv==1 ){ + //all variables are fully handled, this implies this will be handlable regardless of body (e.g. for EPR) + // so, try but not exclusively + ret = 1; + }else{ + //cannot be handled + ret = 0; + } + } + }else{ + // unhandled variable type + ret = 0; + } + if( ret==0 && options::cbqiAll() ){ + //try but not exclusively + ret = 1; } } } - Trace("cbqi") << "doCbqi " << q << " returned " << ret << std::endl; + Trace("cbqi-quant") << "doCbqi " << q << " returned " << ret << std::endl; d_do_cbqi[q] = ret; - return ret; + return ret!=0; }else{ - return it->second; + return it->second!=0; } } -Node InstStrategyCbqi::getNextDecisionRequest(){ - // all counterexample literals that are not asserted - for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ - Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); +Node InstStrategyCbqi::getNextDecisionRequestProc( Node q, std::map< Node, bool >& proc ) { + if( proc.find( q )==proc.end() ){ + proc[q] = true; + //first check children + std::map< Node, std::vector< Node > >::iterator itc = d_children_quant.find( q ); + if( itc!=d_children_quant.end() ){ + for( unsigned j=0; j<itc->second.size(); j++ ){ + Node d = getNextDecisionRequestProc( itc->second[j], proc ); + if( !d.isNull() ){ + return d; + } + } + } + //then check self if( hasAddedCbqiLemma( q ) ){ Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q ); bool value; @@ -245,328 +587,21 @@ Node InstStrategyCbqi::getNextDecisionRequest(){ Trace("cbqi-dec") << "CBQI: get next decision " << cel << std::endl; return cel; } - } + } } - return Node::null(); + return Node::null(); } - - - -//old implementation - -InstStrategySimplex::InstStrategySimplex( TheoryArith* th, QuantifiersEngine* ie ) : InstStrategyCbqi( ie ), d_th( th ), d_counter( 0 ){ - d_negOne = NodeManager::currentNM()->mkConst( Rational(-1) ); - d_zero = NodeManager::currentNM()->mkConst( Rational(0) ); -} - -void getInstantiationConstants( Node n, std::vector< Node >& ics ){ - if( n.getKind()==INST_CONSTANT ){ - if( std::find( ics.begin(), ics.end(), n )==ics.end() ){ - ics.push_back( n ); - } - }else{ - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - getInstantiationConstants( n[i], ics ); - } - } -} - - -void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort ){ - Debug("quant-arith") << "Setting up simplex for instantiator... " << std::endl; - d_quantActive.clear(); - d_instRows.clear(); - d_tableaux_term.clear(); - d_tableaux.clear(); - d_ceTableaux.clear(); - //search for instantiation rows in simplex tableaux - ArithVariables& avnm = d_th->d_internal->d_partialModel; - ArithVariables::var_iterator vi, vend; - for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){ - ArithVar x = *vi; - Node n = avnm.asNode(x); - - //collect instantiation constants - std::vector< Node > ics; - getInstantiationConstants( n, ics ); - for( unsigned i=0; i<ics.size(); i++ ){ - NodeBuilder<> t(kind::PLUS); - if( n.getKind()==PLUS ){ - for( int j=0; j<(int)n.getNumChildren(); j++ ){ - addTermToRow( ics[i], x, n[j], t ); - } - }else{ - addTermToRow( ics[i], x, n, t ); - } - d_instRows[ics[i]].push_back( x ); - //this theory has constraints from f - Node f = TermDb::getInstConstAttr(ics[i]); - Debug("quant-arith") << "Has constraints from " << f << std::endl; - //set that we should process it - d_quantActive[ f ] = true; - //set tableaux term - if( t.getNumChildren()==0 ){ - d_tableaux_term[ics[i]][x] = d_zero; - }else if( t.getNumChildren()==1 ){ - d_tableaux_term[ics[i]][x] = t.getChild( 0 ); - }else{ - d_tableaux_term[ics[i]][x] = t; - } - } - } - //print debug - if( Debug.isOn("quant-arith-debug") ){ - Debug("quant-arith-debug") << std::endl; - debugPrint( "quant-arith-debug" ); - } - d_counter++; -} - -void InstStrategySimplex::addTermToRow( Node i, ArithVar x, Node n, NodeBuilder<>& t ){ - if( n.getKind()==MULT ){ - if( TermDb::hasInstConstAttr(n[1]) && n[0].getKind()==CONST_RATIONAL ){ - if( n[1]==i ){ - d_ceTableaux[i][x][ n[1] ] = n[0]; - }else{ - d_tableaux_ce_term[i][x][ n[1] ] = n[0]; - } - }else{ - d_tableaux[i][x][ n[1] ] = n[0]; - t << n; - } - }else{ - if( TermDb::hasInstConstAttr(n) ){ - if( n==i ){ - d_ceTableaux[i][x][ n ] = Node::null(); - }else{ - d_tableaux_ce_term[i][x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) ); - } - }else{ - d_tableaux[i][x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) ); - t << n; - } - } -} - -void InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){ - if( e==0 ){ - if( d_quantActive.find( f )!=d_quantActive.end() ){ - //the point instantiation - InstMatch m_point( f ); - bool m_point_valid = true; - int lem = 0; - //scan over all instantiation rows - for( unsigned i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){ - Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ); - Debug("quant-arith-simplex") << "InstStrategySimplex check " << ic << ", rows = " << d_instRows[ic].size() << std::endl; - for( unsigned j=0; j<d_instRows[ic].size(); j++ ){ - ArithVar x = d_instRows[ic][j]; - if( !d_ceTableaux[ic][x].empty() ){ - if( Debug.isOn("quant-arith-simplex") ){ - Debug("quant-arith-simplex") << "--- Check row " << ic << " " << x << std::endl; - Debug("quant-arith-simplex") << " "; - for( std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin(); it != d_ceTableaux[ic][x].end(); ++it ){ - if( it!=d_ceTableaux[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; } - Debug("quant-arith-simplex") << it->first << " * " << it->second; - } - Debug("quant-arith-simplex") << " = "; - Node v = getTableauxValue( x, false ); - Debug("quant-arith-simplex") << v << std::endl; - Debug("quant-arith-simplex") << " term : " << d_tableaux_term[ic][x] << std::endl; - Debug("quant-arith-simplex") << " ce-term : "; - for( std::map< Node, Node >::iterator it = d_tableaux_ce_term[ic][x].begin(); it != d_tableaux_ce_term[ic][x].end(); it++ ){ - if( it!=d_tableaux_ce_term[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; } - Debug("quant-arith-simplex") << it->first << " * " << it->second; - } - Debug("quant-arith-simplex") << std::endl; - } - //instantiation row will be A*e + B*t = beta, - // where e is a vector of terms , and t is vector of ground terms. - // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant - // We will construct the term ( beta - B*t)/coeff to use for e_i. - InstMatch m( f ); - for( unsigned k=0; k<f[0].getNumChildren(); k++ ){ - if( f[0][k].getType().isInteger() ){ - m.setValue( k, d_zero ); - } - } - //By default, choose the first instantiation constant to be e_i. - Node var = d_ceTableaux[ic][x].begin()->first; - //if it is integer, we need to find variable with coefficent +/- 1 - if( var.getType().isInteger() ){ - std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin(); - while( !var.isNull() && !d_ceTableaux[ic][x][var].isNull() && d_ceTableaux[ic][x][var]!=d_negOne ){ - ++it; - if( it==d_ceTableaux[ic][x].end() ){ - var = Node::null(); - }else{ - var = it->first; - } - } - //Otherwise, try one that divides all ground term coefficients? - // Might be futile, if rewrite ensures gcd of coeffs is 1. - } - if( !var.isNull() ){ - //add to point instantiation if applicable - if( d_tableaux_ce_term[ic][x].empty() && d_tableaux_term[ic][x]==d_zero ){ - Debug("quant-arith-simplex") << "*** Row contributes to point instantiation." << std::endl; - Node v = getTableauxValue( x, false ); - if( !var.getType().isInteger() || v.getType().isInteger() ){ - m_point.setValue( i, v ); - }else{ - m_point_valid = false; - } - } - Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl; - if( doInstantiation( f, ic, d_tableaux_term[ic][x], x, m, var ) ){ - lem++; - } - }else{ - Debug("quant-arith-simplex") << "Could not find var." << std::endl; - } - } - } - } - if( lem==0 && m_point_valid ){ - if( d_quantEngine->addInstantiation( f, m_point ) ){ - Debug("quant-arith-simplex") << "...added point instantiation." << std::endl; - } - } - } - } -} - - -void InstStrategySimplex::debugPrint( const char* c ){ - ArithVariables& avnm = d_th->d_internal->d_partialModel; - ArithVariables::var_iterator vi, vend; - for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){ - ArithVar x = *vi; - Node n = avnm.asNode(x); - //if( ((TheoryArith*)getTheory())->d_partialModel.hasEitherBound( x ) ){ - Debug(c) << x << " : " << n << ", bounds = "; - if( d_th->d_internal->d_partialModel.hasLowerBound( x ) ){ - Debug(c) << d_th->d_internal->d_partialModel.getLowerBound( x ); - }else{ - Debug(c) << "-infty"; - } - Debug(c) << " <= "; - Debug(c) << d_th->d_internal->d_partialModel.getAssignment( x ); - Debug(c) << " <= "; - if( d_th->d_internal->d_partialModel.hasUpperBound( x ) ){ - Debug(c) << d_th->d_internal->d_partialModel.getUpperBound( x ); - }else{ - Debug(c) << "+infty"; - } - Debug(c) << std::endl; - //Debug(c) << " Term = " << d_tableaux_term[x] << std::endl; - //Debug(c) << " "; - //for( std::map< Node, Node >::iterator it2 = d_tableaux[x].begin(); it2 != d_tableaux[x].end(); ++it2 ){ - // Debug(c) << "( " << it2->first << ", " << it2->second << " ) "; - //} - //for( std::map< Node, Node >::iterator it2 = d_ceTableaux[x].begin(); it2 != d_ceTableaux[x].end(); ++it2 ){ - // Debug(c) << "(CE)( " << it2->first << ", " << it2->second << " ) "; - //} - //for( std::map< Node, Node >::iterator it2 = d_tableaux_ce_term[x].begin(); it2 != d_tableaux_ce_term[x].end(); ++it2 ){ - // Debug(c) << "(CE-term)( " << it2->first << ", " << it2->second << " ) "; - //} - //Debug(c) << std::endl; - //} - } - Debug(c) << std::endl; - +Node InstStrategyCbqi::getNextDecisionRequest(){ + std::map< Node, bool > proc; for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ - Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); - Debug(c) << f << std::endl; - Debug(c) << " Inst constants: "; - for( unsigned j=0; j<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){ - if( j>0 ){ - Debug( c ) << ", "; - } - Debug( c ) << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ); - } - Debug(c) << std::endl; - for( unsigned j=0; j<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){ - Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j ); - Debug(c) << " Instantiation rows for " << ic << " : "; - for( unsigned k=0; k<d_instRows[ic].size(); k++ ){ - if( k>0 ){ - Debug(c) << ", "; - } - Debug(c) << d_instRows[ic][k]; - } - Debug(c) << std::endl; - } - } -} - -//say instantiation row x for quantifier f is coeff*var + A*t[e] + term = beta, -// where var is an instantiation constant from f, -// t[e] is a vector of terms containing instantiation constants from f, -// and term is a ground term (c1*t1 + ... + cn*tn). -// We construct the term ( beta - term )/coeff to use as an instantiation for var. -bool InstStrategySimplex::doInstantiation( Node f, Node ic, Node term, ArithVar x, InstMatch& m, Node var ){ - //first try +delta - if( doInstantiation2( f, ic, term, x, m, var ) ){ - ++(d_quantEngine->d_statistics.d_instantiations_cbqi_arith); - return true; - }else{ -#ifdef ARITH_INSTANTIATOR_USE_MINUS_DELTA - //otherwise try -delta - if( doInstantiation2( f, ic, term, x, m, var, true ) ){ - ++(d_quantEngine->d_statistics.d_instantiations_cbqi_arith); - return true; - }else{ - return false; - } -#else - return false; -#endif - } -} - -bool InstStrategySimplex::doInstantiation2( Node f, Node ic, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta ){ - // make term ( beta - term )/coeff - bool vIsInteger = var.getType().isInteger(); - Node beta = getTableauxValue( x, minus_delta ); - if( !vIsInteger || beta.getType().isInteger() ){ - Node instVal = NodeManager::currentNM()->mkNode( MINUS, beta, term ); - if( !d_ceTableaux[ic][x][var].isNull() ){ - if( vIsInteger ){ - Assert( d_ceTableaux[ic][x][var]==NodeManager::currentNM()->mkConst( Rational(-1) ) ); - instVal = NodeManager::currentNM()->mkNode( MULT, d_ceTableaux[ic][x][var], instVal ); - }else{ - Assert( d_ceTableaux[ic][x][var].getKind()==CONST_RATIONAL ); - Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_ceTableaux[ic][x][var].getConst<Rational>() ); - instVal = NodeManager::currentNM()->mkNode( MULT, coeff, instVal ); - } + Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); + Node d = getNextDecisionRequestProc( q, proc ); + if( !d.isNull() ){ + return d; } - instVal = Rewriter::rewrite( instVal ); - //use as instantiation value for var - int vn = var.getAttribute(InstVarNumAttribute()); - m.setValue( vn, instVal ); - Debug("quant-arith") << "Add instantiation " << m << std::endl; - return d_quantEngine->addInstantiation( f, m ); - }else{ - return false; - } -} -/* -Node InstStrategySimplex::getTableauxValue( Node n, bool minus_delta ){ - if( d_th->d_internal->d_partialModel.hasArithVar(n) ){ - ArithVar v = d_th->d_internal->d_partialModel.asArithVar( n ); - return getTableauxValue( v, minus_delta ); - }else{ - return NodeManager::currentNM()->mkConst( Rational(0) ); } -} -*/ -Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){ - const Rational& delta = d_th->d_internal->d_partialModel.getDelta(); - DeltaRational drv = d_th->d_internal->d_partialModel.getAssignment( v ); - Rational qmodel = drv.substituteDelta( minus_delta ? -delta : delta ); - return mkRationalNode(qmodel); + return Node::null(); } @@ -590,6 +625,7 @@ InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe ) : InstStrategyCbqi( qe ) { d_out = new CegqiOutputInstStrategy( this ); d_small_const = NodeManager::currentNM()->mkConst( Rational(1)/Rational(1000000) ); + d_check_vts_lemma_lc = false; } InstStrategyCegqi::~InstStrategyCegqi() throw () { @@ -654,9 +690,13 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { //check if we need virtual term substitution (if used delta or infinity) bool used_vts = d_quantEngine->getTermDatabase()->containsVtsTerm( subs, false ); if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, used_vts ) ){ + ++(d_quantEngine->d_statistics.d_instantiations_cbqi); //d_added_inst.insert( d_curr_quant ); return true; }else{ + //this should never happen for monotonic selection strategies + Trace("cbqi-warn") << "WARNING: Existing instantiation" << std::endl; + Assert( !options::cbqiNestedQE() || options::cbqiAll() ); return false; } } @@ -671,6 +711,16 @@ bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) { if( n.getKind()==SKOLEM && d_quantEngine->getTermDatabase()->containsVtsTerm( n ) ){ return true; }else{ + TypeNode tn = n.getType(); + if( tn.isSort() ){ + QuantEPR * qepr = d_quantEngine->getQuantEPR(); + if( qepr!=NULL ){ + //legal if in the finite set of constants of type tn + if( qepr->isEPRConstant( tn, n ) ){ + return true; + } + } + } //only legal if current quantified formula contains n return TermDb::containsTerm( d_curr_quant, n ); } @@ -719,7 +769,9 @@ void InstStrategyCegqi::registerCounterexampleLemma( Node q, Node lem ) { void InstStrategyCegqi::presolve() { if( options::cbqiPreRegInst() ){ for( std::map< Node, CegInstantiator * >::iterator it = d_cinst.begin(); it != d_cinst.end(); ++it ){ + Trace("cbqi-presolve") << "Presolve " << it->first << std::endl; it->second->presolve( it->first ); } } } + diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 8ed59778b..c9f62243f 100755 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -34,25 +34,64 @@ namespace quantifiers { class InstStrategyCbqi : public QuantifiersModule { typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; + typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap; protected: bool d_cbqi_set_quant_inactive; bool d_incomplete_check; /** whether we have added cbqi lemma */ NodeSet d_added_cbqi_lemma; + /** whether we have added cbqi lemma */ + NodeSet d_elim_quants; + /** parent guards */ + std::map< Node, std::vector< Node > > d_parent_quant; + std::map< Node, std::vector< Node > > d_children_quant; + std::map< Node, bool > d_active_quant; /** whether we have instantiated quantified formulas */ //NodeSet d_added_inst; - /** whether to do cbqi for this quantified formula */ - std::map< Node, bool > d_do_cbqi; + /** whether to do cbqi for this quantified formula 0 : no, 2 : yes, 1 : yes but not exclusively, -1 : heuristically */ + std::map< Node, int > d_do_cbqi; /** register ce lemma */ + bool registerCbqiLemma( Node q ); virtual void registerCounterexampleLemma( Node q, Node lem ); /** has added cbqi lemma */ bool hasAddedCbqiLemma( Node q ) { return d_added_cbqi_lemma.find( q )!=d_added_cbqi_lemma.end(); } /** helper functions */ - bool hasNonCbqiVariable( Node q ); + int hasNonCbqiVariable( Node q ); bool hasNonCbqiOperator( Node n, std::map< Node, bool >& visited ); + /** get next decision request with dependency checking */ + Node getNextDecisionRequestProc( Node q, std::map< Node, bool >& proc ); /** process functions */ virtual void processResetInstantiationRound( Theory::Effort effort ) = 0; virtual void process( Node q, Theory::Effort effort, int e ) = 0; +protected: + //for identification + uint64_t d_qid_count; + //nested qe map + std::map< Node, Node > d_nested_qe; + //mark ids on quantifiers + Node getIdMarkedQuantNode( Node n, std::map< Node, Node >& visited ); + // id to ce quant + std::map< Node, Node > d_id_to_ce_quant; + std::map< Node, Node > d_ce_quant_to_id; + //do nested quantifier elimination recursive + Node doNestedQENode( Node q, Node ceq, Node n, std::vector< Node >& inst_terms, bool doVts ); + Node doNestedQERec( Node q, Node n, std::map< Node, Node >& visited, std::vector< Node >& inst_terms, bool doVts ); + //elimination information (for delayed elimination) + class NestedQEInfo { + public: + NestedQEInfo() : d_doVts(false){} + ~NestedQEInfo(){} + Node d_q; + std::vector< Node > d_inst_terms; + bool d_doVts; + }; + std::map< Node, NestedQEInfo > d_nested_qe_info; + NodeIntMap d_nested_qe_waitlist_size; + NodeIntMap d_nested_qe_waitlist_proc; + std::map< Node, std::vector< Node > > d_nested_qe_waitlist; +public: + //do nested quantifier elimination + Node doNestedQE( Node q, std::vector< Node >& inst_terms, Node lem, bool doVts ); public: InstStrategyCbqi( QuantifiersEngine * qe ); ~InstStrategyCbqi() throw(); @@ -64,56 +103,13 @@ public: void reset_round( Theory::Effort e ); void check( Theory::Effort e, unsigned quant_e ); bool checkComplete(); + bool checkCompleteFor( Node q ); void preRegisterQuantifier( Node q ); void registerQuantifier( Node q ); /** get next decision request */ Node getNextDecisionRequest(); }; - -class InstStrategySimplex : public InstStrategyCbqi { -protected: - /** reference to theory arithmetic */ - arith::TheoryArith* d_th; - /** quantifiers we should process */ - std::map< Node, bool > d_quantActive; - /** delta */ - std::map< TypeNode, Node > d_deltas; - /** for each quantifier, simplex rows */ - std::map< Node, std::vector< arith::ArithVar > > d_instRows; - /** tableaux */ - std::map< Node, std::map< arith::ArithVar, Node > > d_tableaux_term; - std::map< Node, std::map< arith::ArithVar, std::map< Node, Node > > > d_tableaux_ce_term; - std::map< Node, std::map< arith::ArithVar, std::map< Node, Node > > > d_tableaux; - /** ce tableaux */ - std::map< Node, std::map< arith::ArithVar, std::map< Node, Node > > > d_ceTableaux; - /** get value */ - //Node getTableauxValue( Node n, bool minus_delta = false ); - Node getTableauxValue( arith::ArithVar v, bool minus_delta = false ); - /** do instantiation */ - bool doInstantiation( Node f, Node ic, Node term, arith::ArithVar x, InstMatch& m, Node var ); - bool doInstantiation2( Node f, Node ic, Node term, arith::ArithVar x, InstMatch& m, Node var, bool minus_delta = false ); - /** add term to row */ - void addTermToRow( Node ic, arith::ArithVar x, Node n, NodeBuilder<>& t ); - /** print debug */ - void debugPrint( const char* c ); -private: - /** */ - int d_counter; - /** constants */ - Node d_zero; - Node d_negOne; - /** process functions */ - void processResetInstantiationRound( Theory::Effort effort ); - void process( Node f, Theory::Effort effort, int e ); -public: - InstStrategySimplex( arith::TheoryArith* th, QuantifiersEngine* ie ); - ~InstStrategySimplex() throw() {} - /** identify */ - std::string identify() const { return std::string("Simplex"); } -}; - - //generalized counterexample guided quantifier instantiation class InstStrategyCegqi; diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 49e0a698f..c4bf61b28 100755 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -155,6 +155,7 @@ InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( QuantifiersEngine* qe d_regenerate_frequency = 3; d_regenerate = true; }else{ + d_regenerate_frequency = 1; d_regenerate = false; } } diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index db597d031..afeed1e5d 100755 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -114,6 +114,7 @@ void InstantiationEngine::reset_round( Theory::Effort e ){ } void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ + CodeTimer codeTimer(d_quantEngine->d_statistics.d_ematching_time); if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){ double clSet = 0; if( Trace.isOn("inst-engine") ){ @@ -151,19 +152,9 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ } } -bool InstantiationEngine::checkComplete() { - if( !options::finiteModelFind() ){ - for( unsigned i=0; i<d_quants.size(); i++ ){ - if( isIncomplete( d_quants[i] ) ){ - return false; - } - } - } - return true; -} - -bool InstantiationEngine::isIncomplete( Node q ) { - return true; +bool InstantiationEngine::checkCompleteFor( Node q ) { + //TODO? + return false; } void InstantiationEngine::preRegisterQuantifier( Node q ) { diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index d2b3740a1..79963cb45 100755 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -78,7 +78,7 @@ public: bool needsCheck( Theory::Effort e ); void reset_round( Theory::Effort e ); void check( Theory::Effort e, unsigned quant_e ); - bool checkComplete(); + bool checkCompleteFor( Node q ); void preRegisterQuantifier( Node q ); void registerQuantifier( Node q ); Node explain(TNode n){ return Node::null(); } diff --git a/src/theory/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h index 94abf3c90..04a6bc9c8 100755 --- a/src/theory/quantifiers/local_theory_ext.h +++ b/src/theory/quantifiers/local_theory_ext.h @@ -66,6 +66,8 @@ public: void check( Theory::Effort e, unsigned quant_e ); /* Called for new quantifiers */ void registerQuantifier( Node q ) {} + /* check complete */ + bool checkComplete() { return !d_wasInvoked; } void assertNode( Node n ) {} /** Identify this module (for debugging, dynamic configuration, etc..) */ std::string identify() const { return "LtePartialInst"; } diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp index 582599680..976b81e60 100755 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp @@ -33,6 +33,10 @@ using namespace CVC4::theory::quantifiers; using namespace CVC4::kind; +QuantifierMacros::QuantifierMacros( QuantifiersEngine * qe ) : d_qe( qe ){ + d_ground_macros = false; +} + bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){ unsigned rmax = options::macrosQuantMode()==MACROS_QUANT_MODE_ALL ? 2 : 1; for( unsigned r=0; r<rmax; r++ ){ diff --git a/src/theory/quantifiers/macros.h b/src/theory/quantifiers/macros.h index 39ec2f0a1..60af7ad0a 100755 --- a/src/theory/quantifiers/macros.h +++ b/src/theory/quantifiers/macros.h @@ -60,7 +60,7 @@ private: void addMacro( Node op, Node n, std::vector< Node >& opc ); void debugMacroDefinition( Node oo, Node n ); public: - QuantifierMacros( QuantifiersEngine * qe ) : d_qe( qe ){} + QuantifierMacros( QuantifiersEngine * qe ); ~QuantifierMacros(){} bool simplify( std::vector< Node >& assertions, bool doRewrite = false ); diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 7bbe06108..b30c2addb 100755 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -391,7 +391,7 @@ bool QModelBuilderIG::isTermActive( Node n ){ //do exhaustive instantiation -bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { +int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { if( optUseModel() ){ RepSetIterator riter( d_qe, &(d_qe->getModel()->d_rep_set) ); if( riter.setQuantifier( f ) ){ @@ -470,10 +470,9 @@ bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i } } //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round - d_incomplete_check = riter.isIncomplete(); - return true; + return riter.isIncomplete() ? -1 : 1; }else{ - return false; + return 0; } } diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index e4f9529a8..9b89e5ef6 100755 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -38,13 +38,14 @@ public: virtual ~QModelBuilder() throw() {} // is quantifier active? virtual bool isQuantifierActive( Node f ); - //do exhaustive instantiation - virtual bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { return false; } + //do exhaustive instantiation + // 0 : failed, but resorting to true exhaustive instantiation may work + // >0 : success + // <0 : failed + virtual int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { return false; } //whether to construct model virtual bool optUseModel(); /** number of lemmas generated while building model */ - //is the exhaustive instantiation incomplete? - bool d_incomplete_check; int d_addedLemmas; int d_triedLemmas; /** exist instantiation ? */ @@ -142,7 +143,7 @@ public: // is quantifier active? bool isQuantifierActive( Node f ); //do exhaustive instantiation - bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ); + int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ); //temporary stats int d_numQuantSat; diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 7658f2b6b..9c09371c4 100755 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -73,7 +73,6 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){ Trace("model-engine") << "---Model Engine Round---" << std::endl; clSet = double(clock())/double(CLOCKS_PER_SEC); } - ++(d_statistics.d_inst_rounds); Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl; //let the strong solver verify that the model is minimal @@ -99,7 +98,7 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){ } if( addedLemmas==0 ){ - Trace("model-engine-debug") << "No lemmas added, incomplete = " << d_incomplete_check << std::endl; + Trace("model-engine-debug") << "No lemmas added, incomplete = " << ( d_incomplete_check || !d_incomplete_quants.empty() ) << std::endl; //CVC4 will answer SAT or unknown if( Trace.isOn("fmf-consistent") ){ Trace("fmf-consistent") << std::endl; @@ -113,6 +112,10 @@ bool ModelEngine::checkComplete() { return !d_incomplete_check; } +bool ModelEngine::checkCompleteFor( Node q ) { + return std::find( d_incomplete_quants.begin(), d_incomplete_quants.end(), q )==d_incomplete_quants.end(); +} + void ModelEngine::registerQuantifier( Node f ){ if( Trace.isOn("fmf-warn") ){ bool canHandle = true; @@ -195,17 +198,18 @@ int ModelEngine::checkModel(){ // FMC uses two sub-effort levels int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : ( options::mbqiMode()==MBQI_TRUST ? 0 : 1 ); for( int e=0; e<e_max; e++) { + d_incomplete_quants.clear(); for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ - Node f = fm->getAssertedQuantifier( i, true ); - Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << f << ", effort = " << e << "..." << std::endl; + Node q = fm->getAssertedQuantifier( i, true ); + Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << q << ", effort = " << e << "..." << std::endl; //determine if we should check this quantifier - if( considerQuantifiedFormula( f ) ){ - exhaustiveInstantiate( f, e ); + if( considerQuantifiedFormula( q ) ){ + exhaustiveInstantiate( q, e ); if( d_quantEngine->inConflict() || ( optOneQuantPerRound() && d_addedLemmas>0 ) ){ break; } }else{ - Trace("fmf-exh-inst") << "-> Inactive : " << f << std::endl; + Trace("fmf-exh-inst") << "-> Inactive : " << q << std::endl; } } if( d_addedLemmas>0 ){ @@ -260,13 +264,17 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder(); mb->d_triedLemmas = 0; mb->d_addedLemmas = 0; - mb->d_incomplete_check = false; - if( mb->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort ) ){ - Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl; + int retEi = mb->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort ); + if( retEi!=0 ){ + if( retEi<0 ){ + Trace("fmf-exh-inst") << "-> Builder determined complete instantiation was impossible." << std::endl; + d_incomplete_quants.push_back( f ); + }else{ + Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl; + } d_triedLemmas += mb->d_triedLemmas; d_addedLemmas += mb->d_addedLemmas; - d_incomplete_check = d_incomplete_check || mb->d_incomplete_check; - d_statistics.d_mbqi_inst_lemmas += mb->d_addedLemmas; + d_quantEngine->d_statistics.d_instantiations_fmf_mbqi += mb->d_addedLemmas; }else{ if( Trace.isOn("fmf-exh-inst-debug") ){ Trace("fmf-exh-inst-debug") << " Instantiation Constants: "; @@ -303,13 +311,15 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ } d_addedLemmas += addedLemmas; d_triedLemmas += triedLemmas; - d_statistics.d_exh_inst_lemmas += addedLemmas; + d_quantEngine->d_statistics.d_instantiations_fmf_exh += addedLemmas; } }else{ Trace("fmf-exh-inst") << "...exhaustive instantiation did set, incomplete=" << riter.isIncomplete() << "..." << std::endl; } //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round - d_incomplete_check = d_incomplete_check || riter.isIncomplete(); + if( riter.isIncomplete() ){ + d_incomplete_quants.push_back( f ); + } } } @@ -328,18 +338,3 @@ void ModelEngine::debugPrint( const char* c ){ //d_quantEngine->getModel()->debugPrint( c ); } -ModelEngine::Statistics::Statistics(): - d_inst_rounds("ModelEngine::Inst_Rounds", 0), - d_exh_inst_lemmas("ModelEngine::Instantiations_Exhaustive", 0 ), - d_mbqi_inst_lemmas("ModelEngine::Instantiations_Mbqi", 0 ) -{ - smtStatisticsRegistry()->registerStat(&d_inst_rounds); - smtStatisticsRegistry()->registerStat(&d_exh_inst_lemmas); - smtStatisticsRegistry()->registerStat(&d_mbqi_inst_lemmas); -} - -ModelEngine::Statistics::~Statistics(){ - smtStatisticsRegistry()->unregisterStat(&d_inst_rounds); - smtStatisticsRegistry()->unregisterStat(&d_exh_inst_lemmas); - smtStatisticsRegistry()->unregisterStat(&d_mbqi_inst_lemmas); -} diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index 12f18aa08..e89be8d2b 100755 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -42,6 +42,8 @@ private: //temporary statistics //is the exhaustive instantiation incomplete? bool d_incomplete_check; + // set of quantified formulas for which check was incomplete + std::vector< Node > d_incomplete_quants; int d_addedLemmas; int d_triedLemmas; int d_totalLemmas; @@ -54,21 +56,11 @@ public: void reset_round( Theory::Effort e ); void check( Theory::Effort e, unsigned quant_e ); bool checkComplete(); + bool checkCompleteFor( Node q ); void registerQuantifier( Node f ); void assertNode( Node f ); Node explain(TNode n){ return Node::null(); } void debugPrint( const char* c ); -public: - /** statistics class */ - class Statistics { - public: - IntStat d_inst_rounds; - IntStat d_exh_inst_lemmas; - IntStat d_mbqi_inst_lemmas; - Statistics(); - ~Statistics(); - }; - Statistics d_statistics; /** Identify this module */ std::string identify() const { return "ModelEngine"; } };/* class ModelEngine */ diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index bac2aa35c..1e484311c 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -108,7 +108,7 @@ void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) { } Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl; - if( d_mg->isValid() ){ + if( d_mg->isValid() && options::qcfEagerCheckRd() ){ //optimization : record variable argument positions for terms that must be matched std::vector< TNode > vars; //TODO: revisit this, makes QCF faster, but misses conflicts due to caring about paths that may not be relevant (starExec jobs 14136/14137) @@ -967,7 +967,11 @@ MatchGen::MatchGen() d_n(), d_type( typ_invalid ), d_type_not() -{} +{ + d_qni_size = 0; + d_child_counter = -1; + d_use_children = true; +} MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ) @@ -980,6 +984,10 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ) d_type(), d_type_not() { + //initialize temporary + d_child_counter = -1; + d_use_children = true; + Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << std::endl; std::vector< Node > qni_apps; d_qni_size = 0; @@ -1853,7 +1861,7 @@ void MatchGen::setInvalid() { } bool MatchGen::isHandledBoolConnective( TNode n ) { - return TermDb::isBoolConnective( n.getKind() ) && ( n.getKind()!=ITE || n.getType().isBoolean() ); + return TermDb::isBoolConnective( n.getKind() ) && ( n.getKind()!=ITE || n.getType().isBoolean() ) && n.getKind()!=SEP_STAR; } bool MatchGen::isHandledUfTerm( TNode n ) { @@ -2024,6 +2032,7 @@ void QuantConflictFind::setIrrelevantFunction( TNode f ) { /** check */ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { + CodeTimer codeTimer(d_quantEngine->d_statistics.d_qcf_time); if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT ){ Trace("qcf-check") << "QCF : check : " << level << std::endl; if( d_conflict ){ @@ -2098,7 +2107,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { ++addedLemmas; if( e==effort_conflict ){ d_quantEngine->markRelevant( q ); - ++(d_statistics.d_conflict_inst); + ++(d_quantEngine->d_statistics.d_instantiations_qcf); if( options::qcfAllConflict() ){ isConflict = true; }else{ @@ -2107,7 +2116,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { break; }else if( e==effort_prop_eq ){ d_quantEngine->markRelevant( q ); - ++(d_statistics.d_prop_inst); + ++(d_quantEngine->d_statistics.d_instantiations_qcf); } }else{ Trace("qcf-inst") << " ... Failed to add instantiation" << std::endl; @@ -2234,20 +2243,14 @@ void QuantConflictFind::debugPrintQuantBody( const char * c, Node q, Node n, boo QuantConflictFind::Statistics::Statistics(): d_inst_rounds("QuantConflictFind::Inst_Rounds", 0), - d_conflict_inst("QuantConflictFind::Instantiations_Conflict_Find", 0 ), - d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 ), d_entailment_checks("QuantConflictFind::Entailment_Checks",0) { smtStatisticsRegistry()->registerStat(&d_inst_rounds); - smtStatisticsRegistry()->registerStat(&d_conflict_inst); - smtStatisticsRegistry()->registerStat(&d_prop_inst); smtStatisticsRegistry()->registerStat(&d_entailment_checks); } QuantConflictFind::Statistics::~Statistics(){ smtStatisticsRegistry()->unregisterStat(&d_inst_rounds); - smtStatisticsRegistry()->unregisterStat(&d_conflict_inst); - smtStatisticsRegistry()->unregisterStat(&d_prop_inst); smtStatisticsRegistry()->unregisterStat(&d_entailment_checks); } diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 47a66b1b1..dc8a9acb2 100755 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -260,8 +260,6 @@ public: class Statistics { public: IntStat d_inst_rounds; - IntStat d_conflict_inst; - IntStat d_prop_inst; IntStat d_entailment_checks; Statistics(); ~Statistics(); diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index 5aff1a848..df8533135 100755 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -48,7 +48,7 @@ void QuantDSplit::preRegisterQuantifier( Node q ) { }else{ int score = -1; if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){ - score = dt.isInterpretedFinite() ? 1 : -1; + score = dt.isInterpretedFinite() ? 1 : 0; }else if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_DEFAULT ){ score = dt.isInterpretedFinite() ? 1 : -1; } @@ -73,6 +73,11 @@ bool QuantDSplit::needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_FULL && !d_quant_to_reduce.empty(); } +bool QuantDSplit::checkCompleteFor( Node q ) { + // true if we split q + return d_added_split.find( q )!=d_added_split.end(); +} + /* Call during quantifier engine's check */ void QuantDSplit::check( Theory::Effort e, unsigned quant_e ) { //add lemmas ASAP (they are a reduction) diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h index d36824998..3e3b08814 100755 --- a/src/theory/quantifiers/quant_split.h +++ b/src/theory/quantifiers/quant_split.h @@ -43,6 +43,7 @@ public: /* Called for new quantifiers */ void registerQuantifier( Node q ) {} void assertNode( Node n ) {} + bool checkCompleteFor( Node q ); /** Identify this module (for debugging, dynamic configuration, etc..) */ std::string identify() const { return "QuantDSplit"; } }; diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index b9aab0236..f4284a8ab 100755 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -419,3 +419,107 @@ void QuantPhaseReq::getEntailPolarity( Node n, int child, bool hasPol, bool pol, } } +void QuantEPR::registerNode( Node n, std::map< int, std::map< Node, bool > >& visited, bool beneathQuant, bool hasPol, bool pol ) { + int vindex = hasPol ? ( pol ? 1 : -1 ) : 0; + if( visited[vindex].find( n )==visited[vindex].end() ){ + visited[vindex][n] = true; + Trace("quant-epr-debug") << "QuantEPR::registerNode " << n << std::endl; + if( n.getKind()==FORALL ){ + if( beneathQuant || !hasPol || !pol ){ + for( unsigned i=0; i<n[0].getNumChildren(); i++ ){ + TypeNode tn = n[0][i].getType(); + if( d_non_epr.find( tn )==d_non_epr.end() ){ + Trace("quant-epr") << "Sort " << tn << " is non-EPR because of nested or possible existential quantification." << std::endl; + d_non_epr[tn] = true; + } + } + }else{ + beneathQuant = true; + } + } + TypeNode tn = n.getType(); + + if( n.getNumChildren()>0 ){ + if( tn.isSort() ){ + if( d_non_epr.find( tn )==d_non_epr.end() ){ + Trace("quant-epr") << "Sort " << tn << " is non-EPR because of " << n << std::endl; + d_non_epr[tn] = true; + } + } + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + bool newHasPol; + bool newPol; + QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol ); + registerNode( n[i], visited, beneathQuant, newHasPol, newPol ); + } + }else if( tn.isSort() ){ + if( n.getKind()==BOUND_VARIABLE ){ + if( d_consts.find( tn )==d_consts.end() ){ + //mark that at least one constant must occur + d_consts[tn].clear(); + } + }else if( std::find( d_consts[tn].begin(), d_consts[tn].end(), n )==d_consts[tn].end() ){ + d_consts[tn].push_back( n ); + Trace("quant-epr") << "...constant of type " << tn << " : " << n << std::endl; + } + } + } +} + +void QuantEPR::registerAssertion( Node assertion ) { + std::map< int, std::map< Node, bool > > visited; + registerNode( assertion, visited, false, true, true ); +} + +void QuantEPR::finishInit() { + Trace("quant-epr-debug") << "QuantEPR::finishInit" << std::endl; + for( std::map< TypeNode, std::vector< Node > >::iterator it = d_consts.begin(); it != d_consts.end(); ++it ){ + Assert( d_epr_axiom.find( it->first )==d_epr_axiom.end() ); + Trace("quant-epr-debug") << "process " << it->first << std::endl; + if( d_non_epr.find( it->first )!=d_non_epr.end() ){ + Trace("quant-epr-debug") << "...non-epr" << std::endl; + it->second.clear(); + }else{ + Trace("quant-epr-debug") << "...epr, #consts = " << it->second.size() << std::endl; + if( it->second.empty() ){ + it->second.push_back( NodeManager::currentNM()->mkSkolem( "e", it->first, "EPR base constant" ) ); + } + if( Trace.isOn("quant-epr") ){ + Trace("quant-epr") << "Type " << it->first << " is EPR, with constants : " << std::endl; + for( unsigned i=0; i<it->second.size(); i++ ){ + Trace("quant-epr") << " " << it->second[i] << std::endl; + } + } + } + } +} + +bool QuantEPR::isEPRConstant( TypeNode tn, Node k ) { + return std::find( d_consts[tn].begin(), d_consts[tn].end(), k )!=d_consts[tn].end(); +} + +void QuantEPR::addEPRConstant( TypeNode tn, Node k ) { + Assert( isEPR( tn ) ); + Assert( d_epr_axiom.find( tn )==d_epr_axiom.end() ); + if( !isEPRConstant( tn, k ) ){ + d_consts[tn].push_back( k ); + } +} + +Node QuantEPR::mkEPRAxiom( TypeNode tn ) { + Assert( isEPR( tn ) ); + std::map< TypeNode, Node >::iterator ita = d_epr_axiom.find( tn ); + if( ita==d_epr_axiom.end() ){ + std::vector< Node > disj; + Node x = NodeManager::currentNM()->mkBoundVar( tn ); + for( unsigned i=0; i<d_consts[tn].size(); i++ ){ + disj.push_back( NodeManager::currentNM()->mkNode( tn.isBoolean() ? IFF : EQUAL, x, d_consts[tn][i] ) ); + } + Assert( !disj.empty() ); + d_epr_axiom[tn] = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, x ), disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( OR, disj ) ); + return d_epr_axiom[tn]; + }else{ + return ita->second; + } +} + diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 79cdae437..3ff21aa6e 100755 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -51,8 +51,10 @@ public: virtual void reset_round( Theory::Effort e ){} /* Call during quantifier engine's check */ virtual void check( Theory::Effort e, unsigned quant_e ) = 0; - /* check was complete (e.g. no lemmas implies a model) */ + /* check was complete, return false if there is no way to answer "SAT", true if maybe can answer "SAT" */ virtual bool checkComplete() { return true; } + /* check was complete for quantified formula q (e.g. no lemmas implies a model) */ + virtual bool checkCompleteFor( Node q ) { return false; } /* Called for new quantified formulas */ virtual void preRegisterQuantifier( Node q ) { } /* Called for new quantifiers after owners are finalized */ @@ -149,7 +151,7 @@ public: }; -class EqualityQuery : public QuantifiersUtil{ +class EqualityQuery : public QuantifiersUtil { public: EqualityQuery(){} virtual ~EqualityQuery(){}; @@ -171,6 +173,38 @@ public: virtual TNode getCongruentTerm( Node f, std::vector< TNode >& args ) = 0; };/* class EqualityQuery */ +class QuantEPR +{ +private: + void registerNode( Node n, std::map< int, std::map< Node, bool > >& visited, bool beneathQuant, bool hasPol, bool pol ); + /** non-epr */ + std::map< TypeNode, bool > d_non_epr; + /** axioms for epr */ + std::map< TypeNode, Node > d_epr_axiom; +public: + QuantEPR(){} + virtual ~QuantEPR(){} + /** constants per type */ + std::map< TypeNode, std::vector< Node > > d_consts; + /* reset */ + //bool reset( Theory::Effort e ) {} + /** identify */ + //std::string identify() const { return "QuantEPR"; } + /** register assertion */ + void registerAssertion( Node assertion ); + /** finish init */ + void finishInit(); + /** is EPR */ + bool isEPR( TypeNode tn ) const { return d_non_epr.find( tn )==d_non_epr.end(); } + /** is EPR constant */ + bool isEPRConstant( TypeNode tn, Node k ); + /** add EPR constant */ + void addEPRConstant( TypeNode tn, Node k ); + /** get EPR axiom */ + Node mkEPRAxiom( TypeNode tn ); + /** has EPR axiom */ + bool hasEPRAxiom( TypeNode tn ) const { return d_epr_axiom.find( tn )!=d_epr_axiom.end(); } +}; } } diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 963889a85..de8875ae3 100755 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -20,11 +20,12 @@ #include "theory/quantifiers/trigger.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 { bool QuantifiersRewriter::isClause( Node n ){ if( isLiteral( n ) ){ @@ -1074,9 +1075,9 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& return body; } -Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, bool pol ){ +Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol, bool prenexAgg ){ if( body.getKind()==FORALL ){ - if( pol && ( options::prenexQuant()==PRENEX_ALL || body.getNumChildren()==2 ) ){ + if( ( pol || prenexAgg ) && ( options::prenexQuantUser() || body.getNumChildren()==2 ) ){ std::vector< Node > terms; std::vector< Node > subs; //for doing prenexing of same-signed quantifiers @@ -1085,14 +1086,27 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b terms.push_back( body[0][i] ); subs.push_back( NodeManager::currentNM()->mkBoundVar( body[0][i].getType() ) ); } - args.insert( args.end(), subs.begin(), subs.end() ); + if( pol ){ + args.insert( args.end(), subs.begin(), subs.end() ); + }else{ + nargs.insert( nargs.end(), subs.begin(), subs.end() ); + } Node newBody = body[1]; newBody = newBody.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); return newBody; - }else{ - return body; } - }else{ + //must remove structure + }else if( prenexAgg && body.getKind()==kind::ITE && body.getType().isBoolean() ){ + Node nn = NodeManager::currentNM()->mkNode( kind::AND, + NodeManager::currentNM()->mkNode( kind::OR, body[0].notNode(), body[1] ), + NodeManager::currentNM()->mkNode( kind::OR, body[0], body[2] ) ); + return computePrenex( nn, args, nargs, pol, prenexAgg ); + }else if( prenexAgg && body.getKind()==kind::IFF ){ + Node nn = NodeManager::currentNM()->mkNode( kind::AND, + NodeManager::currentNM()->mkNode( kind::OR, body[0].notNode(), body[1] ), + NodeManager::currentNM()->mkNode( kind::OR, body[0], body[1].notNode() ) ); + return computePrenex( nn, args, nargs, pol, prenexAgg ); + }else if( body.getType().isBoolean() ){ Assert( body.getKind()!=EXISTS ); bool childrenChanged = false; std::vector< Node > newChildren; @@ -1101,7 +1115,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b bool newPol; QuantPhaseReq::getPolarity( body, i, true, pol, newHasPol, newPol ); if( newHasPol ){ - Node n = computePrenex( body[i], args, newPol ); + Node n = computePrenex( body[i], args, nargs, newPol, prenexAgg ); newChildren.push_back( n ); if( n!=body[i] ){ childrenChanged = true; @@ -1116,10 +1130,98 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b }else{ return NodeManager::currentNM()->mkNode( body.getKind(), newChildren ); } + } + } + return body; +} + +Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel ){ + if( containsQuantifiers( n ) ){ + if( topLevel && options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL && ( n.getKind()==AND || ( n.getKind()==NOT && n[0].getKind()==OR ) ) ){ + std::vector< Node > children; + Node nc = n.getKind()==NOT ? n[0] : n; + for( unsigned i=0; i<nc.getNumChildren(); i++ ){ + Node ncc = computePrenexAgg( nc[i], true ); + if( n.getKind()==NOT ){ + ncc = ncc.negate(); + } + children.push_back( ncc ); + } + return NodeManager::currentNM()->mkNode( AND, children ); + }else if( n.getKind()==NOT ){ + return computePrenexAgg( n[0], false ).negate(); + }else if( n.getKind()==FORALL ){ + /* + Node nn = computePrenexAgg( n[1], false ); + if( nn!=n[1] ){ + if( n.getNumChildren()==2 ){ + return NodeManager::currentNM()->mkNode( FORALL, n[0], nn ); + }else{ + return NodeManager::currentNM()->mkNode( FORALL, n[0], nn, n[2] ); + } + } + */ + std::vector< Node > children; + if( n[1].getKind()==OR && options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL ){ + for( unsigned i=0; i<n[1].getNumChildren(); i++ ){ + children.push_back( computePrenexAgg( n[1][i], false ) ); + } + }else{ + children.push_back( computePrenexAgg( n[1], false ) ); + } + std::vector< Node > args; + for( unsigned i=0; i<n[0].getNumChildren(); i++ ){ + args.push_back( n[0][i] ); + } + std::vector< Node > nargs; + //for each child, strip top level quant + for( unsigned i=0; i<children.size(); i++ ){ + if( children[i].getKind()==FORALL ){ + for( unsigned j=0; j<children[i][0].getNumChildren(); j++ ){ + args.push_back( children[i][0][j] ); + } + children[i] = children[i][1]; + } + } + Node nb = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ); + return mkForall( args, nb, true ); }else{ - return body; + std::vector< Node > args; + std::vector< Node > nargs; + Node nn = computePrenex( n, args, nargs, true, true ); + if( n!=nn ){ + Node nnn = computePrenexAgg( nn, false ); + //merge prenex + if( nnn.getKind()==FORALL ){ + for( unsigned i=0; i<nnn[0].getNumChildren(); i++ ){ + args.push_back( nnn[0][i] ); + } + nnn = nnn[1]; + //pos polarity variables are inner + if( !args.empty() ){ + nnn = mkForall( args, nnn, true ); + } + args.clear(); + }else if( nnn.getKind()==NOT && nnn[0].getKind()==FORALL ){ + for( unsigned i=0; i<nnn[0][0].getNumChildren(); i++ ){ + nargs.push_back( nnn[0][0][i] ); + } + nnn = nnn[0][1].negate(); + } + if( !nargs.empty() ){ + nnn = mkForall( nargs, nnn.negate(), true ).negate(); + } + if( !args.empty() ){ + nnn = mkForall( args, nnn, true ); + } + return nnn; + }else{ + Assert( args.empty() ); + Assert( nargs.empty() ); + } } } + return n; } Node QuantifiersRewriter::computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ) { @@ -1237,6 +1339,26 @@ Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, QAttri return NodeManager::currentNM()->mkNode( kind::FORALL, children ); } } +Node QuantifiersRewriter::mkForall( std::vector< Node >& args, Node body, bool marked ) { + if( args.empty() ){ + return body; + }else{ + std::vector< Node > children; + children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) ); + children.push_back( body ); + std::vector< Node > iplc; + if( marked ){ + Node avar = NodeManager::currentNM()->mkSkolem( "id", NodeManager::currentNM()->booleanType() ); + QuantIdNumAttribute ida; + avar.setAttribute(ida,0); + iplc.push_back( NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, avar ) ); + } + if( !iplc.empty() ){ + children.push_back( NodeManager::currentNM()->mkNode( INST_PATTERN_LIST, iplc ) ); + } + return NodeManager::currentNM()->mkNode( FORALL, children ); + } +} //computes miniscoping, also eliminates variables that do not occur free in body Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa ){ @@ -1294,21 +1416,25 @@ Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node bo } Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& args, Node body ){ - std::map< Node, std::vector< Node > > varLits; - std::map< Node, std::vector< Node > > litVars; - if( body.getKind()==OR ){ + std::map<Node, std::vector<Node> > varLits; + std::map<Node, std::vector<Node> > litVars; + if (body.getKind() == OR) { Trace("ag-miniscope") << "compute aggressive miniscoping on " << body << std::endl; - for( size_t i=0; i<body.getNumChildren(); i++ ){ - std::vector< Node > activeArgs; - computeArgVec( args, activeArgs, body[i] ); - for (unsigned j=0; j<activeArgs.size(); j++ ){ - varLits[activeArgs[j]].push_back( body[i] ); - } - litVars[body[i]].insert( litVars[body[i]].begin(), activeArgs.begin(), activeArgs.end() ); + for (size_t i = 0; i < body.getNumChildren(); i++) { + std::vector<Node> activeArgs; + computeArgVec(args, activeArgs, body[i]); + for (unsigned j = 0; j < activeArgs.size(); j++) { + varLits[activeArgs[j]].push_back(body[i]); + } + std::vector<Node>& lit_body_i = litVars[body[i]]; + std::vector<Node>::iterator lit_body_i_begin = lit_body_i.begin(); + std::vector<Node>::const_iterator active_begin = activeArgs.begin(); + std::vector<Node>::const_iterator active_end = activeArgs.end(); + lit_body_i.insert(lit_body_i_begin, active_begin, active_end); } //find the variable in the least number of literals Node bestVar; - for( std::map< Node, std::vector< Node > >::iterator it = varLits.begin(); it != varLits.end(); ++it ){ + for( std::map< Node, std::vector<Node> >::iterator it = varLits.begin(); it != varLits.end(); ++it ){ if( bestVar.isNull() || varLits[bestVar].size()>it->second.size() ){ bestVar = it->first; } @@ -1318,9 +1444,9 @@ Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& arg //we can miniscope Trace("ag-miniscope") << "Miniscope on " << bestVar << std::endl; //make the bodies - std::vector< Node > qlit1; + std::vector<Node> qlit1; qlit1.insert( qlit1.begin(), varLits[bestVar].begin(), varLits[bestVar].end() ); - std::vector< Node > qlitt; + std::vector<Node> qlitt; //for all literals not containing bestVar for( size_t i=0; i<body.getNumChildren(); i++ ){ if( std::find( qlit1.begin(), qlit1.end(), body[i] )==qlit1.end() ){ @@ -1328,9 +1454,9 @@ Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& arg } } //make the variable lists - std::vector< Node > qvl1; - std::vector< Node > qvl2; - std::vector< Node > qvsh; + std::vector<Node> qvl1; + std::vector<Node> qvl2; + std::vector<Node> qvsh; for( unsigned i=0; i<args.size(); i++ ){ bool found1 = false; bool found2 = false; @@ -1358,8 +1484,8 @@ Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& arg Assert( !qvl1.empty() ); Assert( !qvl2.empty() || !qvsh.empty() ); //check for literals that only contain shared variables - std::vector< Node > qlitsh; - std::vector< Node > qlit2; + std::vector<Node> qlitsh; + std::vector<Node> qlit2; for( size_t i=0; i<qlitt.size(); i++ ){ bool hasVar2 = false; for( size_t j=0; j<litVars[qlitt[i]].size(); j++ ){ @@ -1413,7 +1539,7 @@ bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& q }else if( computeOption==COMPUTE_COND_SPLIT ){ return ( options::iteDtTesterSplitQuant() || options::condVarSplitQuant() ) && !is_strict_trigger; }else if( computeOption==COMPUTE_PRENEX ){ - return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant() && is_std; + return options::prenexQuant()!=PRENEX_QUANT_NONE && !options::aggressiveMiniscopeQuant() && is_std; }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ return ( options::varElimQuant() || options::dtVarExpandQuant() ) && is_std; }else{ @@ -1423,7 +1549,7 @@ bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& q //general method for computing various rewrites Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttributes& qa ){ - Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << std::endl; + Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << " " << qa.d_qid_num << std::endl; std::vector< Node > args; for( unsigned i=0; i<f[0].getNumChildren(); i++ ){ args.push_back( f[0][i] ); @@ -1432,6 +1558,12 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut if( computeOption==COMPUTE_ELIM_SYMBOLS ){ n = computeElimSymbols( n ); }else if( computeOption==COMPUTE_MINISCOPING ){ + if( options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL || options::prenexQuant()==PRENEX_QUANT_NORMAL ){ + if( !qa.d_qid_num.isNull() ){ + //already processed this, return self + return f; + } + } //return directly return computeMiniscoping( args, n, qa ); }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){ @@ -1446,7 +1578,14 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut }else if( computeOption==COMPUTE_COND_SPLIT ){ n = computeCondSplit( n, qa ); }else if( computeOption==COMPUTE_PRENEX ){ - n = computePrenex( n, args, true ); + if( options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL || options::prenexQuant()==PRENEX_QUANT_NORMAL ){ + //will rewrite at preprocess time + return f; + }else{ + std::vector< Node > nargs; + n = computePrenex( n, args, nargs, true, false ); + Assert( nargs.empty() ); + } }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ n = computeVarElimination( n, args, qa ); } @@ -1592,6 +1731,15 @@ bool QuantifiersRewriter::containsQuantifiers( Node n ){ return cq; } } +bool QuantifiersRewriter::isPrenexNormalForm( Node n ) { + if( n.getKind()==FORALL ){ + return n[1].getKind()!=FORALL && isPrenexNormalForm( n[1] ); + }else if( n.getKind()==NOT ){ + return n[0].getKind()!=NOT && isPrenexNormalForm( n[0] ); + }else{ + return !containsQuantifiers( n ); + } +} Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector< TNode >& fvs ){ Trace("pre-sk") << "Pre-skolem " << n << " " << polarity << " " << fvs.size() << endl; @@ -1662,21 +1810,37 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v return n; } + Node QuantifiersRewriter::preprocess( Node n, bool isInst ) { Node prev = n; - if( options::preSkolemQuant() ){ - if( !isInst || !options::preSkolemQuantNested() ){ - Trace("quantifiers-preprocess-debug") << "Pre-skolemize " << n << "..." << std::endl; - //apply pre-skolemization to existential quantifiers - std::vector< TypeNode > fvTypes; - std::vector< TNode > fvs; - n = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs ); + if( n.getKind() == kind::REWRITE_RULE ){ + n = quantifiers::QuantifiersRewriter::rewriteRewriteRule( n ); + }else{ + if( options::preSkolemQuant() ){ + if( !isInst || !options::preSkolemQuantNested() ){ + Trace("quantifiers-preprocess-debug") << "Pre-skolemize " << n << "..." << std::endl; + //apply pre-skolemization to existential quantifiers + std::vector< TypeNode > fvTypes; + std::vector< TNode > fvs; + n = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs ); + } } } + //pull all quantifiers globally + if( options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL || options::prenexQuant()==PRENEX_QUANT_NORMAL ){ + Trace("quantifiers-prenex") << "Prenexing : " << n << std::endl; + n = quantifiers::QuantifiersRewriter::computePrenexAgg( n, true ); + n = Rewriter::rewrite( n ); + Trace("quantifiers-prenex") << "Prenexing returned : " << n << std::endl; + //Assert( isPrenexNormalForm( n ) ); + } if( n!=prev ){ - Trace("quantifiers-preprocess") << "Preprocess " << prev<< std::endl; + Trace("quantifiers-preprocess") << "Preprocess " << prev << std::endl; Trace("quantifiers-preprocess") << "..returned " << n << std::endl; } return n; } +}/* CVC4::theory::quantifiers namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 60dc8ab10..90a22f4b7 100755 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -38,7 +38,6 @@ public: private: static bool addCheckElimChild( std::vector< Node >& children, Node c, Kind k, std::map< Node, bool >& lit_pol, bool& childrenChanged ); static void addNodeToOrBuilder( Node n, NodeBuilder<>& t ); - static Node mkForAll( std::vector< Node >& args, Node body, QAttributes& qa ); static void computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n, std::map< Node, bool >& visited ); static void computeArgVec( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n ); static void computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl ); @@ -53,14 +52,15 @@ private: static bool computeVariableElimLit( Node n, bool pol, std::vector< Node >& args, std::vector< Node >& var, std::vector< Node >& subs, std::map< Node, std::map< bool, std::map< Node, bool > > >& num_bounds ); static Node computeVarElimination2( Node body, std::vector< Node >& args, QAttributes& qa ); -private: +public: static Node computeElimSymbols( Node body ); static Node computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa ); static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body ); //cache is dependent upon currCond, icache is not, new_conds are negated conditions static Node computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q, QAttributes& qa ); static Node computeCondSplit( Node body, QAttributes& qa ); - static Node computePrenex( Node body, std::vector< Node >& args, bool pol ); + static Node computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol, bool prenexAgg ); + static Node computePrenexAgg( Node n, bool topLevel ); static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ); static Node computeVarElimination( Node body, std::vector< Node >& args, QAttributes& qa ); private: @@ -89,8 +89,11 @@ private: static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector<TNode>& fvs); public: static Node rewriteRewriteRule( Node r ); - static bool containsQuantifiers(Node n); + static bool containsQuantifiers( Node n ); + static bool isPrenexNormalForm( Node n ); static Node preprocess( Node n, bool isInst = false ); + static Node mkForAll( std::vector< Node >& args, Node body, QAttributes& qa ); + static Node mkForall( std::vector< Node >& args, Node body, bool marked = false ); };/* class QuantifiersRewriter */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 2b90520fd..aae8f6c5b 100755 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -51,7 +51,10 @@ private: //what each literal does class RDomainLit { public: - RDomainLit() : d_merge(false){} + RDomainLit() : d_merge(false){ + d_rd[0] = NULL; + d_rd[1] = NULL; + } ~RDomainLit(){} bool d_merge; RDomain * d_rd[2]; @@ -72,6 +75,7 @@ public: RDomain * getRDomain( Node n, int i, bool getParent = true ); };/* class RelevantDomain */ + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index 2c58b8f77..ec1b41a98 100755 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -20,6 +20,7 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/inst_match_generator.h" #include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/quant_conflict_find.h" #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/term_database.h" #include "theory/theory_engine.h" @@ -204,6 +205,7 @@ int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) { Trace("rewrite-engine-inst-debug") << "...No qinfo." << std::endl; } } + d_quantEngine->d_statistics.d_instantiations_rr += addedLemmas; Trace("rewrite-engine-inst") << "-> Generated " << addedLemmas << " lemmas." << std::endl; return addedLemmas; } @@ -294,6 +296,11 @@ void RewriteEngine::assertNode( Node n ) { } +bool RewriteEngine::checkCompleteFor( Node q ) { + // by semantics of rewrite rules, saturation -> SAT + return std::find( d_rr_quant.begin(), d_rr_quant.end(), q )!=d_rr_quant.end(); +} + 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() ){ diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h index 424530696..ef3337e53 100755 --- a/src/theory/quantifiers/rewrite_engine.h +++ b/src/theory/quantifiers/rewrite_engine.h @@ -18,19 +18,17 @@ #ifndef __CVC4__REWRITE_ENGINE_H #define __CVC4__REWRITE_ENGINE_H -#include "theory/quantifiers_engine.h" -#include "theory/quantifiers/trigger.h" - +#include "context/cdchunk_list.h" #include "context/context.h" #include "context/context_mm.h" -#include "context/cdchunk_list.h" +#include "theory/quantifiers/trigger.h" +#include "theory/quantifiers/quant_conflict_find.h" +#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { namespace quantifiers { -class QuantInfo; - class RewriteEngine : public QuantifiersModule { typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; @@ -57,7 +55,8 @@ public: bool needsCheck( Theory::Effort e ); void check( Theory::Effort e, unsigned quant_e ); void registerQuantifier( Node f ); - void assertNode( Node n ); + void assertNode( Node n ); + bool checkCompleteFor( Node q ); /** Identify this module */ std::string identify() const { return "RewriteEngine"; } }; diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index d3a5e178f..2c6bfb7d3 100755 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -33,14 +33,14 @@ #include "util/bitvector.h" using namespace std; -using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; - using namespace CVC4::theory::inst; +namespace CVC4 { +namespace theory { +namespace quantifiers { + TNode TermArgTrie::existsTerm( std::vector< TNode >& reps, int argIndex ) { if( argIndex==(int)reps.size() ){ if( d_data.empty() ){ @@ -84,15 +84,25 @@ void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) { } } -TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_inactive_map( c ), d_op_id_count( 0 ), d_typ_id_count( 0 ) { - d_true = NodeManager::currentNM()->mkConst( true ); - d_false = NodeManager::currentNM()->mkConst( false ); - d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); - d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); - if( options::ceGuidedInst() ){ - d_sygus_tdb = new TermDbSygus( c, qe ); - }else{ - d_sygus_tdb = NULL; +TermDb::TermDb(context::Context* c, context::UserContext* u, + QuantifiersEngine* qe) + : d_quantEngine(qe), + d_inactive_map(c), + d_op_id_count(0), + d_typ_id_count(0), + d_sygus_tdb(NULL) { + d_consistent_ee = true; + d_true = NodeManager::currentNM()->mkConst(true); + d_false = NodeManager::currentNM()->mkConst(false); + d_zero = NodeManager::currentNM()->mkConst(Rational(0)); + d_one = NodeManager::currentNM()->mkConst(Rational(1)); + if (options::ceGuidedInst()) { + d_sygus_tdb = new TermDbSygus(c, qe); + } +} +TermDb::~TermDb(){ + if(d_sygus_tdb) { + delete d_sygus_tdb; } } @@ -129,7 +139,7 @@ Node TermDb::getMatchOperator( Node n ) { Kind k = n.getKind(); //datatype operators may be parametric, always assume they are if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON || - k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER ){ + k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER || k==SEP_PTO ){ //since it is parametric, use a particular one as op TypeNode tn = n[0].getType(); Node op = n.getOperator(); @@ -175,17 +185,6 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi if( d_sygus_tdb ){ d_sygus_tdb->registerEvalTerm( n ); } - - if( options::eagerInstQuant() ){ - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){ - int addedLemmas = 0; - for( unsigned i=0; i<d_op_triggers[op].size(); i++ ){ - addedLemmas += d_op_triggers[op][i]->addTerm( n ); - } - } - } - } } }else{ setTermInactive( n ); @@ -1319,19 +1318,25 @@ bool TermDb::mayComplete( TypeNode tn ) { void TermDb::computeVarContains( Node n, std::vector< Node >& varContains ) { std::map< Node, bool > visited; - computeVarContains2( n, varContains, visited ); + computeVarContains2( n, INST_CONSTANT, varContains, visited ); +} + +void TermDb::computeQuantContains( Node n, std::vector< Node >& quantContains ) { + std::map< Node, bool > visited; + computeVarContains2( n, FORALL, quantContains, visited ); } -void TermDb::computeVarContains2( Node n, std::vector< Node >& varContains, std::map< Node, bool >& visited ){ + +void TermDb::computeVarContains2( Node n, Kind k, std::vector< Node >& varContains, std::map< Node, bool >& visited ){ if( visited.find( n )==visited.end() ){ visited[n] = true; - if( n.getKind()==INST_CONSTANT ){ + if( n.getKind()==k ){ if( std::find( varContains.begin(), varContains.end(), n )==varContains.end() ){ varContains.push_back( n ); } }else{ for( unsigned i=0; i<n.getNumChildren(); i++ ){ - computeVarContains2( n[i], varContains, visited ); + computeVarContains2( n[i], k, varContains, visited ); } } } @@ -1963,7 +1968,7 @@ bool TermDb::isComm( Kind k ) { } bool TermDb::isBoolConnective( Kind k ) { - return k==OR || k==AND || k==IFF || k==ITE || k==FORALL || k==NOT; + return k==OR || k==AND || k==IFF || k==ITE || k==FORALL || k==NOT || k==SEP_STAR; } void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){ @@ -2163,6 +2168,10 @@ void TermDb::computeQuantAttributes( Node q, QAttributes& qa ){ qa.d_quant_elim_partial = true; //don't set owner, should happen naturally } + if( avar.hasAttribute(QuantIdNumAttribute()) ){ + qa.d_qid_num = avar; + Trace("quant-attr") << "Attribute : id number " << qa.d_qid_num.getAttribute(QuantIdNumAttribute()) << " : " << q << std::endl; + } if( avar.getKind()==REWRITE_RULE ){ Trace("quant-attr") << "Attribute : rewrite rule : " << q << std::endl; Assert( i==0 ); @@ -2254,6 +2263,25 @@ bool TermDb::isQAttrQuantElimPartial( Node q ) { } } +int TermDb::getQAttrQuantIdNum( Node q ) { + std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); + if( it!=d_qattr.end() ){ + if( !it->second.d_qid_num.isNull() ){ + return it->second.d_qid_num.getAttribute(QuantIdNumAttribute()); + } + } + return -1; +} + +Node TermDb::getQAttrQuantIdNumNode( Node q ) { + std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); + if( it==d_qattr.end() ){ + return Node::null(); + }else{ + return it->second.d_qid_num; + } +} + TermDbSygus::TermDbSygus( context::Context* c, QuantifiersEngine* qe ) : d_quantEngine( qe ){ d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); @@ -3125,7 +3153,6 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node > std::string name = std::string( str.begin() + found +1, str.end() ); out << name; }else{ - Trace("ajr-temp") << "[[print operator " << op << "]]" << std::endl; out << op; } if( n.getNumChildren()>0 ){ @@ -3281,3 +3308,6 @@ void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& lems } } +}/* CVC4::theory::quantifiers namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 7ab3668eb..d4fdaa5e5 100755 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -105,6 +105,11 @@ typedef expr::Attribute< QuantElimAttributeId, bool > QuantElimAttribute; struct QuantElimPartialAttributeId {}; typedef expr::Attribute< QuantElimPartialAttributeId, bool > QuantElimPartialAttribute; +/** Attribute for id number */ +struct QuantIdNumAttributeId {}; +typedef expr::Attribute< QuantIdNumAttributeId, uint64_t > QuantIdNumAttribute; + + class QuantifiersEngine; namespace inst{ @@ -145,6 +150,7 @@ public: bool d_quant_elim; bool d_quant_elim_partial; Node d_ipl; + Node d_qid_num; bool isRewriteRule() { return !d_rr.isNull(); } bool isFunDef() { return !d_fundef_f.isNull(); } }; @@ -182,23 +188,25 @@ private: std::map< Node, std::map< TypeNode, Node > > d_par_op_map; /** whether master equality engine is UF-inconsistent */ bool d_consistent_ee; -public: - TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ); - ~TermDb(){} + + public: + TermDb(context::Context* c, context::UserContext* u, QuantifiersEngine* qe); + ~TermDb(); /** boolean terms */ Node d_true; Node d_false; /** constants */ Node d_zero; Node d_one; -public: + + public: /** presolve (called once per user check-sat) */ void presolve(); /** reset (calculate which terms are active) */ bool reset( Theory::Effort effort ); /** identify */ std::string identify() const { return "TermDb"; } -private: + private: /** map from operators to ground terms for that operator */ std::map< Node, std::vector< Node > > d_op_map; /** map from type nodes to terms of that type */ @@ -301,8 +309,6 @@ private: /** map from universal quantifiers to the list of variables */ std::map< Node, std::vector< Node > > d_vars; std::map< Node, std::map< Node, unsigned > > d_var_num; - /** map from universal quantifiers to the list of instantiation constants */ - std::map< Node, std::vector< Node > > d_inst_constants; /** map from universal quantifiers to their inst constant body */ std::map< Node, Node > d_inst_const_body; /** map from universal quantifiers to their counterexample literals */ @@ -312,6 +318,8 @@ private: /** make instantiation constants for */ void makeInstantiationConstantsFor( Node q ); public: + /** map from universal quantifiers to the list of instantiation constants */ + std::map< Node, std::vector< Node > > d_inst_constants; /** get variable number */ unsigned getVariableNum( Node q, Node v ) { return d_var_num[q][v]; } /** get the i^th instantiation constant of q */ @@ -388,7 +396,7 @@ public: //for triggers private: /** helper function for compute var contains */ - static void computeVarContains2( Node n, std::vector< Node >& varContains, std::map< Node, bool >& visited ); + 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 */ @@ -402,6 +410,8 @@ public: static void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains ); /** get var contains for node n */ static void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ); + /** compute quant contains */ + static void computeQuantContains( Node n, std::vector< Node >& quantContains ); /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */ static int isInstanceOf( Node n1, Node n2 ); /** filter all nodes that have instances */ @@ -541,6 +551,10 @@ public: bool isQAttrQuantElim( Node q ); /** is quant elim partial */ bool isQAttrQuantElimPartial( Node q ); + /** get quant id num */ + int getQAttrQuantIdNum( Node q ); + /** get quant id num */ + Node getQAttrQuantIdNumNode( Node q ); /** compute quantifier attributes */ static void computeQuantAttributes( Node q, QAttributes& qa ); };/* class TermDb */ diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 7ad13b3a8..e97a76ce6 100755 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -88,6 +88,13 @@ void TheoryQuantifiers::presolve() { } } +void TheoryQuantifiers::ppNotifyAssertions( std::vector< Node >& assertions ) { + Trace("quantifiers-presolve") << "TheoryQuantifiers::ppNotifyAssertions" << std::endl; + if( getQuantifiersEngine() ){ + getQuantifiersEngine()->ppNotifyAssertions( assertions ); + } +} + Node TheoryQuantifiers::getValue(TNode n) { //NodeManager* nodeManager = NodeManager::currentNM(); switch(n.getKind()) { diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 6775e0536..ba5a75d86 100755 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -61,6 +61,7 @@ public: void notifyEq(TNode lhs, TNode rhs); void preRegisterTerm(TNode n); void presolve(); + void ppNotifyAssertions( std::vector< Node >& assertions ); void check(Effort e); Node getNextDecisionRequest(); Node getValue(TNode n); diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 2faed3af0..3017238ca 100755 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -76,12 +76,6 @@ Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes ) ++(qe->d_statistics.d_multi_triggers); } //Notice() << "Trigger : " << (*this) << " for " << f << std::endl; - if( options::eagerInstQuant() ){ - for( int i=0; i<(int)d_nodes.size(); i++ ){ - Node op = qe->getTermDatabase()->getMatchOperator( d_nodes[i] ); - qe->getTermDatabase()->registerTrigger( this, op ); - } - } Trace("trigger-debug") << "Finished making trigger." << std::endl; } @@ -107,10 +101,6 @@ bool Trigger::getMatch( Node f, Node t, InstMatch& m ){ return ((InstMatchGenerator*)d_mg)->getMatch( f, t, m, d_quantEngine ); } -int Trigger::addTerm( Node t ){ - return d_mg->addTerm( d_f, t, d_quantEngine ); -} - Node Trigger::getInstPattern(){ return NodeManager::currentNM()->mkNode( INST_PATTERN, d_nodes ); } @@ -363,7 +353,8 @@ bool Trigger::isAtomicTrigger( Node n ){ bool Trigger::isAtomicTriggerKind( Kind k ) { return k==APPLY_UF || k==SELECT || k==STORE || k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER || - k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON; + k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON || + k==SEP_PTO; } bool Trigger::isRelationalTrigger( Node n ) { diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 6d7bf1f4d..631627331 100755 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -72,8 +72,6 @@ class Trigger { Currently the trigger should not be a multi-trigger. */ bool getMatch( Node f, Node t, InstMatch& m); - /** add ground term t, called when t is added to the TermDb */ - int addTerm( Node t ); /** return whether this is a multi-trigger */ bool isMultiTrigger() { return d_nodes.size()>1; } /** get inst pattern list */ |