From: Tim King Date: Sat, 4 May 2013 00:53:25 +0000 (-0400) Subject: Adding a smarter technique for pivoting in solutions for glpk. X-Git-Tag: cvc5-1.0.0~7287^2~156 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5a20ba9f1f843fe066bbc8268f511a71902b88cb;p=cvc5.git Adding a smarter technique for pivoting in solutions for glpk. --- diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index ed14e972b..620b8a121 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -51,6 +51,8 @@ libarith_la_SOURCES = \ 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 \ diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index 5777337ee..55e52fc53 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -132,6 +132,8 @@ private: bool d_solvedRelaxation; bool d_solvedMIP; + static int s_verbosity; + public: ApproxGLPK(const ArithVariables& vars); ~ApproxGLPK(); @@ -152,6 +154,9 @@ private: Solution extractSolution(bool mip) const; }; +#warning "set back to 0" +int ApproxGLPK::s_verbosity = 1; + }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ @@ -221,8 +226,10 @@ ApproxGLPK::ApproxGLPK(const ArithVariables& avars) : 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; @@ -407,77 +414,90 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const{ 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); } } } @@ -493,8 +513,10 @@ ApproximateSimplex::ApproxResult ApproxGLPK::solveRelaxation(){ 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){ @@ -551,8 +573,10 @@ ApproximateSimplex::ApproxResult ApproxGLPK::solveMIP(){ 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){ diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h index a2f3cde24..d4680939d 100644 --- a/src/theory/arith/approx_simplex.h +++ b/src/theory/arith/approx_simplex.h @@ -50,11 +50,6 @@ public: 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; diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp new file mode 100644 index 000000000..c8d5b6f68 --- /dev/null +++ b/src/theory/arith/attempt_solution_simplex.cpp @@ -0,0 +1,131 @@ + +#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& 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& 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::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 */ diff --git a/src/theory/arith/attempt_solution_simplex.h b/src/theory/arith/attempt_solution_simplex.h new file mode 100644 index 000000000..5bcdc6aab --- /dev/null +++ b/src/theory/arith/attempt_solution_simplex.h @@ -0,0 +1,97 @@ +/********************* */ +/*! \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& 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 */ + diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp index 1c32f80e4..5817a3629 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -68,7 +68,8 @@ LinearEqualityModule::Statistics::Statistics(): 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); @@ -80,6 +81,7 @@ LinearEqualityModule::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_weakeningSuccesses); StatisticsRegistry::registerStat(&d_weakenings); StatisticsRegistry::registerStat(&d_weakenTime); + StatisticsRegistry::registerStat(&d_forceTime); } LinearEqualityModule::Statistics::~Statistics(){ @@ -93,7 +95,9 @@ 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); @@ -117,19 +121,30 @@ void LinearEqualityModule::includeBoundUpdate(ArithVar v, const BoundsInfo& prev void LinearEqualityModule::updateMany(const DenseMap& many){ for(DenseMap::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& 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; @@ -163,10 +178,12 @@ void LinearEqualityModule::forceNewBasis(const DenseSet& newBasis){ 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); } } diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h index 607ee6244..293a0ddad 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear_equality.h @@ -243,11 +243,6 @@ public: /** 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& many); /** * Updates the value of a basic variable x_i to v, @@ -259,7 +254,14 @@ public: 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& many); void forceNewBasis(const DenseSet& newBasis); + void applySolution(const DenseSet& newBasis, const DenseMap& newValues); + /** * Returns a pointer to the first Tableau entry on the row ridx that does not @@ -689,6 +691,7 @@ private: IntStat d_weakeningAttempts, d_weakeningSuccesses, d_weakenings; TimerStat d_weakenTime; + TimerStat d_forceTime; Statistics(); ~Statistics(); diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index e4b19a683..504727c0b 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -109,6 +109,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context 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), @@ -1590,27 +1591,30 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){ 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: @@ -1620,6 +1624,7 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){ } if(d_qflraStatus == Result::SAT_UNKNOWN){ + Message() << "got sat unknown" << endl; vector toCut = cutAllBounded(); if(toCut.size() > 0){ branchVector(toCut); diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index b97ab3468..f6fb42a9c 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -58,6 +58,7 @@ #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" @@ -317,6 +318,7 @@ private: DualSimplexDecisionProcedure d_dualSimplex; FCSimplexDecisionProcedure d_fcSimplex; SumOfInfeasibilitiesSPD d_soiSimplex; + AttemptSolutionSDP d_attemptSolSimplex; bool solveRealRelaxation(Theory::Effort effortLevel);