Decision strategy: incorporate CEGQI (#2460)

diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 78cc2ac04d8cc3d0fd11657df1c933597dbe98fe..2d8d61736c3464378843afd3091a68e61175df2b 100644 (file)
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -433,7 +433,6 @@ public:
   Node expandDefinition(LogicRequest &logicRequest, Node node);
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);
-  void setQuantifiersEngine(QuantifiersEngine* qe);
 
   void check(Theory::Effort e);
   bool needsCheckLastEffort();

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
index 9b82c1f4b5f990b48c2cb5a4af3f278ae76cd148..95a60afacb8fff6d672f0ade7f525238e5c9db57 100644 (file)
--- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
@@ -69,15 +69,7 @@ InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe)
 
 InstStrategyCegqi::~InstStrategyCegqi()
 {
-  for (std::map<Node, CegInstantiator*>::iterator i = d_cinst.begin(),
-                                                  iend = d_cinst.end();
-       i != iend;
-       ++i)
-  {
-    CegInstantiator* instantiator = (*i).second;
-    delete instantiator;
-  }
-  d_cinst.clear();
+
 }
 
 bool InstStrategyCegqi::needsCheck(Theory::Effort e)
@@ -189,6 +181,27 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q)
         }
       }
     }
+    // The decision strategy for this quantified formula ensures that its
+    // counterexample literal is decided on first. It is user-context dependent.
+    std::map<Node, std::unique_ptr<DecisionStrategy>>::iterator itds =
+        d_dstrat.find(q);
+    DecisionStrategy* dlds = nullptr;
+    if (itds == d_dstrat.end())
+    {
+      d_dstrat[q].reset(
+          new DecisionStrategySingleton("CexLiteral",
+                                        ceLit,
+                                        d_quantEngine->getSatContext(),
+                                        d_quantEngine->getValuation()));
+      dlds = d_dstrat[q].get();
+    }
+    else
+    {
+      dlds = itds->second.get();
+    }
+    // it is appended to the list of strategies
+    d_quantEngine->getTheoryEngine()->getDecisionManager()->registerStrategy(
+        DecisionManager::STRAT_QUANT_CEGQI_FEASIBLE, dlds);
     return true;
   }else{
     return false;
@@ -574,50 +587,6 @@ bool InstStrategyCegqi::doCbqi(Node q)
   return it->second != CEG_UNHANDLED;
 }
 
-Node InstStrategyCegqi::getNextDecisionRequestProc(Node q,
-                                                   std::map<Node, bool>& proc)
-{
-  if( proc.find( q )==proc.end() ){
-    proc[q] = true;
-    //first check children
-    std::map< Node, std::vector< Node > >::iterator itc = d_children_quant.find( q );
-    if( itc!=d_children_quant.end() ){
-      for( unsigned j=0; j<itc->second.size(); j++ ){
-        Node d = getNextDecisionRequestProc( itc->second[j], proc );
-        if( !d.isNull() ){
-          return d;
-        }
-      }
-    }
-    //then check self
-    if( hasAddedCbqiLemma( q ) ){
-      Node cel = d_quantEngine->getTermUtil()->getCounterexampleLiteral( q );
-      bool value;
-      if( !d_quantEngine->getValuation().hasSatValue( cel, value ) ){
-        Trace("cbqi-dec") << "CBQI: get next decision " << cel << std::endl;
-        return cel;
-      }
-    }    
-  }
-  return Node::null(); 
-}
-
-Node InstStrategyCegqi::getNextDecisionRequest(unsigned& priority)
-{
-  std::map< Node, bool > proc;
-  //for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
-  //  Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
-  for( NodeSet::const_iterator it = d_added_cbqi_lemma.begin(); it != d_added_cbqi_lemma.end(); ++it ){
-    Node q = *it;
-    Node d = getNextDecisionRequestProc( q, proc );
-    if( !d.isNull() ){
-      priority = 0;
-      return d;
-    }
-  }
-  return Node::null();
-}
-
 void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) {
   if( e==0 ){
     CegInstantiator * cinst = getInstantiator( q );
@@ -708,23 +677,25 @@ bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) {
 }
 
 CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
-  std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( q );
+  std::map<Node, std::unique_ptr<CegInstantiator>>::iterator it =
+      d_cinst.find(q);
   if( it==d_cinst.end() ){
-    CegInstantiator* cinst =
-        new CegInstantiator(d_quantEngine, d_out.get(), true, true);
-    d_cinst[q] = cinst;
-    return cinst;
-  }else{
-   return it->second;
+    d_cinst[q].reset(
+        new CegInstantiator(d_quantEngine, d_out.get(), true, true));
+    return d_cinst[q].get();
   }
+  return it->second.get();
 }
 
 void InstStrategyCegqi::presolve() {
-  if( options::cbqiPreRegInst() ){
-    for( std::map< Node, CegInstantiator * >::iterator it = d_cinst.begin(); it != d_cinst.end(); ++it ){
-      Trace("cbqi-presolve") << "Presolve " << it->first << std::endl;
-      it->second->presolve( it->first );
-    }
+  if (!options::cbqiPreRegInst())
+  {
+    return;
+  }
+  for (std::pair<const Node, std::unique_ptr<CegInstantiator>>& ci : d_cinst)
+  {
+    Trace("cbqi-presolve") << "Presolve " << ci.first << std::endl;
+    ci.second->presolve(ci.first);
   }
 }
 

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h
index 433de52a8728b3efaaa5f03ae3d6b680c8ab0b11..c3cbf8100a95cd3316599a807630ce5ba5e40108 100644 (file)
--- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h
@@ -18,6 +18,7 @@
 #ifndef __CVC4__INST_STRATEGY_CBQI_H
 #define __CVC4__INST_STRATEGY_CBQI_H
 
+#include "theory/decision_manager.h"
 #include "theory/quantifiers/cegqi/ceg_instantiator.h"
 #include "util/statistics_registry.h"
 
@@ -84,8 +85,6 @@ class InstStrategyCegqi : public QuantifiersModule
   void preRegisterQuantifier(Node q) override;
   // presolve
   void presolve() override;
-  /** get next decision request */
-  Node getNextDecisionRequest(unsigned& priority) override;
   /** Do nested quantifier elimination. */
   Node doNestedQE(Node q, std::vector<Node>& inst_terms, Node lem, bool doVts);
 
@@ -135,7 +134,12 @@ class InstStrategyCegqi : public QuantifiersModule
    * The instantiator for each quantified formula q registered to this class.
    * This object is responsible for finding instantiatons for q.
    */
-  std::map<Node, CegInstantiator*> d_cinst;
+  std::map<Node, std::unique_ptr<CegInstantiator>> d_cinst;
+  /**
+   * The decision strategy for each quantified formula q registered to this
+   * class.
+   */
+  std::map<Node, std::unique_ptr<DecisionStrategy>> d_dstrat;
   /** the current quantified formula we are processing */
   Node d_curr_quant;
   //---------------------- for vts delta minimization
@@ -164,8 +168,6 @@ class InstStrategyCegqi : public QuantifiersModule
   void registerCounterexampleLemma(Node q, Node lem);
   /** has added cbqi lemma */
   bool hasAddedCbqiLemma( Node q ) { return d_added_cbqi_lemma.find( q )!=d_added_cbqi_lemma.end(); }
-  /** get next decision request with dependency checking */
-  Node getNextDecisionRequestProc( Node q, std::map< Node, bool >& proc );  
   /** process functions */
   void process(Node q, Theory::Effort effort, int e);