#include <vector>
#include <stdint.h>
#include <limits>
+#include <ext/hash_map>
namespace CVC4 {
namespace theory {
//static const ArithVar ARITHVAR_SENTINEL = std::numeric_limits<ArithVar>::max();
#define ARITHVAR_SENTINEL std::numeric_limits<ArithVar>::max()
-struct ArithVarAttrID{};
-typedef expr::Attribute<ArithVarAttrID,uint64_t> ArithVarAttr;
+//Maps from Nodes -> ArithVars, and vice versa
+typedef __gnu_cxx::hash_map<Node, ArithVar, NodeHashFunction> NodeToArithVarMap;
+typedef __gnu_cxx::hash_map<ArithVar, Node> ArithVarToNodeMap;
-inline bool hasArithVar(TNode x){
- return x.hasAttribute(ArithVarAttr());
-}
-
-inline ArithVar asArithVar(TNode x){
- Assert(hasArithVar(x));
- Assert(x.getAttribute(ArithVarAttr()) <= ARITHVAR_SENTINEL);
- return x.getAttribute(ArithVarAttr());
-}
-
-inline void setArithVar(TNode x, ArithVar a){
- Assert(!hasArithVar(x));
- return x.setAttribute(ArithVarAttr(), (uint64_t)a);
-}
inline Node mkRationalNode(const Rational& q){
return NodeManager::currentNM()->mkConst<Rational>(q);
size_t size() const {
return d_list.size();
}
+ bool empty() const {
+ return d_list.empty();
+ }
size_t allocated() const {
return d_posVector.size();
return true;
}
+RowVector::~RowVector(){
+ NonZeroIterator curr = beginNonZero();
+ NonZeroIterator end = endNonZero();
+ for(;curr != end; ++curr){
+ ArithVar v = getArithVar(*curr);
+ Assert(d_rowCount[v] >= 1);
+ --(d_rowCount[v]);
+ }
+}
+
bool RowVector::noZeroCoefficients(const VarCoeffArray& arr){
for(NonZeroIterator curr = arr.begin(), end = arr.end();
curr != end; ++curr){
void RowVector::printRow(){
for(NonZeroIterator i = beginNonZero(); i != endNonZero(); ++i){
ArithVar nb = getArithVar(*i);
- Debug("tableau") << "{" << nb << "," << getCoefficient(*i) << "}";
+ Debug("row::print") << "{" << nb << "," << getCoefficient(*i) << "}";
}
- Debug("tableau") << std::endl;
+ Debug("row::print") << std::endl;
}
ReducedRowVector::ReducedRowVector(ArithVar basic,
Assert(wellFormed());
}
+
+
+Node ReducedRowVector::asEquality(const ArithVarToNodeMap& map) const{
+ using namespace CVC4::kind;
+
+ Assert(size() >= 2);
+ Node sum = Node::null();
+ if(size() > 2){
+ NodeBuilder<> sumBuilder(PLUS);
+
+ for(NonZeroIterator i = beginNonZero(); i != endNonZero(); ++i){
+ ArithVar nb = getArithVar(*i);
+ if(nb == basic()) continue;
+ Node var = (map.find(nb))->second;
+ Node coeff = mkRationalNode(getCoefficient(*i));
+
+ Node mult = NodeBuilder<2>(MULT) << coeff << var;
+ sumBuilder << mult;
+ }
+ sum = sumBuilder;
+ }else{
+ Assert(size() == 2);
+ NonZeroIterator i = beginNonZero();
+ if(getArithVar(*i) == basic()){
+ ++i;
+ }
+ Assert(getArithVar(*i) != basic());
+ Node var = (map.find(getArithVar(*i)))->second;
+ Node coeff = mkRationalNode(getCoefficient(*i));
+ sum = NodeBuilder<2>(MULT) << coeff << var;
+ }
+ Node basicVar = (map.find(basic()))->second;
+ return NodeBuilder<2>(EQUAL) << basicVar << sum;
+}
const std::vector< Rational >& coefficients,
std::vector<uint32_t>& counts);
+ ~RowVector();
/** Returns the number of nonzero variables in the vector. */
uint32_t size() const {
void pivot(ArithVar x_j);
void substitute(const ReducedRowVector& other);
+
+ /**
+ * Returns the reduced row as an equality with
+ * the basic variable on the lhs equal to the sum of the non-basics variables.
+ * The mapped from ArithVars to Nodes is specificied by map.
+ */
+ Node asEquality(const ArithVarToNodeMap& map) const;
}; /* class ReducedRowVector */
using namespace CVC4::theory;
using namespace CVC4::theory::arith;
+Tableau::~Tableau(){
+ while(!d_activeBasicVars.empty()){
+ ArithVar curr = *(d_activeBasicVars.begin());
+ ReducedRowVector* vec = removeRow(curr);
+ delete vec;
+ }
+}
+
void Tableau::addRow(ArithVar basicVar,
const std::vector<Rational>& coeffs,
const std::vector<ArithVar>& variables){
d_rowsTable(),
d_basicManager(bm)
{}
+ ~Tableau();
void increaseSize(){
d_activeBasicVars.increaseSize();
case kind::VARIABLE: {
ArithVar var = asArithVar(n);
+ if(d_removedRows.find(var) != d_removedRows.end()){
+ Node eq = d_removedRows.find(var)->second;
+ Assert(n == eq[0]);
+ Node rhs = eq[1];
+ return getValue(rhs, engine);
+ }
+
DeltaRational drat = d_partialModel.getAssignment(var);
const Rational& delta = d_partialModel.getDelta();
Debug("getValue") << n << " " << drat << " " << delta << endl;
// It appears that this can happen after other variables have been removed!
// Tread carefullty with this one.
+ bool noRow = false;
+
if(!d_basicManager.isMember(v)){
ArithVar basic = findShortestBasicRow(v);
if(basic == ARITHVAR_SENTINEL){
- //Case 3) do nothing else.
- //TODO think hard about if this is okay...
- //Probably wrecks havoc with model generation
- //*feh* DO IT ANYWAYS!
- return;
+ noRow = true;
+ }else{
+ Assert(basic != ARITHVAR_SENTINEL);
+ d_tableau.pivot(basic, v);
}
-
- AlwaysAssert(basic != ARITHVAR_SENTINEL);
- d_tableau.pivot(basic, v);
}
- Assert(d_basicManager.isMember(v));
+ if(d_basicManager.isMember(v)){
+ Assert(!noRow);
+ Assert(d_basicManager.isMember(v));
+
+ //remove the row from the tableau
+ ReducedRowVector* row = d_tableau.removeRow(v);
+ Node eq = row->asEquality(d_arithVarToNodeMap);
- //remove the row from the tableau
- ReducedRowVector* row = d_tableau.removeRow(v);
- d_removedRows[v] = row;
+ if(Debug.isOn("row::print")) row->printRow();
+ Debug("arith::permanentlyRemoveVariable") << eq << endl;
+ delete row;
+
+ Assert(d_removedRows.find(v) == d_removedRows.end());
+ d_removedRows[v] = eq;
+ }
- Debug("arith::permanentlyRemoveVariable") << v << " died an ignoble death."<< endl;
+ Debug("arith::permanentlyRemoveVariable") << "Permanently removed variable "
+ << v << ":" << asNode(v) << endl;
++(d_statistics.d_permanentlyRemovedVariables);
}
std::vector<Node> d_variables;
- std::map<ArithVar, ReducedRowVector*> d_removedRows;
+ /**
+ * If ArithVar v maps to the node n in d_removednode,
+ * then n = (= asNode(v) rhs) where rhs is a term that
+ * can be used to determine the value of n uysing getValue().
+ */
+ std::map<ArithVar, Node> d_removedRows;
/**
* Priority Queue of the basic variables that may be inconsistent.
ArithVarSet d_basicManager;
ArithVarSet d_userVariables;
+ /**
+ * Bidirectional map between Nodes and ArithVars.
+ */
+ NodeToArithVarMap d_nodeToArithVarMap;
+ ArithVarToNodeMap d_arithVarToNodeMap;
+
+ inline bool hasArithVar(TNode x) const {
+ return d_nodeToArithVarMap.find(x) != d_nodeToArithVarMap.end();
+ //return x.hasAttribute(ArithVarAttr());
+ }
+
+ inline ArithVar asArithVar(TNode x) const{
+ Assert(hasArithVar(x));
+ Assert((d_nodeToArithVarMap.find(x))->second <= ARITHVAR_SENTINEL);
+ return (d_nodeToArithVarMap.find(x))->second;
+ }
+ inline Node asNode(ArithVar a) const{
+ Assert(d_arithVarToNodeMap.find(a) != d_arithVarToNodeMap.end());
+ return (d_arithVarToNodeMap.find(a))->second;
+ }
+
+ inline void setArithVar(TNode x, ArithVar a){
+ Assert(!hasArithVar(x));
+ Assert(d_arithVarToNodeMap.find(a) == d_arithVarToNodeMap.end());
+ d_arithVarToNodeMap[a] = x;
+ d_nodeToArithVarMap[x] = a;
+ }
+
/**
* List of all of the inequalities asserted in the current context.
*/
projects / cvc5.git / commitdiff