From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 4 Sep 2019 19:45:21 +0000 (-0500)
Subject: Move getCounterexampleLiteral out of term utilities (#3238)
X-Git-Tag: cvc5-1.0.0~3980
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d9ee2ae563b031547e76245d9f01fb24b95bc8cb;p=cvc5.git

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 0f866208d..ab5bbc25f 100644
--- 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 c6a9ddd11..ecae4ab64 100644
--- 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 94bc2c3f8..ffd808ed3 100644
--- 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 302901625..b39a4e129 100644
--- 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