diff options
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/cut_log.h | 2 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 5 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 21 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.h | 4 |
4 files changed, 12 insertions, 20 deletions
diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h index 548035aec..e6475b58e 100644 --- a/src/theory/arith/cut_log.h +++ b/src/theory/arith/cut_log.h @@ -234,8 +234,6 @@ std::ostream& operator<<(std::ostream& os, const NodeLog& nl); class ApproximateSimplex; class TreeLog { private: - ApproximateSimplex* d_generator; - int next_exec_ord; typedef std::map<int, NodeLog> ToNodeMap; ToNodeMap d_toNode; diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 3e414ca6d..51bbd67f3 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -25,10 +25,6 @@ namespace CVC4 { namespace theory { -namespace quantifiers { - class InstStrategySimplex; -} - namespace arith { /** @@ -38,7 +34,6 @@ namespace arith { */ class TheoryArith : public Theory { private: - friend class quantifiers::InstStrategySimplex; friend class TheoryArithPrivate; TheoryArithPrivate* d_internal; diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index e47231128..069d3530c 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -2520,34 +2520,37 @@ struct SizeOrd { return a.size() < b.size(); } }; -void TheoryArithPrivate::subsumption(std::vector<ConstraintCPVec>& confs) const { + +void TheoryArithPrivate::subsumption( + std::vector<ConstraintCPVec> &confs) const { int checks CVC4_UNUSED = 0; int subsumed CVC4_UNUSED = 0; - for(size_t i =0, N= confs.size(); i < N; ++i){ - ConstraintCPVec& conf = confs[i]; + for (size_t i = 0, N = confs.size(); i < N; ++i) { + ConstraintCPVec &conf = confs[i]; std::sort(conf.begin(), conf.end()); } std::sort(confs.begin(), confs.end(), SizeOrd()); - for(size_t i = 0; i < confs.size(); i++){ - ConstraintCPVec& a = confs[i]; + for (size_t i = 0; i < confs.size(); i++) { // i is not subsumed - for(size_t j = i+1; j < confs.size();){ + for (size_t j = i + 1; j < confs.size();) { + ConstraintCPVec& a = confs[i]; ConstraintCPVec& b = confs[j]; checks++; bool subsumes = std::includes(a.begin(), a.end(), b.begin(), b.end()); - if(subsumes){ + if (subsumes) { ConstraintCPVec& back = confs.back(); b.swap(back); confs.pop_back(); subsumed++; - }else{ + } else { j++; } } } - Debug("arith::subsumption") << "subsumed " << subsumed << "/" << checks << endl; + Debug("arith::subsumption") << "subsumed " << subsumed << "/" << checks + << endl; } std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex* approx, int nid, ConstraintP bc, int depth){ diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index edc3a5bc0..ed7efe008 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -70,9 +70,6 @@ namespace CVC4 { namespace theory { -namespace quantifiers { - class InstStrategySimplex; -} namespace arith { class BranchCutInfo; @@ -93,7 +90,6 @@ class InferBoundsResult; */ class TheoryArithPrivate { private: - friend class quantifiers::InstStrategySimplex; static const uint32_t RESET_START = 2; |