Move getCounterexampleLiteral out of term utilities (#3238)

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 0f866208de0f8bef2f3668d75b3ab768761d7a0e..ab5bbc25f9f83bb9ed02662e8d791e193e5198f3 100644 (file)
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -93,7 +93,7 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q)
     Trace("cbqi-debug") << "Do cbqi for " << q << std::endl;
     //add cbqi lemma
     //get the counterexample literal
-    Node ceLit = d_quantEngine->getTermUtil()->getCounterexampleLiteral( q );
+    Node ceLit = getCounterexampleLiteral(q);
     Node ceBody = d_quantEngine->getTermUtil()->getInstConstantBody( q );
     if( !ceBody.isNull() ){
       //add counterexample lemma
@@ -148,7 +148,7 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q)
             d_parent_quant[q].push_back( qi );
             d_children_quant[qi].push_back( q );
             Assert( hasAddedCbqiLemma( qi ) );
-            Node qicel = d_quantEngine->getTermUtil()->getCounterexampleLiteral( qi );
+            Node qicel = getCounterexampleLiteral(qi);
             dep.push_back( qi );
             dep.push_back( qicel );
           }
@@ -220,7 +220,7 @@ void InstStrategyCegqi::reset_round(Theory::Effort effort)
       if( d_quantEngine->getModel()->isQuantifierActive( q ) ){
         d_active_quant[q] = true;
         Debug("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl;
-        Node cel = d_quantEngine->getTermUtil()->getCounterexampleLiteral( q );
+        Node cel = getCounterexampleLiteral(q);
         bool value;
         if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){
           Debug("cbqi-debug") << "...CE Literal has value " << value << std::endl;
@@ -620,6 +620,21 @@ void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) {
   }
 }
 
+Node InstStrategyCegqi::getCounterexampleLiteral(Node q)
+{
+  std::map<Node, Node>::iterator it = d_ce_lit.find(q);
+  if (it != d_ce_lit.end())
+  {
+    return it->second;
+  }
+  NodeManager * nm = NodeManager::currentNM();
+  Node g = nm->mkSkolem("g", nm->booleanType());
+  // ensure that it is a SAT literal
+  Node ceLit = d_quantEngine->getValuation().ensureLiteral(g);
+  d_ce_lit[q] = ceLit;
+  return ceLit;
+}
+
 bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
   Assert( !d_curr_quant.isNull() );
   //if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
index c6a9ddd1156a59203b6518cc9dc545bc2d21e677..ecae4ab64b2348c556ce2327dcc5d439e1dbf259 100644 (file)
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
@@ -171,6 +171,15 @@ class InstStrategyCegqi : public QuantifiersModule
   bool hasAddedCbqiLemma( Node q ) { return d_added_cbqi_lemma.find( q )!=d_added_cbqi_lemma.end(); }
   /** process functions */
   void process(Node q, Theory::Effort effort, int e);
+  /**
+   * Get counterexample literal. This is the fresh Boolean variable whose
+   * semantics is "there exists a set of values for which the body of
+   * quantified formula q does not hold". These literals are cached by this
+   * class.
+   */
+  Node getCounterexampleLiteral(Node q);
+  /** map from universal quantifiers to their counterexample literals */
+  std::map<Node, Node> d_ce_lit;
 
   //for identification
   uint64_t d_qid_count;

diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index 94bc2c3f81618d65e8a4a8c2069a937ec8853217..ffd808ed3716b6d98978c5550f1e052067db8ba0 100644 (file)
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -200,26 +200,6 @@ Node TermUtil::getInstConstantBody( Node q ){
   }
 }
 
-Node TermUtil::getCounterexampleLiteral( Node q ){
-  if( d_ce_lit.find( q )==d_ce_lit.end() ){
-    /*
-    Node ceBody = getInstConstantBody( f );
-    //check if any variable are of bad types, and fail if so
-    for( size_t i=0; i<d_inst_constants[f].size(); i++ ){
-      if( d_inst_constants[f][i].getType().isBoolean() ){
-        d_ce_lit[ f ] = Node::null();
-        return Node::null();
-      }
-    }
-    */
-    Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() );
-    //otherwise, ensure literal
-    Node ceLit = d_quantEngine->getValuation().ensureLiteral( g );
-    d_ce_lit[ q ] = ceLit;
-  }
-  return d_ce_lit[ q ];
-}
-
 Node TermUtil::substituteBoundVariablesToInstConstants(Node n, Node q)
 {
   registerQuantifier( q );

diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h
index 302901625d4ba8f5955bd34646cdc0fd3ad94f67..b39a4e129cfc9e6ad6a61c764f7e154779e8c108 100644 (file)
--- a/src/theory/quantifiers/term_util.h
+++ b/src/theory/quantifiers/term_util.h
@@ -125,8 +125,6 @@ public:
   std::map< Node, std::map< Node, unsigned > > d_var_num;
   /** map from universal quantifiers to their inst constant body */
   std::map< Node, Node > d_inst_const_body;
-  /** map from universal quantifiers to their counterexample literals */
-  std::map< Node, Node > d_ce_lit;
   /** instantiation constants to universal quantifiers */
   std::map< Node, Node > d_inst_constants_map;
 public:
@@ -140,8 +138,6 @@ public:
   unsigned getNumInstantiationConstants( Node q ) const;
   /** get the ce body q[e/x] */
   Node getInstConstantBody( Node q );
-  /** get counterexample literal (for cbqi) */
-  Node getCounterexampleLiteral( Node q );
   /** returns node n with bound vars of q replaced by instantiation constants of q
       node n : is the future pattern
       node q : is the quantifier containing which bind the variable