diff options
author | Tim King <taking@cs.nyu.edu> | 2014-03-07 18:00:37 -0500 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2014-03-07 18:00:52 -0500 |
commit | 9ccdea06edbc72e3ecd282e9e015f6fc4b2e7173 (patch) | |
tree | cde6138cb9ab6ef0b7c15edf42e3e8cc53637002 /src/theory/arith/partial_model.h | |
parent | 42be934ef4d4430944ae9074c7202a7d130c75bb (diff) |
Merging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into master. See the CAV14 submission for an explanation of the changes to the integer solver's behavior. If compiled against the our custom extension of glpk, https://github.com/timothy-king/glpk-cut-log, this should have substantial differences in behavior. This should have moderate performance differences for linear real and integer arithmetic even if these features are disabled.
Diffstat (limited to 'src/theory/arith/partial_model.h')
-rw-r--r-- | src/theory/arith/partial_model.h | 189 |
1 files changed, 82 insertions, 107 deletions
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index c497adb75..33af3d4ef 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -9,10 +9,11 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief [[ Add one-line brief description here ]] + ** \brief Datastructures that track variable by variable information. ** - ** [[ Add lengthier description here ]] - ** \todo document this file + ** This is a datastructure that tracks variable specific information. + ** This is partially context dependent to back track upper/lower bounds + ** and information derived from these. **/ #include "cvc4_private.h" @@ -50,40 +51,44 @@ private: ArithVar d_var; DeltaRational d_assignment; - Constraint d_lb; - Constraint d_ub; + ConstraintP d_lb; + ConstraintP d_ub; int d_cmpAssignmentLB; int d_cmpAssignmentUB; unsigned d_pushCount; ArithType d_type; Node d_node; - bool d_slack; + bool d_auxiliary; public: VarInfo(); bool setAssignment(const DeltaRational& r, BoundsInfo& prev); - bool setLowerBound(Constraint c, BoundsInfo& prev); - bool setUpperBound(Constraint c, BoundsInfo& prev); + bool setLowerBound(ConstraintP c, BoundsInfo& prev); + bool setUpperBound(ConstraintP c, BoundsInfo& prev); /** Returns true if this VarInfo has been initialized. */ bool initialized() const; /** * Initializes the VarInfo with the ArithVar index it is associated with, - * the node that the variable represents, and whether it is a slack variable. + * the node that the variable represents, and whether it is an auxillary + * variable. */ - void initialize(ArithVar v, Node n, bool slack); + void initialize(ArithVar v, Node n, bool aux); + /** Uninitializes the VarInfo. */ void uninitialize(); bool canBeReclaimed() const; - /** Indicator variables for if the assignment is equal to the upper and lower bounds. */ + /** Indicator variables for if the assignment is equal to the upper + * and lower bounds. */ BoundCounts atBoundCounts() const; - /** Combination of indicator variables for whether it has upper and lower bounds. */ + /** Combination of indicator variables for whether it has upper and + * lower bounds. */ BoundCounts hasBoundCounts() const; /** Stores both atBoundCounts() and hasBoundCounts(). */ @@ -92,21 +97,22 @@ private: /**Maps from ArithVar -> VarInfo */ typedef DenseMap<VarInfo> VarInfoVec; + /** This maps an ArithVar to its Variable information.*/ VarInfoVec d_vars; - // Partial Map from Arithvar -> PreviousAssignment + /** Partial Map from Arithvar -> PreviousAssignment */ DenseMap<DeltaRational> d_safeAssignment; - // if d_vars.isKey(x), then x < d_numberOfVariables + /** if d_vars.isKey(x), then x < d_numberOfVariables */ ArithVar d_numberOfVariables; /** [0, d_numberOfVariables) \intersect d_vars.keys == d_pool */ // Everything in the pool is fair game. // There must be NO outstanding assertions std::vector<ArithVar> d_pool; - std::list<ArithVar> d_released; - std::list<ArithVar>::iterator d_releasedIterator; + std::vector<ArithVar> d_released; + //std::list<ArithVar>::iterator d_releasedIterator; // Reverse Map from Node to ArithVar // Inverse of d_vars[x].d_node @@ -118,36 +124,29 @@ private: /** * If this is true, record the incoming changes to the bound information. - * If this is false, the responsibility of recording the changes is LinearEqualities's. + * If this is false, the responsibility of recording the changes is + * LinearEqualities's. */ bool d_enqueueingBoundCounts; public: - inline ArithVar getNumberOfVariables() const { - return d_numberOfVariables; - } + /** Returns the number of variables. */ + ArithVar getNumberOfVariables() const; - inline bool hasArithVar(TNode x) const { - return d_nodeToArithVarMap.find(x) != d_nodeToArithVarMap.end(); - } + /** Returns true if the node has an associated variables. */ + bool hasArithVar(TNode x) const; - inline bool hasNode(ArithVar a) const { - return d_vars.isKey(a); - } - - inline ArithVar asArithVar(TNode x) const{ - Assert(hasArithVar(x)); - Assert((d_nodeToArithVarMap.find(x))->second <= ARITHVAR_SENTINEL); - return (d_nodeToArithVarMap.find(x))->second; - } + /** Returns true if the variable has a defining node. */ + bool hasNode(ArithVar a) const; + /** Returns the ArithVar associated with a node. */ + ArithVar asArithVar(TNode x) const; - inline Node asNode(ArithVar a) const{ - Assert(hasNode(a)); - return d_vars[a].d_node; - } + /** Returns the node associated with an ArithVar. */ + Node asNode(ArithVar a) const; + /** Allocates a freshly allocated variables. */ ArithVar allocateVariable(); class var_iterator { @@ -155,68 +154,47 @@ private: const VarInfoVec* d_vars; VarInfoVec::const_iterator d_wrapped; public: - var_iterator(){} - var_iterator(const VarInfoVec* vars, VarInfoVec::const_iterator ci) - : d_vars(vars), d_wrapped(ci) - { - nextInitialized(); - } - - var_iterator& operator++(){ - ++d_wrapped; - nextInitialized(); - return *this; - } - bool operator==(const var_iterator& other) const{ - return d_wrapped == other.d_wrapped; - } - bool operator!=(const var_iterator& other) const{ - return d_wrapped != other.d_wrapped; - } - ArithVar operator*() const{ - return *d_wrapped; - } + var_iterator(); + var_iterator(const VarInfoVec* vars, VarInfoVec::const_iterator ci); + var_iterator& operator++(); + + bool operator==(const var_iterator& other) const; + bool operator!=(const var_iterator& other) const; + ArithVar operator*() const; + private: - void nextInitialized(){ - VarInfoVec::const_iterator end = d_vars->end(); - while(d_wrapped != end && - !((*d_vars)[*d_wrapped].initialized())){ - ++d_wrapped; - } - } + void nextInitialized(); }; - var_iterator var_begin() const { - return var_iterator(&d_vars, d_vars.begin()); - } - var_iterator var_end() const { - return var_iterator(&d_vars, d_vars.end()); - } + var_iterator var_begin() const; + var_iterator var_end() const; bool canBeReleased(ArithVar v) const; void releaseArithVar(ArithVar v); void attemptToReclaimReleased(); - bool isInteger(ArithVar x) const { - return d_vars[x].d_type >= ATInteger; - } - bool isSlack(ArithVar x) const { - return d_vars[x].d_slack; - } + /** Is this variable guaranteed to have an integer assignment? + * (Should agree with the type system.) */ + bool isInteger(ArithVar x) const; - bool integralAssignment(ArithVar x) const { - return getAssignment(x).isIntegral(); - } + /** Is the assignment to x integral? */ + bool integralAssignment(ArithVar x) const; + + /* Is this variable defined as a linear sum of other variables? */ + bool isAuxiliary(ArithVar x) const; + + /* Is the variable both input and not auxiliary? */ + bool isIntegerInput(ArithVar x) const; private: - typedef std::pair<ArithVar, Constraint> AVCPair; + typedef std::pair<ArithVar, ConstraintP> AVCPair; class LowerBoundCleanUp { private: ArithVariables* d_pm; public: - LowerBoundCleanUp(ArithVariables* pm) : d_pm(pm) {} + LowerBoundCleanUp(ArithVariables* pm); void operator()(AVCPair* restore); }; @@ -224,7 +202,7 @@ private: private: ArithVariables* d_pm; public: - UpperBoundCleanUp(ArithVariables* pm) : d_pm(pm) {} + UpperBoundCleanUp(ArithVariables* pm); void operator()(AVCPair* restore); }; @@ -255,27 +233,27 @@ public: * This sets the lower bound for a variable in the current context. * This must be stronger the previous constraint. */ - void setLowerBoundConstraint(Constraint lb); + void setLowerBoundConstraint(ConstraintP lb); /** * This sets the upper bound for a variable in the current context. * This must be stronger the previous constraint. */ - void setUpperBoundConstraint(Constraint ub); + void setUpperBoundConstraint(ConstraintP ub); /** Returns the constraint for the upper bound of a variable. */ - inline Constraint getUpperBoundConstraint(ArithVar x) const{ + inline ConstraintP getUpperBoundConstraint(ArithVar x) const{ return d_vars[x].d_ub; } /** Returns the constraint for the lower bound of a variable. */ - inline Constraint getLowerBoundConstraint(ArithVar x) const{ + inline ConstraintP getLowerBoundConstraint(ArithVar x) const{ return d_vars[x].d_lb; } /* Initializes a variable to a safe value.*/ - void initialize(ArithVar x, Node n, bool slack); + void initialize(ArithVar x, Node n, bool aux); - ArithVar allocate(Node n, bool slack = false); + ArithVar allocate(Node n, bool aux = false); /* Gets the last assignment to a variable that is known to be consistent. */ const DeltaRational& getSafeAssignment(ArithVar x) const; @@ -288,13 +266,8 @@ public: void commitAssignmentChanges(); - inline bool lowerBoundIsZero(ArithVar x){ - return hasLowerBound(x) && getLowerBound(x).sgn() == 0; - } - - inline bool upperBoundIsZero(ArithVar x){ - return hasUpperBound(x) && getUpperBound(x).sgn() == 0; - } + bool lowerBoundIsZero(ArithVar x); + bool upperBoundIsZero(ArithVar x); bool boundsAreEqual(ArithVar x) const; @@ -393,17 +366,12 @@ public: const Rational& getDelta(); - inline void invalidateDelta() { - d_deltaIsSafe = false; - } + void invalidateDelta(); - void setDelta(const Rational& d){ - d_delta = d; - d_deltaIsSafe = true; - } + void setDelta(const Rational& d); - void startQueueingBoundCounts(){ d_enqueueingBoundCounts = true; } - void stopQueueingBoundCounts(){ d_enqueueingBoundCounts = false; } + void startQueueingBoundCounts(); + void stopQueueingBoundCounts(); void addToBoundQueue(ArithVar v, const BoundsInfo& prev); BoundsInfo selectBoundsInfo(ArithVar v, bool old) const; @@ -413,6 +381,15 @@ public: void printEntireModel(std::ostream& out) const; + + /** + * Precondition: assumes boundsAreEqual(x). + * If the either the lower/ upper bound is an equality, eq, + * this returns make_pair(eq, NullConstraint). + * Otherwise, this returns make_pair(lb, ub). + */ + std::pair<ConstraintP, ConstraintP> explainEqualBounds(ArithVar x) const; + private: /** @@ -423,9 +400,7 @@ private: bool debugEqualSizes(); - bool inMaps(ArithVar x) const{ - return x < getNumberOfVariables(); - } + bool inMaps(ArithVar x) const; };/* class ArithVariables */ |