diff options
-rw-r--r-- | proofs/lfsc_checker/check.cpp | 13 | ||||
-rw-r--r-- | proofs/lfsc_checker/code.cpp | 24 | ||||
-rw-r--r-- | proofs/lfsc_checker/expr.cpp | 4 | ||||
-rw-r--r-- | proofs/lfsc_checker/expr.h | 10 | ||||
-rw-r--r-- | src/proof/array_proof.h | 4 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 7 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 2 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 4 |
8 files changed, 57 insertions, 11 deletions
diff --git a/proofs/lfsc_checker/check.cpp b/proofs/lfsc_checker/check.cpp index 9c7a70fe7..cf68edb87 100644 --- a/proofs/lfsc_checker/check.cpp +++ b/proofs/lfsc_checker/check.cpp @@ -353,6 +353,9 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL, sym->dec(); // the pivar->val reference if (create) return new CExpr(LAM, sym, range); + if (range) { + range->dec(); + } sym->dec(); // the symbol table reference, otherwise in the new LAM return 0; } @@ -830,6 +833,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL, if (mpq_set_str(num,v.c_str(),10) == -1) report_error("Error reading a numeral."); i = new RatExpr(num); + mpq_clear(num); } else { @@ -837,6 +841,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL, if (mpz_init_set_str(num,v.c_str(),10) == -1) report_error("Error reading a numeral."); i = new IntExpr(num); + mpz_clear(num); } } @@ -1374,6 +1379,14 @@ void cleanup() { p->dec(); } } + + //std::cout << Expr::to_free.size() << std::endl; + expr_ptr_set_t::iterator it, it_end; + for (it = Expr::to_free.begin(), it_end = Expr::to_free.end(); it != it_end; it++) { + (*it)->debug(); + std::cout << (*it)->getrefcnt() << std::endl; + } + } void init() { diff --git a/proofs/lfsc_checker/code.cpp b/proofs/lfsc_checker/code.cpp index 48ebc5578..6f6223c8d 100644 --- a/proofs/lfsc_checker/code.cpp +++ b/proofs/lfsc_checker/code.cpp @@ -538,6 +538,7 @@ Expr *read_code() { report_error("Error reading a mpq numeral."); Expr* e = new RatExpr( num ); + mpq_clear(num); return e; } else @@ -545,7 +546,9 @@ Expr *read_code() { mpz_t num; if (mpz_init_set_str(num,v.c_str(),10) == -1) report_error("Error reading a numeral."); - return new IntExpr(num); + Expr* e = new IntExpr(num); + mpz_clear(num); + return e; } } default: @@ -973,7 +976,7 @@ Expr *check_code(Expr *_e) { if (!mtp) mtp = tp; - else + else { if (mtp != tp) report_error(string("Types for bodies of match cases or the default differ.") +string("\n1. type for first case's body: ") @@ -982,6 +985,7 @@ Expr *check_code(Expr *_e) { : (string("\n2. type for the body of case for ") +pat->toString())) +string(": ")+tp->toString()); + } } @@ -1084,7 +1088,9 @@ Expr *run_code(Expr *_e) { mpz_cdiv_q(r, ((IntExpr *)r1)->n, ((IntExpr *)r2)->n); r1->dec(); r2->dec(); - return new IntExpr(r); + Expr* result = new IntExpr(r); + mpz_clear(r); + return result; } else if( r1->getclass()==RAT_EXPR && r2->getclass()==RAT_EXPR ) { @@ -1098,7 +1104,9 @@ Expr *run_code(Expr *_e) { mpq_div(q, ((RatExpr *)r1)->n, ((RatExpr *)r2)->n); r1->dec(); r2->dec(); - return new RatExpr(q); + Expr* result = new RatExpr(q); + mpq_clear(q); + return result; } else { @@ -1117,14 +1125,18 @@ Expr *run_code(Expr *_e) { mpz_init(r); mpz_neg(r, ((IntExpr *)r1)->n); r1->dec(); - return new IntExpr(r); + Expr* result = new IntExpr(r); + mpz_clear(r); + return result; } else if( r1->getclass() == RAT_EXPR ) { mpq_t q; mpq_init(q); mpq_neg(q, ((RatExpr *)r1)->n); r1->dec(); - return new RatExpr(q); + Expr* result = new RatExpr(q); + mpq_clear(q); + return result; } else { diff --git a/proofs/lfsc_checker/expr.cpp b/proofs/lfsc_checker/expr.cpp index 8c8120edb..0ee164655 100644 --- a/proofs/lfsc_checker/expr.cpp +++ b/proofs/lfsc_checker/expr.cpp @@ -10,6 +10,7 @@ using namespace std; int HoleExpr::next_id = 0; int Expr::markedCount = 0; +expr_ptr_set_t Expr::to_free; C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_CC(CExpr,kids,32768); @@ -50,6 +51,9 @@ void Expr::destroy(Expr *_e, bool dec_kids) { case INT_EXPR: delete (IntExpr *)_e; break; + case RAT_EXPR: + delete (RatExpr *)_e; + break; case SYMS_EXPR: { SymSExpr *e = (SymSExpr *)_e; if (e->val && e->val->getop() != PROG) { diff --git a/proofs/lfsc_checker/expr.h b/proofs/lfsc_checker/expr.h index 3473a9eae..f5cf3d02a 100644 --- a/proofs/lfsc_checker/expr.h +++ b/proofs/lfsc_checker/expr.h @@ -103,12 +103,15 @@ protected: Expr(int _class, int _op) : data(1 << 9 /* refcount 1, not cloned */| (_op << 3) | _class) - { } + { /*Expr::to_free.insert(this);*/ } bool _free_in(Expr *x, expr_ptr_set_t *visited); public: - virtual ~Expr() {} + static expr_ptr_set_t to_free; + virtual ~Expr() { + Expr::to_free.erase(this); + } static int markedCount; inline Expr* followDefs(); @@ -143,8 +146,9 @@ protected: debugrefcnt(ref,DEC); #endif assert(ref >= 0); - if (ref == 0) + if (ref == 0) { destroy(this,dec_kids); + } else data = (ref << 9) | (data & 511); } diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h index 2fa659b51..521e19e88 100644 --- a/src/proof/array_proof.h +++ b/src/proof/array_proof.h @@ -71,6 +71,10 @@ private: ArrayProofPrinter d_proofPrinter; public: ProofArray(theory::eq::EqProof* pf) : d_reasonRow(0), d_reasonRow1(0), d_reasonExt(0), d_proofPrinter(), d_proof(pf) {} + ~ProofArray() { + delete d_proof; + } + //it is simply an equality engine proof theory::eq::EqProof *d_proof; void toStream(std::ostream& out); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d74adbbe3..12e31ec1c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1163,6 +1163,13 @@ SmtEngine::~SmtEngine() throw() { try { shutdown(); + PROOF( + std::vector<Command*>::const_iterator itg = d_defineCommands.begin(); + for (; itg != d_defineCommands.end(); ++itg) { + delete (*itg); + } + ); + // global push/pop around everything, to ensure proper destruction // of context-dependent data structures d_context->popto(0); diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 2c7418a77..d8835277b 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -2254,6 +2254,8 @@ void TheoryArrays::conflict(TNode a, TNode b) { } d_out->conflict(d_conflictNode, proof_array); + } else { + delete proof; } d_conflict = true; diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 7a6e0bdfc..943ffafe7 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -996,8 +996,8 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec eqp->d_id = MERGED_THROUGH_CONSTANTS; } else if (eqp->num_children() == 1) { // The transitivity proof has just one child. Simplify. - EqProof* temp = eqp->get_child(0); - eqp->remove_all_children(); + EqProof* temp = eqp->take_child(0); + eqp->discard_children(); *eqp = *temp; delete temp; } |