soi_simplex.cpp \
approx_simplex.h \
approx_simplex.cpp \
+ attempt_solution_simplex.h \
+ attempt_solution_simplex.cpp \
theory_arith.h \
theory_arith.cpp \
theory_arith_private_forward.h \
bool d_solvedRelaxation;
bool d_solvedMIP;
+ static int s_verbosity;
+
public:
ApproxGLPK(const ArithVariables& vars);
~ApproxGLPK();
Solution extractSolution(bool mip) const;
};
+#warning "set back to 0"
+int ApproxGLPK::s_verbosity = 1;
+
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
for(ArithVariables::var_iterator vi = d_vars.var_begin(), vi_end = d_vars.var_end(); vi != vi_end; ++vi){
ArithVar v = *vi;
- //cout << v << " ";
- //d_vars.printModel(v, cout);
+ if(s_verbosity >= 2){
+ Message() << v << " ";
+ d_vars.printModel(v, Message());
+ }
int type;
double lb = 0.0;
int glpk_index = isSlack ? d_rowIndices[vi] : d_colIndices[vi];
int status = isSlack ? glp_get_row_stat(d_prob, glpk_index) : glp_get_col_stat(d_prob, glpk_index);
- //cout << "assignment " << vi << endl;
+ if(s_verbosity >= 2){
+ Message() << "assignment " << vi << endl;
+ }
+
+ bool useDefaultAssignment = false;
switch(status){
case GLP_BS:
//cout << "basic" << endl;
newBasis.add(vi);
+ useDefaultAssignment = true;
break;
case GLP_NL:
case GLP_NS:
if(!mip){
- //cout << "non-basic lb" << endl;
+ if(s_verbosity >= 2){ Message() << "non-basic lb" << endl; }
newValues.set(vi, d_vars.getLowerBound(vi));
- break;
- }// intentionally fall through otherwise
+ }else{// intentionally fall through otherwise
+ useDefaultAssignment = true;
+ }
+ break;
case GLP_NU:
if(!mip){
- // cout << "non-basic ub" << endl;
+ if(s_verbosity >= 2){ Message() << "non-basic ub" << endl; }
newValues.set(vi, d_vars.getUpperBound(vi));
- break;
- }// intentionally fall through otherwise
+ }else {// intentionally fall through otherwise
+ useDefaultAssignment = true;
+ }
+ break;
default:
{
- // cout << "non-basic other" << endl;
+ useDefaultAssignment = true;
+ }
+ break;
+ }
+
+ if(useDefaultAssignment){
+ if(s_verbosity >= 2){ Message() << "non-basic other" << endl; }
- double newAssign =
- mip ?
- (isSlack ? glp_mip_row_val(d_prob, glpk_index) : glp_mip_col_val(d_prob, glpk_index))
- : (isSlack ? glp_get_row_prim(d_prob, glpk_index) : glp_get_col_prim(d_prob, glpk_index));
- const DeltaRational& oldAssign = d_vars.getAssignment(vi);
+ double newAssign =
+ mip ?
+ (isSlack ? glp_mip_row_val(d_prob, glpk_index) : glp_mip_col_val(d_prob, glpk_index))
+ : (isSlack ? glp_get_row_prim(d_prob, glpk_index) : glp_get_col_prim(d_prob, glpk_index));
+ const DeltaRational& oldAssign = d_vars.getAssignment(vi);
- if(d_vars.hasLowerBound(vi) &&
- roughlyEqual(newAssign, d_vars.getLowerBound(vi).approx(SMALL_FIXED_DELTA))){
- //cout << " to lb" << endl;
+ if(d_vars.hasLowerBound(vi) &&
+ roughlyEqual(newAssign, d_vars.getLowerBound(vi).approx(SMALL_FIXED_DELTA))){
+ //cout << " to lb" << endl;
- newValues.set(vi, d_vars.getLowerBound(vi));
- }else if(d_vars.hasUpperBound(vi) &&
- roughlyEqual(newAssign, d_vars.getUpperBound(vi).approx(SMALL_FIXED_DELTA))){
- newValues.set(vi, d_vars.getUpperBound(vi));
- // cout << " to ub" << endl;
+ newValues.set(vi, d_vars.getLowerBound(vi));
+ }else if(d_vars.hasUpperBound(vi) &&
+ roughlyEqual(newAssign, d_vars.getUpperBound(vi).approx(SMALL_FIXED_DELTA))){
+ newValues.set(vi, d_vars.getUpperBound(vi));
+ // cout << " to ub" << endl;
+ }else{
+
+ double rounded = round(newAssign);
+ if(roughlyEqual(newAssign, rounded)){
+ // cout << "roughly equal " << rounded << " " << newAssign << " " << oldAssign << endl;
+ newAssign = rounded;
}else{
+ // cout << "not roughly equal " << rounded << " " << newAssign << " " << oldAssign << endl;
+ }
+
+ DeltaRational proposal = estimateWithCFE(newAssign);
+
- double rounded = round(newAssign);
- if(roughlyEqual(newAssign, rounded)){
- // cout << "roughly equal " << rounded << " " << newAssign << " " << oldAssign << endl;
- newAssign = rounded;
- }else{
- // cout << "not roughly equal " << rounded << " " << newAssign << " " << oldAssign << endl;
- }
-
- DeltaRational proposal = estimateWithCFE(newAssign);
-
-
- if(roughlyEqual(newAssign, oldAssign.approx(SMALL_FIXED_DELTA))){
- // cout << " to prev value" << newAssign << " " << oldAssign << endl;
- proposal = d_vars.getAssignment(vi);
- }
-
-
- if(d_vars.strictlyLessThanLowerBound(vi, proposal)){
- //cout << " round to lb " << d_vars.getLowerBound(vi) << endl;
- proposal = d_vars.getLowerBound(vi);
- }else if(d_vars.strictlyGreaterThanUpperBound(vi, proposal)){
- //cout << " round to ub " << d_vars.getUpperBound(vi) << endl;
- proposal = d_vars.getUpperBound(vi);
- }else{
- //cout << " use proposal" << proposal << " " << oldAssign << endl;
- }
- newValues.set(vi, proposal);
+ if(roughlyEqual(newAssign, oldAssign.approx(SMALL_FIXED_DELTA))){
+ // cout << " to prev value" << newAssign << " " << oldAssign << endl;
+ proposal = d_vars.getAssignment(vi);
}
- break;
+
+
+ if(d_vars.strictlyLessThanLowerBound(vi, proposal)){
+ //cout << " round to lb " << d_vars.getLowerBound(vi) << endl;
+ proposal = d_vars.getLowerBound(vi);
+ }else if(d_vars.strictlyGreaterThanUpperBound(vi, proposal)){
+ //cout << " round to ub " << d_vars.getUpperBound(vi) << endl;
+ proposal = d_vars.getUpperBound(vi);
+ }else{
+ //cout << " use proposal" << proposal << " " << oldAssign << endl;
+ }
+ newValues.set(vi, proposal);
}
}
}
parm.meth = GLP_PRIMAL;
parm.pricing = GLP_PT_PSE;
parm.it_lim = d_pivotLimit;
- //parm.msg_lev = GLP_MSG_ALL;
parm.msg_lev = GLP_MSG_OFF;
+ if(s_verbosity >= 1){
+ parm.msg_lev = GLP_MSG_ALL;
+ }
int res = glp_simplex(d_prob, &parm);
switch(res){
parm.cov_cuts = GLP_ON;
parm.cb_func = stopAtBingoOrPivotLimit;
parm.cb_info = &d_pivotLimit;
- //parm.msg_lev = GLP_MSG_ALL;
parm.msg_lev = GLP_MSG_OFF;
+ if(s_verbosity >= 1){
+ parm.msg_lev = GLP_MSG_ALL;
+ }
int res = glp_intopt(d_prob, &parm);
switch(res){
virtual ApproxResult solveMIP() = 0;
virtual Solution extractMIP() const = 0;
- static void applySolution(LinearEqualityModule& linEq, const Solution& sol){
- linEq.forceNewBasis(sol.newBasis);
- linEq.updateMany(sol.newValues);
- }
-
/** UTILIES FOR DEALING WITH ESTIMATES */
static const double SMALL_FIXED_DELTA;
--- /dev/null
+
+#include "theory/arith/attempt_solution_simplex.h"
+#include "theory/arith/options.h"
+#include "theory/arith/constraint.h"
+
+using namespace std;
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+AttemptSolutionSDP::AttemptSolutionSDP(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc)
+ : SimplexDecisionProcedure(linEq, errors, conflictChannel, tvmalloc)
+ , d_statistics()
+{ }
+
+AttemptSolutionSDP::Statistics::Statistics():
+ d_searchTime("theory::arith::attempt::searchTime"),
+ d_queueTime("theory::arith::attempt::queueTime"),
+ d_conflicts("theory::arith::attempt::conflicts", 0)
+{
+ StatisticsRegistry::registerStat(&d_searchTime);
+ StatisticsRegistry::registerStat(&d_queueTime);
+ StatisticsRegistry::registerStat(&d_conflicts);
+}
+
+AttemptSolutionSDP::Statistics::~Statistics(){
+ StatisticsRegistry::unregisterStat(&d_searchTime);
+ StatisticsRegistry::unregisterStat(&d_queueTime);
+ StatisticsRegistry::unregisterStat(&d_conflicts);
+}
+
+bool AttemptSolutionSDP::matchesNewValue(const DenseMap<DeltaRational>& nv, ArithVar v) const{
+ return nv[v] == d_variables.getAssignment(v);
+}
+
+Result::Sat AttemptSolutionSDP::attempt(const ApproximateSimplex::Solution& sol){
+ const DenseSet& newBasis = sol.newBasis;
+ const DenseMap<DeltaRational>& newValues = sol.newValues;
+
+ DenseSet needsToBeAdded;
+ for(DenseSet::const_iterator i = newBasis.begin(), i_end = newBasis.end(); i != i_end; ++i){
+ ArithVar b = *i;
+ if(!d_tableau.isBasic(b)){
+ needsToBeAdded.add(b);
+ }
+ }
+ DenseMap<DeltaRational>::const_iterator nvi = newValues.begin(), nvi_end = newValues.end();
+ for(; nvi != nvi_end; ++nvi){
+ ArithVar currentlyNb = *nvi;
+ if(!d_tableau.isBasic(currentlyNb)){
+ if(!matchesNewValue(newValues, currentlyNb)){
+ const DeltaRational& newValue = newValues[currentlyNb];
+ Trace("arith::updateMany")
+ << "updateMany:" << currentlyNb << " "
+ << d_variables.getAssignment(currentlyNb) << " to "<< newValue << endl;
+ d_linEq.update(currentlyNb, newValue);
+ Assert(d_variables.assignmentIsConsistent(currentlyNb));
+ }
+ }
+ }
+ d_errorSet.reduceToSignals();
+ d_errorSet.setSelectionRule(VAR_ORDER);
+
+ static int instance = 0;
+ ++instance;
+
+ if(processSignals()){
+ Debug("arith::findModel") << "attemptSolution("<< instance <<") early conflict" << endl;
+ return Result::UNSAT;
+ }else if(d_errorSet.errorEmpty()){
+ Debug("arith::findModel") << "attemptSolution("<< instance <<") fixed itself" << endl;
+ return Result::SAT;
+ }
+
+ while(!needsToBeAdded.empty() && !d_errorSet.errorEmpty()){
+ ArithVar toRemove = ARITHVAR_SENTINEL;
+ ArithVar toAdd = ARITHVAR_SENTINEL;
+ DenseSet::const_iterator i = needsToBeAdded.begin(), i_end = needsToBeAdded.end();
+ for(; toAdd == ARITHVAR_SENTINEL && i != i_end; ++i){
+ ArithVar v = *i;
+
+ Tableau::ColIterator colIter = d_tableau.colIterator(v);
+ for(; !colIter.atEnd(); ++colIter){
+ const Tableau::Entry& entry = *colIter;
+ Assert(entry.getColVar() == v);
+ ArithVar b = d_tableau.rowIndexToBasic(entry.getRowIndex());
+ if(!newBasis.isMember(b)){
+ toAdd = v;
+
+ bool favorBOverToRemove =
+ (toRemove == ARITHVAR_SENTINEL) ||
+ (matchesNewValue(newValues, toRemove) && !matchesNewValue(newValues, b)) ||
+ (d_tableau.basicRowLength(toRemove) > d_tableau.basicRowLength(b));
+
+ if(favorBOverToRemove){
+ toRemove = b;
+ }
+ }
+ }
+ }
+ Assert(toRemove != ARITHVAR_SENTINEL);
+ Assert(toAdd != ARITHVAR_SENTINEL);
+
+ Trace("arith::forceNewBasis") << toRemove << " " << toAdd << endl;
+ Message() << toRemove << " " << toAdd << endl;
+
+ d_linEq.pivotAndUpdate(toRemove, toAdd, newValues[toRemove]);
+
+ Trace("arith::forceNewBasis") << needsToBeAdded.size() << "to go" << endl;
+ Message() << needsToBeAdded.size() << "to go" << endl;
+ needsToBeAdded.remove(toAdd);
+
+ bool conflict = processSignals();
+ if(conflict){
+ d_errorSet.reduceToSignals();
+ return Result::UNSAT;
+ }
+ }
+
+ if(d_errorSet.errorEmpty()){
+ return Result::SAT;
+ }else{
+ d_errorSet.reduceToSignals();
+ return Result::SAT_UNKNOWN;
+ }
+}
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file simplex.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): kshitij, mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 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"
+
+#pragma once
+
+#include "util/statistics_registry.h"
+#include "theory/arith/simplex.h"
+#include "theory/arith/approx_simplex.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+class AttemptSolutionSDP : public SimplexDecisionProcedure {
+public:
+ AttemptSolutionSDP(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc);
+
+ Result::Sat attempt(const ApproximateSimplex::Solution& sol);
+
+ Result::Sat findModel(bool exactResult){
+ Unreachable();
+ }
+
+private:
+ bool matchesNewValue(const DenseMap<DeltaRational>& nv, ArithVar v) const;
+
+ bool processSignals(){
+ TimerStat &timer = d_statistics.d_queueTime;
+ IntStat& conflictStat = d_statistics.d_conflicts;
+ return standardProcessSignals(timer, conflictStat);
+ }
+ /** These fields are designed to be accessible to TheoryArith methods. */
+ class Statistics {
+ public:
+ TimerStat d_searchTime;
+ TimerStat d_queueTime;
+ IntStat d_conflicts;
+
+ Statistics();
+ ~Statistics();
+ } d_statistics;
+};/* class AttemptSolutionSDP */
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
d_weakeningAttempts("theory::arith::weakening::attempts",0),
d_weakeningSuccesses("theory::arith::weakening::success",0),
d_weakenings("theory::arith::weakening::total",0),
- d_weakenTime("theory::arith::weakening::time")
+ d_weakenTime("theory::arith::weakening::time"),
+ d_forceTime("theory::arith::forcing::time")
{
StatisticsRegistry::registerStat(&d_statPivots);
StatisticsRegistry::registerStat(&d_statUpdates);
StatisticsRegistry::registerStat(&d_weakeningSuccesses);
StatisticsRegistry::registerStat(&d_weakenings);
StatisticsRegistry::registerStat(&d_weakenTime);
+ StatisticsRegistry::registerStat(&d_forceTime);
}
LinearEqualityModule::Statistics::~Statistics(){
StatisticsRegistry::unregisterStat(&d_weakeningSuccesses);
StatisticsRegistry::unregisterStat(&d_weakenings);
StatisticsRegistry::unregisterStat(&d_weakenTime);
+ StatisticsRegistry::unregisterStat(&d_forceTime);
}
+
void LinearEqualityModule::includeBoundUpdate(ArithVar v, const BoundsInfo& prev){
Assert(!d_areTracking);
void LinearEqualityModule::updateMany(const DenseMap<DeltaRational>& many){
for(DenseMap<DeltaRational>::const_iterator i = many.begin(), i_end = many.end(); i != i_end; ++i){
ArithVar nb = *i;
- Assert(!d_tableau.isBasic(nb));
- const DeltaRational& newValue = many[nb];
- if(newValue != d_variables.getAssignment(nb)){
- Trace("arith::updateMany")
- << "updateMany:" << nb << " "
- << d_variables.getAssignment(nb) << " to "<< newValue << endl;
- update(nb, newValue);
+ if(!d_tableau.isBasic(nb)){
+ Assert(!d_tableau.isBasic(nb));
+ const DeltaRational& newValue = many[nb];
+ if(newValue != d_variables.getAssignment(nb)){
+ Trace("arith::updateMany")
+ << "updateMany:" << nb << " "
+ << d_variables.getAssignment(nb) << " to "<< newValue << endl;
+ update(nb, newValue);
+ }
}
}
}
+
+
+void LinearEqualityModule::applySolution(const DenseSet& newBasis, const DenseMap<DeltaRational>& newValues){
+ forceNewBasis(newBasis);
+ updateMany(newValues);
+}
+
void LinearEqualityModule::forceNewBasis(const DenseSet& newBasis){
+ TimerStat::CodeTimer codeTimer(d_statistics.d_forceTime);
+ cout << "force begin" << endl;
DenseSet needsToBeAdded;
for(DenseSet::const_iterator i = newBasis.begin(), i_end = newBasis.end(); i != i_end; ++i){
ArithVar b = *i;
Assert(toAdd != ARITHVAR_SENTINEL);
Trace("arith::forceNewBasis") << toRemove << " " << toAdd << endl;
+ Message() << toRemove << " " << toAdd << endl;
d_tableau.pivot(toRemove, toAdd, d_trackCallback);
d_basicVariableUpdates(toAdd);
Trace("arith::forceNewBasis") << needsToBeAdded.size() << "to go" << endl;
+ Message() << needsToBeAdded.size() << "to go" << endl;
needsToBeAdded.remove(toAdd);
}
}
/** Specialization of update if the module is not tracking yet (for Simplex). */
void updateTracked(ArithVar x_i, const DeltaRational& v);
- /**
- * Updates every non-basic to reflect the assignment in many.
- * For use with ApproximateSimplex.
- */
- void updateMany(const DenseMap<DeltaRational>& many);
/**
* Updates the value of a basic variable x_i to v,
ArithVariables& getVariables() const{ return d_variables; }
Tableau& getTableau() const{ return d_tableau; }
+ /**
+ * Updates every non-basic to reflect the assignment in many.
+ * For use with ApproximateSimplex.
+ */
+ void updateMany(const DenseMap<DeltaRational>& many);
void forceNewBasis(const DenseSet& newBasis);
+ void applySolution(const DenseSet& newBasis, const DenseMap<DeltaRational>& newValues);
+
/**
* Returns a pointer to the first Tableau entry on the row ridx that does not
IntStat d_weakeningAttempts, d_weakeningSuccesses, d_weakenings;
TimerStat d_weakenTime;
+ TimerStat d_forceTime;
Statistics();
~Statistics();
d_dualSimplex(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
d_fcSimplex(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
d_soiSimplex(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
+ d_attemptSolSimplex(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
d_DELTA_ZERO(0),
d_fullCheckCounter(0),
d_cutCount(c, 0),
approxSolver->setPivotLimit(mipLimit);
mipRes = approxSolver->solveMIP();
d_errorSet.reduceToSignals();
+ Message() << "here" << endl;
if(mipRes == ApproximateSimplex::ApproxSat){
mipSolution = approxSolver->extractMIP();
- ApproximateSimplex::applySolution(d_linEq, mipSolution);
+ d_qflraStatus = d_attemptSolSimplex.attempt(mipSolution);
+ //d_linEq.applySolution(mipSolution.newBasis, mipSolution.newValues);
}else{
- ApproximateSimplex::applySolution(d_linEq, relaxSolution);
+ d_qflraStatus = d_attemptSolSimplex.attempt(relaxSolution);
+ //d_linEq.applySolution(relaxSolution.newBasis, relaxSolution.newValues);
// if(d_qflraStatus != UNSAT){
// d_likelyIntegerUnsat = true;
// }
}
options::arithStandardCheckVarOrderPivots.set(pass2Limit);
- d_qflraStatus = simplex.findModel(false);
+ if(d_qflraStatus != Result::UNSAT){ d_qflraStatus = simplex.findModel(false); }
}
break;
case ApproximateSimplex::ApproxUnsat:
{
ApproximateSimplex::Solution sol = approxSolver->extractRelaxation();
- d_errorSet.reduceToSignals();
- ApproximateSimplex::applySolution(d_linEq, sol);
- options::arithStandardCheckVarOrderPivots.set(100);
- d_qflraStatus = simplex.findModel(false);
+ d_qflraStatus = d_attemptSolSimplex.attempt(sol);
+ options::arithStandardCheckVarOrderPivots.set(pass2Limit);
+
+ if(d_qflraStatus != Result::UNSAT){ d_qflraStatus = simplex.findModel(false); }
}
break;
default:
}
if(d_qflraStatus == Result::SAT_UNKNOWN){
+ Message() << "got sat unknown" << endl;
vector<ArithVar> toCut = cutAllBounded();
if(toCut.size() > 0){
branchVector(toCut);
#include "theory/arith/dual_simplex.h"
#include "theory/arith/fc_simplex.h"
#include "theory/arith/soi_simplex.h"
+#include "theory/arith/attempt_solution_simplex.h"
#include "theory/arith/constraint.h"
DualSimplexDecisionProcedure d_dualSimplex;
FCSimplexDecisionProcedure d_fcSimplex;
SumOfInfeasibilitiesSPD d_soiSimplex;
+ AttemptSolutionSDP d_attemptSolSimplex;
bool solveRealRelaxation(Theory::Effort effortLevel);
projects / cvc5.git / commitdiff