summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/arith/Makefile.am1
-rw-r--r--src/theory/arith/arithvar.cpp13
-rw-r--r--src/theory/arith/arithvar.h7
-rw-r--r--src/theory/arith/arithvar_node_map.h31
-rw-r--r--src/theory/arith/congruence_manager.cpp2
-rw-r--r--src/theory/arith/constraint.cpp48
-rw-r--r--src/theory/arith/constraint.h20
-rw-r--r--src/theory/arith/linear_equality.cpp19
-rw-r--r--src/theory/arith/linear_equality.h7
-rw-r--r--src/theory/arith/matrix.cpp16
-rw-r--r--src/theory/arith/matrix.h76
-rw-r--r--src/theory/arith/theory_arith.cpp168
-rw-r--r--src/theory/arith/theory_arith.h27
-rwxr-xr-xsrc/theory/quantifiers/inst_strategy_cbqi.cpp18
-rw-r--r--src/util/dense_map.h22
15 files changed, 347 insertions, 128 deletions
diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index b2d1b9f09..76d8d9083 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -9,6 +9,7 @@ libarith_la_SOURCES = \
theory_arith_type_rules.h \
type_enumerator.h \
arithvar.h \
+ arithvar.cpp \
arith_rewriter.h \
arith_rewriter.cpp \
arith_static_learner.h \
diff --git a/src/theory/arith/arithvar.cpp b/src/theory/arith/arithvar.cpp
new file mode 100644
index 000000000..76b143fff
--- /dev/null
+++ b/src/theory/arith/arithvar.cpp
@@ -0,0 +1,13 @@
+
+#include "theory/arith/arithvar.h"
+#include <limits>
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+const ArithVar ARITHVAR_SENTINEL = std::numeric_limits<ArithVar>::max();
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/arith/arithvar.h b/src/theory/arith/arithvar.h
index eac238cba..95614a011 100644
--- a/src/theory/arith/arithvar.h
+++ b/src/theory/arith/arithvar.h
@@ -22,24 +22,23 @@
#ifndef __CVC4__THEORY__ARITH__ARITHVAR_H
#define __CVC4__THEORY__ARITH__ARITHVAR_H
-#include <limits>
#include <ext/hash_map>
#include "expr/node.h"
#include "context/cdhashset.h"
-#include "context/cdhashset.h"
#include "util/index.h"
+#include "util/dense_map.h"
namespace CVC4 {
namespace theory {
namespace arith {
typedef Index ArithVar;
-const ArithVar ARITHVAR_SENTINEL = std::numeric_limits<ArithVar>::max();
+extern const ArithVar ARITHVAR_SENTINEL;
//Maps from Nodes -> ArithVars, and vice versa
typedef __gnu_cxx::hash_map<Node, ArithVar, NodeHashFunction> NodeToArithVarMap;
-typedef __gnu_cxx::hash_map<ArithVar, Node> ArithVarToNodeMap;
+typedef DenseMap<Node> ArithVarToNodeMap;
/**
* ArithVarCallBack provides a mechanism for agreeing on callbacks while
diff --git a/src/theory/arith/arithvar_node_map.h b/src/theory/arith/arithvar_node_map.h
index 3a2cff236..e0e589e57 100644
--- a/src/theory/arith/arithvar_node_map.h
+++ b/src/theory/arith/arithvar_node_map.h
@@ -40,31 +40,50 @@ private:
ArithVarToNodeMap d_arithVarToNodeMap;
public:
+
+ typedef ArithVarToNodeMap::const_iterator var_iterator;
+
ArithVarNodeMap() {}
inline bool hasArithVar(TNode x) const {
return d_nodeToArithVarMap.find(x) != d_nodeToArithVarMap.end();
}
+ inline bool hasNode(ArithVar a) const {
+ return d_arithVarToNodeMap.isKey(a);
+ }
+
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;
+ Assert(hasNode(a));
+ return d_arithVarToNodeMap[a];
}
inline void setArithVar(TNode x, ArithVar a){
Assert(!hasArithVar(x));
- Assert(d_arithVarToNodeMap.find(a) == d_arithVarToNodeMap.end());
- d_arithVarToNodeMap[a] = x;
+ Assert(!d_arithVarToNodeMap.isKey(a));
+ d_arithVarToNodeMap.set(a, x);
d_nodeToArithVarMap[x] = a;
}
- const ArithVarToNodeMap& getArithVarToNodeMap() const {
- return d_arithVarToNodeMap;
+ inline void remove(ArithVar x){
+ Assert(hasNode(x));
+ Node node = asNode(x);
+
+ d_nodeToArithVarMap.erase(d_nodeToArithVarMap.find(node));
+ d_arithVarToNodeMap.remove(x);
+ }
+
+ var_iterator var_begin() const {
+ return d_arithVarToNodeMap.begin();
+ }
+ var_iterator var_end() const {
+ return d_arithVarToNodeMap.end();
}
};/* class ArithVarNodeMap */
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 5ee250c09..de4c7eac3 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -272,7 +272,7 @@ void ArithCongruenceManager::addWatchedPair(ArithVar s, TNode x, TNode y){
d_watchedVariables.add(s);
Node eq = x.eqNode(y);
- d_watchedEqualities[s] = eq;
+ d_watchedEqualities.set(s, eq);
}
void ArithCongruenceManager::assertionToEqualityEngine(bool isEquality, ArithVar s, TNode reason){
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 392d04f6c..cf3aeafee 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -371,6 +371,10 @@ void ConstraintValue::setAssertedToTheTheory(TNode witness) {
d_database->pushAssertionOrderWatch(this, witness);
}
+// bool ConstraintValue::isPsuedoConstraint() const {
+// return d_proof == d_database->d_psuedoConstraintProof;
+// }
+
bool ConstraintValue::isSelfExplaining() const {
return d_proof == d_database->d_selfExplainingProof;
}
@@ -481,6 +485,9 @@ ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Co
d_equalityEngineProof = d_proofs.size();
d_proofs.push_back(NullConstraint);
+
+ // d_psuedoConstraintProof = d_proofs.size();
+ // d_proofs.push_back(NullConstraint);
}
Constraint ConstraintDatabase::getConstraint(ArithVar v, ConstraintType t, const DeltaRational& r){
@@ -566,8 +573,32 @@ ConstraintDatabase::Statistics::~Statistics(){
}
void ConstraintDatabase::addVariable(ArithVar v){
- Assert(v == d_varDatabases.size());
- d_varDatabases.push_back(new PerVariableDatabase(v));
+ if(d_reclaimable.isMember(v)){
+ SortedConstraintMap& scm = getVariableSCM(v);
+
+ std::vector<Constraint> constraintList;
+
+ for(SortedConstraintMapIterator i = scm.begin(), end = scm.end(); i != end; ++i){
+ (i->second).push_into(constraintList);
+ }
+ while(!constraintList.empty()){
+ Constraint c = constraintList.back();
+ constraintList.pop_back();
+ Assert(c->safeToGarbageCollect());
+ delete c;
+ }
+ Assert(scm.empty());
+
+ d_reclaimable.remove(v);
+ }else{
+ Assert(v == d_varDatabases.size());
+ d_varDatabases.push_back(new PerVariableDatabase(v));
+ }
+}
+
+void ConstraintDatabase::removeVariable(ArithVar v){
+ Assert(!d_reclaimable.isMember(v));
+ d_reclaimable.add(v);
}
bool ConstraintValue::safeToGarbageCollect() const{
@@ -802,6 +833,13 @@ void ConstraintValue::impliedBy(const std::vector<Constraint>& b){
}
}
+// void ConstraintValue::setPsuedoConstraint(){
+// Assert(truthIsUnknown());
+// Assert(!hasLiteral());
+
+// d_database->pushProofWatch(this, d_database->d_psuedoConstraintProof);
+// }
+
void ConstraintValue::setEqualityEngineProof(){
Assert(truthIsUnknown());
Assert(hasLiteral());
@@ -818,6 +856,7 @@ void ConstraintValue::markAsTrue(){
void ConstraintValue::markAsTrue(Constraint imp){
Assert(truthIsUnknown());
Assert(imp->hasProof());
+ //Assert(!imp->isPsuedoConstraint());
d_database->d_proofs.push_back(NullConstraint);
d_database->d_proofs.push_back(imp);
@@ -829,6 +868,8 @@ void ConstraintValue::markAsTrue(Constraint impA, Constraint impB){
Assert(truthIsUnknown());
Assert(impA->hasProof());
Assert(impB->hasProof());
+ //Assert(!impA->isPsuedoConstraint());
+ //Assert(!impB->isPsuedoConstraint());
d_database->d_proofs.push_back(NullConstraint);
d_database->d_proofs.push_back(impA);
@@ -845,6 +886,7 @@ void ConstraintValue::markAsTrue(const vector<Constraint>& a){
for(vector<Constraint>::const_iterator i = a.begin(), end = a.end(); i != end; ++i){
Constraint c_i = *i;
Assert(c_i->hasProof());
+ //Assert(!c_i->isPsuedoConstraint());
d_database->d_proofs.push_back(c_i);
}
@@ -861,6 +903,7 @@ SortedConstraintMap& ConstraintValue::constraintSet() const{
bool ConstraintValue::proofIsEmpty() const{
Assert(hasProof());
bool result = d_database->d_proofs[d_proof] == NullConstraint;
+ //Assert((!result) || isSelfExplaining() || hasEqualityEngineProof() || isPsuedoConstraint());
Assert((!result) || isSelfExplaining() || hasEqualityEngineProof());
return result;
}
@@ -869,6 +912,7 @@ void ConstraintValue::explainBefore(NodeBuilder<>& nb, AssertionOrder order) con
Assert(hasProof());
Assert(!isSelfExplaining() || assertedToTheTheory());
+
if(assertedBefore(order)){
nb << getWitness();
}else if(hasEqualityEngineProof()){
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 331fd2bcb..52aa5a5ce 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -485,6 +485,15 @@ public:
void setEqualityEngineProof();
bool hasEqualityEngineProof() const;
+
+ /**
+ * There cannot be a literal associated with this constraint.
+ * The explanation is the constant true.
+ * explainInto() does nothing.
+ */
+ //void setPsuedoConstraint();
+ //bool isPsuedoConstraint() const;
+
/**
* Returns a explanation of the constraint that is appropriate for conflicts.
*
@@ -694,6 +703,14 @@ private:
*/
ProofId d_equalityEngineProof;
+ /**
+ * Marks a node as being true always.
+ * This is only okay for purely internal things.
+ *
+ * This is a special proof that is always a member of the list.
+ */
+ //ProofId d_psuedoConstraintProof;
+
typedef context::CDList<Constraint, ConstraintValue::ProofCleanup> ProofCleanupList;
typedef context::CDList<Constraint, ConstraintValue::CanBePropagatedCleanup> CBPList;
typedef context::CDList<Constraint, ConstraintValue::AssertionOrderCleanup> AOList;
@@ -817,6 +834,7 @@ public:
void addVariable(ArithVar v);
bool variableDatabaseIsSetup(ArithVar v) const;
+ void removeVariable(ArithVar v);
Node eeExplain(ConstConstraint c) const;
void eeExplain(ConstConstraint c, NodeBuilder<>& nb) const;
@@ -881,6 +899,8 @@ public:
private:
void raiseUnateConflict(Constraint ant, Constraint cons);
+ DenseSet d_reclaimable;
+
class Statistics {
public:
IntStat d_unatePropagateCalls;
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index 360e45289..5063a05c7 100644
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -80,7 +80,7 @@ void LinearEqualityModule::update(ArithVar x_i, const DeltaRational& v){
if(Debug.isOn("paranoid:check_tableau")){ debugCheckTableau(); }
}
-void LinearEqualityModule::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v){
+void LinearEqualityModule::pivotAndUpdate(ArithVar x_i, ArithVar x_j, const DeltaRational& v){
Assert(x_i != x_j);
TimerStat::CodeTimer codeTimer(d_statistics.d_pivotTime);
@@ -188,6 +188,23 @@ void LinearEqualityModule::debugCheckTableau(){
Assert(sum == shouldBe);
}
}
+bool LinearEqualityModule::debugEntireLinEqIsConsistent(const string& s){
+ bool result = true;
+ for(ArithVar var = 0, end = d_tableau.getNumColumns(); var != end; ++var){
+ // for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){
+ //ArithVar var = d_arithvarNodeMap.asArithVar(*i);
+ if(!d_partialModel.assignmentIsConsistent(var)){
+ d_partialModel.printModel(var);
+ Warning() << s << ":" << "Assignment is not consistent for " << var ;
+ if(d_tableau.isBasic(var)){
+ Warning() << " (basic)";
+ }
+ Warning() << endl;
+ result = false;
+ }
+ }
+ return result;
+}
DeltaRational LinearEqualityModule::computeBound(ArithVar basic, bool upperBound){
DeltaRational sum(0,0);
diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h
index f337ef0db..7df5ee9c3 100644
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -79,7 +79,7 @@ public:
* and then pivots x_i with the nonbasic variable in its row x_j.
* Updates the assignment of the other basic variables accordingly.
*/
- void pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v);
+ void pivotAndUpdate(ArithVar x_i, ArithVar x_j, const DeltaRational& v);
ArithPartialModel& getPartialModel() const{ return d_partialModel; }
@@ -141,6 +141,11 @@ public:
/** Debugging information for a pivot. */
void debugPivot(ArithVar x_i, ArithVar x_j);
+ /**
+ *
+ */
+ bool debugEntireLinEqIsConsistent(const std::string& s);
+
private:
/** These fields are designed to be accessible to TheoryArith methods. */
diff --git a/src/theory/arith/matrix.cpp b/src/theory/arith/matrix.cpp
index 8e7fe7894..cd7a8a9aa 100644
--- a/src/theory/arith/matrix.cpp
+++ b/src/theory/arith/matrix.cpp
@@ -247,7 +247,7 @@ void Tableau::rowPivot(ArithVar basicOld, ArithVar basicNew){
d_basic2RowIndex.remove(basicOld);
d_basic2RowIndex.set(basicNew, rid);
- d_rowIndex2basic[rid] = basicNew;
+ d_rowIndex2basic.set(rid, basicNew);
}
// void Tableau::addEntry(ArithVar row, ArithVar col, const Rational& coeff){
@@ -397,10 +397,11 @@ void Tableau::addRow(ArithVar basic,
RowIndex newRow = Matrix<Rational>::addRow(coefficients, variables);
addEntry(newRow, basic, Rational(-1));
- Assert(d_rowIndex2basic.size() == newRow);
+ Assert(!d_basic2RowIndex.isKey(basic));
+ Assert(!d_rowIndex2basic.isKey(newRow));
d_basic2RowIndex.set(basic, newRow);
- d_rowIndex2basic.push_back(basic);
+ d_rowIndex2basic.set(newRow, basic);
if(Debug.isOn("matrix")){ printMatrix(); }
@@ -558,6 +559,15 @@ void ReducedRowVector::enqueueNonBasicVariablesAndCoefficients(std::vector< Arit
// return newId;
// }
+void Tableau::removeBasicRow(ArithVar basic){
+ RowIndex rid = basicToRowIndex(basic);
+
+ removeRow(rid);
+ d_basic2RowIndex.remove(basic);
+ d_rowIndex2basic.remove(rid);
+
+}
+
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
diff --git a/src/theory/arith/matrix.h b/src/theory/arith/matrix.h
index ea6c389b9..027397b6a 100644
--- a/src/theory/arith/matrix.h
+++ b/src/theory/arith/matrix.h
@@ -25,6 +25,7 @@
#include "util/dense_map.h"
#include "theory/arith/arithvar.h"
+#include "theory/arith/arithvar_node_map.h"
#include "theory/arith/normal_form.h"
#include <queue>
@@ -377,6 +378,8 @@ protected:
uint32_t d_entriesInUse;
MatrixEntryVector<T> d_entries;
+ std::vector<RowIndex> d_pool;
+
T d_zero;
public:
@@ -446,6 +449,23 @@ protected:
d_entries.freeEntry(id);
}
+ private:
+ RowIndex requestRowIndex(){
+ if(d_pool.empty()){
+ RowIndex ridx = d_rows.size();
+ d_rows.push_back(RowVectorT(&d_entries));
+ return ridx;
+ }else{
+ RowIndex rid = d_pool.back();
+ d_pool.pop_back();
+ return rid;
+ }
+ }
+
+ void releaseRowIndex(RowIndex rid){
+ d_pool.push_back(rid);
+ }
+
public:
size_t getNumRows() const {
@@ -485,8 +505,11 @@ public:
*/
RowIndex addRow(const std::vector<T>& coeffs,
const std::vector<ArithVar>& variables){
- RowIndex ridx = d_rows.size();
- d_rows.push_back(RowVectorT(&d_entries));
+
+ RowIndex ridx = requestRowIndex();
+
+ //RowIndex ridx = d_rows.size();
+ //d_rows.push_back(RowVectorT(&d_entries));
std::vector<Rational>::const_iterator coeffIter = coeffs.begin();
std::vector<ArithVar>::const_iterator varsIter = variables.begin();
@@ -701,36 +724,7 @@ public:
EntryID id = i.getID();
removeEntry(id);
}
- }
-
-
- Node rowAsEquality(RowIndex rid, const ArithVarToNodeMap& map){
- using namespace CVC4::kind;
-
- Assert(getRowLength(rid) >= 2);
-
- std::vector<Node> pairs;
- for(RowIterator i = getRow(rid); !i.atEnd(); ++i){
- const Entry& entry = *i;
- ArithVar colVar = entry.getColVar();
-
- Node var = (map.find(colVar))->second;
- Node coeff = mkRationalNode(entry.getCoefficient());
-
- Node mult = NodeBuilder<2>(MULT) << coeff << var;
- pairs.push_back(mult);
- }
-
- Node sum = Node::null();
- if(pairs.size() == 1 ){
- sum = pairs.front();
- }else{
- Assert(pairs.size() >= 2);
- NodeBuilder<> sumBuilder(PLUS);
- sumBuilder.append(pairs);
- sum = sumBuilder;
- }
- return NodeBuilder<2>(EQUAL) << sum << mkRationalNode(d_zero);
+ releaseRowIndex(rid);
}
double densityMeasure() const{
@@ -754,6 +748,15 @@ public:
}
}
+ void loadSignQueries(RowIndex rid, DenseMap<int>& target) const{
+
+ RowIterator i = getRow(rid).begin(), i_end = getRow(rid).end();
+ for(; i != i_end; ++i){
+ const MatrixEntry<T>& entry = *i;
+ target.set(entry.getColVar(), entry.getCoefficient().sgn());
+ }
+ }
+
protected:
uint32_t numNonZeroEntries() const { return size(); }
@@ -833,8 +836,10 @@ private:
// Set of all of the basic variables in the tableau.
// ArithVarMap<RowIndex> : ArithVar |-> RowIndex
BasicToRowMap d_basic2RowIndex;
+
// RowIndex |-> Basic Variable
- std::vector<ArithVar> d_rowIndex2basic;
+ typedef DenseMap<ArithVar> RowIndexToBasicMap;
+ RowIndexToBasicMap d_rowIndex2basic;
public:
@@ -882,10 +887,6 @@ public:
return getRow(basicToRowIndex(basic)).begin();
}
- // RowIterator rowIterator(RowIndex r) const {
- // return getRow(r).begin();
- // }
-
/**
* Adds a row to the tableau.
* The new row is equivalent to:
@@ -911,7 +912,6 @@ public:
void removeBasicRow(ArithVar basic);
-
private:
/* Changes the basic variable on the row for basicOld to basicNew. */
void rowPivot(ArithVar basicOld, ArithVar basicNew);
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index d2814348a..f036e20fd 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -62,6 +62,8 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha
d_unknownsInARow(0),
d_hasDoneWorkSinceCut(false),
d_learner(u),
+ d_numberOfVariables(0),
+ d_pool(),
d_setupLiteralCallback(this),
d_assertionsThatDoNotMatchTheirLiterals(c),
d_nextIntegerCheckVar(0),
@@ -79,6 +81,7 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha
d_tableauResetPeriod(10),
d_conflicts(c),
d_raiseConflict(d_conflicts),
+ d_tempVarMalloc(*this),
d_congruenceManager(c, d_constraintDatabase, d_setupLiteralCallback, d_arithvarNodeMap, d_raiseConflict),
d_simplex(d_linEq, d_raiseConflict),
d_constraintDatabase(c, u, d_arithvarNodeMap, d_congruenceManager, d_raiseConflict),
@@ -822,8 +825,9 @@ void TheoryArith::setupVariable(const Variable& x){
Assert(!isSetup(n));
++(d_statistics.d_statUserVariables);
- ArithVar varN = requestArithVar(n,false);
- setupInitialValue(varN);
+ requestArithVar(n,false);
+ //ArithVar varN = requestArithVar(n,false);
+ //setupInitialValue(varN);
markSetup(n);
@@ -860,8 +864,9 @@ void TheoryArith::setupVariableList(const VarList& vl){
d_nlIncomplete = true;
++(d_statistics.d_statUserVariables);
- ArithVar av = requestArithVar(vlNode, false);
- setupInitialValue(av);
+ requestArithVar(vlNode, false);
+ //ArithVar av = requestArithVar(vlNode, false);
+ //setupInitialValue(av);
markSetup(vlNode);
}
@@ -1054,7 +1059,7 @@ void TheoryArith::setupPolynomial(const Polynomial& poly) {
ArithVar varSlack = requestArithVar(polyNode, true);
d_tableau.addRow(varSlack, coefficients, variables);
- setupInitialValue(varSlack);
+ setupBasicValue(varSlack);
//Add differences to the difference manager
Polynomial::iterator i = poly.begin(), end = poly.end();
@@ -1125,6 +1130,14 @@ void TheoryArith::preRegisterTerm(TNode n) {
Debug("arith::preregister") << "end arith::preRegisterTerm("<< n <<")" << endl;
}
+void TheoryArith::releaseArithVar(ArithVar v){
+ Assert(d_arithvarNodeMap.hasNode(v));
+
+ d_constraintDatabase.removeVariable(v);
+ d_arithvarNodeMap.remove(v);
+
+ d_pool.push_back(v);
+}
ArithVar TheoryArith::requestArithVar(TNode x, bool slack){
//TODO : The VarList trick is good enough?
@@ -1135,32 +1148,73 @@ ArithVar TheoryArith::requestArithVar(TNode x, bool slack){
Assert(!d_arithvarNodeMap.hasArithVar(x));
Assert(x.getType().isReal());// real or integer
- ArithVar varX = d_variables.size();
- d_variables.push_back(Node(x));
- Debug("integers") << "isInteger[[" << x << "]]: " << x.getType().isInteger() << endl;
+ // ArithVar varX = d_variables.size();
+ // d_variables.push_back(Node(x));
+
+ bool reclaim = !d_pool.empty();
+ ArithVar varX;
+
+ if(reclaim){
+ varX = d_pool.back();
+ d_pool.pop_back();
+
+ d_partialModel.setAssignment(varX, d_DELTA_ZERO, d_DELTA_ZERO);
+ }else{
+ varX = d_numberOfVariables;
+ ++d_numberOfVariables;
+
+ d_slackVars.push_back(true);
+ d_variableTypes.push_back(ATReal);
+ d_simplex.increaseMax();
+
+ d_tableau.increaseSize();
+ d_tableauSizeHasBeenModified = true;
+
+ d_partialModel.initialize(varX, d_DELTA_ZERO);
+ }
+
+ ArithType type;
if(slack){
//The type computation is not quite accurate for Rationals that are integral.
//We'll use the isIntegral check from the polynomial package instead.
Polynomial p = Polynomial::parsePolynomial(x);
- d_variableTypes.push_back(p.isIntegral() ? ATInteger : ATReal);
+ type = p.isIntegral() ? ATInteger : ATReal;
}else{
- d_variableTypes.push_back(nodeToArithType(x));
+ type = nodeToArithType(x);
}
+ d_variableTypes[varX] = type;
+ d_slackVars[varX] = slack;
- d_slackVars.push_back(slack);
-
- d_simplex.increaseMax();
+ d_constraintDatabase.addVariable(varX);
d_arithvarNodeMap.setArithVar(x,varX);
- d_tableau.increaseSize();
- d_tableauSizeHasBeenModified = true;
+ // Debug("integers") << "isInteger[[" << x << "]]: " << x.getType().isInteger() << endl;
- d_constraintDatabase.addVariable(varX);
+ // if(slack){
+ // //The type computation is not quite accurate for Rationals that are integral.
+ // //We'll use the isIntegral check from the polynomial package instead.
+ // Polynomial p = Polynomial::parsePolynomial(x);
+ // d_variableTypes.push_back(p.isIntegral() ? ATInteger : ATReal);
+ // }else{
+ // d_variableTypes.push_back(nodeToArithType(x));
+ // }
+
+ // d_slackVars.push_back(slack);
+
+ // d_simplex.increaseMax();
+
+ // d_tableau.increaseSize();
+ // d_tableauSizeHasBeenModified = true;
+
+ // d_constraintDatabase.addVariable(varX);
Debug("arith::arithvar") << x << " |-> " << varX << endl;
+ Assert(!d_partialModel.hasUpperBound(varX));
+ Assert(!d_partialModel.hasLowerBound(varX));
+
return varX;
}
@@ -1179,18 +1233,7 @@ void TheoryArith::asVectors(const Polynomial& p, std::vector<Rational>& coeffs,
Assert(theoryOf(n) != THEORY_ARITH || d_arithvarNodeMap.hasArithVar(n));
Assert(d_arithvarNodeMap.hasArithVar(n));
- ArithVar av;
- // The first if is likely dead is likely dead code:
- // if (theoryOf(n) != THEORY_ARITH && !d_arithvarNodeMap.hasArithVar(n)) {
- // // The only way not to get it through pre-register is if it's a foreign term
- // ++(d_statistics.d_statUserVariables);
- // av = requestArithVar(n,false);
- // setupInitialValue(av);
- // } else {
- // // Otherwise, we already have it's variable
- // av = d_arithvarNodeMap.asArithVar(n);
- // }
- av = d_arithvarNodeMap.asArithVar(n);
+ ArithVar av = d_arithvarNodeMap.asArithVar(n);
coeffs.push_back(constant.getValue());
variables.push_back(av);
@@ -1200,11 +1243,12 @@ void TheoryArith::asVectors(const Polynomial& p, std::vector<Rational>& coeffs,
/* Requirements:
* For basic variables the row must have been added to the tableau.
*/
-void TheoryArith::setupInitialValue(ArithVar x){
+void TheoryArith::setupBasicValue(ArithVar x){
+ Assert(d_tableau.isBasic(x));
- if(!d_tableau.isBasic(x)){
- d_partialModel.initialize(x, d_DELTA_ZERO);
- }else{
+ // if(!d_tableau.isBasic(x)){
+ // d_partialModel.setAssignment(x, d_DELTA_ZERO, d_DELTA_ZERO);
+ // }else{
//If the variable is basic, assertions may have already happened and updates
//may have occured before setting this variable up.
@@ -1212,9 +1256,11 @@ void TheoryArith::setupInitialValue(ArithVar x){
//time instead of register
DeltaRational safeAssignment = d_linEq.computeRowValue(x, true);
DeltaRational assignment = d_linEq.computeRowValue(x, false);
- d_partialModel.initialize(x,safeAssignment);
- d_partialModel.setAssignment(x,assignment);
- }
+ //d_partialModel.initialize(x,safeAssignment);
+ //d_partialModel.setAssignment(x,assignment);
+ d_partialModel.setAssignment(x,safeAssignment,assignment);
+
+ // }
Debug("arith") << "setupVariable("<<x<<")"<<std::endl;
}
@@ -1254,8 +1300,8 @@ Node TheoryArith::dioCutting(){
context::Context::ScopedPush speculativePush(getSatContext());
//DO NOT TOUCH THE OUTPUTSTREAM
- //TODO: Improve this
- for(ArithVar v = 0, end = d_variables.size(); v != end; ++v){
+ for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
+ ArithVar v = *vi;
if(isInteger(v)){
const DeltaRational& dr = d_partialModel.getAssignment(v);
if(d_partialModel.equalsUpperBound(v, dr) || d_partialModel.equalsLowerBound(v, dr)){
@@ -1485,7 +1531,8 @@ bool TheoryArith::assertionCases(Constraint constraint){
* If this returns true, all integer variables have an integer assignment.
*/
bool TheoryArith::hasIntegerModel(){
- if(d_variables.size() > 0){
+ //if(d_variables.size() > 0){
+ if(getNumberOfVariables()){
const ArithVar rrEnd = d_nextIntegerCheckVar;
do {
//Do not include slack variables
@@ -1495,7 +1542,7 @@ bool TheoryArith::hasIntegerModel(){
return false;
}
}
- } while((d_nextIntegerCheckVar = (1 + d_nextIntegerCheckVar == d_variables.size() ? 0 : 1 + d_nextIntegerCheckVar)) != rrEnd);
+ } while((d_nextIntegerCheckVar = (1 + d_nextIntegerCheckVar == getNumberOfVariables() ? 0 : 1 + d_nextIntegerCheckVar)) != rrEnd);
}
return true;
}
@@ -1576,6 +1623,7 @@ void TheoryArith::check(Effort effortLevel){
Assert(d_conflicts.empty());
d_qflraStatus = d_simplex.findModel(fullEffort(effortLevel));
+
switch(d_qflraStatus){
case Result::SAT:
if(newFacts){
@@ -1822,7 +1870,8 @@ bool TheoryArith::splitDisequalities(){
*/
void TheoryArith::debugPrintAssertions() {
Debug("arith::print_assertions") << "Assertions:" << endl;
- for (ArithVar i = 0; i < d_variables.size(); ++ i) {
+ for (var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
+ ArithVar i = *vi;
if (d_partialModel.hasLowerBound(i)) {
Constraint lConstr = d_partialModel.getLowerBoundConstraint(i);
Debug("arith::print_assertions") << lConstr << endl;
@@ -1842,13 +1891,15 @@ void TheoryArith::debugPrintAssertions() {
void TheoryArith::debugPrintModel(){
Debug("arith::print_model") << "Model:" << endl;
-
- for (ArithVar i = 0; i < d_variables.size(); ++ i) {
- Debug("arith::print_model") << d_variables[i] << " : " <<
- d_partialModel.getAssignment(i);
- if(d_tableau.isBasic(i))
- Debug("arith::print_model") << " (basic)";
- Debug("arith::print_model") << endl;
+ for (var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
+ ArithVar i = *vi;
+ if(d_arithvarNodeMap.hasNode(i)){
+ Debug("arith::print_model") << d_arithvarNodeMap.asNode(i) << " : " <<
+ d_partialModel.getAssignment(i);
+ if(d_tableau.isBasic(i))
+ Debug("arith::print_model") << " (basic)";
+ Debug("arith::print_model") << endl;
+ }
}
}
@@ -2057,7 +2108,8 @@ Rational TheoryArith::deltaValueForTotalOrder() const{
relevantDeltaValues.insert(val);
}
- for(ArithVar v = 0; v < d_variables.size(); ++v){
+ for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
+ ArithVar v = *vi;
const DeltaRational& value = d_partialModel.getAssignment(v);
relevantDeltaValues.insert(value);
if( d_partialModel.hasLowerBound(v)){
@@ -2108,7 +2160,8 @@ void TheoryArith::collectModelInfo( TheoryModel* m, bool fullModel ){
// TODO:
// This is not very good for user push/pop....
// Revisit when implementing push/pop
- for(ArithVar v = 0; v < d_variables.size(); ++v){
+ for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
+ ArithVar v = *vi;
if(!isSlackVariable(v)){
Node term = d_arithvarNodeMap.asNode(v);
@@ -2187,13 +2240,13 @@ void TheoryArith::notifyRestart(){
}
bool TheoryArith::entireStateIsConsistent(const string& s){
- typedef std::vector<Node>::const_iterator VarIter;
bool result = true;
- for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){
- ArithVar var = d_arithvarNodeMap.asArithVar(*i);
+ for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
+ ArithVar var = *vi;
+ //ArithVar var = d_arithvarNodeMap.asArithVar(*i);
if(!d_partialModel.assignmentIsConsistent(var)){
d_partialModel.printModel(var);
- Warning() << s << ":" << "Assignment is not consistent for " << var << *i;
+ Warning() << s << ":" << "Assignment is not consistent for " << var << d_arithvarNodeMap.asNode(var);
if(d_tableau.isBasic(var)){
Warning() << " (basic)";
}
@@ -2205,15 +2258,14 @@ bool TheoryArith::entireStateIsConsistent(const string& s){
}
bool TheoryArith::unenqueuedVariablesAreConsistent(){
- typedef std::vector<Node>::const_iterator VarIter;
bool result = true;
- for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){
- ArithVar var = d_arithvarNodeMap.asArithVar(*i);
+ for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
+ ArithVar var = *vi;
if(!d_partialModel.assignmentIsConsistent(var)){
if(!d_simplex.debugIsInCollectionQueue(var)){
d_partialModel.printModel(var);
- Warning() << "Unenqueued var is not consistent for " << var << *i;
+ Warning() << "Unenqueued var is not consistent for " << var << d_arithvarNodeMap.asNode(var);
if(d_tableau.isBasic(var)){
Warning() << " (basic)";
}
@@ -2221,7 +2273,7 @@ bool TheoryArith::unenqueuedVariablesAreConsistent(){
result = false;
} else if(Debug.isOn("arith::consistency::initial")){
d_partialModel.printModel(var);
- Warning() << "Initial var is not consistent for " << var << *i;
+ Warning() << "Initial var is not consistent for " << var << d_arithvarNodeMap.asNode(var);
if(d_tableau.isBasic(var)){
Warning() << " (basic)";
}
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index b791186cf..7d1150fb1 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -89,17 +89,20 @@ private:
/** Static learner. */
ArithStaticLearner d_learner;
- /**
- * List of the variables in the system.
- * This is needed to keep a positive ref count on slack variables.
- */
- std::vector<Node> d_variables;
+
+ ArithVar d_numberOfVariables;
+ inline ArithVar getNumberOfVariables() const { return d_numberOfVariables; }
+ std::vector<ArithVar> d_pool;
+ void releaseArithVar(ArithVar v);
/**
* The map between arith variables to nodes.
*/
ArithVarNodeMap d_arithvarNodeMap;
+ typedef ArithVarNodeMap::var_iterator var_iterator;
+ var_iterator var_begin() const { return d_arithvarNodeMap.var_begin(); }
+ var_iterator var_end() const { return d_arithvarNodeMap.var_end(); }
NodeSet d_setupNodes;
bool isSetup(Node n) const {
@@ -273,6 +276,18 @@ private:
void outputConflicts();
+ class TempVarMalloc : public ArithVarMalloc {
+ private:
+ TheoryArith& d_ta;
+ public:
+ TempVarMalloc(TheoryArith& ta) : d_ta(ta) {}
+ ArithVar request(){
+ Node skolem = mkRealSkolem("tmpVar");
+ return d_ta.requestArithVar(skolem, false);
+ }
+ void release(ArithVar v){ d_ta.releaseArithVar(v); }
+ } d_tempVarMalloc;
+
/**
* A copy of the tableau.
* This is equivalent to the original tableau if d_tableauSizeHasBeenModified
@@ -433,7 +448,7 @@ private:
ArithVar requestArithVar(TNode x, bool slack);
/** Initial (not context dependent) sets up for a variable.*/
- void setupInitialValue(ArithVar x);
+ void setupBasicValue(ArithVar x);
/** Initial (not context dependent) sets up for a new slack variable.*/
void setupSlack(TNode left);
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index d79ddee31..ddf763b73 100755
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -46,11 +46,12 @@ void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort
d_tableaux.clear();
d_ceTableaux.clear();
//search for instantiation rows in simplex tableaux
- ArithVarToNodeMap avtnm = d_th->d_arithvarNodeMap.getArithVarToNodeMap();
- for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){
- ArithVar x = (*it).first;
+ ArithVarNodeMap& avnm = d_th->d_arithvarNodeMap;
+ ArithVarNodeMap::var_iterator vi, vend;
+ for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){
+ ArithVar x = *vi;
if( d_th->d_partialModel.hasEitherBound( x ) ){
- Node n = (*it).second;
+ Node n = avnm.asNode(x);
Node f;
NodeBuilder<> t(kind::PLUS);
if( n.getKind()==PLUS ){
@@ -167,10 +168,11 @@ void InstStrategySimplex::addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder
}
void InstStrategySimplex::debugPrint( const char* c ){
- ArithVarToNodeMap avtnm = d_th->d_arithvarNodeMap.getArithVarToNodeMap();
- for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){
- ArithVar x = (*it).first;
- Node n = (*it).second;
+ const ArithVarNodeMap& avnm = d_th->d_arithvarNodeMap;
+ ArithVarNodeMap::var_iterator vi, vend;
+ for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){
+ ArithVar x = *vi;
+ Node n = avnm.asNode(x);
//if( ((TheoryArith*)getTheory())->d_partialModel.hasEitherBound( x ) ){
Debug(c) << x << " : " << n << ", bounds = ";
if( d_th->d_partialModel.hasLowerBound( x ) ){
diff --git a/src/util/dense_map.h b/src/util/dense_map.h
index fa78e6787..222a761c3 100644
--- a/src/util/dense_map.h
+++ b/src/util/dense_map.h
@@ -151,6 +151,7 @@ public:
pop_back();
}
+ /** Returns the key at the back of a non-empty list.*/
Key back() const {
return d_list.back();
}
@@ -164,6 +165,27 @@ public:
d_list.pop_back();
}
+
+ /** Adds at least a constant fraction of the elements in the current map to another map. */
+ void splitInto(DenseMap<T>& target){
+ uint32_t targetSize = size()/2;
+ while(size() > targetSize){
+ Key key = back();
+ target.set(key, get(key));
+ pop_back();
+ }
+ }
+
+ /** Adds the current target map to the current map.*/
+ void addAll(const DenseMap<T>& target){
+ for(const_iterator i = target.begin(), e = target.end(); i != e; ++i){
+ Key k = *i;
+ set(k, target[k]);
+ }
+ }
+
+
+
private:
size_t allocated() const {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback