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.h | |
parent | a9174ce4dc3939bbe14c9aa1fd11c79c7877eb16 (diff) |
FCSimplex branch merge
Diffstat (limited to 'src/theory/arith/error_set.h')
-rw-r--r-- | src/theory/arith/error_set.h | 407 |
1 files changed, 407 insertions, 0 deletions
diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h new file mode 100644 index 000000000..ce6412573 --- /dev/null +++ b/src/theory/arith/error_set.h @@ -0,0 +1,407 @@ +/********************* */ +/*! \file arith_priority_queue.h + ** \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 "cvc4_private.h" + +#pragma once + +#include "theory/arith/arithvar.h" +#include "theory/arith/bound_counts.h" +#include "theory/arith/delta_rational.h" +#include "theory/arith/partial_model.h" +#include "theory/arith/arith_heuristic_pivot_rule.h" +#include "theory/arith/tableau_sizes.h" + +#include "util/statistics_registry.h" +//#include <boost/heap/d_ary_heap.hpp> +#include <ext/pb_ds/priority_queue.hpp> + +#include <vector> + +namespace CVC4 { +namespace theory { +namespace arith { + + +/** + * The priority queue has 3 different modes of operation: + * - Collection + * This passively collects arithmetic variables that may be inconsistent. + * This does not maintain any heap structure. + * dequeueInconsistentBasicVariable() does not work in this mode! + * Entering this mode requires the queue to be empty. + * + * - Difference Queue + * This mode uses the difference between a variables and its bound + * to determine which to dequeue first. + * + * - Variable Order Queue + * This mode uses the variable order to determine which ArithVar is dequeued first. + * + * The transitions between the modes of operation are: + * Collection => Difference Queue + * Difference Queue => Variable Order Queue + * Difference Queue => Collection (queue must be empty!) + * Variable Order Queue => Collection (queue must be empty!) + * + * The queue begins in Collection mode. + */ + + +class ErrorSet; +class ErrorInfoMap; + +class ComparatorPivotRule { +private: + const ErrorSet* d_errorSet; + + ErrorSelectionRule d_rule; +public: + ComparatorPivotRule(); + ComparatorPivotRule(const ErrorSet* es, ErrorSelectionRule r); + + bool operator()(ArithVar v, ArithVar u) const; + ErrorSelectionRule getRule() const { return d_rule; } +}; + +// typedef boost::heap::d_ary_heap< +// ArithVar, +// boost::heap::arity<2>, +// boost::heap::compare<ComparatorPivotRule>, +// boost::heap::mutable_<true> > FocusSet; +// +// typedef FocusSet::handle_type FocusSetHandle; + +typedef __gnu_pbds::priority_queue< + ArithVar, + ComparatorPivotRule, + __gnu_pbds::pairing_heap_tag> FocusSet; + +typedef FocusSet::point_iterator FocusSetHandle; + +class ErrorInformation { +private: + /** The variable that is in error. */ + ArithVar d_variable; + + /** + * The constraint that was violated. + * This needs to be saved in case that the + * violated constraint + */ + Constraint d_violated; + + /** + * This is the sgn of the first derivate the variable must move to satisfy + * the bound violated. + * If d_sgn > 0, then d_violated was a lowerbound. + * If d_sgn < 0, then d_violated was an upperbound. + */ + int d_sgn; + + /** + * If this is true, then the bound is no longer set on d_variables. + * This MUST be undone before this is deleted. + */ + bool d_relaxed; + + /** + * If this is true, then the variable is in the focus set and the focus heap. + * d_handle is then a reasonable thing to interpret. + * If this is false, the variable is somewhere in + */ + bool d_inFocus; + FocusSetHandle d_handle; + + /** + * Auxillary information for storing the difference between a variable and its bound. + * Only set on signals. + */ + DeltaRational* d_amount; + + /** */ + uint32_t d_metric; + +public: + ErrorInformation(); + ErrorInformation(ArithVar var, Constraint vio, int sgn); + ~ErrorInformation(); + ErrorInformation(const ErrorInformation& ei); + ErrorInformation& operator=(const ErrorInformation& ei); + + void reset(Constraint c, int sgn); + + inline ArithVar getVariable() const { return d_variable; } + + bool isRelaxed() const { return d_relaxed; } + void setRelaxed(){ Assert(!d_relaxed); d_relaxed = true; } + void setUnrelaxed(){ Assert(d_relaxed); d_relaxed = false; } + + inline int sgn() const { return d_sgn; } + + inline bool inFocus() const { return d_inFocus; } + inline int focusSgn() const { + return (d_inFocus) ? sgn() : 0; + } + + inline void setInFocus(bool inFocus) { d_inFocus = inFocus; } + + const DeltaRational& getAmount() const { + Assert(d_amount != NULL); + return *d_amount; + } + + void setAmount(const DeltaRational& am); + void setMetric(uint32_t m) { d_metric = m; } + uint32_t getMetric() const { return d_metric; } + + inline void setHandle(FocusSetHandle h) { + Assert(d_inFocus); + d_handle = h; + } + inline const FocusSetHandle& getHandle() const{ return d_handle; } + + inline Constraint getViolated() const { return d_violated; } + + bool debugInitialized() const { + return + d_variable != ARITHVAR_SENTINEL && + d_violated != NullConstraint && + d_sgn != 0; + } + void print(std::ostream& os) const { + os << "{ErrorInfo: " << d_variable + << ", " << d_violated + << ", " << d_sgn + << ", " << d_relaxed + << ", " << d_inFocus; + if(d_amount == NULL){ + os << "NULL"; + }else{ + os << (*d_amount); + } + os << "}"; + } +}; + +class ErrorInfoMap : public DenseMap<ErrorInformation> {}; + +class ErrorSet { +private: + /** + * Reference to the arithmetic partial model for checking if a variable + * is consistent with its upper and lower bounds. + */ + ArithVariables& d_variables; + + /** + * The set of all variables that violate exactly one of their bounds. + */ + ErrorInfoMap d_errInfo; + + ErrorSelectionRule d_selectionRule; + /** + * The ordered heap for the variables that are in ErrorSet. + */ + FocusSet d_focus; + + + /** + * A strict subset of the error set. + * d_outOfFocus \neq d_errInfo. + * + * Its symbolic complement is Focus. + * d_outOfFocus \intersect Focus == \emptyset + * d_outOfFocus \union Focus == d_errInfo + */ + ArithVarVec d_outOfFocus; + + /** + * Before a variable is added to the error set, it is added to the signals list. + * A variable may appear on the list multiple times. + * This introduces a delay. + */ + ArithVarVec d_signals; + + TableauSizes d_tableauSizes; + + BoundCountingLookup d_boundLookup; + + /** + * Computes the difference between the assignment and its bound for x. + */ +public: + DeltaRational computeDiff(ArithVar x) const; +private: + void recomputeAmount(ErrorInformation& ei, ErrorSelectionRule r); + + void update(ErrorInformation& ei); + void transitionVariableOutOfError(ArithVar v); + void transitionVariableIntoError(ArithVar v); + void addBackIntoFocus(ArithVar v); + +public: + + /** The new focus set is the entire error set. */ + void blur(); + void dropFromFocus(ArithVar v); + + void dropFromFocusAll(const ArithVarVec& vec) { + for(ArithVarVec::const_iterator i = vec.begin(), i_end = vec.end(); i != i_end; ++i){ + ArithVar v = *i; + dropFromFocus(v); + } + } + + ErrorSet(ArithVariables& var, TableauSizes tabSizes, BoundCountingLookup boundLookup); + + typedef ErrorInfoMap::const_iterator error_iterator; + error_iterator errorBegin() const { return d_errInfo.begin(); } + error_iterator errorEnd() const { return d_errInfo.end(); } + + bool inError(ArithVar v) const { return d_errInfo.isKey(v); } + bool inFocus(ArithVar v) const { return d_errInfo[v].inFocus(); } + + void pushErrorInto(ArithVarVec& vec) const; + void pushFocusInto(ArithVarVec& vec) const; + + ErrorSelectionRule getSelectionRule() const; + void setSelectionRule(ErrorSelectionRule rule); + + inline ArithVar topFocusVariable() const{ + Assert(!focusEmpty()); + return d_focus.top(); + } + + inline void signalVariable(ArithVar var){ + d_signals.push_back(var); + } + + inline void signalUnderCnd(ArithVar var, bool b){ + if(b){ signalVariable(var); } + } + + inline bool inconsistent(ArithVar var) const{ + return !d_variables.assignmentIsConsistent(var) ; + } + inline void signalIfInconsistent(ArithVar var){ + signalUnderCnd(var, inconsistent(var)); + } + + inline bool errorEmpty() const{ + return d_errInfo.empty(); + } + inline uint32_t errorSize() const{ + return d_errInfo.size(); + } + + inline bool focusEmpty() const { + return d_focus.empty(); + } + inline uint32_t focusSize() const{ + return d_focus.size(); + } + + inline int getSgn(ArithVar x) const { + Assert(inError(x)); + return d_errInfo[x].sgn(); + } + inline int focusSgn(ArithVar v) const { + if(inError(v)){ + return d_errInfo[v].focusSgn(); + }else{ + return 0; + } + } + + void focusDownToJust(ArithVar v); + + void clearFocus(); + + /** Clears the set. */ + void clear(); + void reduceToSignals(); + + bool noSignals() const { + return d_signals.empty(); + } + bool moreSignals() const { + return !noSignals(); + } + ArithVar topSignal() const { + Assert(moreSignals()); + return d_signals.back(); + } + + /** + * Moves a variable out of the signals. + * This moves it into the error set. + * Return the previous focus sign. + */ + int popSignal(); + + const DeltaRational& getAmount(ArithVar v) const { + return d_errInfo[v].getAmount(); + } + + uint32_t sumMetric(ArithVar a) const{ + Assert(inError(a)); + BoundCounts bcs = d_boundLookup.boundCounts(a); + uint32_t count = getSgn(a) > 0 ? bcs.atUpperBounds() : bcs.atLowerBounds(); + + uint32_t length = d_tableauSizes.getRowLength(a); + + return (length - count); + } + + uint32_t getMetric(ArithVar a) const { + return d_errInfo[a].getMetric(); + } + + Constraint getViolated(ArithVar a) const { + return d_errInfo[a].getViolated(); + } + + + typedef FocusSet::const_iterator focus_iterator; + focus_iterator focusBegin() const { return d_focus.begin(); } + focus_iterator focusEnd() const { return d_focus.end(); } + + void debugPrint(std::ostream& out) const; + +private: + class Statistics { + public: + IntStat d_enqueues; + IntStat d_enqueuesCollection; + IntStat d_enqueuesDiffMode; + IntStat d_enqueuesVarOrderMode; + + IntStat d_enqueuesCollectionDuplicates; + IntStat d_enqueuesVarOrderModeDuplicates; + + Statistics(); + ~Statistics(); + }; + + Statistics d_statistics; +}; + +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ |