Refactor ceg conjecture initialization (#2411)

5 files changed, 100 insertions, 74 deletions

diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
index e3057da29..1d070417e 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
@@ -70,6 +70,7 @@ void CegConjecture::assign( Node q ) {
   Assert( q.getKind()==FORALL );
   Trace("cegqi") << "CegConjecture : assign : " << q << std::endl;
   d_quant = q;
+  NodeManager* nm = NodeManager::currentNM();
 
   // pre-simplify the quantified formula based on the process utility
   d_simp_quant = d_ceg_proc->preSimplify(d_quant);
@@ -163,10 +164,19 @@ void CegConjecture::assign( Node q ) {
   }
   
   // initialize the guard
-  if (d_ceg_si->getGuard().isNull())
+  d_feasible_guard = nm->mkSkolem("G", nm->booleanType());
+  d_feasible_guard = Rewriter::rewrite(d_feasible_guard);
+  d_feasible_guard = d_qe->getValuation().ensureLiteral(d_feasible_guard);
+  AlwaysAssert(!d_feasible_guard.isNull());
+  // this must be called, both to ensure that the feasible guard is
+  // decided on with true polariy, but also to ensure that output channel
+  // has been used on this call to check.
+  d_qe->getOutputChannel().requirePhase(d_feasible_guard, true);
+
+  if (isSingleInvocation())
   {
     std::vector< Node > lems;
-    d_ceg_si->getInitialSingleInvLemma( lems );
+    d_ceg_si->getInitialSingleInvLemma(d_feasible_guard, lems);
     for( unsigned i=0; i<lems.size(); i++ ){
       Trace("cegqi-lemma") << "Cegqi::Lemma : single invocation " << i << " : " << lems[i] << std::endl;
       d_qe->getOutputChannel().lemma( lems[i] );
@@ -176,10 +186,9 @@ void CegConjecture::assign( Node q ) {
       }
     }
   }
-  Assert( !getGuard().isNull() );
-  Node gneg = getGuard().negate();
+  Node gneg = d_feasible_guard.negate();
   for( unsigned i=0; i<guarded_lemmas.size(); i++ ){
-    Node lem = NodeManager::currentNM()->mkNode( OR, gneg, guarded_lemmas[i] );
+    Node lem = nm->mkNode(OR, gneg, guarded_lemmas[i]);
     Trace("cegqi-lemma") << "Cegqi::Lemma : initial (guarded) lemma : " << lem << std::endl;
     d_qe->getOutputChannel().lemma( lem );
   }
@@ -187,7 +196,7 @@ void CegConjecture::assign( Node q ) {
   Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation() << std::endl;
 }
 
-Node CegConjecture::getGuard() { return d_ceg_si->getGuard(); }
+Node CegConjecture::getGuard() const { return d_feasible_guard; }
 
 bool CegConjecture::isSingleInvocation() const {
   return d_ceg_si->isSingleInvocation();
@@ -196,20 +205,25 @@ bool CegConjecture::isSingleInvocation() const {
 bool CegConjecture::needsCheck( std::vector< Node >& lem ) {
   if( isSingleInvocation() && !d_ceg_si->needsCheck() ){
     return false;
-  }else{
-    bool value;
-    Assert( !getGuard().isNull() );
-    // non or fully single invocation : look at guard only
-    if( d_qe->getValuation().hasSatValue( getGuard(), value ) ) {
-      if( !value ){
-        Trace("cegqi-engine-debug") << "Conjecture is infeasible." << std::endl;
-        return false;
-      }
-    }else{
-      Assert( false );
+  }
+  bool value;
+  Assert(!d_feasible_guard.isNull());
+  // non or fully single invocation : look at guard only
+  if (d_qe->getValuation().hasSatValue(d_feasible_guard, value))
+  {
+    if (!value)
+    {
+      Trace("cegqi-engine-debug") << "Conjecture is infeasible." << std::endl;
+      return false;
     }
-    return true;
   }
+  else
+  {
+    Trace("cegqi-warn") << "WARNING: Guard " << d_feasible_guard
+                        << " is not assigned!" << std::endl;
+    Assert(false);
+  }
+  return true;
 }
 
 
@@ -563,7 +577,7 @@ Node CegConjecture::getStreamGuardedLemma(Node n) const
 Node CegConjecture::getNextDecisionRequest( unsigned& priority ) {
   // first, must try the guard
   // which denotes "this conjecture is feasible"
-  Node feasible_guard = getGuard();
+  Node feasible_guard = d_feasible_guard;
   bool value;
   if( !d_qe->getValuation().hasSatValue( feasible_guard, value ) ) {
     priority = 0;
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.h b/src/theory/quantifiers/sygus/ce_guided_conjecture.h
index 25f063e06..48d307f1e 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.h
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.h
@@ -97,8 +97,11 @@ public:
    * module to get synthesis solutions.
    */
   void getSynthSolutions(std::map<Node, Node>& sol_map, bool singleInvocation);
-  /** get guard, this is "G" in Figure 3 of Reynolds et al CAV 2015 */
-  Node getGuard();
+  /**
+   * The feasible guard whose semantics are "this conjecture is feasiable".
+   * This is "G" in Figure 3 of Reynolds et al CAV 2015.
+   */
+  Node getGuard() const;
   /** is ground */
   bool isGround() { return d_inner_vars.empty(); }
   /** are we using single invocation techniques */
@@ -132,6 +135,8 @@ public:
 private:
   /** reference to quantifier engine */
   QuantifiersEngine * d_qe;
+  /** The feasible guard. */
+  Node d_feasible_guard;
   /** single invocation utility */
   std::unique_ptr<CegConjectureSingleInv> d_ceg_si;
   /** utility for static preprocessing and analysis of conjectures */
diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
index 1e0b36a3c..83a576d37 100644
--- a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
@@ -59,10 +59,10 @@ void CegInstantiation::check(Theory::Effort e, QEffort quant_e)
     d_waiting_conj = Node::null();
     if (!d_conj->isAssigned())
     {
-      if (!assignConjecture(q))
-      {
-        return;
-      }
+      assignConjecture(q);
+      // assign conjecture always uses the output channel, we return and
+      // re-check here.
+      return;
     }
   }
   unsigned echeck =
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 39c3baf5c..7d8db8c03 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -49,12 +49,12 @@ CegConjectureSingleInv::CegConjectureSingleInv(QuantifiersEngine* qe,
       d_sip(new SingleInvocationPartition),
       d_sol(new CegConjectureSingleInvSol(qe)),
       d_cosi(new CegqiOutputSingleInv(this)),
-      d_cinst(NULL),
+      d_cinst(new CegInstantiator(d_qe, d_cosi, false, false)),
       d_c_inst_match_trie(NULL),
-      d_single_invocation(false) {
-  //  third and fourth arguments set to (false,false) until we have solution
-  //  reconstruction for delta and infinity
-  d_cinst = new CegInstantiator(d_qe, d_cosi, false, false);
+      d_single_invocation(false)
+{
+  // The third and fourth arguments of d_cosi set to (false,false) until we have
+  // solution reconstruction for delta and infinity.
 
   if (options::incrementalSolving()) {
     d_c_inst_match_trie = new inst::CDInstMatchTrie(qe->getUserContext());
@@ -65,51 +65,53 @@ CegConjectureSingleInv::~CegConjectureSingleInv() {
   if (d_c_inst_match_trie) {
     delete d_c_inst_match_trie;
   }
-  delete d_cinst;
   delete d_cosi;
   delete d_sol;  // (new CegConjectureSingleInvSol(qe)),
   delete d_sip;  // d_sip(new SingleInvocationPartition),
 }
 
-void CegConjectureSingleInv::getInitialSingleInvLemma( std::vector< Node >& lems ) {
-  Assert( d_si_guard.isNull() );
-  //single invocation guard
-  d_si_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) );
-  d_si_guard = d_qe->getValuation().ensureLiteral( d_si_guard );
-  AlwaysAssert( !d_si_guard.isNull() );
-  d_qe->getOutputChannel().requirePhase( d_si_guard, true );
-
-  if( !d_single_inv.isNull() ) {
-    //make for new var/sk
-    d_single_inv_var.clear();
-    d_single_inv_sk.clear();
-    Node inst;
-    if( d_single_inv.getKind()==FORALL ){
-      for( unsigned i=0; i<d_single_inv[0].getNumChildren(); i++ ){
-        std::stringstream ss;
-        ss << "k_" << d_single_inv[0][i];
-        Node k = NodeManager::currentNM()->mkSkolem( ss.str(), d_single_inv[0][i].getType(), "single invocation function skolem" );
-        d_single_inv_var.push_back( d_single_inv[0][i] );
-        d_single_inv_sk.push_back( k );
-        d_single_inv_sk_index[k] = i;
-      }
-      inst = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
-    }else{
-      inst = d_single_inv;
-    }
-    inst = TermUtil::simpleNegate( inst );
-    Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl;
-
-    //register with the instantiator
-    Node ginst = NodeManager::currentNM()->mkNode( OR, d_si_guard.negate(), inst );
-    lems.push_back( ginst );
-    //make and register the instantiator
-    if( d_cinst ){
-      delete d_cinst;
+void CegConjectureSingleInv::getInitialSingleInvLemma(Node g,
+                                                      std::vector<Node>& lems)
+{
+  Assert(!g.isNull());
+  Assert(!d_single_inv.isNull());
+  // make for new var/sk
+  d_single_inv_var.clear();
+  d_single_inv_sk.clear();
+  Node inst;
+  NodeManager* nm = NodeManager::currentNM();
+  if (d_single_inv.getKind() == FORALL)
+  {
+    for (unsigned i = 0, size = d_single_inv[0].getNumChildren(); i < size; i++)
+    {
+      std::stringstream ss;
+      ss << "k_" << d_single_inv[0][i];
+      Node k = nm->mkSkolem(ss.str(),
+                            d_single_inv[0][i].getType(),
+                            "single invocation function skolem");
+      d_single_inv_var.push_back(d_single_inv[0][i]);
+      d_single_inv_sk.push_back(k);
+      d_single_inv_sk_index[k] = i;
     }
-    d_cinst = new CegInstantiator( d_qe, d_cosi, false, false );
-    d_cinst->registerCounterexampleLemma( lems, d_single_inv_sk );
+    inst = d_single_inv[1].substitute(d_single_inv_var.begin(),
+                                      d_single_inv_var.end(),
+                                      d_single_inv_sk.begin(),
+                                      d_single_inv_sk.end());
   }
+  else
+  {
+    inst = d_single_inv;
+  }
+  inst = TermUtil::simpleNegate(inst);
+  Trace("cegqi-si") << "Single invocation initial lemma : " << inst
+                    << std::endl;
+
+  // register with the instantiator
+  Node ginst = nm->mkNode(OR, g.negate(), inst);
+  lems.push_back(ginst);
+  // make and register the instantiator
+  d_cinst.reset(new CegInstantiator(d_qe, d_cosi, false, false));
+  d_cinst->registerCounterexampleLemma(lems, d_single_inv_sk);
 }
 
 void CegConjectureSingleInv::initialize( Node q ) {
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
index 00b50a4a1..09829e894 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
@@ -149,7 +149,7 @@ class CegConjectureSingleInv {
   // the instantiator's output channel
   CegqiOutputSingleInv* d_cosi;
   // the instantiator
-  CegInstantiator* d_cinst;
+  std::unique_ptr<CegInstantiator> d_cinst;
 
   // list of skolems for each argument of programs
   std::vector<Node> d_single_inv_arg_sk;
@@ -188,7 +188,6 @@ class CegConjectureSingleInv {
   bool d_single_invocation;
   // single invocation portion of quantified formula
   Node d_single_inv;
-  Node d_si_guard;
   // transition relation version per program
   std::map< Node, Node > d_trans_pre;
   std::map< Node, Node > d_trans_post;
@@ -203,11 +202,17 @@ class CegConjectureSingleInv {
 
   // get simplified conjecture
   Node getSimplifiedConjecture() { return d_simp_quant; }
-  // get single invocation guard
-  Node getGuard() { return d_si_guard; }
  public:
-  //get the single invocation lemma(s)
-  void getInitialSingleInvLemma( std::vector< Node >& lems );
+  /** get the single invocation lemma(s)
+   *
+   * This adds lemmas to lem that initializes this class for doing
+   * counterexample-guided instantiation for the synthesis conjecture. These
+   * lemmas correspond to the negation of the body of the (anti-skolemized)
+   * form of the conjecture for fresh skolems.
+   *
+   * Argument g is guard, for which all the above lemmas are guarded.
+   */
+  void getInitialSingleInvLemma(Node g, std::vector<Node>& lems);
   // initialize this class for synthesis conjecture q
   void initialize( Node q );
   /** finish initialize