diff options
author | Tim King <taking@cs.nyu.edu> | 2013-04-26 17:10:21 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-04-26 17:10:21 -0400 |
commit | 9098391fe334d829ec4101f190b8f1fa21c30752 (patch) | |
tree | b134fc1fe1c767a50013e1449330ca6a7ee18a3d /src/theory/arith/fc_simplex.cpp | |
parent | a9174ce4dc3939bbe14c9aa1fd11c79c7877eb16 (diff) |
FCSimplex branch merge
Diffstat (limited to 'src/theory/arith/fc_simplex.cpp')
-rw-r--r-- | src/theory/arith/fc_simplex.cpp | 853 |
1 files changed, 853 insertions, 0 deletions
diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp new file mode 100644 index 000000000..ac4625ba3 --- /dev/null +++ b/src/theory/arith/fc_simplex.cpp @@ -0,0 +1,853 @@ +/********************* */ +/*! \file simplex.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): 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 [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + + +#include "theory/arith/fc_simplex.h" +#include "theory/arith/options.h" +#include "theory/arith/constraint.h" + +#include "util/statistics_registry.h" + +using namespace std; + +namespace CVC4 { +namespace theory { +namespace arith { + + +FCSimplexDecisionProcedure::FCSimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc) + : SimplexDecisionProcedure(linEq, errors, conflictChannel, tvmalloc) + , d_focusSize(0) + , d_focusErrorVar(ARITHVAR_SENTINEL) + , d_focusCoefficients() + , d_pivotBudget(0) + , d_prevWitnessImprovement(AntiProductive) + , d_witnessImprovementInARow(0) + , d_sgnDisagreements() + , d_statistics(d_pivots) +{ } + +FCSimplexDecisionProcedure::Statistics::Statistics(uint32_t& pivots): + d_initialSignalsTime("theory::arith::FC::initialProcessTime"), + d_initialConflicts("theory::arith::FC::UpdateConflicts", 0), + d_fcFoundUnsat("theory::arith::FC::FoundUnsat", 0), + d_fcFoundSat("theory::arith::FC::FoundSat", 0), + d_fcMissed("theory::arith::FC::Missed", 0), + d_fcTimer("theory::arith::FC::Timer"), + d_fcFocusConstructionTimer("theory::arith::FC::Construction"), + d_selectUpdateForDualLike("theory::arith::FC::selectUpdateForDualLike"), + d_selectUpdateForPrimal("theory::arith::FC::selectUpdateForPrimal"), + d_finalCheckPivotCounter("theory::arith::FC::lastPivots", pivots) +{ + StatisticsRegistry::registerStat(&d_initialSignalsTime); + StatisticsRegistry::registerStat(&d_initialConflicts); + + StatisticsRegistry::registerStat(&d_fcFoundUnsat); + StatisticsRegistry::registerStat(&d_fcFoundSat); + StatisticsRegistry::registerStat(&d_fcMissed); + + StatisticsRegistry::registerStat(&d_fcTimer); + StatisticsRegistry::registerStat(&d_fcFocusConstructionTimer); + + StatisticsRegistry::registerStat(&d_selectUpdateForDualLike); + StatisticsRegistry::registerStat(&d_selectUpdateForPrimal); + + StatisticsRegistry::registerStat(&d_finalCheckPivotCounter); +} + +FCSimplexDecisionProcedure::Statistics::~Statistics(){ + StatisticsRegistry::unregisterStat(&d_initialSignalsTime); + StatisticsRegistry::unregisterStat(&d_initialConflicts); + + StatisticsRegistry::unregisterStat(&d_fcFoundUnsat); + StatisticsRegistry::unregisterStat(&d_fcFoundSat); + StatisticsRegistry::unregisterStat(&d_fcMissed); + + StatisticsRegistry::unregisterStat(&d_fcTimer); + StatisticsRegistry::unregisterStat(&d_fcFocusConstructionTimer); + + StatisticsRegistry::unregisterStat(&d_selectUpdateForDualLike); + StatisticsRegistry::unregisterStat(&d_selectUpdateForPrimal); + + StatisticsRegistry::unregisterStat(&d_finalCheckPivotCounter); +} + +Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){ + Assert(d_conflictVariables.empty()); + Assert(d_sgnDisagreements.empty()); + + d_pivots = 0; + static CVC4_THREADLOCAL(unsigned int) instance = 0; + instance = instance + 1; + static const bool verbose = false; + + if(d_errorSet.errorEmpty() && !d_errorSet.moreSignals()){ + Debug("arith::findModel") << "fcFindModel("<< instance <<") trivial" << endl; + Assert(d_conflictVariables.empty()); + //if(verbose){ Message() << "fcFindModel("<< instance <<") trivial" << endl; } + return Result::SAT; + } + + // We need to reduce this because of + d_errorSet.reduceToSignals(); + + // We must start tracking NOW + d_errorSet.setSelectionRule(SUM_METRIC); + + + if(initialProcessSignals()){ + d_conflictVariables.purge(); + if(verbose){ Message() << "fcFindModel("<< instance <<") early conflict" << endl; } + Debug("arith::findModel") << "fcFindModel("<< instance <<") early conflict" << endl; + Assert(d_conflictVariables.empty()); + return Result::UNSAT; + }else if(d_errorSet.errorEmpty()){ + //if(verbose){ Message() << "fcFindModel("<< instance <<") fixed itself" << endl; } + Debug("arith::findModel") << "fcFindModel("<< instance <<") fixed itself" << endl; + if(verbose) + Assert(!d_errorSet.moreSignals()); + Assert(d_conflictVariables.empty()); + return Result::SAT; + } + + Debug("arith::findModel") << "fcFindModel(" << instance <<") start non-trivial" << endl; + + exactResult |= options::arithStandardCheckVarOrderPivots() < 0; + + d_prevWitnessImprovement = HeuristicDegenerate; + d_witnessImprovementInARow = 0; + + Result::Sat result = Result::SAT_UNKNOWN; + + if(result == Result::SAT_UNKNOWN){ + if(exactResult){ + d_pivotBudget = -1; + }else{ + d_pivotBudget = options::arithStandardCheckVarOrderPivots(); + } + + result = dualLike(); + + if(result == Result::UNSAT){ + ++(d_statistics.d_fcFoundUnsat); + if(verbose){ Message() << "fc found unsat";} + }else if(d_errorSet.errorEmpty()){ + ++(d_statistics.d_fcFoundSat); + if(verbose){ Message() << "fc found model"; } + }else{ + ++(d_statistics.d_fcMissed); + if(verbose){ Message() << "fc missed"; } + } + } + if(verbose){ + Message() << "(" << instance << ") pivots " << d_pivots << endl; + } + + Assert(!d_errorSet.moreSignals()); + if(result == Result::SAT_UNKNOWN && d_errorSet.errorEmpty()){ + result = Result::SAT; + } + + // ensure that the conflict variable is still in the queue. + d_conflictVariables.purge(); + + Debug("arith::findModel") << "end findModel() " << instance << " " << result << endl; + + Assert(d_conflictVariables.empty()); + return result; +} + + +void FCSimplexDecisionProcedure::logPivot(WitnessImprovement w){ + if(d_pivotBudget > 0) { + --d_pivotBudget; + } + Assert(w != AntiProductive); + + if(w == d_prevWitnessImprovement){ + ++d_witnessImprovementInARow; + // ignore overflow : probably never reached + if(d_witnessImprovementInARow == 0){ + --d_witnessImprovementInARow; + } + }else{ + if(w != BlandsDegenerate){ + d_witnessImprovementInARow = 1; + } + // if w == BlandsDegenerate do not reset the counter + d_prevWitnessImprovement = w; + } + if(strongImprovement(w)){ + d_leavingCountSinceImprovement.purge(); + } + + Debug("logPivot") << "logPivot " << d_prevWitnessImprovement << " " << d_witnessImprovementInARow << endl; + +} + +uint32_t FCSimplexDecisionProcedure::degeneratePivotsInARow() const { + switch(d_prevWitnessImprovement){ + case ConflictFound: + case ErrorDropped: + case FocusImproved: + return 0; + case HeuristicDegenerate: + case BlandsDegenerate: + return d_witnessImprovementInARow; + // Degenerate is unreachable for its own reasons + case Degenerate: + case FocusShrank: + case AntiProductive: + Unreachable(); + return -1; + } + Unreachable(); +} + +void FCSimplexDecisionProcedure::adjustFocusAndError(const UpdateInfo& up, const AVIntPairVec& focusChanges){ + uint32_t newErrorSize = d_errorSet.errorSize(); + uint32_t newFocusSize = d_errorSet.focusSize(); + + //Assert(!d_conflictVariables.empty() || newFocusSize <= d_focusSize); + Assert(!d_conflictVariables.empty() || newErrorSize <= d_errorSize); + + if(newFocusSize == 0 || !d_conflictVariables.empty() ){ + tearDownInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer, d_focusErrorVar); + d_focusErrorVar = ARITHVAR_SENTINEL; + }else if(2*newFocusSize < d_focusSize ){ + tearDownInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer, d_focusErrorVar); + d_focusErrorVar = constructInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer); + }else{ + adjustInfeasFunc(d_statistics.d_fcFocusConstructionTimer, d_focusErrorVar, focusChanges); + } + + d_errorSize = newErrorSize; + d_focusSize = newFocusSize; +} + +WitnessImprovement FCSimplexDecisionProcedure::adjustFocusShrank(const ArithVarVec& dropped){ + Assert(dropped.size() > 0); + Assert(d_errorSet.focusSize() == d_focusSize); + Assert(d_errorSet.focusSize() > dropped.size()); + + uint32_t newFocusSize = d_focusSize - dropped.size(); + Assert(newFocusSize > 0); + + if(2 * newFocusSize <= d_focusSize){ + d_errorSet.dropFromFocusAll(dropped); + tearDownInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer, d_focusErrorVar); + d_focusErrorVar = constructInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer); + }else{ + shrinkInfeasFunc(d_statistics.d_fcFocusConstructionTimer, d_focusErrorVar, dropped); + d_errorSet.dropFromFocusAll(dropped); + } + + d_focusSize = newFocusSize; + Assert(d_errorSet.focusSize() == d_focusSize); + return FocusShrank; +} + +WitnessImprovement FCSimplexDecisionProcedure::focusDownToJust(ArithVar v){ + // uint32_t newErrorSize = d_errorSet.errorSize(); + // uint32_t newFocusSize = d_errorSet.focusSize(); + Assert(d_focusSize == d_errorSet.focusSize()); + Assert(d_focusSize > 1); + Assert(d_errorSet.inFocus(v)); + + d_errorSet.focusDownToJust(v); + Assert(d_errorSet.focusSize() == 1); + d_focusSize = 1; + + tearDownInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer, d_focusErrorVar); + d_focusErrorVar = constructInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer); + + return FocusShrank; +} + + + +UpdateInfo FCSimplexDecisionProcedure::selectPrimalUpdate(ArithVar basic, LinearEqualityModule::UpdatePreferenceFunction upf, LinearEqualityModule::VarPreferenceFunction bpf) { + UpdateInfo selected; + + static int instance = 0 ; + ++instance; + + Debug("arith::selectPrimalUpdate") + << "selectPrimalUpdate " << instance << endl + << basic << " " << d_tableau.basicRowLength(basic) + << " " << d_linEq._countBounds(basic) << endl; + + static const int s_maxCandidatesAfterImprove = 3; + bool isFocus = basic == d_focusErrorVar; + Assert(isFocus || d_errorSet.inError(basic)); + int basicDir = isFocus? 1 : d_errorSet.getSgn(basic); + bool dualLike = !isFocus && d_focusSize > 1; + + if(!isFocus){ + loadFocusSigns(); + } + + decreasePenalties(); + + typedef std::vector<Cand> CandVector; + CandVector candidates; + + for(Tableau::RowIterator ri = d_tableau.basicRowIterator(basic); !ri.atEnd(); ++ri){ + const Tableau::Entry& e = *ri; + ArithVar curr = e.getColVar(); + if(curr == basic){ continue; } + + int sgn = e.getCoefficient().sgn(); + int curr_movement = basicDir * sgn; + + bool candidate = + (curr_movement > 0 && d_variables.cmpAssignmentUpperBound(curr) < 0) || + (curr_movement < 0 && d_variables.cmpAssignmentLowerBound(curr) > 0); + + Debug("arith::selectPrimalUpdate") + << "storing " << basic + << " " << curr + << " " << candidate + << " " << e.getCoefficient() + << " " << curr_movement + << " " << focusCoefficient(curr) << endl; + + if(!candidate) { continue; } + + if(!isFocus){ + const Rational& focusC = focusCoefficient(curr); + Assert(dualLike || !focusC.isZero()); + if(dualLike && curr_movement != focusC.sgn()){ + Debug("arith::selectPrimalUpdate") << "sgn disagreement " << curr << endl; + d_sgnDisagreements.push_back(curr); + continue; + }else{ + candidates.push_back(Cand(curr, penalty(curr), curr_movement, &focusC)); + } + }else{ + candidates.push_back(Cand(curr, penalty(curr), curr_movement, &e.getCoefficient())); + } + } + + CompPenaltyColLength colCmp(&d_linEq); + CandVector::iterator i = candidates.begin(); + CandVector::iterator end = candidates.end(); + std::make_heap(i, end, colCmp); + + bool checkEverything = d_pivots == 0; + + int candidatesAfterFocusImprove = 0; + while(i != end && (checkEverything || candidatesAfterFocusImprove <= s_maxCandidatesAfterImprove)){ + std::pop_heap(i, end, colCmp); + --end; + Cand& cand = (*end); + ArithVar curr = cand.d_nb; + const Rational& coeff = *cand.d_coeff; + +#warning "Who is using computeSafeUpdate?" + LinearEqualityModule::UpdatePreferenceFunction leavingPrefFunc = selectLeavingFunction(curr); + UpdateInfo currProposal = d_linEq.speculativeUpdate(curr, coeff, leavingPrefFunc); + + //int curr_movement = cand.d_sgn; + // if(isFocus){ + // currProposal = d_linEq.speculativeUpdate(curr, coeff, upf); + // }else{ + // currProposal = UpdateInfo(curr, curr_movement); + // d_linEq.computeSafeUpdate(currProposal, bpf); + // } + + Debug("arith::selectPrimalUpdate") + << "selected " << selected << endl + << "currProp " << currProposal << endl + << "coeff " << coeff << endl; + + Assert(!currProposal.uninitialized()); + + if(candidatesAfterFocusImprove > 0){ + candidatesAfterFocusImprove++; + } + + if(selected.uninitialized() || (d_linEq.*upf)(selected, currProposal)){ + + selected = currProposal; + WitnessImprovement w = selected.getWitness(false); + Debug("arith::selectPrimalUpdate") << "selected " << w << endl; + setPenalty(curr, w); + if(improvement(w)){ + bool exitEarly; + switch(w){ + case ConflictFound: exitEarly = true; break; + case ErrorDropped: + if(checkEverything){ + exitEarly = d_errorSize + selected.errorsChange() == 0; + Debug("arith::selectPrimalUpdate") + << "ee " << d_errorSize << " " + << selected.errorsChange() << " " + << d_errorSize + selected.errorsChange() << endl; + }else{ + exitEarly = true; + } + break; + case FocusImproved: + candidatesAfterFocusImprove = 1; + exitEarly = false; + break; + default: + exitEarly = false; break; + } + if(exitEarly){ break; } + } + }else{ + Debug("arith::selectPrimalUpdate") << "dropped "<< endl; + } + + } + + if(!isFocus){ + unloadFocusSigns(); + } + return selected; +} + +bool FCSimplexDecisionProcedure::debugCheckWitness(const UpdateInfo& inf, WitnessImprovement w, bool useBlands){ + if(inf.getWitness(useBlands) == w){ + switch(w){ + case ConflictFound: return inf.foundConflict(); + case ErrorDropped: return inf.errorsChange() < 0; + case FocusImproved: return inf.focusDirection() > 0; + case FocusShrank: return false; // This is not a valid output + case Degenerate: return false; // This is not a valid output + case BlandsDegenerate: return useBlands; + case HeuristicDegenerate: return !useBlands; + case AntiProductive: return false; + } + } + return false; +} + +WitnessImprovement FCSimplexDecisionProcedure::primalImproveError(ArithVar errorVar){ + bool useBlands = degeneratePivotsInARow() >= s_maxDegeneratePivotsBeforeBlandsOnLeaving; + UpdateInfo selected = selectUpdateForPrimal (errorVar, useBlands); + Assert(!selected.uninitialized()); + WitnessImprovement w = selected.getWitness(useBlands); + Assert(debugCheckWitness(selected, w, useBlands)); + + updateAndSignal(selected, w); + logPivot(w); + return w; +} + + +WitnessImprovement FCSimplexDecisionProcedure::focusUsingSignDisagreements(ArithVar basic){ + Assert(!d_sgnDisagreements.empty()); + Assert(d_errorSet.focusSize() >= 2); + + if(Debug.isOn("arith::focus")){ + d_errorSet.debugPrint(Debug("arith::focus")); + } + + ArithVar nb = d_linEq.minBy(d_sgnDisagreements, &LinearEqualityModule::minColLength); + const Tableau::Entry& e_evar_nb = d_tableau.basicFindEntry(basic, nb); + int oppositeSgn = - (e_evar_nb.getCoefficient().sgn()); + Debug("arith::focus") << "focusUsingSignDisagreements " << basic << " " << oppositeSgn << endl; + + ArithVarVec dropped; + + Tableau::ColIterator colIter = d_tableau.colIterator(nb); + for(; !colIter.atEnd(); ++colIter){ + const Tableau::Entry& entry = *colIter; + Assert(entry.getColVar() == nb); + + int sgn = entry.getCoefficient().sgn(); + Debug("arith::focus") + << "on row " + << d_tableau.rowIndexToBasic(entry.getRowIndex()) + << " " + << entry.getCoefficient() << endl; + ArithVar currRow = d_tableau.rowIndexToBasic(entry.getRowIndex()); + if(d_errorSet.inError(currRow) && d_errorSet.inFocus(currRow)){ + int errSgn = d_errorSet.getSgn(currRow); + + if(errSgn * sgn == oppositeSgn){ + dropped.push_back(currRow); + Debug("arith::focus") << "dropping from focus " << currRow << endl; + } + } + } + + d_sgnDisagreements.clear(); + return adjustFocusShrank(dropped); +} + +bool debugSelectedErrorDropped(const UpdateInfo& selected, int32_t prevErrorSize, int32_t currErrorSize){ + int diff = currErrorSize - prevErrorSize; + return selected.foundConflict() || diff == selected.errorsChange(); +} + +void FCSimplexDecisionProcedure::debugPrintSignal(ArithVar updated) const{ + Debug("updateAndSignal") << "updated basic " << updated; + Debug("updateAndSignal") << " length " << d_tableau.basicRowLength(updated); + Debug("updateAndSignal") << " consistent " << d_variables.assignmentIsConsistent(updated); + int dir = !d_variables.assignmentIsConsistent(updated) ? + d_errorSet.getSgn(updated) : 0; + Debug("updateAndSignal") << " dir " << dir; + Debug("updateAndSignal") << " _countBounds " << d_linEq._countBounds(updated) << endl; +} + +bool debugUpdatedBasic(const UpdateInfo& selected, ArithVar updated){ + if(selected.describesPivot() && updated == selected.leaving()){ + return selected.foundConflict(); + }else{ + return true; + } +} + +void FCSimplexDecisionProcedure::updateAndSignal(const UpdateInfo& selected, WitnessImprovement w){ + ArithVar nonbasic = selected.nonbasic(); + + static bool verbose = false; + + Debug("updateAndSignal") << "updateAndSignal " << selected << endl; + + stringstream ss; + if(verbose){ + d_errorSet.debugPrint(ss); + if(selected.describesPivot()){ + ArithVar leaving = selected.leaving(); + ss << "leaving " << leaving + << " " << d_tableau.basicRowLength(leaving) + << " " << d_linEq._countBounds(leaving) + << endl; + } + if(degenerate(w) && selected.describesPivot()){ + ArithVar leaving = selected.leaving(); + Message() + << "degenerate " << leaving + << ", atBounds " << d_linEq.basicsAtBounds(selected) + << ", len " << d_tableau.basicRowLength(leaving) + << ", bc " << d_linEq._countBounds(leaving) + << endl; + } + } + + if(selected.describesPivot()){ + Constraint limiting = selected.limiting(); + ArithVar basic = limiting->getVariable(); + Assert(d_linEq.basicIsTracked(basic)); + d_linEq.pivotAndUpdate(basic, nonbasic, limiting->getValue()); + }else{ + Assert(!selected.unbounded() || selected.errorsChange() < 0); + + DeltaRational newAssignment = + d_variables.getAssignment(nonbasic) + selected.nonbasicDelta(); + + d_linEq.updateTracked(nonbasic, newAssignment); + } + d_pivots++; + + increaseLeavingCount(nonbasic); + + vector< pair<ArithVar, int> > focusChanges; + while(d_errorSet.moreSignals()){ + ArithVar updated = d_errorSet.topSignal(); + int prevFocusSgn = d_errorSet.popSignal(); + + if(d_tableau.isBasic(updated)){ + Assert(!d_variables.assignmentIsConsistent(updated) == d_errorSet.inError(updated)); + if(Debug.isOn("updateAndSignal")){debugPrintSignal(updated);} + if(!d_variables.assignmentIsConsistent(updated)){ + if(checkBasicForConflict(updated)){ + reportConflict(updated); + Assert(debugUpdatedBasic(selected, updated)); + } + } + }else{ + Debug("updateAndSignal") << "updated nonbasic " << updated << endl; + } + int currFocusSgn = d_errorSet.focusSgn(updated); + if(currFocusSgn != prevFocusSgn){ + int change = currFocusSgn - prevFocusSgn; + focusChanges.push_back(make_pair(updated, change)); + } + } + + if(verbose){ + Message() << "conflict variable " << selected << endl; + Message() << ss.str(); + } + if(Debug.isOn("error")){ d_errorSet.debugPrint(Debug("error")); } + + Assert(debugSelectedErrorDropped(selected, d_errorSize, d_errorSet.errorSize())); + + adjustFocusAndError(selected, focusChanges); +} + +WitnessImprovement FCSimplexDecisionProcedure::dualLikeImproveError(ArithVar errorVar){ + Assert(d_sgnDisagreements.empty()); + Assert(d_focusSize > 1); + + UpdateInfo selected = selectUpdateForDualLike(errorVar); + + if(selected.uninitialized()){ + // we found no proposals + // If this is empty, there must be an error on this variable! + // this should not be possible. It Should have been caught as a signal earlier + WitnessImprovement dropped = focusUsingSignDisagreements(errorVar); + Assert(d_sgnDisagreements.empty()); + + return dropped; + }else{ + d_sgnDisagreements.clear(); + } + + Assert(d_sgnDisagreements.empty()); + Assert(!selected.uninitialized()); + + if(selected.focusDirection() == 0 && + d_prevWitnessImprovement == HeuristicDegenerate && + d_witnessImprovementInARow >= s_focusThreshold){ + + Debug("focusDownToJust") << "focusDownToJust " << errorVar << endl; + + return focusDownToJust(errorVar); + }else{ + WitnessImprovement w = selected.getWitness(false); + Assert(debugCheckWitness(selected, w, false)); + updateAndSignal(selected, w); + logPivot(w); + return w; + } +} + +WitnessImprovement FCSimplexDecisionProcedure::focusDownToLastHalf(){ + Assert(d_focusSize >= 2); + + Debug("focusDownToLastHalf") << "focusDownToLastHalf " + << d_errorSet.errorSize() << " " + << d_errorSet.focusSize() << " "; + + uint32_t half = d_focusSize/2; + ArithVarVec buf; + for(ErrorSet::focus_iterator i = d_errorSet.focusBegin(), + i_end = d_errorSet.focusEnd(); i != i_end; ++i){ + if(half > 0){ + --half; + } else{ + buf.push_back(*i); + } + } + WitnessImprovement w = adjustFocusShrank(buf); + Debug("focusDownToLastHalf") << "-> " << d_errorSet.focusSize() << endl; + return w; +} + +WitnessImprovement FCSimplexDecisionProcedure::selectFocusImproving() { + Assert(d_focusErrorVar != ARITHVAR_SENTINEL); + Assert(d_focusSize >= 2); + + LinearEqualityModule::UpdatePreferenceFunction upf = + &LinearEqualityModule::preferWitness<true>; + + LinearEqualityModule::VarPreferenceFunction bpf = + &LinearEqualityModule::minRowLength; + + UpdateInfo selected = selectPrimalUpdate(d_focusErrorVar, upf, bpf); + + if(selected.uninitialized()){ + Debug("selectFocusImproving") << "focus is optimum, but we don't have sat/conflict yet" << endl; + + return focusDownToLastHalf(); + } + Assert(!selected.uninitialized()); + WitnessImprovement w = selected.getWitness(false); + Assert(debugCheckWitness(selected, w, false)); + + if(degenerate(w)){ + Debug("selectFocusImproving") << "only degenerate" << endl; + if(d_prevWitnessImprovement == HeuristicDegenerate && + d_witnessImprovementInARow >= s_focusThreshold){ + Debug("selectFocusImproving") << "focus down been degenerate too long" << endl; + return focusDownToLastHalf(); + }else{ + Debug("selectFocusImproving") << "taking degenerate" << endl; + } + } + Debug("selectFocusImproving") << "selectFocusImproving did this " << selected << endl; + + updateAndSignal(selected, w); + logPivot(w); + return w; +} + +bool FCSimplexDecisionProcedure::debugDualLike(WitnessImprovement w, ostream& out, int instance, uint32_t prevFocusSize, uint32_t prevErrorSize ) const{ + out << "DLV("<<instance<<") "; + switch(w){ + case ConflictFound: + out << "found conflict" << endl; + return !d_conflictVariables.empty(); + case ErrorDropped: + out << "dropped " << prevErrorSize - d_errorSize << endl; + return d_errorSize < prevErrorSize; + case FocusImproved: + out << "focus improved"<< endl; + return d_errorSize == prevErrorSize; + case FocusShrank: + out << "focus shrank"<< endl; + return d_errorSize == prevErrorSize && prevFocusSize > d_focusSize; + case BlandsDegenerate: + out << "bland degenerate"<< endl; + return true; + case HeuristicDegenerate: + out << "heuristic degenerate"<< endl; + return true; + case AntiProductive: + out << "focus blur" << endl; + return prevFocusSize == 0; + case Degenerate: + return false; + } + return false; +} + +Result::Sat FCSimplexDecisionProcedure::dualLike(){ + static int instance = 0; + static bool verbose = false; + + TimerStat::CodeTimer codeTimer(d_statistics.d_fcTimer); + + Assert(d_sgnDisagreements.empty()); + Assert(d_pivotBudget != 0); + Assert(d_errorSize == d_errorSet.errorSize()); + Assert(d_errorSize > 0); + Assert(d_focusSize == d_errorSet.focusSize()); + Assert(d_focusSize > 0); + Assert(d_conflictVariables.empty()); + Assert(d_focusErrorVar == ARITHVAR_SENTINEL); + + + d_scores.purge(); + d_focusErrorVar = constructInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer); + + + while(d_pivotBudget != 0 && d_errorSize > 0 && d_conflictVariables.empty()){ + ++instance; + Debug("dualLike") << "dualLike " << instance << endl; + + Assert(d_errorSet.noSignals()); + + WitnessImprovement w = AntiProductive; + uint32_t prevFocusSize = d_focusSize; + uint32_t prevErrorSize = d_errorSize; + + if(d_focusSize == 0){ + Assert(d_errorSize == d_errorSet.errorSize()); + Assert(d_focusErrorVar == ARITHVAR_SENTINEL); + + d_errorSet.blur(); + + d_focusSize = d_errorSet.focusSize(); + + Assert( d_errorSize == d_focusSize); + Assert( d_errorSize >= 1 ); + + d_focusErrorVar = constructInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer); + + Debug("dualLike") << "blur " << d_focusSize << endl; + }else if(d_focusSize == 1){ + // Possible outcomes: + // - errorSet size shrunk + // -- fixed v + // -- fixed something other than v + // - conflict + // - budget was exhausted + + ArithVar e = d_errorSet.topFocusVariable(); + Debug("dualLike") << "primalImproveError " << e << endl; + w = primalImproveError(e); + }else{ + + // Possible outcomes: + // - errorSet size shrunk + // -- fixed v + // -- fixed something other than v + // - conflict + // - budget was exhausted + // - focus went down + Assert(d_focusSize > 1); + ArithVar e = d_errorSet.topFocusVariable(); + static const unsigned s_sumMetricThreshold = 1; + if(d_errorSet.sumMetric(e) <= s_sumMetricThreshold){ + Debug("dualLike") << "dualLikeImproveError " << e << endl; + w = dualLikeImproveError(e); + }else{ + Debug("dualLike") << "selectFocusImproving " << endl; + w = selectFocusImproving(); + } + } + Assert(d_focusSize == d_errorSet.focusSize()); + Assert(d_errorSize == d_errorSet.errorSize()); + + if(verbose){ + debugDualLike(w, Message(), instance, prevFocusSize, prevErrorSize); + } + Assert(debugDualLike(w, Debug("dualLike"), instance, prevFocusSize, prevErrorSize)); + } + + + if(d_focusErrorVar != ARITHVAR_SENTINEL){ + tearDownInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer, d_focusErrorVar); + d_focusErrorVar = ARITHVAR_SENTINEL; + } + + Assert(d_focusErrorVar == ARITHVAR_SENTINEL); + if(!d_conflictVariables.empty()){ + return Result::UNSAT; + }else if(d_errorSet.errorEmpty()){ + Assert(d_errorSet.noSignals()); + return Result::SAT; + }else{ + Assert(d_pivotBudget == 0); + return Result::SAT_UNKNOWN; + } +} + + +void FCSimplexDecisionProcedure::loadFocusSigns(){ + Assert(d_focusCoefficients.empty()); + Assert(d_focusErrorVar != ARITHVAR_SENTINEL); + for(Tableau::RowIterator ri = d_tableau.basicRowIterator(d_focusErrorVar); !ri.atEnd(); ++ri){ + const Tableau::Entry& e = *ri; + ArithVar curr = e.getColVar(); + d_focusCoefficients.set(curr, &e.getCoefficient()); + } +} + +void FCSimplexDecisionProcedure::unloadFocusSigns(){ + d_focusCoefficients.purge(); +} + +const Rational& FCSimplexDecisionProcedure::focusCoefficient(ArithVar nb) const { + if(d_focusCoefficients.isKey(nb)){ + return *(d_focusCoefficients[nb]); + }else{ + return d_zero; + } +} + +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ |