-/********************* */
-/*! \file soi_simplex.h
- ** \verbatim
- ** Original author: Tim King
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief This is an implementation of the Simplex Module for the Simplex for DPLL(T)
- ** decision procedure.
- **
- ** This implements the Simplex module for the Simpelx for DPLL(T) decision procedure.
- ** See the Simplex for DPLL(T) technical report for more background.(citation?)
- ** This shares with the theory a Tableau, and a PartialModel that:
- ** - satisfies the equalities in the Tableau, and
- ** - the assignment for the non-basic variables satisfies their bounds.
- ** This is required to either produce a conflict or satisifying PartialModel.
- ** Further, we require being told when a basic variable updates its value.
- **
- ** During the Simplex search we maintain a queue of variables.
- ** The queue is required to contain all of the basic variables that voilate their bounds.
- ** As elimination from the queue is more efficient to be done lazily,
- ** we do not maintain that the queue of variables needs to be only basic variables or only
- ** variables that satisfy their bounds.
- **
- ** The simplex procedure roughly follows Alberto's thesis. (citation?)
- ** There is one round of selecting using a heuristic pivoting rule. (See PreferenceFunction
- ** Documentation for the available options.)
- ** The non-basic variable is the one that appears in the fewest pivots. (Bruno says that
- ** Leonardo invented this first.)
- ** After this, Bland's pivot rule is invoked.
- **
- ** During this proccess, we periodically inspect the queue of variables to
- ** 1) remove now extraneous extries,
- ** 2) detect conflicts that are "waiting" on the queue but may not be detected by the
- ** current queue heuristics, and
- ** 3) detect multiple conflicts.
- **
- ** Conflicts are greedily slackened to use the weakest bounds that still produce the
- ** conflict.
- **
- ** Extra things tracked atm: (Subject to change at Tim's whims)
- ** - A superset of all of the newly pivoted variables.
- ** - A queue of additional conflicts that were discovered by Simplex.
- ** These are theory valid and are currently turned into lemmas
- **/
-
-#include "cvc4_private.h"
+/******************************************************************************
+ * Top contributors (to current version):
+ * Tim King, Morgan Deters, Mathias Preiner
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * This is an implementation of the Simplex Module for the Simplex for
+ * DPLL(T) decision procedure.
+ *
+ * This implements the Simplex module for the Simpelx for DPLL(T) decision
+ * procedure.
+ * See the Simplex for DPLL(T) technical report for more background.(citation?)
+ * This shares with the theory a Tableau, and a PartialModel that:
+ * - satisfies the equalities in the Tableau, and
+ * - the assignment for the non-basic variables satisfies their bounds.
+ * This is required to either produce a conflict or satisifying PartialModel.
+ * Further, we require being told when a basic variable updates its value.
+ *
+ * During the Simplex search we maintain a queue of variables.
+ * The queue is required to contain all of the basic variables that voilate
+ * their bounds.
+ * As elimination from the queue is more efficient to be done lazily,
+ * we do not maintain that the queue of variables needs to be only basic
+ * variables or only variables that satisfy their bounds.
+ *
+ * The simplex procedure roughly follows Alberto's thesis. (citation?)
+ * There is one round of selecting using a heuristic pivoting rule.
+ * (See PreferenceFunction Documentation for the available options.)
+ * The non-basic variable is the one that appears in the fewest pivots.
+ * (Bruno says that Leonardo invented this first.)
+ * After this, Bland's pivot rule is invoked.
+ *
+ * During this proccess, we periodically inspect the queue of variables to
+ * 1) remove now extraneous extries,
+ * 2) detect conflicts that are "waiting" on the queue but may not be detected
+ * by the current queue heuristics, and
+ * 3) detect multiple conflicts.
+ *
+ * Conflicts are greedily slackened to use the weakest bounds that still
+ * produce the conflict.
+ *
+ * Extra things tracked atm: (Subject to change at Tim's whims)
+ * - A superset of all of the newly pivoted variables.
+ * - A queue of additional conflicts that were discovered by Simplex.
+ * These are theory valid and are currently turned into lemmas
+ */
+
+#include "cvc5_private.h"
#pragma once
+#include "theory/arith/linear_equality.h"
#include "theory/arith/simplex.h"
+#include "theory/arith/simplex_update.h"
#include "util/dense_map.h"
-#include "util/statistics_registry.h"
-#include <stdint.h>
+#include "util/statistics_stats.h"
-namespace CVC4 {
+namespace cvc5 {
namespace theory {
namespace arith {
class SumOfInfeasibilitiesSPD : public SimplexDecisionProcedure {
public:
- SumOfInfeasibilitiesSPD(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc);
+ SumOfInfeasibilitiesSPD(Env& env,
+ 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);
- WitnessImprovement primalImproveError(ArithVar evar);
+ // other error variables are dropping
+ WitnessImprovement dualLikeImproveError(ArithVar evar);
+ WitnessImprovement primalImproveError(ArithVar evar);
private:
/** The current sum of infeasibilities variable. */
// - satisfied error set
Result::Sat sumOfInfeasibilities();
- // static const uint32_t PENALTY = 4;
- // DenseMultiset d_scores;
- // void decreasePenalties(){ d_scores.removeOneOfEverything(); }
- // uint32_t penalty(ArithVar x) const { return d_scores.count(x); }
- // void setPenalty(ArithVar x, WitnessImprovement w){
- // if(improvement(w)){
- // if(d_scores.count(x) > 0){
- // d_scores.removeAll(x);
- // }
- // }else{
- // d_scores.setCount(x, PENALTY);
- // }
- // }
-
int32_t d_pivotBudget;
- // enum PivotImprovement {
- // ErrorDropped,
- // NonDegenerate,
- // HeuristicDegenerate,
- // BlandsDegenerate
- // };
WitnessImprovement d_prevWitnessImprovement;
uint32_t d_witnessImprovementInARow;
uint32_t degeneratePivotsInARow() const;
- static const uint32_t s_focusThreshold = 6;
- static const uint32_t s_maxDegeneratePivotsBeforeBlandsOnLeaving = 100;
- static const uint32_t s_maxDegeneratePivotsBeforeBlandsOnEntering = 10;
+ static constexpr uint32_t s_focusThreshold = 6;
+ static constexpr uint32_t s_maxDegeneratePivotsBeforeBlandsOnLeaving = 100;
+ static constexpr uint32_t s_maxDegeneratePivotsBeforeBlandsOnEntering = 10;
DenseMap<uint32_t> d_leavingCountSinceImprovement;
void increaseLeavingCount(ArithVar x){
}
}
- bool debugSOI(WitnessImprovement w, std::ostream& out, int instance) const;
-
void debugPrintSignal(ArithVar updated) const;
ArithVarVec d_sgnDisagreements;
ReferenceStat<uint32_t> d_finalCheckPivotCounter;
- Statistics(uint32_t& pivots);
- ~Statistics();
+ Statistics(const std::string& name, uint32_t& pivots);
} d_statistics;
};/* class FCSimplexDecisionProcedure */
-}/* CVC4::theory::arith namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
+} // namespace arith
+} // namespace theory
+} // namespace cvc5
projects / cvc5.git / blobdiff