From 6e61a7ad085774c222afa9ffcd2602b827883556 Mon Sep 17 00:00:00 2001 From: Tim King Date: Mon, 7 Nov 2016 11:10:17 -0800 Subject: [PATCH] Fixing a memory leak in the CnfStream unit tests. --- src/prop/cnf_stream.h | 111 +++++++++++---------- test/unit/prop/cnf_stream_white.h | 156 +++++++++++++----------------- 2 files changed, 121 insertions(+), 146 deletions(-) diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 661108dd0..a965018f8 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -46,19 +46,18 @@ class PropEngine; * @author Tim King */ class CnfStream { - -public: - + public: /** Cache of what nodes have been registered to a literal. */ - typedef context::CDInsertHashMap LiteralToNodeMap; + typedef context::CDInsertHashMap + LiteralToNodeMap; /** Cache of what literals have been registered to a node. */ - typedef context::CDInsertHashMap NodeToLiteralMap; - -protected: + typedef context::CDInsertHashMap + NodeToLiteralMap; + protected: /** The SAT solver we will be using */ - SatSolver *d_satSolver; + SatSolver* d_satSolver; /** Boolean variables that we translated */ context::CDList 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 98417c492..c93accd33 100644 --- 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)); } }; -- 2.30.2