summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/theory/arith/arith_utilities.h20
-rw-r--r--src/theory/arith/arithvar_set.h3
-rw-r--r--src/theory/arith/row_vector.cpp48
-rw-r--r--src/theory/arith/row_vector.h8
-rw-r--r--src/theory/arith/tableau.cpp8
-rw-r--r--src/theory/arith/tableau.h1
-rw-r--r--src/theory/arith/theory_arith.cpp42
-rw-r--r--src/theory/arith/theory_arith.h35
8 files changed, 133 insertions, 32 deletions
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 6a9102a19..2053379d9 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -28,6 +28,7 @@
#include <vector>
#include <stdint.h>
#include <limits>
+#include <ext/hash_map>
namespace CVC4 {
namespace theory {
@@ -38,23 +39,10 @@ typedef uint32_t ArithVar;
//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);
diff --git a/src/theory/arith/arithvar_set.h b/src/theory/arith/arithvar_set.h
index 95617c5a0..de215696e 100644
--- a/src/theory/arith/arithvar_set.h
+++ b/src/theory/arith/arithvar_set.h
@@ -54,6 +54,9 @@ public:
size_t size() const {
return d_list.size();
}
+ bool empty() const {
+ return d_list.empty();
+ }
size_t allocated() const {
return d_posVector.size();
diff --git a/src/theory/arith/row_vector.cpp b/src/theory/arith/row_vector.cpp
index 6486077fb..07fc0186d 100644
--- a/src/theory/arith/row_vector.cpp
+++ b/src/theory/arith/row_vector.cpp
@@ -21,6 +21,16 @@ bool RowVector::isSorted(const VarCoeffArray& arr, bool strictlySorted) {
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){
@@ -149,9 +159,9 @@ void RowVector::addRowTimesConstant(const Rational& c, const RowVector& other){
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,
@@ -193,3 +203,37 @@ void ReducedRowVector::pivot(ArithVar x_j){
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;
+}
diff --git a/src/theory/arith/row_vector.h b/src/theory/arith/row_vector.h
index 05ceeb986..2b48564a4 100644
--- a/src/theory/arith/row_vector.h
+++ b/src/theory/arith/row_vector.h
@@ -89,6 +89,7 @@ public:
const std::vector< Rational >& coefficients,
std::vector<uint32_t>& counts);
+ ~RowVector();
/** Returns the number of nonzero variables in the vector. */
uint32_t size() const {
@@ -195,6 +196,13 @@ public:
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 */
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
index 5f142fe8a..5ba173eb6 100644
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.cpp
@@ -24,6 +24,14 @@ using namespace CVC4;
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){
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index bd30dc13e..433f6472f 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -58,6 +58,7 @@ public:
d_rowsTable(),
d_basicManager(bm)
{}
+ ~Tableau();
void increaseSize(){
d_activeBasicVars.increaseSize();
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index dbfa86a98..9fbec23ac 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -575,6 +575,13 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) {
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;
@@ -667,28 +674,37 @@ void TheoryArith::permanentlyRemoveVariable(ArithVar v){
// 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);
}
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index fd3cf0c45..efd1adde4 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -64,7 +64,12 @@ private:
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.
@@ -88,6 +93,34 @@ private:
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.
*/
context::CDSet<Node, NodeHashFunction> d_diseq;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback