/********************* */ /*! \file fc_simplex.cpp ** \verbatim ** Original author: Tim King ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. ** Copyright (c) 2009-2013 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.debugBasicAtBoundCount(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 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; LinearEqualityModule::UpdatePreferenceFunction leavingPrefFunc = selectLeavingFunction(curr); UpdateInfo currProposal = d_linEq.speculativeUpdate(curr, coeff, leavingPrefFunc); 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") << " debugBasicAtBoundCount " << d_linEq.debugBasicAtBoundCount(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.debugBasicAtBoundCount(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.debugBasicAtBoundCount(leaving) << endl; } } if(selected.describesPivot()){ ConstraintP 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 > 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; 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("< 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 */