diff options
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/attempt_solution_simplex.h | 6 | ||||
-rw-r--r-- | src/theory/arith/callbacks.h | 10 | ||||
-rw-r--r-- | src/theory/arith/congruence_manager.h | 19 | ||||
-rw-r--r-- | src/theory/arith/dual_simplex.h | 3 | ||||
-rw-r--r-- | src/theory/arith/fc_simplex.h | 2 | ||||
-rw-r--r-- | src/theory/arith/linear_equality.h | 12 | ||||
-rw-r--r-- | src/theory/arith/matrix.h | 6 | ||||
-rw-r--r-- | src/theory/arith/soi_simplex.h | 2 |
8 files changed, 33 insertions, 27 deletions
diff --git a/src/theory/arith/attempt_solution_simplex.h b/src/theory/arith/attempt_solution_simplex.h index 73798f94c..fa65214e7 100644 --- a/src/theory/arith/attempt_solution_simplex.h +++ b/src/theory/arith/attempt_solution_simplex.h @@ -67,11 +67,9 @@ public: Result::Sat attempt(const ApproximateSimplex::Solution& sol); - Result::Sat findModel(bool exactResult){ - Unreachable(); - } + Result::Sat findModel(bool exactResult) override { Unreachable(); } -private: + private: bool matchesNewValue(const DenseMap<DeltaRational>& nv, ArithVar v) const; bool processSignals(){ diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h index 3710ac5c0..f84550dcc 100644 --- a/src/theory/arith/callbacks.h +++ b/src/theory/arith/callbacks.h @@ -73,7 +73,7 @@ private: TheoryArithPrivate& d_arith; public: SetupLiteralCallBack(TheoryArithPrivate& ta); - void operator()(TNode lit); + void operator()(TNode lit) override; }; class DeltaComputeCallback : public RationalCallBack { @@ -81,7 +81,7 @@ private: const TheoryArithPrivate& d_ta; public: DeltaComputeCallback(const TheoryArithPrivate& ta); - Rational operator()() const; + Rational operator()() const override; }; class BasicVarModelUpdateCallBack : public ArithVarCallBack{ @@ -89,7 +89,7 @@ private: TheoryArithPrivate& d_ta; public: BasicVarModelUpdateCallBack(TheoryArithPrivate& ta); - void operator()(ArithVar x); + void operator()(ArithVar x) override; }; class TempVarMalloc : public ArithVarMalloc { @@ -97,8 +97,8 @@ private: TheoryArithPrivate& d_ta; public: TempVarMalloc(TheoryArithPrivate& ta); - ArithVar request(); - void release(ArithVar v); + ArithVar request() override; + void release(ArithVar v) override; }; class RaiseConflict { diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 228f29838..5085dc841 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -61,17 +61,20 @@ private: public: ArithCongruenceNotify(ArithCongruenceManager& acm); - bool eqNotifyTriggerEquality(TNode equality, bool value); + bool eqNotifyTriggerEquality(TNode equality, bool value) override; - bool eqNotifyTriggerPredicate(TNode predicate, bool value); + bool eqNotifyTriggerPredicate(TNode predicate, bool value) override; - bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value); + bool eqNotifyTriggerTermEquality(TheoryId tag, + TNode t1, + TNode t2, + bool value) override; - void eqNotifyConstantTermMerge(TNode t1, TNode t2); - void eqNotifyNewClass(TNode t); - void eqNotifyPreMerge(TNode t1, TNode t2); - void eqNotifyPostMerge(TNode t1, TNode t2); - void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); + void eqNotifyConstantTermMerge(TNode t1, TNode t2) override; + void eqNotifyNewClass(TNode t) override; + void eqNotifyPreMerge(TNode t1, TNode t2) override; + void eqNotifyPostMerge(TNode t1, TNode t2) override; + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override; }; ArithCongruenceNotify d_notify; diff --git a/src/theory/arith/dual_simplex.h b/src/theory/arith/dual_simplex.h index 2911592c7..10d18170e 100644 --- a/src/theory/arith/dual_simplex.h +++ b/src/theory/arith/dual_simplex.h @@ -63,7 +63,8 @@ class DualSimplexDecisionProcedure : public SimplexDecisionProcedure{ public: DualSimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc); - Result::Sat findModel(bool exactResult) { + Result::Sat findModel(bool exactResult) override + { return dualFindModel(exactResult); } diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h index c4f996f9f..a93fa88e8 100644 --- a/src/theory/arith/fc_simplex.h +++ b/src/theory/arith/fc_simplex.h @@ -66,7 +66,7 @@ class FCSimplexDecisionProcedure : public SimplexDecisionProcedure{ public: FCSimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc); - Result::Sat findModel(bool exactResult); + Result::Sat findModel(bool exactResult) override; // other error variables are dropping WitnessImprovement dualLikeImproveError(ArithVar evar); diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h index c2fa99e31..0f2862a72 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear_equality.h @@ -588,13 +588,16 @@ private: LinearEqualityModule* d_linEq; public: TrackingCallback(LinearEqualityModule* le) : d_linEq(le) {} - void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn){ + void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn) override + { d_linEq->trackingCoefficientChange(ridx, nb, oldSgn, currSgn); } - void multiplyRow(RowIndex ridx, int sgn){ + void multiplyRow(RowIndex ridx, int sgn) override + { d_linEq->trackingMultiplyRow(ridx, sgn); } - bool canUseRow(RowIndex ridx) const { + bool canUseRow(RowIndex ridx) const override + { ArithVar basic = d_linEq->getTableau().rowIndexToBasic(ridx); return d_linEq->basicIsTracked(basic); } @@ -746,7 +749,8 @@ private: LinearEqualityModule* d_mod; public: UpdateTrackingCallback(LinearEqualityModule* mod): d_mod(mod){} - void operator()(ArithVar v, const BoundsInfo& bi){ + void operator()(ArithVar v, const BoundsInfo& bi) override + { d_mod->includeBoundUpdate(v, bi); } }; diff --git a/src/theory/arith/matrix.h b/src/theory/arith/matrix.h index 2e0a1ebb2..eda5b9dac 100644 --- a/src/theory/arith/matrix.h +++ b/src/theory/arith/matrix.h @@ -48,9 +48,9 @@ public: class NoEffectCCCB : public CoefficientChangeCallback { public: - void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn); - void multiplyRow(RowIndex ridx, int Sgn); - bool canUseRow(RowIndex ridx) const; + void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn) override; + void multiplyRow(RowIndex ridx, int Sgn) override; + bool canUseRow(RowIndex ridx) const override; }; template<class T> diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h index 5f2233b3f..54a47ac4d 100644 --- a/src/theory/arith/soi_simplex.h +++ b/src/theory/arith/soi_simplex.h @@ -66,7 +66,7 @@ class SumOfInfeasibilitiesSPD : public SimplexDecisionProcedure { public: SumOfInfeasibilitiesSPD(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc); - Result::Sat findModel(bool exactResult); + Result::Sat findModel(bool exactResult) override; // other error variables are dropping WitnessImprovement dualLikeImproveError(ArithVar evar); |