if( !options::rewriteDivk.wasSetByUser()) {
options::rewriteDivk.set( true );
}
+ if (options::incrementalSolving())
+ {
+ // cannot do nested quantifier elimination in incremental mode
+ options::cbqiNestedQE.set(false);
+ }
if (d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV))
{
options::cbqiAll.set( false );
}
}
-void InstStrategyCbqi::preRegisterQuantifier( Node q ) {
+void InstStrategyCbqi::checkOwnership(Node q)
+{
if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){
if (d_do_cbqi[q] == CEG_HANDLED)
{
//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, we are reducing this quantified formula to a marked
- // one
- d_do_cbqi[q] = CEG_UNHANDLED;
- //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 );
- }
- }
}
}
}
-void InstStrategyCbqi::registerQuantifier( Node q ) {
+void InstStrategyCbqi::preRegisterQuantifier(Node q)
+{
+ // mark all nested quantifiers with id
+ if (options::cbqiNestedQE())
+ {
+ if( d_quantEngine->getOwner(q)==this )
+ {
+ std::map<Node, Node> visited;
+ Node mq = getIdMarkedQuantNode(q[1], visited);
+ if (mq != q[1])
+ {
+ // do not do cbqi, we are reducing this quantified formula to a marked
+ // one
+ d_do_cbqi[q] = CEG_UNHANDLED;
+ // 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->addLemma(mlem);
+ }
+ }
+ }
if( doCbqi( q ) ){
if( registerCbqiLemma( q ) ){
Trace("cbqi") << "Registered cbqi lemma for quantifier : " << q << std::endl;
}
}
-void InstStrategyCegqi::registerQuantifier( Node q ) {
+void InstStrategyCegqi::preRegisterQuantifier(Node q)
+{
if( doCbqi( q ) ){
// get the instantiator
if( options::cbqiPreRegInst() ){
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;
- void registerQuantifier(Node q) override;
/** get next decision request */
Node getNextDecisionRequest(unsigned& priority) override;
};
//get instantiator for quantifier
CegInstantiator * getInstantiator( Node q );
- //register quantifier
- void registerQuantifier(Node q) override;
+ /** pre-register quantifier */
+ void preRegisterQuantifier(Node q) override;
//presolve
void presolve() override;
};
return addedLemmas;
}
-void ConjectureGenerator::registerQuantifier( Node q ) {
-
-}
-
-void ConjectureGenerator::assertNode( Node n ) {
-
-}
-
bool ConjectureGenerator::considerTermCanon( Node ln, bool genRelevant ){
if( !ln.isNull() ){
//do not consider if it is non-canonical, and either:
void reset_round(Theory::Effort e) override;
/* Call during quantifier engine's check */
void check(Theory::Effort e, QEffort quant_e) override;
- /* Called for new quantifiers */
- void registerQuantifier(Node q) override;
- void assertNode(Node n) override;
/** Identify this module (for debugging, dynamic configuration, etc..) */
std::string identify() const override { return "ConjectureGenerator"; }
// options
return false;
}
-void InstantiationEngine::preRegisterQuantifier( Node q ) {
+void InstantiationEngine::checkOwnership(Node q)
+{
if( options::strictTriggers() && q.getNumChildren()==3 ){
//if strict triggers, take ownership of this quantified formula
bool hasPat = false;
void reset_round(Theory::Effort e) override;
void check(Theory::Effort e, QEffort quant_e) override;
bool checkCompleteFor(Node q) override;
- void preRegisterQuantifier(Node q) override;
+ void checkOwnership(Node q) override;
void registerQuantifier(Node q) override;
Node explain(TNode n) { return Node::null(); }
/** add user pattern */
Trace("bound-int-var") << "Bound variable #" << d_set_nums[q][v] << " : " << v << std::endl;
}
-void BoundedIntegers::preRegisterQuantifier( Node f ) {
+void BoundedIntegers::checkOwnership(Node f)
+{
//this needs to be done at preregister since it affects e.g. QuantDSplit's preregister
- Trace("bound-int") << "preRegister quantifier " << f << std::endl;
-
+ Trace("bound-int") << "check ownership quantifier " << f << std::endl;
+
bool success;
do{
std::map< Node, unsigned > bound_lit_type_map;
}
}
-void BoundedIntegers::registerQuantifier( Node q ) {
-
-}
-
void BoundedIntegers::assertNode( Node n ) {
Trace("bound-int-assert") << "Assert " << n << std::endl;
Node nlit = n.getKind()==NOT ? n[0] : n;
void presolve() override;
bool needsCheck(Theory::Effort e) override;
void check(Theory::Effort e, QEffort quant_e) override;
- void registerQuantifier(Node q) override;
- void preRegisterQuantifier(Node q) override;
+ void checkOwnership(Node q) override;
void assertNode(Node n) override;
Node getNextDecisionRequest(unsigned& priority) override;
bool isBoundVar( Node q, Node v ) { return std::find( d_set[q].begin(), d_set[q].end(), v )!=d_set[q].end(); }
return false;
}
-void InstStrategyEnum::registerQuantifier(Node q) {}
} /* CVC4::theory::quantifiers namespace */
} /* CVC4::theory namespace */
} /* CVC4 namespace */
* quantified formulas via calls to process(...)
*/
void check(Theory::Effort e, QEffort quant_e) override;
- /** Register quantifier. */
- void registerQuantifier(Node q) override;
/** Identify. */
std::string identify() const override
{
}
/** add quantifier */
-void LtePartialInst::preRegisterQuantifier( Node q ) {
+void LtePartialInst::checkOwnership(Node q)
+{
if( !q.getAttribute(LtePartialInstAttribute()) ){
if( d_do_inst.find( q )!=d_do_inst.end() ){
if( d_do_inst[q] ){
public:
LtePartialInst( QuantifiersEngine * qe, context::Context* c );
/** determine whether this quantified formula will be reduced */
- void preRegisterQuantifier(Node q) override;
+ void checkOwnership(Node q) override;
/** was invoked */
bool wasInvoked() { return d_wasInvoked; }
bool needsCheck(Theory::Effort e) override;
/* Call during quantifier engine's check */
void check(Theory::Effort e, QEffort quant_e) override;
- /* Called for new quantifiers */
- void registerQuantifier(Node q) override {}
/* check complete */
bool checkComplete() override { return !d_wasInvoked; }
- void assertNode(Node n) override {}
/** Identify this module (for debugging, dynamic configuration, etc..) */
std::string identify() const override { return "LtePartialInst"; }
};
}
-/** pre register quantifier */
-void QuantDSplit::preRegisterQuantifier( Node q ) {
+void QuantDSplit::checkOwnership(Node q)
+{
int max_index = -1;
int max_score = -1;
if( q.getNumChildren()==3 ){
public:
QuantDSplit( QuantifiersEngine * qe, context::Context* c );
/** determine whether this quantified formula will be reduced */
- void preRegisterQuantifier(Node q) override;
+ void checkOwnership(Node q) override;
/* whether this module needs to check this round */
bool needsCheck(Theory::Effort e) override;
* we are incomplete for other reasons.
*/
virtual bool checkCompleteFor( Node q ) { return false; }
- /** Pre register quantifier.
+ /** Check ownership
*
- * Called once for new quantified formulas that are
- * pre-registered by the quantifiers theory.
+ * Called once for new quantified formulas that are registered by the
+ * quantifiers theory. The primary purpose of this function is to establish
+ * if this module is the owner of quantified formula q.
*/
- virtual void preRegisterQuantifier( Node q ) { }
+ virtual void checkOwnership(Node q) {}
/** Register quantifier
+ *
+ * Called once for new quantified formulas q that are pre-registered by the
+ * quantifiers theory, after internal ownership of quantified formulas is
+ * finalized. This does context-dependent initialization of this module.
+ */
+ virtual void registerQuantifier(Node q) {}
+ /** Pre-register quantifier
*
* Called once for new quantified formulas that are
* pre-registered by the quantifiers theory, after
* internal ownership of quantified formulas is finalized.
*/
- virtual void registerQuantifier( Node q ) = 0;
+ virtual void preRegisterQuantifier(Node q) {}
/** Assert node.
*
* Called when a quantified formula q is asserted to the quantifiers theory
}
void TheoryQuantifiers::preRegisterTerm(TNode n) {
+ if (n.getKind() != FORALL)
+ {
+ return;
+ }
Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl;
- if( n.getKind()==FORALL ){
- if( !options::cbqi() || options::recurseCbqi() || !TermUtil::hasInstConstAttr(n) ){
- getQuantifiersEngine()->registerQuantifier( n );
- Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() done " << n << endl;
- }
+ if (options::cbqi() && !options::recurseCbqi()
+ && TermUtil::hasInstConstAttr(n))
+ {
+ Debug("quantifiers-prereg")
+ << "TheoryQuantifiers::preRegisterTerm() done, unused " << n << endl;
+ return;
}
+ // Preregister the quantified formula.
+ // This initializes the modules used for handling n in this user context.
+ getQuantifiersEngine()->preRegisterQuantifier(n);
+ Debug("quantifiers-prereg")
+ << "TheoryQuantifiers::preRegisterTerm() done " << n << endl;
}
void assertUniversal( Node n );
void assertExistential( Node n );
void computeCareGraph() override;
-
- using BoolMap = context::CDHashMap<Node, bool, NodeHashFunction>;
-
/** number of instantiations */
int d_numInstantiations;
int d_baseDecLevel;
d_term_enum(new quantifiers::TermEnumeration),
d_conflict_c(c, false),
// d_quants(u),
+ d_quants_prereg(u),
d_quants_red(u),
d_lemmas_produced_c(u),
d_ierCounter_c(c),
}
}
-bool QuantifiersEngine::registerQuantifier( Node f ){
+void QuantifiersEngine::registerQuantifierInternal(Node f)
+{
std::map< Node, bool >::iterator it = d_quants.find( f );
if( it==d_quants.end() ){
Trace("quant") << "QuantifiersEngine : Register quantifier ";
Trace("quant") << " : " << f << std::endl;
+ unsigned prev_lemma_waiting = d_lemmas_waiting.size();
++(d_statistics.d_num_quant);
Assert( f.getKind()==FORALL );
+ // register with utilities
+ for (unsigned i = 0; i < d_util.size(); i++)
+ {
+ d_util[i]->registerQuantifier(f);
+ }
+ // compute attributes
+ d_quant_attr->computeAttributes(f);
- //check whether we should apply a reduction
- if( reduceQuantifier( f ) ){
- Trace("quant") << "...reduced." << std::endl;
- d_quants[f] = false;
- return false;
- }else{
- // register with utilities
- for (unsigned i = 0; i < d_util.size(); i++)
- {
- d_util[i]->registerQuantifier(f);
- }
- // compute attributes
- d_quant_attr->computeAttributes(f);
-
- for( unsigned i=0; i<d_modules.size(); i++ ){
- Trace("quant-debug") << "pre-register with " << d_modules[i]->identify() << "..." << std::endl;
- d_modules[i]->preRegisterQuantifier( f );
- }
- QuantifiersModule * qm = getOwner( f );
- if( qm!=NULL ){
- Trace("quant") << " Owner : " << qm->identify() << std::endl;
- }
- //register with each module
- for( unsigned i=0; i<d_modules.size(); i++ ){
- Trace("quant-debug") << "register with " << d_modules[i]->identify() << "..." << std::endl;
- d_modules[i]->registerQuantifier( f );
- }
- //TODO: remove this
- Node ceBody = d_term_util->getInstConstantBody( f );
- Trace("quant-debug") << "...finish." << std::endl;
- d_quants[f] = true;
- // flush lemmas
- flushLemmas();
- return true;
+ for (QuantifiersModule*& mdl : d_modules)
+ {
+ Trace("quant-debug") << "check ownership with " << mdl->identify()
+ << "..." << std::endl;
+ mdl->checkOwnership(f);
}
- }else{
- return (*it).second;
+ QuantifiersModule* qm = getOwner(f);
+ Trace("quant") << " Owner : " << (qm == nullptr ? "[none]" : qm->identify())
+ << std::endl;
+ // register with each module
+ for (QuantifiersModule*& mdl : d_modules)
+ {
+ Trace("quant-debug") << "register with " << mdl->identify() << "..."
+ << std::endl;
+ mdl->registerQuantifier(f);
+ // since this is context-independent, we should not add any lemmas during
+ // this call
+ Assert(d_lemmas_waiting.size() == prev_lemma_waiting);
+ }
+ // TODO (#2020): remove this
+ Node ceBody = d_term_util->getInstConstantBody(f);
+ Trace("quant-debug") << "...finish." << std::endl;
+ d_quants[f] = true;
+ AlwaysAssert(d_lemmas_waiting.size() == prev_lemma_waiting);
}
}
+void QuantifiersEngine::preRegisterQuantifier(Node q)
+{
+ NodeSet::const_iterator it = d_quants_prereg.find(q);
+ if (it != d_quants_prereg.end())
+ {
+ return;
+ }
+ Trace("quant-debug") << "QuantifiersEngine : Pre-register " << q << std::endl;
+ d_quants_prereg.insert(q);
+ // ensure that it is registered
+ registerQuantifierInternal(q);
+ // register with each module
+ for (QuantifiersModule*& mdl : d_modules)
+ {
+ Trace("quant-debug") << "pre-register with " << mdl->identify() << "..."
+ << std::endl;
+ mdl->preRegisterQuantifier(q);
+ }
+ // flush the lemmas
+ flushLemmas();
+ Trace("quant-debug") << "...finish pre-register " << q << "..." << std::endl;
+}
+
void QuantifiersEngine::registerPattern( std::vector<Node> & pattern) {
for(std::vector<Node>::iterator p = pattern.begin(); p != pattern.end(); ++p){
std::set< Node > added;
}
void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
+ if (reduceQuantifier(f))
+ {
+ // if we can reduce it, nothing left to do
+ return;
+ }
if( !pol ){
- //if not reduced
- if( !reduceQuantifier( f ) ){
- //do skolemization
- Node lem = d_skolemize->process(f);
- if (!lem.isNull())
+ // do skolemization
+ Node lem = d_skolemize->process(f);
+ if (!lem.isNull())
+ {
+ if (Trace.isOn("quantifiers-sk-debug"))
{
- if( Trace.isOn("quantifiers-sk-debug") ){
- Node slem = Rewriter::rewrite( lem );
- Trace("quantifiers-sk-debug") << "Skolemize lemma : " << slem << std::endl;
- }
- getOutputChannel().lemma( lem, false, true );
+ Node slem = Rewriter::rewrite(lem);
+ Trace("quantifiers-sk-debug")
+ << "Skolemize lemma : " << slem << std::endl;
}
+ getOutputChannel().lemma(lem, false, true);
}
- }else{
- //assert to modules TODO : also for !pol?
- //register the quantifier, assert it to each module
- if( registerQuantifier( f ) ){
- d_model->assertQuantifier( f );
- for( unsigned i=0; i<d_modules.size(); i++ ){
- d_modules[i]->assertNode( f );
- }
- addTermToDatabase( d_term_util->getInstConstantBody( f ), true );
- }
+ return;
+ }
+ // ensure the quantified formula is registered
+ registerQuantifierInternal(f);
+ // assert it to each module
+ d_model->assertQuantifier(f);
+ for (QuantifiersModule*& mdl : d_modules)
+ {
+ mdl->assertNode(f);
}
+ addTermToDatabase(d_term_util->getInstConstantBody(f), true);
}
void QuantifiersEngine::propagate( Theory::Effort level ){
private:
/** list of all quantifiers seen */
std::map< Node, bool > d_quants;
+ /** quantifiers pre-registered */
+ NodeSet d_quants_prereg;
/** quantifiers reduced */
BoolMap d_quants_red;
std::map< Node, Node > d_quants_red_lem;
void check( Theory::Effort e );
/** notify that theories were combined */
void notifyCombineTheories();
- /** register quantifier */
- bool registerQuantifier( Node f );
+ /** preRegister quantifier
+ *
+ * This function is called after registerQuantifier for quantified formulas
+ * that are pre-registered to the quantifiers theory.
+ */
+ void preRegisterQuantifier(Node q);
/** register quantifier */
void registerPattern( std::vector<Node> & pattern);
/** assert universal quantifier */
/** get next decision request */
Node getNextDecisionRequest( unsigned& priority );
private:
- /** reduceQuantifier, return true if reduced */
- bool reduceQuantifier( Node q );
- /** flush lemmas */
- void flushLemmas();
+ /** (context-indepentent) register quantifier internal
+ *
+ * This is called when a quantified formula q is pre-registered to the
+ * quantifiers theory, and updates the modules in this class with
+ * context-independent information about how to handle q. This includes basic
+ * information such as which module owns q.
+ */
+ void registerQuantifierInternal(Node q);
+ /** reduceQuantifier, return true if reduced */
+ bool reduceQuantifier(Node q);
+ /** flush lemmas */
+ void flushLemmas();
+
public:
/** add lemma lem */
bool addLemma( Node lem, bool doCache = true, bool doRewrite = true );
projects / cvc5.git / commitdiff