Fixing a memory leak in the CnfStream unit tests.

diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 661108dd0b50a8c9f6d6cfe1992db896b29607c5..a965018f83ea235e38c22c57c9c0015893178327 100644 (file)
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -46,19 +46,18 @@ class PropEngine;
  * @author Tim King <taking@cs.nyu.edu>
  */
 class CnfStream {
-
-public:
-
+ public:
   /** Cache of what nodes have been registered to a literal. */
-  typedef context::CDInsertHashMap<SatLiteral, TNode, SatLiteralHashFunction> LiteralToNodeMap;
+  typedef context::CDInsertHashMap<SatLiteral, TNode, SatLiteralHashFunction>
+      LiteralToNodeMap;
 
   /** Cache of what literals have been registered to a node. */
-  typedef context::CDInsertHashMap<Node, SatLiteral, NodeHashFunction> NodeToLiteralMap;
-
-protected:
+  typedef context::CDInsertHashMap<Node, SatLiteral, NodeHashFunction>
+      NodeToLiteralMap;
 
+ protected:
   /** The SAT solver we will be using */
-  SatSolver *d_satSolver;
+  SatSolver* d_satSolver;
 
   /** Boolean variables that we translated */
   context::CDList<TNode> d_booleanVariables;
@@ -107,7 +106,8 @@ protected:
    * detection," when BIG FORMULA is later asserted, it is clausified
    * separately, and "lit" is never asserted as a unit clause.
    */
-  //KEEP_STATISTIC(IntStat, d_fortunateLiterals, "prop::CnfStream::fortunateLiterals", 0);
+  // KEEP_STATISTIC(IntStat, d_fortunateLiterals,
+  //               "prop::CnfStream::fortunateLiterals", 0);
 
   /** Remove nots from the node */
   TNode stripNot(TNode node) {
@@ -160,12 +160,15 @@ protected:
    * Acquires a new variable from the SAT solver to represent the node
    * and inserts the necessary data it into the mapping tables.
    * @param node a formula
-   * @param isTheoryAtom is this a theory atom that needs to be asserted to theory
+   * @param isTheoryAtom is this a theory atom that needs to be asserted to
+   * theory.
    * @param preRegister whether to preregister the atom with the theory
-   * @param canEliminate whether the sat solver can safely eliminate this variable
+   * @param canEliminate whether the sat solver can safely eliminate this
+   * variable.
    * @return the literal corresponding to the formula
    */
-  SatLiteral newLiteral(TNode node, bool isTheoryAtom = false, bool preRegister = false, bool canEliminate = true);
+  SatLiteral newLiteral(TNode node, bool isTheoryAtom = false,
+                        bool preRegister = false, bool canEliminate = true);
 
   /**
    * Constructs a new literal for an atom and returns it.  Calls
@@ -177,31 +180,28 @@ protected:
    */
   SatLiteral convertAtom(TNode node, bool noPreprocessing = false);
 
-public:
-
+ public:
   /**
    * Constructs a CnfStream that sends constructs an equi-satisfiable
-   * set of clauses and sends them to the given sat solver.
-   * @param satSolver the sat solver to use
-   * @param registrar the entity that takes care of preregistration of Nodes
-   * @param context the context that the CNF should respect
-   * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping,
+   * set of clauses and sends them to the given sat solver. This does not take
+   * ownership of satSolver, registrar, or context.
+   * @param satSolver the sat solver to use.
+   * @param registrar the entity that takes care of preregistration of Nodes.
+   * @param context the context that the CNF should respect.
+   * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping.
    * @param name string identifier to distinguish between different instances
-   * even for non-theory literals
+   * even for non-theory literals.
    */
-  CnfStream(SatSolver* satSolver,
-            Registrar* registrar,
-            context::Context* context,
-            bool fullLitToNodeMap = false,
-            std::string name="");
+  CnfStream(SatSolver* satSolver, Registrar* registrar,
+            context::Context* context, bool fullLitToNodeMap = false,
+            std::string name = "");
 
   /**
    * Destructs a CnfStream.  This implementation does nothing, but we
    * need a virtual destructor for safety in case subclasses have a
    * destructor.
    */
-  virtual ~CnfStream() {
-  }
+  virtual ~CnfStream() {}
 
   /**
    * Converts and asserts a formula.
@@ -209,7 +209,9 @@ public:
    * @param removable whether the sat solver can choose to remove the clauses
    * @param negated whether we are asserting the node negated
    */
-  virtual void convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from = TNode::null()) = 0;
+  virtual void convertAndAssert(TNode node, bool removable, bool negated,
+                                ProofRule proof_id,
+                                TNode from = TNode::null()) = 0;
 
   /**
    * Get the node that is represented by the given SatLiteral.
@@ -219,17 +221,17 @@ public:
   TNode getNode(const SatLiteral& literal);
 
   /**
-   * Returns true iff the node has an assigned literal (it might not be translated).
+   * Returns true iff the node has an assigned literal (it might not be
+   * translated).
    * @param node the node
    */
   bool hasLiteral(TNode node) const;
 
   /**
-   * Ensure that the given node will have a designated SAT literal
-   * that is definitionally equal to it.  The result of this function
-   * is that the Node can be queried via getSatValue().  Essentially,
-   * this is like a "convert-but-don't-assert" version of
-   * convertAndAssert().
+   * Ensure that the given node will have a designated SAT literal that is
+   * definitionally equal to it.  The result of this function is that the Node
+   * can be queried via getSatValue(). Essentially, this is like a "convert-but-
+   * don't-assert" version of convertAndAssert().
    */
   virtual void ensureLiteral(TNode n, bool noPreregistration = false) = 0;
 
@@ -250,13 +252,10 @@ public:
     return d_nodeToLiteralMap;
   }
 
