diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-30 15:34:05 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-05-30 13:34:05 -0700 |
commit | eb733c1a2c806b34abcdf0d8497fa579f2b1e66e (patch) | |
tree | a67b50d23afa90f8f8b47f7bbb8ad70b310a4fc1 /src/theory/quantifiers | |
parent | 551a914cf9c09353712089bb0d7ad33b56adcc3f (diff) |
Fixes for quantifiers + incremental (#2009)
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp | 58 | ||||
-rw-r--r-- | src/theory/quantifiers/cegqi/inst_strategy_cbqi.h | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/conjecture_generator.cpp | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/conjecture_generator.h | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/instantiation_engine.cpp | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/instantiation_engine.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.cpp | 11 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.h | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_enumerative.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_enumerative.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/local_theory_ext.cpp | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/local_theory_ext.h | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_split.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_split.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_util.h | 18 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 20 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.h | 3 |
17 files changed, 78 insertions, 74 deletions
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp index 4b79c4e79..678d87156 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp @@ -344,39 +344,46 @@ Node InstStrategyCbqi::getIdMarkedQuantNode( Node n, std::map< Node, Node >& vis } } -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; @@ -673,7 +680,8 @@ CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) { } } -void InstStrategyCegqi::registerQuantifier( Node q ) { +void InstStrategyCegqi::preRegisterQuantifier(Node q) +{ if( doCbqi( q ) ){ // get the instantiator if( options::cbqiPreRegInst() ){ diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h index 5a4db0e53..3445c3f9f 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h @@ -103,8 +103,8 @@ class InstStrategyCbqi : public QuantifiersModule { 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; }; @@ -147,8 +147,8 @@ class InstStrategyCegqi : public InstStrategyCbqi { //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; }; diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 404f64471..807a7a58c 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -923,14 +923,6 @@ unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, in 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: diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index 2db175fae..8a6339a85 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -428,9 +428,6 @@ public: 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 diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index 184add8c3..bd95b316d 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -157,7 +157,8 @@ bool InstantiationEngine::checkCompleteFor( Node q ) { 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; diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h index 32ddb19ed..e4cb986da 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.h +++ b/src/theory/quantifiers/ematching/instantiation_engine.h @@ -81,7 +81,7 @@ class InstantiationEngine : public QuantifiersModule { 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 */ diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index d96fb4e05..b493d6a0c 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -384,10 +384,11 @@ void BoundedIntegers::setBoundedVar( Node q, Node v, unsigned bound_type ) { 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; @@ -546,10 +547,6 @@ void BoundedIntegers::preRegisterQuantifier( Node f ) { } } -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; diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index 3e990067a..93b6436d5 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -146,8 +146,7 @@ public: 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(); } diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index 54689b32a..743e7ccc8 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -295,7 +295,6 @@ bool InstStrategyEnum::process(Node f, bool fullEffort) return false; } -void InstStrategyEnum::registerQuantifier(Node q) {} } /* CVC4::theory::quantifiers namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h index cf97518fc..51c0c1d0c 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.h +++ b/src/theory/quantifiers/inst_strategy_enumerative.h @@ -72,8 +72,6 @@ class InstStrategyEnum : public QuantifiersModule * 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 { diff --git a/src/theory/quantifiers/local_theory_ext.cpp b/src/theory/quantifiers/local_theory_ext.cpp index 375754b26..c76d97255 100644 --- a/src/theory/quantifiers/local_theory_ext.cpp +++ b/src/theory/quantifiers/local_theory_ext.cpp @@ -32,7 +32,8 @@ QuantifiersModule( qe ), d_wasInvoked( false ), d_needsCheck( false ){ } /** 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] ){ diff --git a/src/theory/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h index 76a781e1c..2390eb40c 100644 --- a/src/theory/quantifiers/local_theory_ext.h +++ b/src/theory/quantifiers/local_theory_ext.h @@ -56,7 +56,7 @@ private: 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; } @@ -64,11 +64,8 @@ public: 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"; } }; diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index 68a0f30dc..da6b0a6b4 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -31,8 +31,8 @@ QuantifiersModule( qe ), d_added_split( qe->getUserContext() ){ } -/** 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 ){ diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h index 1ea57433a..94bfa0f20 100644 --- a/src/theory/quantifiers/quant_split.h +++ b/src/theory/quantifiers/quant_split.h @@ -34,7 +34,7 @@ private: 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; diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index f3fdfa6f4..874baa482 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -108,19 +108,27 @@ class QuantifiersModule { * 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 diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 5016bd87f..79b7d9a99 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -83,13 +83,23 @@ void TheoryQuantifiers::finishInit() } 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; } diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 4f0302bf3..b82dccd73 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -65,9 +65,6 @@ class TheoryQuantifiers : public Theory { 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; |