Decision strategy: incorporate separation logic. (#2494)

3 files changed, 12 insertions, 39 deletions

diff --git a/src/theory/sep/kinds b/src/theory/sep/kinds
index b83515d38..235b61172 100644
--- a/src/theory/sep/kinds
+++ b/src/theory/sep/kinds
@@ -8,7 +8,7 @@ theory THEORY_SEP ::CVC4::theory::sep::TheorySep "theory/sep/theory_sep.h"
 typechecker "theory/sep/theory_sep_type_rules.h"
 
 properties polite stable-infinite parametric
-properties check propagate presolve getNextDecisionRequest
+properties check propagate presolve
 
 rewriter ::CVC4::theory::sep::TheorySepRewriter "theory/sep/theory_sep_rewriter.h"
 
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 6085b1f23..d1ba65dd8 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -311,6 +311,7 @@ void TheorySep::check(Effort e) {
 
   TimerStat::CodeTimer checkTimer(d_checkTime);
   Trace("sep-check") << "Sep::check(): " << e << endl;
+  NodeManager* nm = NodeManager::currentNM();
 
   while( !done() && !d_conflict ){
     // Get all the assertions
@@ -454,12 +455,16 @@ void TheorySep::check(Effort e) {
             if( !use_polarity ){
               // introduce guard, assert positive version
               Trace("sep-lemma-debug") << "Negated spatial constraint asserted to sep theory: " << fact << std::endl;
-              Node lit = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) );
-              lit = getValuation().ensureLiteral( lit );
+              Node g = nm->mkSkolem("G", nm->booleanType());
+              d_neg_guard_strategy[g].reset(new DecisionStrategySingleton(
+                  "sep_neg_guard", g, getSatContext(), getValuation()));
+              DecisionStrategySingleton* ds = d_neg_guard_strategy[g].get();
+              getDecisionManager()->registerStrategy(
+                  DecisionManager::STRAT_SEP_NEG_GUARD, ds);
+              Node lit = ds->getLiteral(0);
               d_neg_guard[s_lbl][s_atom] = lit;
               Trace("sep-lemma-debug") << "Neg guard : " << s_lbl << " " << s_atom << " " << lit << std::endl;
               AlwaysAssert( !lit.isNull() );
-              d_out->requirePhase( lit, true );
               d_neg_guards.push_back( lit );
               d_guard_to_assertion[lit] = s_atom;
               //Node lem = NodeManager::currentNM()->mkNode( kind::EQUAL, lit, conc );
@@ -822,40 +827,6 @@ bool TheorySep::needsCheckLastEffort() {
   return hasFacts();
 }
 
-Node TheorySep::getNextDecisionRequest( unsigned& priority ) {
-  for( unsigned i=0; i<d_neg_guards.size(); i++ ){
-    Node g = d_neg_guards[i];
-    bool success = true;
-    if( getLogicInfo().isQuantified() ){
-      Assert( d_guard_to_assertion.find( g )!= d_guard_to_assertion.end() );
-      Node a = d_guard_to_assertion[g];
-      Node q = quantifiers::TermUtil::getInstConstAttr( a );
-      if( !q.isNull() ){
-        //must wait to decide on counterexample literal from quantified formula
-        Node cel = getQuantifiersEngine()->getTermUtil()->getCounterexampleLiteral( q );
-        bool value;
-        if( d_valuation.hasSatValue( cel, value ) ){
-          Trace("sep-dec-debug") << "TheorySep::getNextDecisionRequest : dependent guard " << g << " depends on value for guard for quantified formula : " << value << std::endl;
-          success = value;
-        }else{
-          Trace("sep-dec-debug") << "TheorySep::getNextDecisionRequest : wait to decide on " << g << " until " << cel << " is set " << std::endl;
-          success = false;
-        }
-      }
-    }
-    if( success ){
-      bool value;
-      if( !d_valuation.hasSatValue( g, value ) ) {
-        Trace("sep-dec") << "TheorySep::getNextDecisionRequest : " << g << " (" << i << "/" << d_neg_guards.size() << ")" << std::endl;
-        priority = 0;
-        return g;
-      }
-    }
-  }
-  Trace("sep-dec-debug") << "TheorySep::getNextDecisionRequest : null" << std::endl;
-  return Node::null();
-}
-
 void TheorySep::conflict(TNode a, TNode b) {
   Trace("sep-conflict") << "Sep::conflict : " << a << " " << b << std::endl;
   Node conflictNode = explain(a.eqNode(b));
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index df384739d..f8bb58784 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -112,7 +112,6 @@ class TheorySep : public Theory {
   /////////////////////////////////////////////////////////////////////////////
 
  public:
-  Node getNextDecisionRequest(unsigned& priority) override;
 
   void presolve() override;
   void shutdown() override {}
@@ -218,6 +217,9 @@ class TheorySep : public Theory {
   std::map< Node, std::map< Node, Node > > d_red_conc;
   std::map< Node, std::map< Node, Node > > d_neg_guard;
   std::vector< Node > d_neg_guards;
+  /** a (singleton) decision strategy for each negative guard. */
+  std::map<Node, std::unique_ptr<DecisionStrategySingleton> >
+      d_neg_guard_strategy;
   std::map< Node, Node > d_guard_to_assertion;
   /** inferences: maintained to ensure ref count for internally introduced nodes */
   NodeList d_infer;