From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 16 Apr 2019 15:38:35 +0000 (-0500)
Subject: Minor simplifications to theory quantifiers (#2953)
X-Git-Tag: cvc5-1.0.0~4179
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0da111d8649a535e83823c5d386c3582045e2fc4;p=cvc5.git

Minor simplifications to theory quantifiers (#2953)
---

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
@@ -1464,15 +1464,6 @@ header = "options/quantifiers_options.h"
   default    = "false"
   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"
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 */
diff --git a/test/regress/regress0/quantifiers/ARI176e1.smt2 b/test/regress/regress0/quantifiers/ARI176e1.smt2
index caed9c603..36dccc21f 100644
--- a/test/regress/regress0/quantifiers/ARI176e1.smt2
+++ b/test/regress/regress0/quantifiers/ARI176e1.smt2
@@ -1,5 +1,4 @@
-; COMMAND-LINE: --cbqi-recurse
-; EXPECT: unsat
 (set-logic LIA)
+(set-info :status unsat)
 (assert (forall ((U Int) (V Int)) (not (= (* 3 U) (+ 22 (* (- 5) V)))) ) )
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/nested-delta.smt2 b/test/regress/regress0/quantifiers/nested-delta.smt2
index 9352f0410..137a5eee3 100644
--- a/test/regress/regress0/quantifiers/nested-delta.smt2
+++ b/test/regress/regress0/quantifiers/nested-delta.smt2
@@ -1,6 +1,4 @@
-; COMMAND-LINE: --cbqi-recurse
-; EXPECT: sat
 (set-logic LRA)
 (set-info :status sat)
 (assert (forall ((x Real)) (or (exists ((y Real)) (and (< y 0) (< y x))) (<= x 0))))
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/nested-inf.smt2 b/test/regress/regress0/quantifiers/nested-inf.smt2
index f27a876db..ea397f8db 100644
--- a/test/regress/regress0/quantifiers/nested-inf.smt2
+++ b/test/regress/regress0/quantifiers/nested-inf.smt2
@@ -1,6 +1,4 @@
-; COMMAND-LINE: --cbqi-recurse
-; EXPECT: sat
 (set-logic LRA)
 (set-info :status sat)
 (assert (forall ((x Real)) (exists ((y Real)) (> y x))))
-(check-sat)
\ No newline at end of file
+(check-sat)