FCSimplex branch merge

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 */