Freeing CegConjecture::d_ceg_si. Also making d_ceg_si a provate member of CegConjecture.

3 files changed, 123 insertions, 52 deletions

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 345a5eaef..0584a0cae 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -22,19 +22,25 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/theory_engine.h"
 
-using namespace CVC4;
 using namespace CVC4::kind;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
 using namespace std;
 
 namespace CVC4 {
+namespace theory {
+namespace quantifiers {
 
-CegConjecture::CegConjecture( QuantifiersEngine * qe, context::Context* c ) : d_qe( qe ), d_curr_lit( c, 0 ){
+
+CegConjecture::CegConjecture( QuantifiersEngine * qe, context::Context* c )
+    : d_qe( qe ), d_curr_lit( c, 0 )
+{
   d_refine_count = 0;
   d_ceg_si = new CegConjectureSingleInv( qe, this );
 }
 
+CegConjecture::~CegConjecture() {
+  delete d_ceg_si;
+}
+
 void CegConjecture::assign( Node q ) {
   Assert( d_quant.isNull() );
   Assert( q.getKind()==FORALL );
@@ -149,7 +155,7 @@ CegqiFairMode CegConjecture::getCegqiFairMode() {
   return isSingleInvocation() ? CEGQI_FAIR_NONE : options::ceGuidedInstFair();
 }
 
-bool CegConjecture::isSingleInvocation() {
+bool CegConjecture::isSingleInvocation() const {
   return d_ceg_si->isSingleInvocation();
 }
 
@@ -219,11 +225,13 @@ bool CegInstantiation::needsCheck( Theory::Effort e ) {
 }
 
 unsigned CegInstantiation::needsModel( Theory::Effort e ) {
-  return d_conj->d_ceg_si->isSingleInvocation() ? QuantifiersEngine::QEFFORT_STANDARD : QuantifiersEngine::QEFFORT_MODEL;
+  return d_conj->getCegConjectureSingleInv()->isSingleInvocation()
+      ? QuantifiersEngine::QEFFORT_STANDARD : QuantifiersEngine::QEFFORT_MODEL;
 }
 
 void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) {
-  unsigned echeck = d_conj->d_ceg_si->isSingleInvocation() ? QuantifiersEngine::QEFFORT_STANDARD : QuantifiersEngine::QEFFORT_MODEL;
+  unsigned echeck = d_conj->getCegConjectureSingleInv()->isSingleInvocation() ?
+      QuantifiersEngine::QEFFORT_STANDARD : QuantifiersEngine::QEFFORT_MODEL;
   if( quant_e==echeck ){
     Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---" << std::endl;
     Trace("cegqi-engine-debug") << std::endl;
@@ -294,12 +302,13 @@ Node CegInstantiation::getNextDecisionRequest() {
   if( d_conj->isAssigned() ){
     d_conj->initializeGuard( d_quantEngine );
     std::vector< Node > req_dec;
-    if( !d_conj->d_ceg_si->d_full_guard.isNull() ){
-      req_dec.push_back( d_conj->d_ceg_si->d_full_guard );
+    const CegConjectureSingleInv* ceg_si = d_conj->getCegConjectureSingleInv();
+    if( ! ceg_si->d_full_guard.isNull() ){
+      req_dec.push_back( ceg_si->d_full_guard );
     }
     //must decide ns guard before s guard
-    if( !d_conj->d_ceg_si->d_ns_guard.isNull() ){
-      req_dec.push_back( d_conj->d_ceg_si->d_ns_guard );
+    if( !ceg_si->d_ns_guard.isNull() ){
+      req_dec.push_back( ceg_si->d_ns_guard );
     }
     req_dec.push_back( d_conj->getGuard() );
     for( unsigned i=0; i<req_dec.size(); i++ ){
@@ -348,9 +357,9 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
   if( conj->d_ce_sk.empty() ){
     Trace("cegqi-engine") << "  *** Check candidate phase..." << std::endl;
     if( conj->d_syntax_guided ){
-      if( conj->d_ceg_si ){
+      if( conj->getCegConjectureSingleInv() != NULL ){
         std::vector< Node > lems;
-        if( conj->d_ceg_si->check( lems ) ){
+        if( conj->doCegConjectureCheck( lems ) ){
           if( !lems.empty() ){
             d_last_inst_si = true;
             for( unsigned j=0; j<lems.size(); j++ ){
@@ -600,39 +609,53 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
       Node sol;
       int status;
       if( d_last_inst_si ){
-        Assert( d_conj->d_ceg_si );
-        sol = d_conj->d_ceg_si->getSolution( i, tn, status );
+        Assert( d_conj->getCegConjectureSingleInv() != NULL );
+        sol = d_conj->getSingleInvocationSolution( i, tn, status );
         sol = sol.getKind()==LAMBDA ? sol[1] : sol;
       }else{
         if( !d_conj->d_candidate_inst[i].empty() ){
           sol = d_conj->d_candidate_inst[i].back();
-          //check if this was based on a template, if so, we must do reconstruction
+          // Check if this was based on a template, if so, we must do
+          // Reconstruction
           if( d_conj->d_assert_quant!=d_conj->d_quant ){
             Node sygus_sol = sol;
-            Trace("cegqi-inv") << "Sygus version of solution is : " << sol << ", type : " << sol.getType() << std::endl;
+            Trace("cegqi-inv") << "Sygus version of solution is : " << sol
+                               << ", type : " << sol.getType() << std::endl;
             std::vector< Node > subs;
             Expr svl = dt.getSygusVarList();
             for( unsigned j=0; j<svl.getNumChildren(); j++ ){
               subs.push_back( Node::fromExpr( svl[j] ) );
             }
             if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){
-              if( d_conj->d_ceg_si->d_trans_pre.find( prog )!=d_conj->d_ceg_si->d_trans_pre.end() ){
-                Assert( d_conj->d_ceg_si->d_prog_templ_vars[prog].size()==subs.size() );
-                Node pre = d_conj->d_ceg_si->d_trans_pre[prog];
-                pre = pre.substitute( d_conj->d_ceg_si->d_prog_templ_vars[prog].begin(), d_conj->d_ceg_si->d_prog_templ_vars[prog].end(),
+              const CegConjectureSingleInv* ceg_si =
+                  d_conj->getCegConjectureSingleInv();
+              if(ceg_si->d_trans_pre.find( prog ) != ceg_si->d_trans_pre.end()){
+                std::vector<Node>& templ_vars = d_conj->getProgTempVars(prog);
+                Assert(templ_vars.size() == subs.size());
+                Node pre = ceg_si->getTransPre(prog);
+                pre = pre.substitute( templ_vars.begin(), templ_vars.end(),
                                       subs.begin(), subs.end() );
-                sol = getTermDatabase()->getTermDatabaseSygus()->sygusToBuiltin( sol, sol.getType() );
-                Trace("cegqi-inv") << "Builtin version of solution is : " << sol << ", type : " << sol.getType() << std::endl;
+                TermDbSygus* sygusDb = getTermDatabase()->getTermDatabaseSygus();
+                sol = sygusDb->sygusToBuiltin( sol, sol.getType() );
+                Trace("cegqi-inv") << "Builtin version of solution is : "
+                                   << sol << ", type : " << sol.getType()
+                                   << std::endl;
                 sol = NodeManager::currentNM()->mkNode( OR, sol, pre );
               }
-            }else if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST ){
-              if( d_conj->d_ceg_si->d_trans_post.find( prog )!=d_conj->d_ceg_si->d_trans_post.end() ){
-                Assert( d_conj->d_ceg_si->d_prog_templ_vars[prog].size()==subs.size() );
-                Node post = d_conj->d_ceg_si->d_trans_post[prog];
-                post = post.substitute( d_conj->d_ceg_si->d_prog_templ_vars[prog].begin(), d_conj->d_ceg_si->d_prog_templ_vars[prog].end(),
+            }else if(options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST){
+              const CegConjectureSingleInv* ceg_si =
+                  d_conj->getCegConjectureSingleInv();
+              if(ceg_si->d_trans_post.find(prog) != ceg_si->d_trans_post.end()){
+                std::vector<Node>& templ_vars = d_conj->getProgTempVars(prog);
+                Assert( templ_vars.size()==subs.size() );
+                Node post = ceg_si->getTransPost(prog);
+                post = post.substitute( templ_vars.begin(), templ_vars.end(),
                                         subs.begin(), subs.end() );
-                sol = getTermDatabase()->getTermDatabaseSygus()->sygusToBuiltin( sol, sol.getType() );
-                Trace("cegqi-inv") << "Builtin version of solution is : " << sol << ", type : " << sol.getType() << std::endl;
+                TermDbSygus* sygusDb = getTermDatabase()->getTermDatabaseSygus();
+                sol = sygusDb->sygusToBuiltin( sol, sol.getType() );
+                Trace("cegqi-inv") << "Builtin version of solution is : "
+                                   << sol << ", type : " << sol.getType()
+                                   << std::endl;
                 sol = NodeManager::currentNM()->mkNode( AND, sol, post );
               }
             }
@@ -643,7 +666,7 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
               Trace("cegqi-inv-debug") << "With template : " << sol << std::endl;
               sol = Rewriter::rewrite( sol );
               Trace("cegqi-inv-debug") << "Simplified : " << sol << std::endl;
-              sol = d_conj->d_ceg_si->reconstructToSyntax( sol, tn, status );
+              sol = d_conj->reconstructToSyntaxSingleInvocation(sol, tn, status);
               sol = sol.getKind()==LAMBDA ? sol[1] : sol;
             }
           }else{
@@ -712,5 +735,6 @@ CegInstantiation::Statistics::~Statistics(){
   smtStatisticsRegistry()->unregisterStat(&d_cegqi_si_lemmas);
 }
 
-
-}
+}/* namespace CVC4::theory::quantifiers */
+}/* namespace CVC4::theory */
+}/* namespace CVC4 */
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 8274561ca..4a93e566c 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -33,6 +33,8 @@ private:
   QuantifiersEngine * d_qe;
 public:
   CegConjecture( QuantifiersEngine * qe, context::Context* c );
+  ~CegConjecture();
+
   /** quantified formula asserted */
   Node d_assert_quant;
   /** quantified formula (after processing) */
@@ -56,12 +58,36 @@ public:
   unsigned d_refine_count;
   /** current extential quantifeirs whose couterexamples we must refine */
   std::vector< std::vector< Node > > d_ce_sk;
+
+  const CegConjectureSingleInv* getCegConjectureSingleInv() const {
+    return d_ceg_si;
+  }
+
+  bool doCegConjectureCheck(std::vector< Node >& lems) {
+    return d_ceg_si->check(lems);
+  }
+
+  Node getSingleInvocationSolution(unsigned sol_index, TypeNode stn,
+                                   int& reconstructed, bool rconsSygus=true){
+    return d_ceg_si->getSolution(sol_index, stn, reconstructed, rconsSygus);
+  }
+
+  Node reconstructToSyntaxSingleInvocation(
+      Node s, TypeNode stn, int& reconstructed, bool rconsSygus = true ) {
+    return d_ceg_si->reconstructToSyntax(s, stn, reconstructed, rconsSygus);
+  }
+
+  std::vector<Node>& getProgTempVars(Node prog) {
+    return d_ceg_si->d_prog_templ_vars[prog];
+  }
+
+ private:
   /** single invocation utility */
   CegConjectureSingleInv * d_ceg_si;
 public: //non-syntax guided (deprecated)
   /** guard */
   bool d_syntax_guided;
-  Node d_nsg_guard;  
+  Node d_nsg_guard;
 public:  //for fairness
   /** the cardinality literals */
   std::map< int, Node > d_lits;
@@ -76,7 +102,7 @@ public:  //for fairness
   /** fairness */
   CegqiFairMode getCegqiFairMode();
   /** is single invocation */
-  bool isSingleInvocation();
+  bool isSingleInvocation() const;
   /** is single invocation */
   bool isFullySingleInvocation();
   /** needs check */
@@ -151,10 +177,10 @@ public:
     ~Statistics();
   };/* class CegInstantiation::Statistics */
   Statistics d_statistics;
-};
+}; /* class CegInstantiation */
 
-}
-}
-}
+} /* namespace CVC4::theory::quantifiers */
+} /* namespace CVC4::theory */
+} /* namespace CVC4 */
 
 #endif
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index c25cf7633..69fe13d52 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -58,13 +58,21 @@ private:
   CegqiOutputSingleInv * d_cosi;
   CegInstantiator * d_cinst;
   //for recognizing templates for invariant synthesis
-  Node substituteInvariantTemplates( Node n, std::map< Node, Node >& prog_templ, std::map< Node, std::vector< Node > >& prog_templ_vars );
+  Node substituteInvariantTemplates(
+      Node n, std::map< Node, Node >& prog_templ,
+      std::map< Node, std::vector< Node > >& prog_templ_vars );
   // partially single invocation
-  Node removeDeepEmbedding( Node n, std::vector< Node >& progs, std::vector< TypeNode >& types, int& type_valid, std::map< Node, Node >& visited );
+  Node removeDeepEmbedding( Node n, std::vector< Node >& progs,
+                            std::vector< TypeNode >& types, int& type_valid,
+                            std::map< Node, Node >& visited );
   Node addDeepEmbedding( Node n, std::map< Node, Node >& visited );
   //presolve
-  void collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq );
-  void getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms, std::map< Node, std::vector< Node > >& teq, Node n, std::vector< Node >& conj );
+  void collectPresolveEqTerms( Node n,
+                               std::map< Node, std::vector< Node > >& teq );
+  void getPresolveEqConjuncts( std::vector< Node >& vars,
+                               std::vector< Node >& terms,
+                               std::map< Node, std::vector< Node > >& teq,
+                               Node n, std::vector< Node >& conj );
   //constructing solution
   Node constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index );
   Node postProcessSolution( Node n );
@@ -113,7 +121,7 @@ public:
   Node d_full_inv;
   Node d_full_guard;
   //explanation for current single invocation conjecture
-  Node d_single_inv_exp;  
+  Node d_single_inv_exp;
   // transition relation version per program
   std::map< Node, Node > d_trans_pre;
   std::map< Node, Node > d_trans_post;
@@ -132,19 +140,33 @@ public:
   //get solution
   Node getSolution( unsigned sol_index, TypeNode stn, int& reconstructed, bool rconsSygus = true );
   //reconstruct to syntax
-  Node reconstructToSyntax( Node s, TypeNode stn, int& reconstructed, bool rconsSygus = true );
+  Node reconstructToSyntax( Node s, TypeNode stn, int& reconstructed,
+                            bool rconsSygus = true );
   // has ites
   bool hasITEs() { return d_has_ites; }
   // is single invocation
-  bool isSingleInvocation() { return !d_single_inv.isNull(); }
+  bool isSingleInvocation() const { return !d_single_inv.isNull(); }
   // is single invocation
-  bool isFullySingleInvocation() { return !d_single_inv.isNull() && d_nsingle_inv.isNull(); }
+  bool isFullySingleInvocation() const {
+    return !d_single_inv.isNull() && d_nsingle_inv.isNull();
+  }
   //needs check
   bool needsCheck();
   /** preregister conjecture */
   void preregisterConjecture( Node q );
   //initialize next candidate si conjecture (if not fully single invocation)
-  void initializeNextSiConjecture();  
+  void initializeNextSiConjecture();
+
+  Node getTransPre(Node prog) const {
+    std::map<Node, Node>::const_iterator location = d_trans_pre.find(prog);
+    return location->second;
+  }
+
+  Node getTransPost(Node prog) const {
+    std::map<Node, Node>::const_iterator location = d_trans_post.find(prog);
+    return location->second;
+  }
+
 };
 
 // partitions any formulas given to it into single invocation/non-single invocation
@@ -198,9 +220,8 @@ public:
   void debugPrint( const char * c );
 };
 
-
-}
-}
-}
+}/* namespace CVC4::theory::quantifiers */
+}/* namespace CVC4::theory */
+}/* namespace CVC4 */
 
 #endif