-  const LiteralToNodeMap& getNodeCache() const {
-    return d_literalToNodeMap;
-  }
+  const LiteralToNodeMap& getNodeCache() const { return d_literalToNodeMap; }
 
   void setProof(CnfProof* proof);
-};/* class CnfStream */
-
+}; /* class CnfStream */
 
 /**
  * TseitinCnfStream is based on the following recursive algorithm
@@ -269,22 +268,13 @@ public:
  * This implementation does this in a single recursive pass. [??? -Chris]
  */
 class TseitinCnfStream : public CnfStream {
-
-public:
-
-  /**
-   * Convert a given formula to CNF and assert it to the SAT solver.
-   * @param node the formula to assert
-   * @param removable is this something that can be erased
-   * @param negated true if negated
-   */
-  void convertAndAssert(TNode node, bool removable,
-                        bool negated, ProofRule rule, TNode from = TNode::null());
-
+ public:
   /**
-   * Constructs the stream to use the given sat solver.
+   * Constructs the stream to use the given sat solver.  This does not take
+   * ownership of satSolver, registrar, or context.
    * @param satSolver the sat solver to use
    * @param registrar the entity that takes care of pre-registration of Nodes
+   * @param context the context that the CNF should respect.
    * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping,
    * even for non-theory literals
    */
@@ -292,8 +282,16 @@ public:
                    context::Context* context, bool fullLitToNodeMap = false,
                    std::string name = "");
 
-private:
+  /**
+   * Convert a given formula to CNF and assert it to the SAT solver.
+   * @param node the formula to assert
+   * @param removable is this something that can be erased
+   * @param negated true if negated
+   */
+  void convertAndAssert(TNode node, bool removable, bool negated,
+                        ProofRule rule, TNode from = TNode::null());
 
+ private:
   /**
    * Same as above, except that removable is remembered.
    */
@@ -334,10 +332,9 @@ private:
 
   void ensureLiteral(TNode n, bool noPreregistration = false);
 
