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<Node>& 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<Node, CegInstantiator*>::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; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
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;
}
}
-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();
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)
{
}
}
-bool InstStrategyCbqi::checkComplete() {
+bool InstStrategyCegqi::checkComplete()
+{
if( ( !options::cbqiSat() && d_cbqi_set_quant_inactive ) || d_incomplete_check ){
return false;
}else{
}
}
-bool InstStrategyCbqi::checkCompleteFor( Node q ) {
+bool InstStrategyCegqi::checkCompleteFor(Node q)
+{
std::map<Node, CegHandledStatus>::iterator it = d_do_cbqi.find(q);
if( it!=d_do_cbqi.end() ){
return it->second != CEG_UNHANDLED;
}
}
-Node InstStrategyCbqi::getIdMarkedQuantNode( Node n, std::map< Node, Node >& visited ){
+Node InstStrategyCegqi::getIdMarkedQuantNode(Node n,
+ std::map<Node, Node>& visited)
+{
std::map< Node, Node >::iterator it = visited.find( n );
if( it==visited.end() ){
Node ret = n;
}
}
-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)
}
}
-void InstStrategyCbqi::preRegisterQuantifier(Node q)
+void InstStrategyCegqi::preRegisterQuantifier(Node q)
{
// mark all nested quantifiers with id
if (options::cbqiNestedQE())
}
}
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<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.
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<Node, Node>& visited,
+ std::vector<Node>& inst_terms,
+ bool doVts)
+{
if( visited.find( n )==visited.end() ){
Node ret = n;
if( n.getKind()==FORALL ){
}
}
-Node InstStrategyCbqi::doNestedQE( Node q, std::vector< Node >& inst_terms, Node lem, bool doVts ) {
+Node InstStrategyCegqi::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 );
+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;
+ 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<Node> 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<Node, CegHandledStatus>::iterator it = d_do_cbqi.find(q);
if( it==d_do_cbqi.end() ){
CegHandledStatus ret = CegInstantiator::isCbqiQuant(q, d_quantEngine);
return it->second != CEG_UNHANDLED;
}
-Node InstStrategyCbqi::getNextDecisionRequestProc( Node q, std::map< Node, bool >& proc ) {
+Node InstStrategyCegqi::getNextDecisionRequestProc(Node q,
+ std::map<Node, bool>& proc)
+{
if( proc.find( q )==proc.end() ){
proc[q] = true;
//first check children
return Node::null();
}
-Node InstStrategyCbqi::getNextDecisionRequest( unsigned& priority ){
+Node InstStrategyCegqi::getNextDecisionRequest(unsigned& priority)
+{
std::map< Node, bool > proc;
//for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
// Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
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 );
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{
}
}
-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; i<d_quantEngine->getTermUtil()->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; i<lems.size(); i++ ){
- Trace("cbqi-debug") << "Counterexample lemma " << i << " : " << lems[i] << std::endl;
- d_quantEngine->addLemma( lems[i], false );
- }
-}
-
void InstStrategyCegqi::presolve() {
if( options::cbqiPreRegInst() ){
for( std::map< Node, CegInstantiator * >::iterator it = d_cinst.begin(); it != d_cinst.end(); ++it ){
#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<Node>& 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<Node, NodeHashFunction> 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<Node>& inst_terms, Node lem, bool doVts);
+
+ //------------------- interface for CegqiOutputInstStrategy
+ /** Instantiate the current quantified formula forall x. Q with x -> subs. */
+ bool doAddInstantiation(std::vector<Node>& 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
*
std::map< Node, bool > d_active_quant;
/** Whether cegqi handles each quantified formula. */
std::map<Node, CegHandledStatus> d_do_cbqi;
+ /**
+ * An output channel used by instantiators for communicating with this
+ * class.
+ */
+ std::unique_ptr<CegqiOutputInstStrategy> d_out;
+ /**
+ * The instantiator for each quantified formula q registered to this class.
+ * This object is responsible for finding instantiatons for q.
+ */
+ std::map<Node, CegInstantiator*> 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
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<Node>& 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;
-};
}
}
projects / cvc5.git / commitdiff