diff options
author | Tim King <taking@cs.nyu.edu> | 2012-12-05 21:45:12 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-12-05 21:45:12 +0000 |
commit | bd0a6c39c56c6ad2bf12e7b9fd41db1772fed9cd (patch) | |
tree | 51f4bc5994a0716e6f4cfeed136360954ce505ac /src/theory/arith/constraint.cpp | |
parent | 356a8b6e5ea2622d0fef5cf209159caf08ba5297 (diff) |
Improved garbage collection for TheoryArith. The merges all of the code over from branches/arithmetic/converge except for the new code for simplex.
Diffstat (limited to 'src/theory/arith/constraint.cpp')
-rw-r--r-- | src/theory/arith/constraint.cpp | 48 |
1 files changed, 46 insertions, 2 deletions
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index 392d04f6c..cf3aeafee 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -371,6 +371,10 @@ void ConstraintValue::setAssertedToTheTheory(TNode witness) { d_database->pushAssertionOrderWatch(this, witness); } +// bool ConstraintValue::isPsuedoConstraint() const { +// return d_proof == d_database->d_psuedoConstraintProof; +// } + bool ConstraintValue::isSelfExplaining() const { return d_proof == d_database->d_selfExplainingProof; } @@ -481,6 +485,9 @@ ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Co d_equalityEngineProof = d_proofs.size(); d_proofs.push_back(NullConstraint); + + // d_psuedoConstraintProof = d_proofs.size(); + // d_proofs.push_back(NullConstraint); } Constraint ConstraintDatabase::getConstraint(ArithVar v, ConstraintType t, const DeltaRational& r){ @@ -566,8 +573,32 @@ ConstraintDatabase::Statistics::~Statistics(){ } void ConstraintDatabase::addVariable(ArithVar v){ - Assert(v == d_varDatabases.size()); - d_varDatabases.push_back(new PerVariableDatabase(v)); + if(d_reclaimable.isMember(v)){ + SortedConstraintMap& scm = getVariableSCM(v); + + std::vector<Constraint> constraintList; + + for(SortedConstraintMapIterator i = scm.begin(), end = scm.end(); i != end; ++i){ + (i->second).push_into(constraintList); + } + while(!constraintList.empty()){ + Constraint c = constraintList.back(); + constraintList.pop_back(); + Assert(c->safeToGarbageCollect()); + delete c; + } + Assert(scm.empty()); + + d_reclaimable.remove(v); + }else{ + Assert(v == d_varDatabases.size()); + d_varDatabases.push_back(new PerVariableDatabase(v)); + } +} + +void ConstraintDatabase::removeVariable(ArithVar v){ + Assert(!d_reclaimable.isMember(v)); + d_reclaimable.add(v); } bool ConstraintValue::safeToGarbageCollect() const{ @@ -802,6 +833,13 @@ void ConstraintValue::impliedBy(const std::vector<Constraint>& b){ } } +// void ConstraintValue::setPsuedoConstraint(){ +// Assert(truthIsUnknown()); +// Assert(!hasLiteral()); + +// d_database->pushProofWatch(this, d_database->d_psuedoConstraintProof); +// } + void ConstraintValue::setEqualityEngineProof(){ Assert(truthIsUnknown()); Assert(hasLiteral()); @@ -818,6 +856,7 @@ void ConstraintValue::markAsTrue(){ void ConstraintValue::markAsTrue(Constraint imp){ Assert(truthIsUnknown()); Assert(imp->hasProof()); + //Assert(!imp->isPsuedoConstraint()); d_database->d_proofs.push_back(NullConstraint); d_database->d_proofs.push_back(imp); @@ -829,6 +868,8 @@ void ConstraintValue::markAsTrue(Constraint impA, Constraint impB){ Assert(truthIsUnknown()); Assert(impA->hasProof()); Assert(impB->hasProof()); + //Assert(!impA->isPsuedoConstraint()); + //Assert(!impB->isPsuedoConstraint()); d_database->d_proofs.push_back(NullConstraint); d_database->d_proofs.push_back(impA); @@ -845,6 +886,7 @@ void ConstraintValue::markAsTrue(const vector<Constraint>& a){ for(vector<Constraint>::const_iterator i = a.begin(), end = a.end(); i != end; ++i){ Constraint c_i = *i; Assert(c_i->hasProof()); + //Assert(!c_i->isPsuedoConstraint()); d_database->d_proofs.push_back(c_i); } @@ -861,6 +903,7 @@ SortedConstraintMap& ConstraintValue::constraintSet() const{ bool ConstraintValue::proofIsEmpty() const{ Assert(hasProof()); bool result = d_database->d_proofs[d_proof] == NullConstraint; + //Assert((!result) || isSelfExplaining() || hasEqualityEngineProof() || isPsuedoConstraint()); Assert((!result) || isSelfExplaining() || hasEqualityEngineProof()); return result; } @@ -869,6 +912,7 @@ void ConstraintValue::explainBefore(NodeBuilder<>& nb, AssertionOrder order) con Assert(hasProof()); Assert(!isSelfExplaining() || assertedToTheTheory()); + if(assertedBefore(order)){ nb << getWitness(); }else if(hasEqualityEngineProof()){ |