-};/* class TseitinCnfStream */
-
+}; /* class TseitinCnfStream */
 
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
+} /* CVC4::prop namespace */
+} /* CVC4 namespace */
 
 #endif /* __CVC4__PROP__CNF_STREAM_H */

diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h
index 98417c492865654cc7bc5d903808cb50b4f5aae9..c93accd33b0317c6658450acb0018a67979a16b4 100644 (file)
--- a/test/unit/prop/cnf_stream_white.h
+++ b/test/unit/prop/cnf_stream_white.h
@@ -46,23 +46,16 @@ class FakeSatSolver : public SatSolver {
   SatVariable d_nextVar;
   bool d_addClauseCalled;
 
-public:
-  FakeSatSolver() :
-    d_nextVar(0),
-    d_addClauseCalled(false) {
-  }
+ public:
+  FakeSatSolver() : d_nextVar(0), d_addClauseCalled(false) {}
 
   SatVariable newVar(bool theoryAtom, bool preRegister, bool canErase) {
     return d_nextVar++;
   }
 
-  SatVariable trueVar() {
-    return d_nextVar++;
-  }
+  SatVariable trueVar() { return d_nextVar++; }
 
-  SatVariable falseVar() {
-    return d_nextVar++;
-  }
+  SatVariable falseVar() { return d_nextVar++; }
 
   ClauseId addClause(SatClause& c, bool lemma) {
     d_addClauseCalled = true;
@@ -76,59 +69,35 @@ public:
 
   bool nativeXor() { return false; }
 
-  
-  void reset() {
-    d_addClauseCalled = false;
-  }
+  void reset() { d_addClauseCalled = false; }
 
-  unsigned int addClauseCalled() {
-    return d_addClauseCalled;
-  }
+  unsigned int addClauseCalled() { return d_addClauseCalled; }
 
-  unsigned getAssertionLevel() const {
-    return 0;
-  }
+  unsigned getAssertionLevel() const { return 0; }
 
-  bool isDecision(Node) const {
-    return false;
-  }
+  bool isDecision(Node) const { return false; }
 
-  void unregisterVar(SatLiteral lit) {
-  }
+  void unregisterVar(SatLiteral lit) {}
 
-  void renewVar(SatLiteral lit, int level = -1) {
-  }
+  void renewVar(SatLiteral lit, int level = -1) {}
 
-  bool spendResource() {
-    return false;
-  }
+  bool spendResource() { return false; }
 
-  void interrupt() {
-  }
-  
-  SatValue solve() {
-    return SAT_VALUE_UNKNOWN;
-  }
+  void interrupt() {}
 
-  SatValue solve(long unsigned int& resource) {
-    return SAT_VALUE_UNKNOWN;
-  }
+  SatValue solve() { return SAT_VALUE_UNKNOWN; }
 
-  SatValue value(SatLiteral l) {
-    return SAT_VALUE_UNKNOWN;
-  }
+  SatValue solve(long unsigned int& resource) { return SAT_VALUE_UNKNOWN; }
 
-  SatValue modelValue(SatLiteral l) {
-    return SAT_VALUE_UNKNOWN;
-  }
+  SatValue value(SatLiteral l) { return SAT_VALUE_UNKNOWN; }
 
-  bool properExplanation(SatLiteral lit, SatLiteral expl) const {
-    return true;
-  }
+  SatValue modelValue(SatLiteral l) { return SAT_VALUE_UNKNOWN; }
+
+  bool properExplanation(SatLiteral lit, SatLiteral expl) const { return true; }
 
   bool ok() const { return true; }
 
-};/* class FakeSatSolver */
+}; /* class FakeSatSolver */
 
 class CnfStreamWhite : public CxxTest::TestSuite {
   /** The SAT solver proxy */
@@ -140,11 +109,11 @@ class CnfStreamWhite : public CxxTest::TestSuite {
   /** The CNF converter in use */
   CnfStream* d_cnfStream;
 
-  /** The context */
-  Context* d_context;
+  /** The context of the CnfStream. */
+  Context* d_cnfContext;
 
-  /** The user context */
-  UserContext* d_userContext;
+  /** The registrar used by the CnfStream. */
+  theory::TheoryRegistrar* d_cnfRegistrar;
 
   /** The node manager */
   NodeManager* d_nodeManager;
@@ -160,27 +129,26 @@ class CnfStreamWhite : public CxxTest::TestSuite {
     d_nodeManager = NodeManager::fromExprManager(d_exprManager);
     d_scope = new SmtScope(d_smt);
 
-    d_context = d_smt->d_context;
-    d_userContext = d_smt->d_userContext;
-
     d_theoryEngine = d_smt->d_theoryEngine;
 
     d_satSolver = new FakeSatSolver();
+    d_cnfContext = new context::Context();
+    d_cnfRegistrar = new theory::TheoryRegistrar(d_theoryEngine);
     d_cnfStream = new CVC4::prop::TseitinCnfStream(
-        d_satSolver, new theory::TheoryRegistrar(d_theoryEngine),
-        new context::Context(), d_smt->channels());
+        d_satSolver, d_cnfRegistrar, d_cnfContext, d_smt->channels());
   }
 
   void tearDown() {
     delete d_cnfStream;
+    delete d_cnfContext;
+    delete d_cnfRegistrar;
     delete d_satSolver;
     delete d_scope;
     delete d_smt;
     delete d_exprManager;
   }
 
-public:
-
+ public:
   /* [chris 5/26/2010] In the tests below, we don't attempt to delve into the
    * deep structure of the CNF conversion. Firstly, we just want to make sure
    * that the conversion doesn't choke on any boolean Exprs. We'll also check
@@ -193,8 +161,9 @@ public:
     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
     Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::AND, a, b, c), false, false, RULE_INVALID, Node::null());
-    TS_ASSERT( d_satSolver->addClauseCalled() );
+    d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::AND, a, b, c),
+                                  false, false, RULE_INVALID, Node::null());
+    TS_ASSERT(d_satSolver->addClauseCalled());
   }
 
   void testComplexExpr() {
@@ -205,45 +174,51 @@ public:
     Node d = d_nodeManager->mkVar(d_nodeManager->booleanType());
     Node e = d_nodeManager->mkVar(d_nodeManager->booleanType());
     Node f = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::IMPLIES,
-                                                        d_nodeManager->mkNode(kind::AND, a, b),
-                                                        d_nodeManager->mkNode(kind::IFF,
-                                                                              d_nodeManager->mkNode(kind::OR, c, d),
-                                                                              d_nodeManager->mkNode(kind::NOT,
-                                                                                                    d_nodeManager->mkNode(kind::XOR, e, f)))), false, false, RULE_INVALID, Node::null());
-    TS_ASSERT( d_satSolver->addClauseCalled() );
+    d_cnfStream->convertAndAssert(
+        d_nodeManager->mkNode(
+            kind::IMPLIES, d_nodeManager->mkNode(kind::AND, a, b),
+            d_nodeManager->mkNode(
+                kind::IFF, d_nodeManager->mkNode(kind::OR, c, d),
+                d_nodeManager->mkNode(kind::NOT,
+                                      d_nodeManager->mkNode(kind::XOR, e, f)))),
+        false, false, RULE_INVALID, Node::null());
+    TS_ASSERT(d_satSolver->addClauseCalled());
   }
 
   void testTrue() {
     NodeManagerScope nms(d_nodeManager);
-    d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false, false, RULE_INVALID, Node::null() );
-    TS_ASSERT( d_satSolver->addClauseCalled() );
+    d_cnfStream->convertAndAssert(d_nodeManager->mkConst(true), false, false,
+                                  RULE_INVALID, Node::null());
+    TS_ASSERT(d_satSolver->addClauseCalled());
   }
 
   void testFalse() {
     NodeManagerScope nms(d_nodeManager);
-    d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false, false, RULE_INVALID, Node::null() );
-    TS_ASSERT( d_satSolver->addClauseCalled() );
+    d_cnfStream->convertAndAssert(d_nodeManager->mkConst(false), false, false,
+                                  RULE_INVALID, Node::null());
+    TS_ASSERT(d_satSolver->addClauseCalled());
   }
 
   void testIff() {
     NodeManagerScope nms(d_nodeManager);
     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::IFF, a, b), false, false, RULE_INVALID, Node::null() );
-    TS_ASSERT( d_satSolver->addClauseCalled() );
+    d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::IFF, a, b), false,
+                                  false, RULE_INVALID, Node::null());
+    TS_ASSERT(d_satSolver->addClauseCalled());
   }
 
   void testImplies() {
     NodeManagerScope nms(d_nodeManager);
     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false, RULE_INVALID, Node::null() );
-    TS_ASSERT( d_satSolver->addClauseCalled() );
+    d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::IMPLIES, a, b),
+                                  false, false, RULE_INVALID, Node::null());
+    TS_ASSERT(d_satSolver->addClauseCalled());
   }
 
   // ITEs should be removed before going to CNF
-  //void testIte() {
+  // void testIte() {
   //  NodeManagerScope nms(d_nodeManager);
   //  d_cnfStream->convertAndAssert(
   //      d_nodeManager->mkNode(
@@ -262,8 +237,9 @@ public:
   void testNot() {
     NodeManagerScope nms(d_nodeManager);
     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::NOT, a), false, false, RULE_INVALID, Node::null() );
-    TS_ASSERT( d_satSolver->addClauseCalled() );
+    d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::NOT, a), false,
+                                  false, RULE_INVALID, Node::null());
+    TS_ASSERT(d_satSolver->addClauseCalled());
   }
 
   void testOr() {
@@ -271,8 +247,9 @@ public:
     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
     Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::OR, a, b, c), false, false, RULE_INVALID, Node::null() );
-    TS_ASSERT( d_satSolver->addClauseCalled() );
+    d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::OR, a, b, c),
+                                  false, false, RULE_INVALID, Node::null());
+    TS_ASSERT(d_satSolver->addClauseCalled());
   }
 
   void testVar() {
@@ -280,18 +257,19 @@ public:
     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
     d_cnfStream->convertAndAssert(a, false, false, RULE_INVALID, Node::null());
-    TS_ASSERT( d_satSolver->addClauseCalled() );
+    TS_ASSERT(d_satSolver->addClauseCalled());
     d_satSolver->reset();
     d_cnfStream->convertAndAssert(b, false, false, RULE_INVALID, Node::null());
-    TS_ASSERT( d_satSolver->addClauseCalled() );
+    TS_ASSERT(d_satSolver->addClauseCalled());
   }
 
   void testXor() {
     NodeManagerScope nms(d_nodeManager);
     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::XOR, a, b), false, false, RULE_INVALID, Node::null() );
-    TS_ASSERT( d_satSolver->addClauseCalled() );
+    d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::XOR, a, b), false,
+                                  false, RULE_INVALID, Node::null());
+    TS_ASSERT(d_satSolver->addClauseCalled());
   }
 
   void testEnsureLiteral() {
@@ -301,7 +279,7 @@ public:
     Node a_and_b = d_nodeManager->mkNode(kind::AND, a, b);
     d_cnfStream->ensureLiteral(a_and_b);
     // Clauses are necessary to "literal-ize" a_and_b
-    TS_ASSERT( d_satSolver->addClauseCalled() );
-    TS_ASSERT( d_cnfStream->hasLiteral(a_and_b) );
+    TS_ASSERT(d_satSolver->addClauseCalled());
+    TS_ASSERT(d_cnfStream->hasLiteral(a_and_b));
   }
 };