Always enable cbqi literal dependency (#4116)

Fixes #4105.

It appears that the two (experimental) options in that issue were incompatible.

A block of code changed indentation in this PR and was updated to guidelines.

2 files changed, 26 insertions, 31 deletions

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 12549152d..5f07e687e 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1764,15 +1764,6 @@ header = "options/quantifiers_options.h"
   read_only  = true
   help       = "non-optimal bounds for counterexample-based quantifier instantiation"
 
-[[option]]
-  name       = "cbqiLitDepend"
-  category   = "regular"
-  long       = "cbqi-lit-dep"
-  type       = "bool"
-  default    = "true"
-  read_only  = true
-  help       = "dependency lemmas for quantifier alternation in counterexample-based quantifier instantiation"
-
 # CEGQI for EPR
 
 [[option]]
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 4f670bef4..dafcc365e 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -94,6 +94,7 @@ QuantifiersModule::QEffort InstStrategyCegqi::needsModel(Theory::Effort e)
 bool InstStrategyCegqi::registerCbqiLemma(Node q)
 {
   if( !hasAddedCbqiLemma( q ) ){
+    NodeManager* nm = NodeManager::currentNM();
     d_added_cbqi_lemma.insert( q );
     Trace("cbqi-debug") << "Do cbqi for " << q << std::endl;
     //add cbqi lemma
@@ -141,30 +142,33 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q)
       }      
       
       //compute dependencies between quantified formulas
-      if( options::cbqiLitDepend() || options::cbqiInnermost() ){
-        std::vector< Node > ics;
-        TermUtil::computeInstConstContains(q, ics);
-        d_parent_quant[q].clear();
-        d_children_quant[q].clear();
-        std::vector< Node > dep;
-        for( unsigned i=0; i<ics.size(); i++ ){
-          Node qi = ics[i].getAttribute(InstConstantAttribute());
-          if( std::find( d_parent_quant[q].begin(), d_parent_quant[q].end(), qi )==d_parent_quant[q].end() ){
-            d_parent_quant[q].push_back( qi );
-            d_children_quant[qi].push_back( q );
-            Assert(hasAddedCbqiLemma(qi));
-            Node qicel = getCounterexampleLiteral(qi);
-            dep.push_back( qi );
-            dep.push_back( qicel );
-          }
-        }
-        if( !dep.empty() ){
-          Node dep_lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, ceLit, NodeManager::currentNM()->mkNode( kind::AND, dep ) );
-          Trace("cbqi-lemma") << "Counterexample dependency lemma : " << dep_lemma << std::endl;
-          d_quantEngine->getOutputChannel().lemma( dep_lemma );
+      std::vector<Node> ics;
+      TermUtil::computeInstConstContains(q, ics);
+      d_parent_quant[q].clear();
+      d_children_quant[q].clear();
+      std::vector<Node> dep;
+      for (const Node& ic : ics)
+      {
+        Node qi = ic.getAttribute(InstConstantAttribute());
+        if (std::find(d_parent_quant[q].begin(), d_parent_quant[q].end(), qi)
+            == d_parent_quant[q].end())
+        {
+          d_parent_quant[q].push_back(qi);
+          d_children_quant[qi].push_back(q);
+          Assert(hasAddedCbqiLemma(qi));
+          Node qicel = getCounterexampleLiteral(qi);
+          dep.push_back(qi);
+          dep.push_back(qicel);
         }
       }
-      
+      if (!dep.empty())
+      {
+        Node dep_lemma = nm->mkNode(IMPLIES, ceLit, nm->mkNode(AND, dep));
+        Trace("cbqi-lemma")
+            << "Counterexample dependency lemma : " << dep_lemma << std::endl;
+        d_quantEngine->getOutputChannel().lemma(dep_lemma);
+      }
+
       //must register all sub-quantifiers of counterexample lemma, register their lemmas
       std::vector< Node > quants;
       TermUtil::computeQuantContains( lem, quants );