From: Tim King <taking@cs.nyu.edu>
Date: Mon, 25 Sep 2017 20:02:48 +0000 (-0700)
Subject: Fixing CID 1362917: There was a branch where d_issup was not initialized. Switching... 
X-Git-Tag: cvc5-1.0.0~5620
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e849f5c87c6a92cc06cfae611ce0cab0851e6905;p=cvc5.git

Fixing CID 1362917: There was a branch where d_issup was not initialized. Switching members of InstantiationEngine to uniqur_ptr to simplify such cases. (#1133)
---

diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index c90a3c386..1cdd224e7 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -29,30 +29,27 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 using namespace CVC4::theory::inst;
 
-InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe ) :
-QuantifiersModule( qe ){
-  if( options::eMatching() ){
-    //these are the instantiation strategies for E-matching
-    //user-provided patterns
-    if( options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){
-      d_isup = new InstStrategyUserPatterns( d_quantEngine );
-      d_instStrategies.push_back( d_isup );
+InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe)
+    : QuantifiersModule(qe),
+      d_instStrategies(),
+      d_isup(),
+      d_i_ag(),
+      d_quants() {
+  if (options::eMatching()) {
+    // these are the instantiation strategies for E-matching
+    // user-provided patterns
+    if (options::userPatternsQuant() != USER_PAT_MODE_IGNORE) {
+      d_isup.reset(new InstStrategyUserPatterns(d_quantEngine));
+      d_instStrategies.push_back(d_isup.get());
     }
 
-    //auto-generated patterns
-    d_i_ag = new InstStrategyAutoGenTriggers( d_quantEngine );
-    d_instStrategies.push_back( d_i_ag );
-  }else{
-    d_isup = NULL;
-    d_i_ag = NULL;
+    // auto-generated patterns
+    d_i_ag.reset(new InstStrategyAutoGenTriggers(d_quantEngine));
+    d_instStrategies.push_back(d_i_ag.get());
   }
 }
 
-InstantiationEngine::~InstantiationEngine() {
-  delete d_i_ag;
-  delete d_isup;
-}
-
+InstantiationEngine::~InstantiationEngine() {}
 
 void InstantiationEngine::presolve() {
   for( unsigned i=0; i<d_instStrategies.size(); ++i ){
@@ -194,14 +191,14 @@ void InstantiationEngine::registerQuantifier( Node f ){
   }
 }
 
-void InstantiationEngine::addUserPattern( Node q, Node pat ){
-  if( d_isup ){
-    d_isup->addUserPattern( q, pat );
+void InstantiationEngine::addUserPattern(Node q, Node pat) {
+  if (d_isup) {
+    d_isup->addUserPattern(q, pat);
   }
 }
 
-void InstantiationEngine::addUserNoPattern( Node q, Node pat ){
-  if( d_i_ag ){
-    d_i_ag->addUserNoPattern( q, pat );
+void InstantiationEngine::addUserNoPattern(Node q, Node pat) {
+  if (d_i_ag) {
+    d_i_ag->addUserNoPattern(q, pat);
   }
 }
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 308024f4d..140ea9250 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -17,6 +17,8 @@
 #ifndef __CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H
 #define __CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H
 
+#include <memory>
+
 #include "theory/quantifiers_engine.h"
 #include "theory/quantifiers/theory_quantifiers.h"
 
@@ -53,42 +55,41 @@ public:
   //virtual void registerQuantifier( Node q ) {}
 };/* class InstStrategy */
 
-class InstantiationEngine : public QuantifiersModule
-{
-private:
+class InstantiationEngine : public QuantifiersModule {
+ private:
   /** instantiation strategies */
-  std::vector< InstStrategy* > d_instStrategies;
+  std::vector<InstStrategy*> d_instStrategies;
   /** user-pattern instantiation strategy */
-  InstStrategyUserPatterns* d_isup;
+  std::unique_ptr<InstStrategyUserPatterns> d_isup;
   /** auto gen triggers; only kept for destructor cleanup */
-  InstStrategyAutoGenTriggers* d_i_ag;
-private:
-  typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
+  std::unique_ptr<InstStrategyAutoGenTriggers> d_i_ag;
+
+  typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
   /** current processing quantified formulas */
-  std::vector< Node > d_quants;
-private:
+  std::vector<Node> d_quants;
+
   /** is the engine incomplete for this quantifier */
-  bool isIncomplete( Node q );
+  bool isIncomplete(Node q);
   /** do instantiation round */
-  void doInstantiationRound( Theory::Effort effort );
-public:
-  InstantiationEngine( QuantifiersEngine* qe );
+  void doInstantiationRound(Theory::Effort effort);
+
+ public:
+  InstantiationEngine(QuantifiersEngine* qe);
   ~InstantiationEngine();
   void presolve();
-  bool needsCheck( Theory::Effort e );
-  void reset_round( Theory::Effort e );
-  void check( Theory::Effort e, unsigned quant_e );
-  bool checkCompleteFor( Node q );
-  void preRegisterQuantifier( Node q );
-  void registerQuantifier( Node q );
-  Node explain(TNode n){ return Node::null(); }
+  bool needsCheck(Theory::Effort e);
+  void reset_round(Theory::Effort e);
+  void check(Theory::Effort e, unsigned quant_e);
+  bool checkCompleteFor(Node q);
+  void preRegisterQuantifier(Node q);
+  void registerQuantifier(Node q);
+  Node explain(TNode n) { return Node::null(); }
   /** add user pattern */
-  void addUserPattern( Node q, Node pat );
-  void addUserNoPattern( Node q, Node pat );
-public:
+  void addUserPattern(Node q, Node pat);
+  void addUserNoPattern(Node q, Node pat);
   /** Identify this module */
   std::string identify() const { return "InstEngine"; }
-};/* class InstantiationEngine */
+}; /* class InstantiationEngine */
 
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */