1 files changed, 0 insertions, 184 deletions
diff --git a/src/theory/arith/arith_prop_manager.h b/src/theory/arith/arith_prop_manager.h
deleted file mode 100644
index 900a0ed58..000000000
--- a/src/theory/arith/arith_prop_manager.h
+++ /dev/null
@@ -1,184 +0,0 @@
-/*********************                                                        */
-/*! \file arith_prop_manager.h
- ** \verbatim
- ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** 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"
-
-#ifndef __CVC4__THEORY__ARITH__ARITH_PROP_MANAGER_H
-#define __CVC4__THEORY__ARITH__ARITH_PROP_MANAGER_H
-
-#include "theory/valuation.h"
-#include "theory/arith/arithvar.h"
-#include "theory/arith/arithvar_node_map.h"
-#include "theory/arith/atom_database.h"
-#include "theory/arith/delta_rational.h"
-#include "context/context.h"
-#include "context/cdlist.h"
-#include "context/cdhashmap.h"
-#include "context/cdo.h"
-#include "theory/rewriter.h"
-#include "util/stats.h"
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-class PropManager {
-public:
-  struct PropUnit {
-    // consequent <= antecedent
-    // i.e. the antecedent is the explanation of the consequent.
-    Node consequent;
-    Node antecedent;
-    bool flag;
-    PropUnit(Node c, Node a, bool f) :
-      consequent(c), antecedent(a), flag(f)
-    {}
-  };
-
-private:
-  context::CDList<PropUnit> d_propagated;
-  context::CDO<uint32_t> d_propagatedPos;
-
-  /* This maps the node a theory engine will request on an explain call to
-   * to its corresponding PropUnit.
-   * This is node is potentially both the consequent or Rewriter::rewrite(consequent).
-   */
-  typedef context::CDHashMap<Node, size_t, NodeHashFunction> ExplainMap;
-  ExplainMap d_explanationMap;
-
-  size_t getIndex(TNode n) const {
-    Assert(isPropagated(n));
-    return (*(d_explanationMap.find(n))).second;
-  }
-
-public:
-
-  PropManager(context::Context* c):
-    d_propagated(c),
-    d_propagatedPos(c, 0),
-    d_explanationMap(c)
-  { }
-
-  const PropUnit& getUnit(TNode n) const {
-    return d_propagated[getIndex(n)];
-  }
-
-  bool isPropagated(TNode n) const {
-    return d_explanationMap.find(n) != d_explanationMap.end();
-  }
-
-  bool isFlagged(TNode n) const {
-    return getUnit(n).flag;
-  }
-
-  void propagate(TNode n, Node reason, bool flag) {
-    Assert(!isPropagated(n));
-
-    if(flag){
-      Node rewritten =  Rewriter::rewrite(n);
-      d_explanationMap.insert(rewritten, d_propagated.size());
-    }else{
-      //If !flag, then the rewriter is idempotent on n.
-      Assert(Rewriter::rewrite(n) == n);
-    }
-    d_explanationMap.insert(n, d_propagated.size());
-    d_propagated.push_back(PropUnit(n, reason, flag));
-
-    Debug("ArithPropManager") << n  << std::endl << "<="<< reason<< std::endl;
-  }
-
-  bool hasMorePropagations() const {
-    return d_propagatedPos < d_propagated.size();
-  }
-
-  const PropUnit& getNextPropagation() {
-    Assert(hasMorePropagations());
-    const PropUnit& prop = d_propagated[d_propagatedPos];
-    d_propagatedPos = d_propagatedPos + 1;
-    return prop;
-  }
-
-  TNode explain(TNode n) const {
-    return getUnit(n).antecedent;
-  }
-
-};/* class PropManager */
-
-class ArithPropManager : public PropManager {
-private:
-  const ArithVarNodeMap& d_arithvarNodeMap;
-  const ArithAtomDatabase& d_atomDatabase;
-  Valuation d_valuation;
-
-public:
-  ArithPropManager(context::Context* c,
-                   const ArithVarNodeMap& map,
-                   const ArithAtomDatabase& db,
-                   Valuation v):
-    PropManager(c), d_arithvarNodeMap(map), d_atomDatabase(db), d_valuation(v)
-  {}
-
-  /**
-   * Returns true if the node has a value in sat solver in the current context.
-   * In debug mode this fails an Assert() if the node has a negative assignment.
-   */
-  bool isAsserted(TNode n) const;
-
-  /** Returns true if a bound was added. */
-  bool propagateArithVar(bool upperbound, ArithVar var, const DeltaRational& b, TNode reason);
-
-  Node boundAsNode(bool upperbound, ArithVar var, const DeltaRational& b) const;
-
-  Node strictlyWeakerLowerBound(TNode n) const{
-    return d_atomDatabase.getWeakerImpliedLowerBound(n);
-  }
-  Node strictlyWeakerUpperBound(TNode n) const{
-    return d_atomDatabase.getWeakerImpliedUpperBound(n);
-  }
-
-  Node strictlyWeakerAssertedUpperBound(ArithVar v, const DeltaRational& b) const;
-
-  Node strictlyWeakerAssertedLowerBound(ArithVar v, const DeltaRational& b) const;
-
-  Node getBestImpliedLowerBound(ArithVar v, const DeltaRational& b) const;
-  Node getBestImpliedUpperBound(ArithVar v, const DeltaRational& b) const;
-
-  bool containsLiteral(TNode n) const {
-    return d_atomDatabase.containsLiteral(n);
-  }
-
-private:
-  class Statistics {
-  public:
-    IntStat d_propagateArithVarCalls;
-    IntStat d_addedPropagation;
-    IntStat d_alreadySetSatLiteral;
-    IntStat d_alreadyPropagatedNode;
-
-    Statistics();
-    ~Statistics();
-  };
-  Statistics d_statistics;
-};
-
-}/* CVC4::theory::arith namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__ARITH__ARITH_PROP_MANAGER_H */