Remove support for inst closure (#5874)

This was a feature implemented for "Deciding Local Theory Extensions via E-matching" CAV 2015 that is not used anymore, and will be a burden to maintain further with potential changes to term database.

It also simplifies the TermDatabase::addTerm method (which changed indentation).

14 files changed, 54 insertions, 180 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 541c5f5a5..10f39cb38 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -333,7 +333,6 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{
     {FORALL, CVC4::Kind::FORALL},
     {EXISTS, CVC4::Kind::EXISTS},
     {BOUND_VAR_LIST, CVC4::Kind::BOUND_VAR_LIST},
-    {INST_CLOSURE, CVC4::Kind::INST_CLOSURE},
     {INST_PATTERN, CVC4::Kind::INST_PATTERN},
     {INST_NO_PATTERN, CVC4::Kind::INST_NO_PATTERN},
     {INST_ATTRIBUTE, CVC4::Kind::INST_ATTRIBUTE},
@@ -629,7 +628,6 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
         {CVC4::Kind::FORALL, FORALL},
         {CVC4::Kind::EXISTS, EXISTS},
         {CVC4::Kind::BOUND_VAR_LIST, BOUND_VAR_LIST},
-        {CVC4::Kind::INST_CLOSURE, INST_CLOSURE},
         {CVC4::Kind::INST_PATTERN, INST_PATTERN},
         {CVC4::Kind::INST_NO_PATTERN, INST_NO_PATTERN},
         {CVC4::Kind::INST_ATTRIBUTE, INST_ATTRIBUTE},
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index 0bd4117dc..3fb16abcb 100644
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -2743,14 +2743,6 @@ enum CVC4_PUBLIC Kind : int32_t
    */
   BOUND_VAR_LIST,
   /*
-   * A predicate for specifying term in instantiation closure.
-   * Parameters: 1
-   *   -[1]: Term
-   * Create with:
-   *   mkTerm(Kind kind, Term child)
-   */
-  INST_CLOSURE,
-  /*
    * An instantiation pattern.
    * Specifies a (list of) terms to be used as a pattern for quantifier
    * instantiation.
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 4b98cb84d..fd781ab2b 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1762,17 +1762,6 @@ header = "options/quantifiers_options.h"
   default    = "true"
   help       = "compute inverse for concat over equalities rather than producing an invertibility condition"
 
-### Local theory extensions options
-
-[[option]]
-  name       = "lteRestrictInstClosure"
-  category   = "regular"
-  long       = "lte-restrict-inst-closure"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "treat arguments of inst closure as restricted terms for instantiation"
-
 ### Reduction options
 
 [[option]]
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 9c5474a47..4d75a982b 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -82,10 +82,6 @@ void Smt2::addTranscendentalOperators()
 
 void Smt2::addQuantifiersOperators()
 {
-  if (!strictModeEnabled())
-  {
-    addOperator(api::INST_CLOSURE, "inst-closure");
-  }
 }
 
 void Smt2::addBitvectorOperators() {
diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index 97693fae0..eb02eb19e 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -189,7 +189,8 @@ Node CandidateGeneratorQEAll::getNextCandidate() {
     if( n.getType().isComparableTo( d_match_pattern_type ) ){
       TNode nh = tdb->getEligibleTermInEqc(n);
       if( !nh.isNull() ){
-        if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){
+        if (options::instMaxLevel() != -1)
+        {
           nh = d_qe->getInternalRepresentative( nh, d_f, d_index );
           //don't consider this if already the instantiation is ineligible
           if (!nh.isNull() && !tdb->isTermEligibleForInstantiation(nh, d_f))
diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp
index c60c98d70..def27fe5a 100644
--- a/src/theory/quantifiers/equality_query.cpp
+++ b/src/theory/quantifiers/equality_query.cpp
@@ -172,11 +172,6 @@ int EqualityQueryQuantifiersEngine::getRepScore(Node n,
     return -2;
   }else if( !n.getType().isSubtypeOf( v_tn ) ){  //reject if incorrect type
     return -2;
-  }
-  else if (options::lteRestrictInstClosure()
-           && (!d_tdb->isInstClosure(n) || !d_tdb->hasTermCurrent(n, false)))
-  {
-    return -1;
   }else if( options::instMaxLevel()!=-1 ){
     //score prefer lowest instantiation level
     if( n.hasAttribute(InstLevelAttribute()) ){
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 3bbe15b8c..49f1fe116 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -217,7 +217,7 @@ bool Instantiate::addInstantiation(
   }
 
   // check based on instantiation level
-  if (options::instMaxLevel() != -1 || options::lteRestrictInstClosure())
+  if (options::instMaxLevel() != -1)
   {
     for (Node& t : terms)
     {
diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds
index 1534d2d4d..3f15ef916 100644
--- a/src/theory/quantifiers/kinds
+++ b/src/theory/quantifiers/kinds
@@ -44,15 +44,12 @@ sort INST_PATTERN_LIST_TYPE \
 # a list of instantiation patterns
 operator INST_PATTERN_LIST 1: "a list of instantiation patterns"
 
-operator INST_CLOSURE 1 "predicate for specifying term in instantiation closure."
-
 typerule FORALL ::CVC4::theory::quantifiers::QuantifierForallTypeRule 
 typerule EXISTS ::CVC4::theory::quantifiers::QuantifierExistsTypeRule 
 typerule BOUND_VAR_LIST ::CVC4::theory::quantifiers::QuantifierBoundVarListTypeRule 
 typerule INST_PATTERN ::CVC4::theory::quantifiers::QuantifierInstPatternTypeRule 
 typerule INST_NO_PATTERN ::CVC4::theory::quantifiers::QuantifierInstNoPatternTypeRule 
 typerule INST_ATTRIBUTE ::CVC4::theory::quantifiers::QuantifierInstAttributeTypeRule 
-typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule 
-typerule INST_CLOSURE ::CVC4::theory::quantifiers::QuantifierInstClosureTypeRule 
+typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule
 
 endtheory
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 5a6e38b78..1498c29b7 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -198,60 +198,45 @@ Node TermDb::getMatchOperator( Node n ) {
   }
 }
 
-void TermDb::addTerm(Node n,
-                     std::set<Node>& added,
-                     bool withinQuant,
-                     bool withinInstClosure)
+void TermDb::addTerm(Node n)
 {
-  //don't add terms in quantifier bodies
-  if( withinQuant && !options::registerQuantBodyTerms() ){
+  if (d_processed.find(n) != d_processed.end())
+  {
     return;
   }
-  bool rec = false;
-  if (d_processed.find(n) == d_processed.end())
+  d_processed.insert(n);
+  if (!TermUtil::hasInstConstAttr(n))
   {
-    d_processed.insert(n);
-    if (!TermUtil::hasInstConstAttr(n))
+    Trace("term-db-debug") << "register term : " << n << std::endl;
+    d_type_map[n.getType()].push_back(n);
+    // if this is an atomic trigger, consider adding it
+    if (inst::TriggerTermInfo::isAtomicTrigger(n))
     {
-      Trace("term-db-debug") << "register term : " << n << std::endl;
-      d_type_map[n.getType()].push_back(n);
-      // if this is an atomic trigger, consider adding it
-      if (inst::TriggerTermInfo::isAtomicTrigger(n))
-      {
-        Trace("term-db") << "register term in db " << n << std::endl;
+      Trace("term-db") << "register term in db " << n << std::endl;
 
-        Node op = getMatchOperator(n);
-        Trace("term-db-debug") << "  match operator is : " << op << std::endl;
-        if (d_op_map.find(op) == d_op_map.end())
-        {
-          d_ops.push_back(op);
-        }
-        d_op_map[op].push_back(n);
-        added.insert(n);
-        // If we are higher-order, we may need to register more terms.
-        if (options::ufHo())
-        {
-          addTermHo(n, added, withinQuant, withinInstClosure);
-        }
+      Node op = getMatchOperator(n);
+      Trace("term-db-debug") << "  match operator is : " << op << std::endl;
+      if (d_op_map.find(op) == d_op_map.end())
+      {
+        d_ops.push_back(op);
+      }
+      d_op_map[op].push_back(n);
+      // If we are higher-order, we may need to register more terms.
+      if (options::ufHo())
+      {
+        addTermHo(n);
       }
     }
-    else
-    {
-      setTermInactive(n);
-    }
-    rec = true;
   }
-  if (withinInstClosure
-      && d_iclosure_processed.find(n) == d_iclosure_processed.end())
+  else
   {
-    d_iclosure_processed.insert(n);
-    rec = true;
+    setTermInactive(n);
   }
-  if (rec && !n.isClosure())
+  if (!n.isClosure())
   {
     for (const Node& nc : n)
     {
-      addTerm(nc, added, withinQuant, withinInstClosure);
+      addTerm(nc);
     }
   }
 }
@@ -442,10 +427,7 @@ void TermDb::computeUfTerms( TNode f ) {
   }
 }
 
-void TermDb::addTermHo(Node n,
-                       std::set<Node>& added,
-                       bool withinQuant,
-                       bool withinInstClosure)
+void TermDb::addTermHo(Node n)
 {
   Assert(options::ufHo());
   if (n.getType().isFunction())
@@ -494,7 +476,7 @@ void TermDb::addTermHo(Node n,
     // also add standard application version
     args.insert(args.begin(), curr);
     Node uf_n = nm->mkNode(APPLY_UF, args);
-    addTerm(uf_n, added, withinQuant, withinInstClosure);
+    addTerm(uf_n);
   }
 }
 
@@ -918,18 +900,6 @@ bool TermDb::hasTermCurrent( Node n, bool useMode ) {
 
 bool TermDb::isTermEligibleForInstantiation(TNode n, TNode f)
 {
-  if( options::lteRestrictInstClosure() ){
-    //has to be both in inst closure and in ground assertions
-    if( !isInstClosure( n ) ){
-      Trace("inst-add-debug") << "Term " << n << " is not an inst-closure term." << std::endl;
-      return false;
-    }
-    // hack : since theories preregister terms not in assertions, we are using hasTermCurrent to approximate this
-    if( !hasTermCurrent( n, false ) ){
-      Trace("inst-add-debug") << "Term " << n << " is not in a ground assertion." << std::endl;
-      return false;
-    }
-  }
   if( options::instMaxLevel()!=-1 ){
     if( n.hasAttribute(InstLevelAttribute()) ){
       int fml = f.isNull() ? -1 : d_quantEngine->getQuantAttributes()->getQuantInstLevel( f );
@@ -979,10 +949,6 @@ Node TermDb::getEligibleTermInEqc( TNode r ) {
   }
 }
 
-bool TermDb::isInstClosure( Node r ) {
-  return d_iclosure_processed.find( r )!=d_iclosure_processed.end();
-}
-
 void TermDb::setHasTerm( Node n ) {
   Trace("term-db-debug2") << "hasTerm : " << n  << std::endl;
   if( d_has_map.find( n )==d_has_map.end() ){
@@ -1001,7 +967,6 @@ void TermDb::presolve() {
     d_op_map.clear();
     d_type_map.clear();
     d_processed.clear();
-    d_iclosure_processed.clear();
   }
 }
 
@@ -1060,8 +1025,7 @@ bool TermDb::reset( Theory::Effort effort ){
   }
 
   //compute has map
-  if (options::termDbMode() == options::TermDbMode::RELEVANT
-      || options::lteRestrictInstClosure())
+  if (options::termDbMode() == options::TermDbMode::RELEVANT)
   {
     d_has_map.clear();
     d_term_elig_eqc.clear();
@@ -1103,21 +1067,10 @@ bool TermDb::reset( Theory::Effort effort ){
            it != it_end;
            ++it)
       {
-        if ((*it).d_assertion.getKind() != INST_CLOSURE)
-        {
-          setHasTerm((*it).d_assertion);
-        }
+        setHasTerm((*it).d_assertion);
       }
     }
   }
-  //explicitly add inst closure terms to the equality engine to ensure only EE terms are indexed
-  for (const Node& n : d_iclosure_processed)
-  {
-    if (!ee->hasTerm(n))
-    {
-      ee->addTerm(n);
-    }
-  }
 
   if( options::ufHo() && options::hoMergeTermDb() ){
     Trace("quant-ho") << "TermDb::reset : compute equal functions..." << std::endl;
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 244762d24..6a695e70e 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -108,15 +108,11 @@ class TermDb : public QuantifiersUtil {
   * variable per type.
   */
   Node getOrMakeTypeFreshVariable(TypeNode tn);
-  /** add a term to the database
-  * withinQuant is whether n is within the body of a quantified formula
-  * withinInstClosure is whether n is within an inst-closure operator (see
-  * Bansal et al CAV 2015).
-  */
-  void addTerm(Node n,
-               std::set<Node>& added,
-               bool withinQuant = false,
-               bool withinInstClosure = false);
+  /**
+   * Add a term to the database, which registers it as a term that may be
+   * matched with via E-matching, and can be used in entailment tests below.
+   */
+  void addTerm(Node n);
   /** get match operator for term n
   *
   * If n has a kind that we index, this function will
@@ -268,12 +264,6 @@ class TermDb : public QuantifiersUtil {
   bool isTermEligibleForInstantiation(TNode n, TNode f);
   /** get eligible term in equivalence class of r */
   Node getEligibleTermInEqc(TNode r);
-  /** is r a inst closure node?
-   * This terminology was used for specifying
-   * a particular status of nodes for
-   * Bansal et al., CAV 2015.
-   */
-  bool isInstClosure(Node r);
   /** get higher-order type match predicate
    *
    * This predicate is used to force certain functions f of type tn to appear as
@@ -292,8 +282,6 @@ class TermDb : public QuantifiersUtil {
   QuantifiersInferenceManager& d_qim;
   /** terms processed */
   std::unordered_set< Node, NodeHashFunction > d_processed;
-  /** terms processed */
-  std::unordered_set< Node, NodeHashFunction > d_iclosure_processed;
   /** select op map */
   std::map< Node, std::map< TypeNode, Node > > d_par_op_map;
   /** whether master equality engine is UF-inconsistent */
@@ -407,10 +395,7 @@ class TermDb : public QuantifiersUtil {
    * Above, we set d_ho_fun_op_purify[(@ f 0)] = pfun, and
    * d_ho_purify_to_term[(pfun 1)] = (@ (@ f 0) 1).
    */
-  void addTermHo(Node n,
-                 std::set<Node>& added,
-                 bool withinQuant,
-                 bool withinInstClosure);
+  void addTermHo(Node n);
   /** get operator representative */
   Node getOperatorRepresentative( TNode op ) const;
   //------------------------------end higher-order term indexing
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 1cbb2ce40..7c2bbb019 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -162,18 +162,6 @@ bool TheoryQuantifiers::preNotifyFact(
   {
     getQuantifiersEngine()->assertQuantifier(atom, polarity);
   }
-  else if (k == INST_CLOSURE)
-  {
-    if (!polarity)
-    {
-      Unhandled() << "Unexpected inst-closure fact " << fact;
-    }
-    getQuantifiersEngine()->addTermToDatabase(atom[0], false, true);
-    if (!options::lteRestrictInstClosure())
-    {
-      d_qstate.getEqualityEngine()->addTerm(atom[0]);
-    }
-  }
   else
   {
     Unhandled() << "Unexpected fact " << fact;
diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h
index c7cbb278f..01bea3707 100644
--- a/src/theory/quantifiers/theory_quantifiers_type_rules.h
+++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h
@@ -127,20 +127,6 @@ struct QuantifierInstPatternListTypeRule {
   }
 };/* struct QuantifierInstPatternListTypeRule */
 
-struct QuantifierInstClosureTypeRule {
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    Assert(n.getKind() == kind::INST_CLOSURE);
-    if( check ){
-      TypeNode tn = n[0].getType(check);
-      if( tn.isBoolean() ){
-        throw TypeCheckingExceptionPrivate(n, "argument of inst-closure must be non-boolean");
-      }
-    }
-    return nodeManager->booleanType();
-  }
-};/* struct QuantifierInstClosureTypeRule */
-
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index a1d3f0ac7..0e28cab76 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -58,9 +58,7 @@ QuantifiersEngine::QuantifiersEngine(
       d_ierCounter_c(qstate.getSatContext()),
       d_presolve(qstate.getUserContext(), true),
       d_presolve_in(qstate.getUserContext()),
-      d_presolve_cache(qstate.getUserContext()),
-      d_presolve_cache_wq(qstate.getUserContext()),
-      d_presolve_cache_wic(qstate.getUserContext())
+      d_presolve_cache(qstate.getUserContext())
 {
   //---- utilities
   // term util must come before the other utilities
@@ -273,8 +271,9 @@ void QuantifiersEngine::presolve() {
   //add all terms to database
   if( options::incrementalSolving() ){
     Trace("quant-engine-proc") << "Add presolve cache " << d_presolve_cache.size() << std::endl;
-    for( unsigned i=0; i<d_presolve_cache.size(); i++ ){
-      addTermToDatabase( d_presolve_cache[i], d_presolve_cache_wq[i], d_presolve_cache_wic[i] );
+    for (const Node& t : d_presolve_cache)
+    {
+      addTermToDatabase(t);
     }
     Trace("quant-engine-proc") << "Done add presolve cache " << std::endl;
   }
@@ -754,26 +753,25 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
   addTermToDatabase(d_term_util->getInstConstantBody(f), true);
 }
 
-void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool withinInstClosure ){
+void QuantifiersEngine::addTermToDatabase(Node n, bool withinQuant)
+{
+  // don't add terms in quantifier bodies
+  if (withinQuant && !options::registerQuantBodyTerms())
+  {
+    return;
+  }
   if( options::incrementalSolving() ){
     if( d_presolve_in.find( n )==d_presolve_in.end() ){
       d_presolve_in.insert( n );
       d_presolve_cache.push_back( n );
-      d_presolve_cache_wq.push_back( withinQuant );
-      d_presolve_cache_wic.push_back( withinInstClosure );
     }
   }
   //only wait if we are doing incremental solving
   if( !d_presolve || !options::incrementalSolving() ){
-    std::set< Node > added;
-    d_term_db->addTerm(n, added, withinQuant, withinInstClosure);
-
-    if (!withinQuant)
+    d_term_db->addTerm(n);
+    if (d_sygus_tdb && options::sygusEvalUnfold())
     {
-      if (d_sygus_tdb && options::sygusEvalUnfold())
-      {
-        d_sygus_tdb->getEvalUnfold()->registerEvalTerm(n);
-      }
+      d_sygus_tdb->getEvalUnfold()->registerEvalTerm(n);
     }
   }
 }
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index d8f94f864..83e01e9e6 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -210,9 +210,7 @@ public:
 
 public:
  /** add term to database */
- void addTermToDatabase(Node n,
-                        bool withinQuant = false,
-                        bool withinInstClosure = false);
+ void addTermToDatabase(Node n, bool withinQuant = false);
  /** notification when master equality engine is updated */
  void eqNotifyNewClass(TNode t);
  /** debug print equality engine */
@@ -379,8 +377,6 @@ public:
   /** presolve cache */
   NodeSet d_presolve_in;
   NodeList d_presolve_cache;
-  BoolList d_presolve_cache_wq;
-  BoolList d_presolve_cache_wic;
 };/* class QuantifiersEngine */
 
 }/* CVC4::theory namespace */