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/error_set.cpp | |
parent | a9174ce4dc3939bbe14c9aa1fd11c79c7877eb16 (diff) |
FCSimplex branch merge
Diffstat (limited to 'src/theory/arith/error_set.cpp')
-rw-r--r-- | src/theory/arith/error_set.cpp | 493 |
1 files changed, 493 insertions, 0 deletions
diff --git a/src/theory/arith/error_set.cpp b/src/theory/arith/error_set.cpp new file mode 100644 index 000000000..ee72d1949 --- /dev/null +++ b/src/theory/arith/error_set.cpp @@ -0,0 +1,493 @@ +/********************* */ +/*! \file arith_priority_queue.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: mdeters + ** Minor contributors (to current version): none + ** 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/error_set.h" +#include "theory/arith/constraint.h" + +using namespace std; + +namespace CVC4 { +namespace theory { +namespace arith { + + +ErrorInformation::ErrorInformation() + : d_variable(ARITHVAR_SENTINEL) + , d_violated(NullConstraint) + , d_sgn(0) + , d_relaxed(false) + , d_inFocus(false) + , d_handle() + , d_amount(NULL) + , d_metric(0) +{ + Debug("arith::error::mem") << "def constructor " << d_variable << " " << d_amount << endl; +} + +ErrorInformation::ErrorInformation(ArithVar var, Constraint vio, int sgn) + : d_variable(var) + , d_violated(vio) + , d_sgn(sgn) + , d_relaxed(false) + , d_inFocus(false) + , d_handle() + , d_amount(NULL) + , d_metric(0) +{ + Assert(debugInitialized()); + Debug("arith::error::mem") << "constructor " << d_variable << " " << d_amount << endl; +} + + +ErrorInformation::~ErrorInformation() { + Assert(d_relaxed != true); + if(d_amount != NULL){ + Debug("arith::error::mem") << d_amount << endl; + Debug("arith::error::mem") << "destroy " << d_variable << " " << d_amount << endl; + delete d_amount; + d_amount = NULL; + } +} + +ErrorInformation::ErrorInformation(const ErrorInformation& ei) + : d_variable(ei.d_variable) + , d_violated(ei.d_violated) + , d_sgn(ei.d_sgn) + , d_relaxed(ei.d_relaxed) + , d_inFocus(ei.d_inFocus) + , d_handle(ei.d_handle) + , d_metric(0) +{ + if(ei.d_amount == NULL){ + d_amount = NULL; + }else{ + d_amount = new DeltaRational(*ei.d_amount); + } + Debug("arith::error::mem") << "copy const " << d_variable << " " << d_amount << endl; +} + +ErrorInformation& ErrorInformation::operator=(const ErrorInformation& ei){ + d_variable = ei.d_variable; + d_violated = ei.d_violated; + d_sgn = ei.d_sgn; + d_relaxed = (ei.d_relaxed); + d_inFocus = (ei.d_inFocus); + d_handle = (ei.d_handle); + d_metric = ei.d_metric; + if(d_amount != NULL && ei.d_amount != NULL){ + Debug("arith::error::mem") << "assignment assign " << d_variable << " " << d_amount << endl; + *d_amount = *ei.d_amount; + }else if(ei.d_amount != NULL){ + d_amount = new DeltaRational(*ei.d_amount); + Debug("arith::error::mem") << "assignment alloc " << d_variable << " " << d_amount << endl; + }else if(d_amount != NULL){ + Debug("arith::error::mem") << "assignment release " << d_variable << " " << d_amount << endl; + delete d_amount; + d_amount = NULL; + }else{ + d_amount = NULL; + } + return *this; +} + +void ErrorInformation::reset(Constraint c, int sgn){ + Assert(!isRelaxed()); + Assert(c != NullConstraint); + d_violated = c; + d_sgn = sgn; + + if(d_amount != NULL){ + delete d_amount; + Debug("arith::error::mem") << "reset " << d_variable << " " << d_amount << endl; + d_amount = NULL; + } +} + +void ErrorInformation::setAmount(const DeltaRational& am){ + if(d_amount == NULL){ + d_amount = new DeltaRational; + Debug("arith::error::mem") << "setAmount " << d_variable << " " << d_amount << endl; + } + (*d_amount) = am; +} + +ErrorSet::Statistics::Statistics(): + d_enqueues("theory::arith::pqueue::enqueues", 0), + d_enqueuesCollection("theory::arith::pqueue::enqueuesCollection", 0), + d_enqueuesDiffMode("theory::arith::pqueue::enqueuesDiffMode", 0), + d_enqueuesVarOrderMode("theory::arith::pqueue::enqueuesVarOrderMode", 0), + d_enqueuesCollectionDuplicates("theory::arith::pqueue::enqueuesCollectionDuplicates", 0), + d_enqueuesVarOrderModeDuplicates("theory::arith::pqueue::enqueuesVarOrderModeDuplicates", 0) +{ + StatisticsRegistry::registerStat(&d_enqueues); + StatisticsRegistry::registerStat(&d_enqueuesCollection); + StatisticsRegistry::registerStat(&d_enqueuesDiffMode); + StatisticsRegistry::registerStat(&d_enqueuesVarOrderMode); + StatisticsRegistry::registerStat(&d_enqueuesCollectionDuplicates); + StatisticsRegistry::registerStat(&d_enqueuesVarOrderModeDuplicates); +} + +ErrorSet::Statistics::~Statistics(){ + StatisticsRegistry::unregisterStat(&d_enqueues); + StatisticsRegistry::unregisterStat(&d_enqueuesCollection); + StatisticsRegistry::unregisterStat(&d_enqueuesDiffMode); + StatisticsRegistry::unregisterStat(&d_enqueuesVarOrderMode); + StatisticsRegistry::unregisterStat(&d_enqueuesCollectionDuplicates); + StatisticsRegistry::unregisterStat(&d_enqueuesVarOrderModeDuplicates); +} + +ErrorSet::ErrorSet(ArithVariables& vars, TableauSizes tabSizes, BoundCountingLookup lookups): + d_variables(vars), + d_errInfo(), + d_selectionRule(VAR_ORDER), + d_focus(ComparatorPivotRule(this,d_selectionRule)), + d_outOfFocus(), + d_signals(), + d_tableauSizes(tabSizes), + d_boundLookup(lookups) +{} + +ErrorSelectionRule ErrorSet::getSelectionRule() const{ + return d_selectionRule; +} + +void ErrorSet::recomputeAmount(ErrorInformation& ei, ErrorSelectionRule rule){ + switch(rule){ + case MINIMUM_AMOUNT: + case MAXIMUM_AMOUNT: + ei.setAmount(computeDiff(ei.getVariable())); + break; + case SUM_METRIC: + ei.setMetric(sumMetric(ei.getVariable())); + break; + case VAR_ORDER: + //do nothing + break; + } +} + +void ErrorSet::setSelectionRule(ErrorSelectionRule rule){ + if(rule != getSelectionRule()){ + FocusSet into(ComparatorPivotRule(this, rule)); + FocusSet::const_iterator iter = d_focus.begin(); + FocusSet::const_iterator i_end = d_focus.end(); + for(; iter != i_end; ++iter){ + ArithVar v = *iter; + ErrorInformation& ei = d_errInfo.get(v); + if(ei.inFocus()){ + recomputeAmount(ei, rule); + FocusSetHandle handle = into.push(v); + ei.setHandle(handle); + } + } + d_focus.swap(into); + d_selectionRule = rule; + } + Assert(getSelectionRule() == rule); +} + +ComparatorPivotRule::ComparatorPivotRule(const ErrorSet* es, ErrorSelectionRule r): + d_errorSet(es), d_rule (r) +{} + +bool ComparatorPivotRule::operator()(ArithVar v, ArithVar u) const { + switch(d_rule){ + case VAR_ORDER: + // This needs to be the reverse of the minVariableOrder + return v > u; + case SUM_METRIC: + { + uint32_t v_metric = d_errorSet->getMetric(v); + uint32_t u_metric = d_errorSet->getMetric(u); + if(v_metric == u_metric){ + return v > u; + }else{ + return v_metric > u_metric; + } + } + case MINIMUM_AMOUNT: + { + const DeltaRational& vamt = d_errorSet->getAmount(v); + const DeltaRational& uamt = d_errorSet->getAmount(u); + int cmp = vamt.cmp(uamt); + if(cmp == 0){ + return v > u; + }else{ + return cmp > 0; + } + } + case MAXIMUM_AMOUNT: + { + const DeltaRational& vamt = d_errorSet->getAmount(v); + const DeltaRational& uamt = d_errorSet->getAmount(u); + int cmp = vamt.cmp(uamt); + if(cmp == 0){ + return v > u; + }else{ + return cmp < 0; + } + } + } + Unreachable(); +} + +void ErrorSet::update(ErrorInformation& ei){ + if(ei.inFocus()){ + + switch(getSelectionRule()){ + case MINIMUM_AMOUNT: + case MAXIMUM_AMOUNT: + ei.setAmount(computeDiff(ei.getVariable())); + d_focus.modify(ei.getHandle(), ei.getVariable()); + break; + case SUM_METRIC: + ei.setMetric(sumMetric(ei.getVariable())); + d_focus.modify(ei.getHandle(), ei.getVariable()); + break; + case VAR_ORDER: + //do nothing + break; + } + } +} + +/** A variable becomes satisfied. */ +void ErrorSet::transitionVariableOutOfError(ArithVar v) { + Assert(!inconsistent(v)); + ErrorInformation& ei = d_errInfo.get(v); + Assert(ei.debugInitialized()); + if(ei.isRelaxed()){ + Constraint viol = ei.getViolated(); + if(ei.sgn() > 0){ + d_variables.setLowerBoundConstraint(viol); + }else{ + d_variables.setUpperBoundConstraint(viol); + } + Assert(!inconsistent(v)); + ei.setUnrelaxed(); + } + if(ei.inFocus()){ + d_focus.erase(ei.getHandle()); + ei.setInFocus(false); + } + d_errInfo.remove(v); +} + + +void ErrorSet::transitionVariableIntoError(ArithVar v) { + Assert(inconsistent(v)); + bool vilb = d_variables.cmpAssignmentLowerBound(v) < 0; + int sgn = vilb ? 1 : -1; + Constraint c = vilb ? + d_variables.getLowerBoundConstraint(v) : d_variables.getUpperBoundConstraint(v); + d_errInfo.set(v, ErrorInformation(v, c, sgn)); + ErrorInformation& ei = d_errInfo.get(v); + + switch(getSelectionRule()){ + case MINIMUM_AMOUNT: + case MAXIMUM_AMOUNT: + ei.setAmount(computeDiff(v)); + break; + case SUM_METRIC: + ei.setMetric(sumMetric(ei.getVariable())); + break; + case VAR_ORDER: + //do nothing + break; + } + ei.setInFocus(true); + FocusSetHandle handle = d_focus.push(v); + ei.setHandle(handle); +} + +void ErrorSet::dropFromFocus(ArithVar v) { + Assert(inError(v)); + ErrorInformation& ei = d_errInfo.get(v); + Assert(ei.inFocus()); + d_focus.erase(ei.getHandle()); + ei.setInFocus(false); + d_outOfFocus.push_back(v); +} + +void ErrorSet::addBackIntoFocus(ArithVar v) { + Assert(inError(v)); + ErrorInformation& ei = d_errInfo.get(v); + Assert(!ei.inFocus()); + switch(getSelectionRule()){ + case MINIMUM_AMOUNT: + case MAXIMUM_AMOUNT: + ei.setAmount(computeDiff(v)); + break; + case SUM_METRIC: + ei.setMetric(sumMetric(v)); + break; + case VAR_ORDER: + //do nothing + break; + } + + ei.setInFocus(true); + FocusSetHandle handle = d_focus.push(v); + ei.setHandle(handle); +} + +void ErrorSet::blur(){ + while(!d_outOfFocus.empty()){ + ArithVar v = d_outOfFocus.back(); + d_outOfFocus.pop_back(); + + if(inError(v) && !inFocus(v)){ + addBackIntoFocus(v); + } + } +} + + + +int ErrorSet::popSignal() { + ArithVar back = d_signals.back(); + d_signals.pop_back(); + + if(inError(back)){ + ErrorInformation& ei = d_errInfo.get(back); + int prevSgn = ei.sgn(); + int focusSgn = ei.focusSgn(); + bool vilb = d_variables.cmpAssignmentLowerBound(back) < 0; + bool viub = d_variables.cmpAssignmentUpperBound(back) > 0; + if(vilb || viub){ + Assert(!vilb || !viub); + int currSgn = vilb ? 1 : -1; + if(currSgn != prevSgn){ + Constraint curr = vilb ? d_variables.getLowerBoundConstraint(back) + : d_variables.getUpperBoundConstraint(back); + ei.reset(curr, currSgn); + } + update(ei); + }else{ + transitionVariableOutOfError(back); + } + return focusSgn; + }else if(inconsistent(back)){ + transitionVariableIntoError(back); + } + return 0; +} + +void ErrorSet::clear(){ + // Nothing should be relaxed! + d_signals.clear(); + d_errInfo.purge(); + d_focus.clear(); +} + +void ErrorSet::clearFocus(){ + for(ErrorSet::focus_iterator i =focusBegin(), i_end = focusEnd(); i != i_end; ++i){ + ArithVar f = *i; + ErrorInformation& fei = d_errInfo.get(f); + fei.setInFocus(false); + d_outOfFocus.push_back(f); + } + d_focus.clear(); +} + +void ErrorSet::reduceToSignals(){ + for(error_iterator ei=errorBegin(), ei_end=errorEnd(); ei != ei_end; ++ei){ + ArithVar curr = *ei; + signalVariable(curr); + } + + d_errInfo.purge(); + d_focus.clear(); + d_outOfFocus.clear(); +} + +DeltaRational ErrorSet::computeDiff(ArithVar v) const{ + Assert(inconsistent(v)); + const DeltaRational& beta = d_variables.getAssignment(v); + DeltaRational diff = d_variables.cmpAssignmentLowerBound(v) < 0 ? + d_variables.getLowerBound(v) - beta: + beta - d_variables.getUpperBound(v); + + Assert(diff.sgn() > 0); + return diff; +} + +ostream& operator<<(ostream& out, ErrorSelectionRule rule) { + switch(rule) { + case VAR_ORDER: + out << "VAR_ORDER"; + break; + case MINIMUM_AMOUNT: + out << "MINIMUM_AMOUNT"; + break; + case MAXIMUM_AMOUNT: + out << "MAXIMUM_AMOUNT"; + break; + case SUM_METRIC: + out << "SUM_METRIC"; + break; + } + + return out; +} + +void ErrorSet::debugPrint(std::ostream& out) const { + static int instance = 0; + ++instance; + out << "error set debugprint " << instance << endl; + for(error_iterator i = errorBegin(), i_end = errorEnd(); + i != i_end; ++i){ + ArithVar e = *i; + const ErrorInformation& ei = d_errInfo[e]; + ei.print(out); + out << " "; + d_variables.printModel(e, out); + out << endl; + } + out << "focus "; + for(focus_iterator i = focusBegin(), i_end = focusEnd(); + i != i_end; ++i){ + out << *i << " "; + } + out << ";" << endl; +} + +void ErrorSet::focusDownToJust(ArithVar v) { + clearFocus(); + + ErrorInformation& vei = d_errInfo.get(v); + vei.setInFocus(true); + FocusSetHandle handle = d_focus.push(v); + vei.setHandle(handle); +} + +void ErrorSet::pushErrorInto(ArithVarVec& vec) const{ + for(error_iterator i = errorBegin(), e = errorEnd(); i != e; ++i ){ + vec.push_back(*i); + } +} + +void ErrorSet::pushFocusInto(ArithVarVec& vec) const{ + for(focus_iterator i = focusBegin(), e = focusEnd(); i != e; ++i ){ + vec.push_back(*i); + } +} + +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ |