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

1 files changed, 32 insertions, 6 deletions

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