diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/options/quantifiers_options.toml | 9 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 27 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.h | 7 |
3 files changed, 2 insertions, 41 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 1ff85c96d..1c13590eb 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1465,15 +1465,6 @@ header = "options/quantifiers_options.h" help = "turns on full effort counterexample-based quantifier instantiation, which may resort to model-value instantiation" [[option]] - name = "recurseCbqi" - category = "regular" - long = "cbqi-recurse" - type = "bool" - default = "true" - read_only = true - help = "turns on recursive counterexample-based quantifier instantiation" - -[[option]] name = "cbqiSat" category = "regular" long = "cbqi-sat" diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index ac6e194eb..f24a4bb2b 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -38,8 +38,6 @@ using namespace CVC4::theory::quantifiers; TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo) { - d_numInstantiations = 0; - d_baseDecLevel = -1; out.handleUserAttribute( "axiom", this ); out.handleUserAttribute( "conjecture", this ); out.handleUserAttribute( "fun-def", this ); @@ -71,13 +69,6 @@ void TheoryQuantifiers::preRegisterTerm(TNode n) { return; } Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << 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); @@ -135,7 +126,7 @@ void TheoryQuantifiers::check(Effort e) { Trace("quantifiers-assert") << "quantifiers::assert(): " << assertion << std::endl; switch(assertion.getKind()) { case kind::FORALL: - assertUniversal( assertion ); + getQuantifiersEngine()->assertQuantifier(assertion, true); break; case kind::INST_CLOSURE: getQuantifiersEngine()->addTermToDatabase( assertion[0], false, true ); @@ -150,7 +141,7 @@ void TheoryQuantifiers::check(Effort e) { { switch( assertion[0].getKind()) { case kind::FORALL: - assertExistential( assertion ); + getQuantifiersEngine()->assertQuantifier(assertion[0], false); break; case kind::EQUAL: //do nothing @@ -171,20 +162,6 @@ void TheoryQuantifiers::check(Effort e) { getQuantifiersEngine()->check( e ); } -void TheoryQuantifiers::assertUniversal( Node n ){ - Assert( n.getKind()==FORALL ); - if( !options::cbqi() || options::recurseCbqi() || !TermUtil::hasInstConstAttr(n) ){ - getQuantifiersEngine()->assertQuantifier( n, true ); - } -} - -void TheoryQuantifiers::assertExistential( Node n ){ - Assert( n.getKind()== NOT && n[0].getKind()==FORALL ); - if( !options::cbqi() || options::recurseCbqi() || !TermUtil::hasInstConstAttr(n[0]) ){ - getQuantifiersEngine()->assertQuantifier( n[0], false ); - } -} - void TheoryQuantifiers::setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value){ QuantAttributes::setUserAttribute( attr, n, node_values, str_value ); } diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 09cda76fb..f6e19f700 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -56,13 +56,6 @@ class TheoryQuantifiers : public Theory { std::vector<Node> node_values, std::string str_value) override; - private: - void assertUniversal( Node n ); - void assertExistential( Node n ); - /** number of instantiations */ - int d_numInstantiations; - int d_baseDecLevel; - };/* class TheoryQuantifiers */ }/* CVC4::theory::quantifiers namespace */ |