From: Andrew Reynolds Date: Mon, 10 Sep 2018 20:52:05 +0000 (-0500) Subject: Squash implementation of counterexample-guided instantiation (#2423) X-Git-Tag: cvc5-1.0.0~4667 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=29acf0bb9fa0f7b5679360920c062179498e4a3b;p=cvc5.git Squash implementation of counterexample-guided instantiation (#2423) --- diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp index ac76ee31f..9b82c1f4b 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp @@ -34,28 +34,58 @@ using namespace CVC4::kind; using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; -using namespace CVC4::theory::arith; -#define ARITH_INSTANTIATOR_USE_MINUS_DELTA +bool CegqiOutputInstStrategy::doAddInstantiation(std::vector& subs) +{ + return d_out->doAddInstantiation(subs); +} + +bool CegqiOutputInstStrategy::isEligibleForInstantiation(Node n) +{ + return d_out->isEligibleForInstantiation(n); +} -InstStrategyCbqi::InstStrategyCbqi(QuantifiersEngine* qe) +bool CegqiOutputInstStrategy::addLemma(Node lem) +{ + return d_out->addLemma(lem); +} + +InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe) : QuantifiersModule(qe), d_cbqi_set_quant_inactive(false), d_incomplete_check(false), d_added_cbqi_lemma(qe->getUserContext()), d_elim_quants(qe->getSatContext()), + d_out(new CegqiOutputInstStrategy(this)), d_nested_qe_waitlist_size(qe->getUserContext()), d_nested_qe_waitlist_proc(qe->getUserContext()) //, d_added_inst( qe->getUserContext() ) { d_qid_count = 0; + d_small_const = + NodeManager::currentNM()->mkConst(Rational(1) / Rational(1000000)); + d_check_vts_lemma_lc = false; +} + +InstStrategyCegqi::~InstStrategyCegqi() +{ + for (std::map::iterator i = d_cinst.begin(), + iend = d_cinst.end(); + i != iend; + ++i) + { + CegInstantiator* instantiator = (*i).second; + delete instantiator; + } + d_cinst.clear(); } -bool InstStrategyCbqi::needsCheck( Theory::Effort e ) { +bool InstStrategyCegqi::needsCheck(Theory::Effort e) +{ return e>=Theory::EFFORT_LAST_CALL; } -QuantifiersModule::QEffort InstStrategyCbqi::needsModel(Theory::Effort e) +QuantifiersModule::QEffort InstStrategyCegqi::needsModel(Theory::Effort e) { for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); @@ -66,7 +96,8 @@ QuantifiersModule::QEffort InstStrategyCbqi::needsModel(Theory::Effort e) return QEFFORT_NONE; } -bool InstStrategyCbqi::registerCbqiLemma( Node q ) { +bool InstStrategyCegqi::registerCbqiLemma(Node q) +{ if( !hasAddedCbqiLemma( q ) ){ d_added_cbqi_lemma.insert( q ); Trace("cbqi-debug") << "Do cbqi for " << q << std::endl; @@ -164,7 +195,8 @@ bool InstStrategyCbqi::registerCbqiLemma( Node q ) { } } -void InstStrategyCbqi::reset_round( Theory::Effort effort ) { +void InstStrategyCegqi::reset_round(Theory::Effort effort) +{ d_cbqi_set_quant_inactive = false; d_incomplete_check = false; d_active_quant.clear(); @@ -238,11 +270,10 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) { Trace("cbqi-debug") << "...done removing." << std::endl; } } - - processResetInstantiationRound( effort ); + d_check_vts_lemma_lc = false; } -void InstStrategyCbqi::check(Theory::Effort e, QEffort quant_e) +void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e) { if (quant_e == QEFFORT_STANDARD) { @@ -284,7 +315,8 @@ void InstStrategyCbqi::check(Theory::Effort e, QEffort quant_e) } } -bool InstStrategyCbqi::checkComplete() { +bool InstStrategyCegqi::checkComplete() +{ if( ( !options::cbqiSat() && d_cbqi_set_quant_inactive ) || d_incomplete_check ){ return false; }else{ @@ -292,7 +324,8 @@ bool InstStrategyCbqi::checkComplete() { } } -bool InstStrategyCbqi::checkCompleteFor( Node q ) { +bool InstStrategyCegqi::checkCompleteFor(Node q) +{ std::map::iterator it = d_do_cbqi.find(q); if( it!=d_do_cbqi.end() ){ return it->second != CEG_UNHANDLED; @@ -301,7 +334,9 @@ bool InstStrategyCbqi::checkCompleteFor( Node q ) { } } -Node InstStrategyCbqi::getIdMarkedQuantNode( Node n, std::map< Node, Node >& visited ){ +Node InstStrategyCegqi::getIdMarkedQuantNode(Node n, + std::map& visited) +{ std::map< Node, Node >::iterator it = visited.find( n ); if( it==visited.end() ){ Node ret = n; @@ -348,7 +383,7 @@ Node InstStrategyCbqi::getIdMarkedQuantNode( Node n, std::map< Node, Node >& vis } } -void InstStrategyCbqi::checkOwnership(Node q) +void InstStrategyCegqi::checkOwnership(Node q) { if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){ if (d_do_cbqi[q] == CEG_HANDLED) @@ -359,7 +394,7 @@ void InstStrategyCbqi::checkOwnership(Node q) } } -void InstStrategyCbqi::preRegisterQuantifier(Node q) +void InstStrategyCegqi::preRegisterQuantifier(Node q) { // mark all nested quantifiers with id if (options::cbqiNestedQE()) @@ -389,13 +424,21 @@ void InstStrategyCbqi::preRegisterQuantifier(Node q) } } if( doCbqi( q ) ){ + // get the instantiator + if (options::cbqiPreRegInst()) + { + getInstantiator(q); + } + // register the cbqi lemma if( registerCbqiLemma( q ) ){ Trace("cbqi") << "Registered cbqi lemma for quantifier : " << q << std::endl; } } } -Node InstStrategyCbqi::doNestedQENode( Node q, Node ceq, Node n, std::vector< Node >& inst_terms, bool doVts ) { +Node InstStrategyCegqi::doNestedQENode( + Node q, Node ceq, Node n, std::vector& 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. @@ -425,7 +468,12 @@ Node InstStrategyCbqi::doNestedQENode( Node q, Node ceq, Node n, std::vector< No return ret; } -Node InstStrategyCbqi::doNestedQERec( Node q, Node n, std::map< Node, Node >& visited, std::vector< Node >& inst_terms, bool doVts ) { +Node InstStrategyCegqi::doNestedQERec(Node q, + Node n, + std::map& visited, + std::vector& inst_terms, + bool doVts) +{ if( visited.find( n )==visited.end() ){ Node ret = n; if( n.getKind()==FORALL ){ @@ -482,17 +530,40 @@ Node InstStrategyCbqi::doNestedQERec( Node q, Node n, std::map< Node, Node >& vi } } -Node InstStrategyCbqi::doNestedQE( Node q, std::vector< Node >& inst_terms, Node lem, bool doVts ) { +Node InstStrategyCegqi::doNestedQE(Node q, + std::vector& 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 ); +void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem) +{ + // must register with the instantiator + // must explicitly remove ITEs so that we record dependencies + std::vector ce_vars; + TermUtil* tutil = d_quantEngine->getTermUtil(); + for (unsigned i = 0, nics = tutil->getNumInstantiationConstants(q); i < nics; + i++) + { + ce_vars.push_back(tutil->getInstantiationConstant(q, i)); + } + std::vector lems; + lems.push_back(lem); + CegInstantiator* cinst = getInstantiator(q); + cinst->registerCounterexampleLemma(lems, ce_vars); + for (unsigned i = 0, size = lems.size(); i < size; i++) + { + Trace("cbqi-debug") << "Counterexample lemma " << i << " : " << lems[i] + << std::endl; + d_quantEngine->addLemma(lems[i], false); + } } -bool InstStrategyCbqi::doCbqi( Node q ){ +bool InstStrategyCegqi::doCbqi(Node q) +{ std::map::iterator it = d_do_cbqi.find(q); if( it==d_do_cbqi.end() ){ CegHandledStatus ret = CegInstantiator::isCbqiQuant(q, d_quantEngine); @@ -503,7 +574,9 @@ bool InstStrategyCbqi::doCbqi( Node q ){ return it->second != CEG_UNHANDLED; } -Node InstStrategyCbqi::getNextDecisionRequestProc( Node q, std::map< Node, bool >& proc ) { +Node InstStrategyCegqi::getNextDecisionRequestProc(Node q, + std::map& proc) +{ if( proc.find( q )==proc.end() ){ proc[q] = true; //first check children @@ -529,7 +602,8 @@ Node InstStrategyCbqi::getNextDecisionRequestProc( Node q, std::map< Node, bool return Node::null(); } -Node InstStrategyCbqi::getNextDecisionRequest( unsigned& priority ){ +Node InstStrategyCegqi::getNextDecisionRequest(unsigned& priority) +{ std::map< Node, bool > proc; //for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ // Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); @@ -544,46 +618,6 @@ Node InstStrategyCbqi::getNextDecisionRequest( unsigned& priority ){ return Node::null(); } - - -//new implementation - -bool CegqiOutputInstStrategy::doAddInstantiation( std::vector< Node >& subs ) { - return d_out->doAddInstantiation( subs ); -} - -bool CegqiOutputInstStrategy::isEligibleForInstantiation( Node n ) { - return d_out->isEligibleForInstantiation( n ); -} - -bool CegqiOutputInstStrategy::addLemma( Node lem ) { - return d_out->addLemma( lem ); -} - - -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() -{ - delete d_out; - - for(std::map< Node, CegInstantiator * >::iterator i = d_cinst.begin(), - iend = d_cinst.end(); i != iend; ++i) { - CegInstantiator * instantiator = (*i).second; - delete instantiator; - } - d_cinst.clear(); -} - -void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) { - d_check_vts_lemma_lc = false; -} - void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) { if( e==0 ){ CegInstantiator * cinst = getInstantiator( q ); @@ -676,7 +710,8 @@ bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) { CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) { std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( q ); if( it==d_cinst.end() ){ - CegInstantiator * cinst = new CegInstantiator( d_quantEngine, d_out, true, true ); + CegInstantiator* cinst = + new CegInstantiator(d_quantEngine, d_out.get(), true, true); d_cinst[q] = cinst; return cinst; }else{ @@ -684,37 +719,6 @@ CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) { } } -void InstStrategyCegqi::preRegisterQuantifier(Node q) -{ - if( doCbqi( q ) ){ - // get the instantiator - if( options::cbqiPreRegInst() ){ - getInstantiator( q ); - } - // register the cbqi lemma - if( registerCbqiLemma( q ) ){ - Trace("cbqi") << "Registered cbqi lemma for quantifier : " << q << std::endl; - } - } -} - -void InstStrategyCegqi::registerCounterexampleLemma( Node q, Node lem ) { - //must register with the instantiator - //must explicitly remove ITEs so that we record dependencies - std::vector< Node > ce_vars; - for( unsigned i=0; igetTermUtil()->getNumInstantiationConstants( q ); i++ ){ - ce_vars.push_back( d_quantEngine->getTermUtil()->getInstantiationConstant( q, i ) ); - } - std::vector< Node > lems; - lems.push_back( lem ); - CegInstantiator * cinst = getInstantiator( q ); - cinst->registerCounterexampleLemma( lems, ce_vars ); - for( unsigned i=0; iaddLemma( lems[i], false ); - } -} - void InstStrategyCegqi::presolve() { if( options::cbqiPreRegInst() ){ for( std::map< Node, CegInstantiator * >::iterator it = d_cinst.begin(); it != d_cinst.end(); ++it ){ diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h index 4334652da..433de52a8 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h @@ -18,24 +18,90 @@ #ifndef __CVC4__INST_STRATEGY_CBQI_H #define __CVC4__INST_STRATEGY_CBQI_H -#include "theory/arith/arithvar.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" -#include "theory/quantifiers/ematching/instantiation_engine.h" #include "util/statistics_registry.h" namespace CVC4 { namespace theory { +namespace quantifiers { -namespace arith { - class TheoryArith; -} +class InstStrategyCegqi; -namespace quantifiers { +/** + * An output channel class, used by instantiator objects below. The methods + * of this class call the corresponding functions of InstStrategyCegqi below. + */ +class CegqiOutputInstStrategy : public CegqiOutput +{ + public: + CegqiOutputInstStrategy(InstStrategyCegqi* out) : d_out(out) {} + /** The module whose functions we call. */ + InstStrategyCegqi* d_out; + /** add instantiation */ + bool doAddInstantiation(std::vector& subs) override; + /** is eligible for instantiation */ + bool isEligibleForInstantiation(Node n) override; + /** add lemma */ + bool addLemma(Node lem) override; +}; -class InstStrategyCbqi : public QuantifiersModule { +/** + * Counterexample-guided quantifier instantiation module. + * + * This class manages counterexample-guided instantiation strategies for all + * asserted quantified formulas. + */ +class InstStrategyCegqi : public QuantifiersModule +{ typedef context::CDHashSet NodeSet; typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap; + public: + InstStrategyCegqi(QuantifiersEngine* qe); + ~InstStrategyCegqi(); + + /** whether to do counterexample-guided instantiation for quantifier q */ + bool doCbqi(Node q); + /** needs check at effort */ + bool needsCheck(Theory::Effort e) override; + /** needs model at effort */ + QEffort needsModel(Theory::Effort e) override; + /** reset round */ + void reset_round(Theory::Effort e) override; + /** check */ + void check(Theory::Effort e, QEffort quant_e) override; + /** check complete */ + bool checkComplete() override; + /** check complete for quantified formula */ + bool checkCompleteFor(Node q) override; + /** check ownership */ + void checkOwnership(Node q) override; + /** identify */ + std::string identify() const override { return std::string("Cegqi"); } + /** get instantiator for quantifier */ + CegInstantiator* getInstantiator(Node q); + /** pre-register quantifier */ + void preRegisterQuantifier(Node q) override; + // presolve + void presolve() override; + /** get next decision request */ + Node getNextDecisionRequest(unsigned& priority) override; + /** Do nested quantifier elimination. */ + Node doNestedQE(Node q, std::vector& inst_terms, Node lem, bool doVts); + + //------------------- interface for CegqiOutputInstStrategy + /** Instantiate the current quantified formula forall x. Q with x -> subs. */ + bool doAddInstantiation(std::vector& subs); + /** + * Are we allowed to instantiate the current quantified formula with n? This + * includes restrictions such as if n is a variable, it must occur free in + * the current quantified formula. + */ + bool isEligibleForInstantiation(Node n); + /** Add lemma lem via the output channel of this class. */ + bool addLemma(Node lem); + //------------------- end interface for CegqiOutputInstStrategy + protected: /** set quantified formula inactive * @@ -60,18 +126,49 @@ class InstStrategyCbqi : public QuantifiersModule { std::map< Node, bool > d_active_quant; /** Whether cegqi handles each quantified formula. */ std::map d_do_cbqi; + /** + * An output channel used by instantiators for communicating with this + * class. + */ + std::unique_ptr d_out; + /** + * The instantiator for each quantified formula q registered to this class. + * This object is responsible for finding instantiatons for q. + */ + std::map d_cinst; + /** the current quantified formula we are processing */ + Node d_curr_quant; + //---------------------- for vts delta minimization + /** + * Whether we will use vts delta minimization. If this flag is true, we + * add lemmas on demand of the form delta < c^1, delta < c^2, ... where c + * is a small (< 1) constant. This heuristic is used in strategies where + * vts delta cannot be fully eliminated from assertions (for example, when + * using nested quantifiers and a non-innermost instantiation strategy). + * The same strategy applies for vts infinity, which we add lemmas of the + * form inf > (1/c)^1, inf > (1/c)^2, .... + */ + bool d_check_vts_lemma_lc; + /** a small constant, used as a coefficient above */ + Node d_small_const; + //---------------------- end for vts delta minimization /** register ce lemma */ bool registerCbqiLemma( Node q ); - virtual void registerCounterexampleLemma( Node q, Node lem ); + /** register counterexample lemma + * + * This is called when we have constructed lem, the negation of the body of + * quantified formula q, skolemized with the instantiation constants of q. + * This function is used for setting up the proper information in the + * instantiator for q. + */ + 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(); } /** 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; + void process(Node q, Theory::Effort effort, int e); - protected: //for identification uint64_t d_qid_count; //nested qe map @@ -98,71 +195,8 @@ class InstStrategyCbqi : public QuantifiersModule { 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 ); - - /** whether to do CBQI for quantifier q */ - bool doCbqi( Node q ); - /** process functions */ - bool needsCheck(Theory::Effort e) override; - QEffort needsModel(Theory::Effort e) override; - void reset_round(Theory::Effort e) override; - void check(Theory::Effort e, QEffort quant_e) override; - bool checkComplete() override; - bool checkCompleteFor(Node q) override; - void checkOwnership(Node q) override; - void preRegisterQuantifier(Node q) override; - /** get next decision request */ - Node getNextDecisionRequest(unsigned& priority) override; }; -//generalized counterexample guided quantifier instantiation - -class InstStrategyCegqi; - -class CegqiOutputInstStrategy : public CegqiOutput { -public: - CegqiOutputInstStrategy( InstStrategyCegqi * out ) : d_out( out ){} - InstStrategyCegqi * d_out; - bool doAddInstantiation(std::vector& subs) override; - bool isEligibleForInstantiation(Node n) override; - bool addLemma(Node lem) override; -}; - -class InstStrategyCegqi : public InstStrategyCbqi { - protected: - CegqiOutputInstStrategy * d_out; - std::map< Node, CegInstantiator * > d_cinst; - Node d_small_const; - Node d_curr_quant; - bool d_check_vts_lemma_lc; - /** process functions */ - void processResetInstantiationRound(Theory::Effort effort) override; - void process(Node f, Theory::Effort effort, int e) override; - /** register ce lemma */ - void registerCounterexampleLemma(Node q, Node lem) override; - - public: - InstStrategyCegqi( QuantifiersEngine * qe ); - ~InstStrategyCegqi() override; - - bool doAddInstantiation( std::vector< Node >& subs ); - bool isEligibleForInstantiation( Node n ); - bool addLemma( Node lem ); - /** identify */ - std::string identify() const override { return std::string("Cegqi"); } - - //get instantiator for quantifier - CegInstantiator * getInstantiator( Node q ); - /** pre-register quantifier */ - void preRegisterQuantifier(Node q) override; - //presolve - void presolve() override; -}; } } diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 24f418b0c..13597c338 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -245,10 +245,10 @@ bool Instantiate::addInstantiation( Node orig_body = body; if (options::cbqiNestedQE()) { - InstStrategyCbqi* icbqi = d_qe->getInstStrategyCbqi(); - if (icbqi) + InstStrategyCegqi* icegqi = d_qe->getInstStrategyCegqi(); + if (icegqi) { - body = icbqi->doNestedQE(q, terms, body, doVts); + body = icegqi->doNestedQE(q, terms, body, doVts); } } body = quantifiers::QuantifiersRewriter::preprocess(body, true); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 038fa9e73..305f3182d 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -382,7 +382,7 @@ quantifiers::InstStrategyEnum* QuantifiersEngine::getInstStrategyEnum() const { return d_fs.get(); } -quantifiers::InstStrategyCbqi* QuantifiersEngine::getInstStrategyCbqi() const +quantifiers::InstStrategyCegqi* QuantifiersEngine::getInstStrategyCegqi() const { return d_i_cbqi.get(); } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 662803323..2c97fd099 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -72,7 +72,6 @@ namespace quantifiers { class LtePartialInst; class AlphaEquivalence; class InstStrategyEnum; - class InstStrategyCbqi; class InstStrategyCegqi; class QuantDSplit; class QuantAntiSkolem; @@ -155,7 +154,7 @@ public: /** get full saturation */ quantifiers::InstStrategyEnum* getInstStrategyEnum() const; /** get inst strategy cbqi */ - quantifiers::InstStrategyCbqi* getInstStrategyCbqi() const; + quantifiers::InstStrategyCegqi* getInstStrategyCegqi() const; //---------------------- end modules private: /** owner of quantified formulas */ @@ -384,7 +383,7 @@ public: /** full saturation */ std::unique_ptr d_fs; /** counterexample-based quantifier instantiation */ - std::unique_ptr d_i_cbqi; + std::unique_ptr d_i_cbqi; /** quantifiers splitting */ std::unique_ptr d_qsplit; /** quantifiers anti-skolemization */