arith_rewriter.cpp \
arith_utilities.h \
arith_constants.h \
+ arith_activity.h \
delta_rational.h \
delta_rational.cpp \
partial_model.h \
--- /dev/null
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARITH__ARITH_ACTIVITY_H
+#define __CVC4__THEORY__ARITH__ARITH_ACTIVITY_H
+
+#include "expr/node.h"
+#include "expr/attribute.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+
+struct ArithActivityID {};
+typedef expr::Attribute<ArithActivityID, uint64_t> ArithActivity;
+
+inline void resetActivity(TNode var){
+ var.setAttribute(ArithActivity(), 0);
+}
+inline void initActivity(TNode var){
+ resetActivity(var);
+}
+
+inline uint64_t getActivity(TNode var){
+ return var.getAttribute(ArithActivity());
+}
+
+inline void increaseActivity(TNode var, uint64_t x){
+ Assert(var.hasAttribute(ArithActivity()));
+ uint64_t newValue = x + getActivity(var);
+ var.setAttribute(ArithActivity(), newValue);
+}
+
+const static uint64_t ACTIVITY_THRESHOLD = 100;
+
+}; /* namesapce arith */
+}; /* namespace theory */
+}; /* namespace CVC4 */
+
+
+#endif
Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
Debug("partial_model") << "setUpperBound(" << x << "," << r << ")" << endl;
+ x.setAttribute(partial_model::HasHadABound(), true);
d_UpperBoundMap[x] = r;
}
void ArithPartialModel::setLowerBound(TNode x, const DeltaRational& r){
Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
Debug("partial_model") << "setLowerBound(" << x << "," << r << ")" << endl;
+ x.setAttribute(partial_model::HasHadABound(), true);
+
d_LowerBoundMap[x] = r;
}
Debug("partial_model") << "pm: updating the assignment to" << x
<< " now " << r <<endl;
}
+void ArithPartialModel::setAssignment(TNode x, const DeltaRational& safe, const DeltaRational& r){
+ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+ Assert(x.hasAttribute(partial_model::Assignment()));
+ Assert(x.hasAttribute(partial_model::SafeAssignment()));
+
+ DeltaRational* curr = x.getAttribute(partial_model::Assignment());
+ DeltaRational* saved = x.getAttribute(partial_model::SafeAssignment());
+
+ if(safe == r){
+ if(saved != NULL){
+ x.setAttribute(partial_model::SafeAssignment(), NULL);
+ delete saved;
+ }
+ }else{
+ if(saved == NULL){
+ saved = new DeltaRational(safe);
+ x.setAttribute(partial_model::SafeAssignment(), saved);
+ }else{
+ *saved = safe;
+ }
+ d_history.push_back(x);
+ }
+ *curr = r;
+
+ Debug("partial_model") << "pm: updating the assignment to" << x
+ << " now " << r <<endl;
+}
void ArithPartialModel::initialize(TNode x, const DeltaRational& r){
Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
}
}
+bool ArithPartialModel::hasBounds(TNode x){
+ return
+ d_UpperBoundMap.find(x) != d_UpperBoundMap.end() ||
+ d_LowerBoundMap.find(x) != d_LowerBoundMap.end();
+}
+
bool ArithPartialModel::strictlyBelowUpperBound(TNode x){
DeltaRational* assign;
AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
struct TheoryArithPropagatedID {};
typedef expr::CDAttribute<TheoryArithPropagatedID, bool> TheoryArithPropagated;
+struct HasHadABoundID {};
+typedef expr::Attribute<HasHadABoundID, bool> HasHadABound;
+
}; /*namespace partial_model*/
+
void setUpperBound(TNode x, const DeltaRational& r);
void setLowerBound(TNode x, const DeltaRational& r);
/* Sets an unsafe variable assignment */
void setAssignment(TNode x, const DeltaRational& r);
+ void setAssignment(TNode x, const DeltaRational& safe, const DeltaRational& r);
+
/** Must know that the bound exists before calling this! */
DeltaRational getUpperBound(TNode x) const;
void printModel(TNode x);
+ bool hasBounds(TNode x);
+ bool hasEverHadABound(TNode var){
+ return var.getAttribute(partial_model::HasHadABound());
+ }
+
private:
/**
#include "expr/attribute.h"
#include "theory/arith/basic.h"
+#include "theory/arith/arith_activity.h"
+
#include <ext/hash_map>
#include <set>
private:
typedef __gnu_cxx::hash_map<TNode, Row*, NodeHashFunction> RowsTable;
- VarSet d_basicVars;
- RowsTable d_rows;
+ VarSet d_activeBasicVars;
+ RowsTable d_activeRows, d_inactiveRows;
public:
/**
* Constructs an empty tableau.
*/
- Tableau() : d_basicVars(), d_rows() {}
+ Tableau() : d_activeBasicVars(), d_activeRows(), d_inactiveRows() {}
VarSet::iterator begin(){
- return d_basicVars.begin();
+ return d_activeBasicVars.begin();
}
VarSet::iterator end(){
- return d_basicVars.end();
+ return d_activeBasicVars.end();
}
Row* lookup(TNode var){
- Assert(contains(var));
- return d_rows[var];
+ Assert(isActiveBasicVariable(var));
+ return d_activeRows[var];
+ }
+
+private:
+ Row* lookupEjected(TNode var){
+ Assert(isEjected(var));
+ return d_inactiveRows[var];
}
+public:
void addRow(TNode eq){
Assert(eq.getKind() == kind::EQUAL);
Assert(var.getAttribute(IsBasic()));
//The new basic variable cannot already be a basic variable
- Assert(d_basicVars.find(var) == d_basicVars.end());
- d_basicVars.insert(var);
+ Assert(!isActiveBasicVariable(var));
+ d_activeBasicVars.insert(var);
Row* row_var = new Row(var,sum);
- d_rows[var] = row_var;
+ d_activeRows[var] = row_var;
//A variable in the row may have been made non-basic already.
//If this is the case we fake pivoting this variable
Assert(child[0].getKind() == kind::CONST_RATIONAL);
TNode c = child[1];
Assert(var.getMetaKind() == kind::metakind::VARIABLE);
- if(contains(c)){
+ if(isActiveBasicVariable(c)){
Row* row_c = lookup(c);
row_var->subsitute(*row_c);
}
* a_rs != 0.
*/
void pivot(TNode x_r, TNode x_s){
- RowsTable::iterator ptrRow_r = d_rows.find(x_r);
- Assert(ptrRow_r != d_rows.end());
+ RowsTable::iterator ptrRow_r = d_activeRows.find(x_r);
+ Assert(ptrRow_r != d_activeRows.end());
Row* row_s = (*ptrRow_r).second;
Assert(row_s->has(x_s));
row_s->pivot(x_s);
- d_rows.erase(ptrRow_r);
- d_basicVars.erase(x_r);
+ d_activeRows.erase(ptrRow_r);
+ d_activeBasicVars.erase(x_r);
makeNonbasic(x_r);
- d_rows.insert(std::make_pair(x_s,row_s));
- d_basicVars.insert(x_s);
+ d_activeRows.insert(std::make_pair(x_s,row_s));
+ d_activeBasicVars.insert(x_s);
makeBasic(x_s);
- for(VarSet::iterator basicIter = begin(); basicIter != end(); ++basicIter){
+ for(VarSet::iterator basicIter = begin(), endIter = end();
+ basicIter != endIter; ++basicIter){
TNode basic = *basicIter;
Row* row_k = lookup(basic);
if(row_k->basicVar() != x_s){
if(row_k->has(x_s)){
+ increaseActivity(basic, 30);
+
row_k->subsitute(*row_s);
}
}
}
}
void printTableau(){
- for(VarSet::iterator basicIter = begin(); basicIter != end(); ++basicIter){
+ for(VarSet::iterator basicIter = begin(), endIter = end();
+ basicIter != endIter; ++basicIter){
TNode basic = *basicIter;
Row* row_k = lookup(basic);
row_k->printRow();
}
}
+
+ bool isEjected(TNode var){
+ return d_inactiveRows.find(var) != d_inactiveRows.end();
+ }
+
+ void ejectBasic(TNode basic){
+ Assert(isActiveBasicVariable(basic));
+
+ Row* row = lookup(basic);
+ d_activeRows.erase(basic);
+ d_activeBasicVars.erase(basic);
+
+ d_inactiveRows.insert(make_pair(basic, row));
+ }
+
+ void reinjectBasic(TNode basic){
+ Assert(isEjected(basic));
+
+ Row* row = lookupEjected(basic);
+
+ d_inactiveRows.erase(basic);
+ d_activeBasicVars.insert(basic);
+ d_activeRows.insert(make_pair(basic, row));
+
+ updateRow(row);
+ }
private:
- inline bool contains(TNode var){
- return d_basicVars.find(var) != d_basicVars.end();
+ inline bool isActiveBasicVariable(TNode var){
+ return d_activeBasicVars.find(var) != d_activeBasicVars.end();
+ }
+
+ void updateRow(Row* row){
+ for(Row::iterator i=row->begin(), endIter = row->end(); i != endIter; ){
+ TNode var = *i;
+ ++i;
+ if(isBasic(var)){
+ Row* row_var = isActiveBasicVariable(var) ? lookup(var) : lookupEjected(var);
+
+ Assert(row_var != row);
+ row->subsitute(*row_var);
+
+ i = row->begin();
+ endIter = row->end();
+ }
+ }
}
};
#include "util/integer.h"
#include "theory/arith/arith_utilities.h"
-#include "theory/arith/theory_arith.h"
#include "theory/arith/delta_rational.h"
#include "theory/arith/partial_model.h"
#include "theory/arith/tableau.h"
#include "theory/arith/slack.h"
#include "theory/arith/basic.h"
+#include "theory/arith/arith_activity.h"
#include "theory/arith/arith_rewriter.h"
#include "theory/arith/arith_propagator.h"
}
}
+
+
+bool TheoryArith::shouldEject(TNode var){
+ if(d_partialModel.hasBounds(var)){
+ return false;
+ }else if(d_tableau.isEjected(var)) {
+ return false;
+ }else if(!d_partialModel.hasEverHadABound(var)){
+ return true;
+ }else if(getActivity(var) >= ACTIVITY_THRESHOLD){
+ return true;
+ }
+ return false;
+}
+
+TNode TheoryArith::findBasicRow(TNode variable){
+ for(Tableau::VarSet::iterator basicIter = d_tableau.begin();
+ basicIter != d_tableau.end();
+ ++basicIter){
+ TNode x_j = *basicIter;
+ Row* row_j = d_tableau.lookup(x_j);
+
+ if(row_j->has(variable)){
+ return x_j;
+ }
+ }
+ return TNode::null();
+}
+
+void TheoryArith::ejectInactiveVariables(){
+ Debug("decay") << "begin ejectInactiveVariables()" << endl;
+ for(std::vector<Node>::iterator i = d_variables.begin(),
+ end = d_variables.end(); i != end; ++i){
+ TNode variable = *i;
+ if(shouldEject(variable)){
+ if(isBasic(variable)){
+ Debug("decay") << "ejecting basic " << variable << endl;;
+ d_tableau.ejectBasic(variable);
+ }
+ }
+ }
+}
+
+void TheoryArith::reinjectVariable(TNode x){
+ d_tableau.reinjectBasic(x);
+
+
+ DeltaRational safeAssignment = computeRowValueUsingSavedAssignment(x);
+ DeltaRational assignment = computeRowValueUsingAssignment(x);
+ d_partialModel.setAssignment(x,safeAssignment,assignment);
+}
+
void TheoryArith::preRegisterTerm(TNode n) {
Debug("arith_preregister") <<"begin arith::preRegisterTerm("<< n <<")"<< endl;
Kind k = n.getKind();
Assert(x.getMetaKind() == kind::metakind::VARIABLE);
d_variables.push_back(Node(x));
+ initActivity(x);
+
if(!isBasic(x)){
d_partialModel.initialize(x,d_constants.d_ZERO_DELTA);
}else{
Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
-
+ if(isBasic(x_i) && d_tableau.isEjected(x_i)){
+ reinjectVariable(x_i);
+ }
if(d_partialModel.aboveUpperBound(x_i, c_i, false) ){ // \upperbound(x_i) <= c_i
return false; //sat
d_partialModel.setUpperConstraint(x_i,original);
d_partialModel.setUpperBound(x_i, c_i);
+ resetActivity(x_i);
+
if(!isBasic(x_i)){
if(d_partialModel.getAssignment(x_i) > c_i){
update(x_i, c_i);
Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl;
+ if(isBasic(x_i) && d_tableau.isEjected(x_i)){
+ reinjectVariable(x_i);
+ }
+
if(d_partialModel.belowLowerBound(x_i, c_i, false)){
return false; //sat
}
d_partialModel.setLowerConstraint(x_i,original);
d_partialModel.setLowerBound(x_i, c_i);
+ resetActivity(x_i);
if(!isBasic(x_i)){
if(d_partialModel.getAssignment(x_i) < c_i){
Debug("arith") << "AssertEquality(" << x_i << " " << c_i << ")"<< std::endl;
+ if(isBasic(x_i) && d_tableau.isEjected(x_i)){
+ reinjectVariable(x_i);
+ }
// u_i <= c_i <= l_i
// This can happen if both c_i <= x_i and x_i <= c_i are in the system.
d_partialModel.setUpperConstraint(x_i,original);
d_partialModel.setUpperBound(x_i, c_i);
+ resetActivity(x_i);
if(!isBasic(x_i)){
if(!(d_partialModel.getAssignment(x_i) == c_i)){
const DeltaRational& assignment = d_partialModel.getAssignment(x_j);
DeltaRational nAssignment = assignment+(diff * a_ji);
d_partialModel.setAssignment(x_j, nAssignment);
+
+ increaseActivity(x_j, 1);
+
checkBasicVariable(x_j);
}
}
const Rational& a_kj = row_k->lookup(x_j);
DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj);
d_partialModel.setAssignment(x_k, nextAssignment);
+
+ increaseActivity(x_j, 1);
+
checkBasicVariable(x_k);
}
}
Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
Debug("arith") << "updateInconsistentVars" << endl;
+ static int iteratationNum = 0;
+ static const int EJECT_FREQUENCY = 10;
while(true){
if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); }
Debug("arith_update") << "No inconsistent variables" << endl;
return Node::null(); //sat
}
+
+ ++iteratationNum;
+ if(iteratationNum % EJECT_FREQUENCY == 0)
+ ejectInactiveVariables();
+
DeltaRational beta_i = d_partialModel.getAssignment(x_i);
if(d_partialModel.belowLowerBound(x_i, beta_i, true)){
*/
bool assertionCases(TNode original, TNode assertion);
+ TNode findBasicRow(TNode variable);
+ bool shouldEject(TNode var);
+ void ejectInactiveVariables();
+ void reinjectVariable(TNode x);
//TODO get rid of this!
Node simulatePreprocessing(TNode n);
Statistics d_statistics;
+
};
}/* CVC4::theory::arith namespace */
projects / cvc5.git / commitdiff