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/partial_model.h | |
parent | a9174ce4dc3939bbe14c9aa1fd11c79c7877eb16 (diff) |
FCSimplex branch merge
Diffstat (limited to 'src/theory/arith/partial_model.h')
-rw-r--r-- | src/theory/arith/partial_model.h | 277 |
1 files changed, 243 insertions, 34 deletions
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index 820b1b909..dcfe97079 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -20,53 +20,216 @@ #include "expr/node.h" #include "context/context.h" -#include "context/cdvector.h" -#include "context/cdo.h" +#include "context/cdlist.h" + #include "theory/arith/arithvar.h" +#include "theory/arith/arith_utilities.h" #include "theory/arith/delta_rational.h" #include "theory/arith/constraint_forward.h" +#include "theory/arith/callbacks.h" +#include "theory/arith/bound_counts.h" #include <vector> +#include <list> -#ifndef __CVC4__THEORY__ARITH__PARTIAL_MODEL_H -#define __CVC4__THEORY__ARITH__PARTIAL_MODEL_H +#pragma once namespace CVC4 { namespace theory { namespace arith { -class ArithPartialModel { + + +class ArithVariables { private: + class VarInfo { + friend class ArithVariables; + ArithVar d_var; + + DeltaRational d_assignment; + Constraint d_lb; + Constraint d_ub; + int d_cmpAssignmentLB; + int d_cmpAssignmentUB; + + unsigned d_pushCount; + ArithType d_type; + Node d_node; + bool d_slack; + + public: + VarInfo(); + + bool setAssignment(const DeltaRational& r, BoundCounts& prev); + bool setLowerBound(Constraint c, BoundCounts& prev); + bool setUpperBound(Constraint c, BoundCounts& prev); + + bool initialized() const { + return d_var != ARITHVAR_SENTINEL; + } + void initialize(ArithVar v, Node n, bool slack); + void uninitialize(); + + bool canBeReclaimed() const{ + return d_pushCount == 0; + } + + BoundCounts boundCounts() const { + uint32_t lbIndc = (d_cmpAssignmentLB == 0) ? 1 : 0; + uint32_t ubIndc = (d_cmpAssignmentUB == 0) ? 1 : 0; + return BoundCounts(lbIndc, ubIndc); + } + }; + + //Maps from ArithVar -> VarInfo + typedef DenseMap<VarInfo> VarInfoVec; + VarInfoVec d_vars; + + // Partial Map from Arithvar -> PreviousAssignment + DenseMap<DeltaRational> d_safeAssignment; + + // 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; + + // Reverse Map from Node to ArithVar + // Inverse of d_vars[x].d_node + NodeToArithVarMap d_nodeToArithVarMap; + + DenseMap<BoundCounts> d_atBoundsQueue; + + public: + + inline ArithVar getNumberOfVariables() const { + return d_numberOfVariables; + } + + inline bool hasArithVar(TNode x) const { + return d_nodeToArithVarMap.find(x) != d_nodeToArithVarMap.end(); + } - unsigned d_mapSize; + inline bool hasNode(ArithVar a) const { + return d_vars.isKey(a); + } - //Maps from ArithVar -> T - std::vector<bool> d_hasSafeAssignment; - std::vector<DeltaRational> d_assignment; - std::vector<DeltaRational> d_safeAssignment; + inline ArithVar asArithVar(TNode x) const{ + Assert(hasArithVar(x)); + Assert((d_nodeToArithVarMap.find(x))->second <= ARITHVAR_SENTINEL); + return (d_nodeToArithVarMap.find(x))->second; + } - context::CDVector<Constraint> d_ubc; - context::CDVector<Constraint> d_lbc; + + inline Node asNode(ArithVar a) const{ + Assert(hasNode(a)); + return d_vars[a].d_node; + } + + ArithVar allocateVariable(); + + class var_iterator { + 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; + } + private: + void nextInitialized(){ + VarInfoVec::const_iterator end = d_vars->end(); + while(d_wrapped != end && + !((*d_vars)[*d_wrapped].initialized())){ + ++d_wrapped; + } + } + }; + 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()); + } + + + 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; + } + private: + + typedef std::pair<ArithVar, Constraint> AVCPair; + class LowerBoundCleanUp { + private: + ArithVariables* d_pm; + public: + LowerBoundCleanUp(ArithVariables* pm) : d_pm(pm) {} + void operator()(AVCPair* restore); + }; + + class UpperBoundCleanUp { + private: + ArithVariables* d_pm; + public: + UpperBoundCleanUp(ArithVariables* pm) : d_pm(pm) {} + void operator()(AVCPair* restore); + }; + + typedef context::CDList<AVCPair, LowerBoundCleanUp> LBReverts; + LBReverts d_lbRevertHistory; + + typedef context::CDList<AVCPair, UpperBoundCleanUp> UBReverts; + UBReverts d_ubRevertHistory; + + void pushUpperBound(VarInfo&); + void popUpperBound(AVCPair*); + void pushLowerBound(VarInfo&); + void popLowerBound(AVCPair*); // This is true when setDelta() is called, until invalidateDelta is called bool d_deltaIsSafe; // Cache of a value of delta to ensure a total order. Rational d_delta; // Function to call if the value of delta needs to be recomputed. - RationalCallBack& d_deltaComputingFunc; - - /** - * List contains all of the variables that have an unsafe assignment. - */ - typedef std::vector<ArithVar> HistoryList; - HistoryList d_history; + DeltaComputeCallback d_deltaComputingFunc; + bool d_enqueueingBoundCounts; public: - ArithPartialModel(context::Context* c, RationalCallBack& deltaComputation); + ArithVariables(context::Context* c, DeltaComputeCallback deltaComputation); /** * This sets the lower bound for a variable in the current context. @@ -82,11 +245,11 @@ public: /** Returns the constraint for the upper bound of a variable. */ inline Constraint getUpperBoundConstraint(ArithVar x) const{ - return d_ubc[x]; + return d_vars[x].d_ub; } /** Returns the constraint for the lower bound of a variable. */ inline Constraint getLowerBoundConstraint(ArithVar x) const{ - return d_lbc[x]; + return d_vars[x].d_lb; } /** @@ -94,17 +257,20 @@ public: * This is done by forcing the lower bound to be NullConstraint. * This is an expert only operation! (See primal simplex for an example.) */ - void forceRelaxLowerBound(ArithVar x); + //void forceRelaxLowerBound(ArithVar x); /** * This forces the upper bound for a variable to be relaxed in the current context. * This is done by forcing the upper bound to be NullConstraint. * This is an expert only operation! (See primal simplex for an example.) */ - void forceRelaxUpperBound(ArithVar x); + //void forceRelaxUpperBound(ArithVar x); /* Initializes a variable to a safe value.*/ - void initialize(ArithVar x, const DeltaRational& r); + //void initialize(ArithVar x, const DeltaRational& r); + void initialize(ArithVar x, Node n, bool slack); + + ArithVar allocate(Node n, bool slack = false); /* Gets the last assignment to a variable that is known to be consistent. */ const DeltaRational& getSafeAssignment(ArithVar x) const; @@ -187,20 +353,31 @@ public: return cmpToUpperBound(x, c) >= 0; } + inline int cmpAssignmentLowerBound(ArithVar x) const{ + return d_vars[x].d_cmpAssignmentLB; + } + inline int cmpAssignmentUpperBound(ArithVar x) const{ + return d_vars[x].d_cmpAssignmentUB; + } + + inline BoundCounts boundCounts(ArithVar x) const { + return d_vars[x].boundCounts(); + } bool strictlyBelowUpperBound(ArithVar x) const; bool strictlyAboveLowerBound(ArithVar x) const; bool assignmentIsConsistent(ArithVar x) const; - void printModel(ArithVar x); + void printModel(ArithVar x, std::ostream& out) const; + void printModel(ArithVar x) const; /** returns true iff x has both a lower and upper bound. */ bool hasEitherBound(ArithVar x) const; inline bool hasLowerBound(ArithVar x) const{ - return d_lbc[x] != NullConstraint; + return d_vars[x].d_lb != NullConstraint; } inline bool hasUpperBound(ArithVar x) const{ - return d_ubc[x] != NullConstraint; + return d_vars[x].d_ub != NullConstraint; } const Rational& getDelta(); @@ -214,6 +391,41 @@ public: d_deltaIsSafe = true; } + // inline bool initialized(ArithVar x) const { + // return d_vars[x].initialized(); + // } + + void addToBoundQueue(ArithVar v, BoundCounts prev){ + if(d_enqueueingBoundCounts && !d_atBoundsQueue.isKey(v)){ + d_atBoundsQueue.set(v, prev); + } + } + + BoundCounts oldBoundCounts(ArithVar v) const { + if(d_atBoundsQueue.isKey(v)){ + return d_atBoundsQueue[v]; + }else{ + return boundCounts(v); + } + } + + void startQueueingAtBoundQueue(){ d_enqueueingBoundCounts = true; } + void stopQueueingAtBoundQueue(){ d_enqueueingBoundCounts = false; } + + void processAtBoundQueue(BoundCountsCallback& changed){ + while(!d_atBoundsQueue.empty()){ + ArithVar v = d_atBoundsQueue.back(); + BoundCounts prev = d_atBoundsQueue[v]; + d_atBoundsQueue.pop_back(); + BoundCounts curr = boundCounts(v); + if(prev != curr){ + changed(v, prev); + } + } + } + + void printEntireModel(std::ostream& out) const; + private: /** @@ -222,19 +434,16 @@ private: */ void clearSafeAssignments(bool revert); - bool equalSizes(); + bool debugEqualSizes(); bool inMaps(ArithVar x) const{ - return x < d_mapSize; + return x < getNumberOfVariables(); } -};/* class ArithPartialModel */ +};/* class ArithVariables */ }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ - - -#endif /* __CVC4__THEORY__ARITH__PARTIAL_MODEL_H */ |