void ArithPartialModel::setAssignment(TNode x, const DeltaRational& r){
Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
- if(d_savingAssignments){
- DeltaRational current = getAssignment(x);
- d_history.push_back(make_pair(x,current));
- }
-
Assert(x.hasAttribute(partial_model::Assignment()));
- DeltaRational* c = x.getAttribute(partial_model::Assignment());
- *c = r;
+ DeltaRational* curr = x.getAttribute(partial_model::Assignment());
+
+ if(d_unsafeMode){
+ Assert(x.hasAttribute(partial_model::SafeAssignment()));
+ DeltaRational* saved = x.getAttribute(partial_model::SafeAssignment());
+ if(saved == NULL){
+ saved = new DeltaRational(*curr);
+ x.setAttribute(partial_model::SafeAssignment(), saved);
+ 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);
-
Assert(!x.hasAttribute(partial_model::Assignment()));
+ Assert(!x.hasAttribute(partial_model::SafeAssignment()));
+
DeltaRational* c = new DeltaRational(r);
x.setAttribute(partial_model::Assignment(), c);
+ x.setAttribute(partial_model::SafeAssignment(), NULL);
Debug("partial_model") << "pm: constructing an assignment for " << x
<< " initially " << (*c) <<endl;
return DeltaRational((*i).second);
}
+DeltaRational ArithPartialModel::getSafeAssignment(TNode x) const{
+ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+ if(d_unsafeMode){
+ Assert( x.hasAttribute(partial_model::SafeAssignment()));
+ DeltaRational* safeAssignment = x.getAttribute(partial_model::SafeAssignment());
+ if(safeAssignment != NULL){
+ return *safeAssignment;
+ }
+ }
+ return getAssignment(x);
+}
-DeltaRational ArithPartialModel::getAssignment(TNode x) const{
+const DeltaRational& ArithPartialModel::getAssignment(TNode x) const{
Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
DeltaRational* assign;
return *assign;
}
-DeltaRational ArithPartialModel::getSavedAssignment(TNode x) const{
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
- if(d_savingAssignments){
- for(HistoryStack::const_iterator i = d_history.begin(); i != d_history.end(); ++i){
- pair<TNode, DeltaRational> curr = *i;
- if(curr.first == x){
- return DeltaRational(curr.second);
- }
- }
- }
- return getAssignment(x);
-}
void ArithPartialModel::setLowerConstraint(TNode x, TNode constraint){
// }
-bool ArithPartialModel::belowLowerBound(TNode x, DeltaRational& c, bool strict){
+bool ArithPartialModel::belowLowerBound(TNode x, const DeltaRational& c, bool strict){
CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
if(i == d_LowerBoundMap.end()){
// l = -\intfy
}
}
-bool ArithPartialModel::aboveUpperBound(TNode x, DeltaRational& c, bool strict){
+bool ArithPartialModel::aboveUpperBound(TNode x, const DeltaRational& c, bool strict){
CDDRationalMap::iterator i = d_UpperBoundMap.find(x);
if(i == d_UpperBoundMap.end()){
// u = -\intfy
}
bool ArithPartialModel::assignmentIsConsistent(TNode x){
- DeltaRational beta = getAssignment(x);
+ const DeltaRational& beta = getAssignment(x);
bool above_li = !belowLowerBound(x,beta,true);
bool below_ui = !aboveUpperBound(x,beta,true);
return above_li && below_ui;
}
-void ArithPartialModel::beginRecordingAssignments(){
- Assert(!d_savingAssignments);
+void ArithPartialModel::turnOnUnsafeMode(){
+ Assert(!d_unsafeMode);
Assert(d_history.empty());
- d_savingAssignments = true;
+ d_unsafeMode = true;
}
+void ArithPartialModel::turnOffUnsafeMode(){
+ Assert(d_unsafeMode);
+ Assert(d_history.empty());
+
+ d_unsafeMode = false;
+}
-void ArithPartialModel::stopRecordingAssignments(bool revert){
- Assert(d_savingAssignments);
+void ArithPartialModel::clearSafeAssignments(bool revert){
+ Assert(d_unsafeMode);
- d_savingAssignments = false; //
+ for(HistoryList::iterator i = d_history.begin(); i != d_history.end(); ++i){
+ TNode x = *i;
- if(revert){
- while(!d_history.empty()){
- pair<TNode, DeltaRational>& curr = d_history.back();
+ Assert(x.hasAttribute(partial_model::SafeAssignment()));
- setAssignment(curr.first,curr.second);
+ DeltaRational* safeAssignment = x.getAttribute(partial_model::SafeAssignment());
- d_history.pop_back();
+ if(revert){
+ Assert(x.hasAttribute(partial_model::Assignment()));
+
+ DeltaRational* assign = x.getAttribute(partial_model::Assignment());
+ *assign = *safeAssignment;
}
- }else{
- d_history.clear();
+ x.setAttribute(partial_model::SafeAssignment(), NULL);
+ delete safeAssignment;
}
+ d_history.clear();
+}
+
+void ArithPartialModel::revertAssignmentChanges(){
+ clearSafeAssignments(true);
+}
+void ArithPartialModel::commitAssignmentChanges(){
+ clearSafeAssignments(false);
}
+
void ArithPartialModel::printModel(TNode x){
Debug("model") << "model" << x << ":"<< getAssignment(x) << " ";
struct DeltaRationalCleanupStrategy{
static void cleanup(DeltaRational* dq){
Debug("arithgc") << "cleaning up " << dq << "\n";
- delete dq;
+ if(dq != NULL){
+ delete dq;
+ }
}
};
DeltaRational*,
DeltaRationalCleanupStrategy> Assignment;
+
+struct SafeAssignmentAttrID {};
+typedef expr::Attribute<SafeAssignmentAttrID,
+ DeltaRational*,
+ DeltaRationalCleanupStrategy> SafeAssignment;
+
/**
* This defines a context dependent delta rational map.
* This is used to keep track of the current lower and upper bounds on
partial_model::CDDRationalMap d_LowerBoundMap;
partial_model::CDDRationalMap d_UpperBoundMap;
- typedef std::pair<TNode, DeltaRational> HistoryPair;
- typedef std::deque< HistoryPair > HistoryStack;
- HistoryStack d_history;
+ typedef std::vector<TNode> HistoryList;
+ HistoryList d_history;
- bool d_savingAssignments;
+ bool d_unsafeMode;
public:
d_LowerBoundMap(c),
d_UpperBoundMap(c),
d_history(),
- d_savingAssignments(false)
+ d_unsafeMode(false)
{ }
void setLowerConstraint(TNode x, TNode constraint);
TNode getUpperConstraint(TNode x);
- void beginRecordingAssignments();
- /* */
- void stopRecordingAssignments(bool revert);
- bool isRecording() { return d_savingAssignments; }
+ void initialize(TNode x, const DeltaRational& r);
+
+ DeltaRational getSafeAssignment(TNode x) const;
+
+ bool isInUnsafeMode() { return d_unsafeMode; }
+
+ void turnOnUnsafeMode();
+ void turnOffUnsafeMode();
+
+ void revertAssignmentChanges();
+ void commitAssignmentChanges();
+
+
+
void setUpperBound(TNode x, const DeltaRational& r);
void setLowerBound(TNode x, const DeltaRational& r);
/** Must know that the bound exists before calling this! */
DeltaRational getUpperBound(TNode x) const;
DeltaRational getLowerBound(TNode x) const;
- DeltaRational getAssignment(TNode x) const;
+ const DeltaRational& getAssignment(TNode x) const;
/**
* x <= l
* ? c < l
*/
- bool belowLowerBound(TNode x, DeltaRational& c, bool strict);
+ bool belowLowerBound(TNode x, const DeltaRational& c, bool strict);
/**
* x <= u
* ? c < u
*/
- bool aboveUpperBound(TNode x, DeltaRational& c, bool strict);
+ bool aboveUpperBound(TNode x, const DeltaRational& c, bool strict);
bool strictlyBelowUpperBound(TNode x);
bool strictlyAboveLowerBound(TNode x);
void printModel(TNode x);
- void initialize(TNode x, const DeltaRational& r);
-
- DeltaRational getSavedAssignment(TNode x) const;
-
+private:
+ void clearSafeAssignments(bool revert);
};
#include "theory/arith/delta_rational.h"
#include "theory/arith/partial_model.h"
#include "theory/arith/tableau.h"
-#include "theory/arith/normal.h"
+//#include "theory/arith/normal.h"
#include "theory/arith/slack.h"
#include "theory/arith/basic.h"
uint64_t ass_id = partial_model::Assignment::getId();
Debug("arithsetup") << "Assignment: " << ass_id << std::endl;
- d_partialModel.beginRecordingAssignments();
}
TheoryArith::~TheoryArith(){
for(vector<Node>::iterator i=d_variables.begin(); i!= d_variables.end(); ++i){
}
}
+bool isBasicSum(TNode n){
+ if(n.getKind() != kind::PLUS) return false;
+
+ for(TNode::const_iterator i=n.begin(); i!=n.end(); ++i){
+ TNode child = *i;
+ if(child.getKind() != MULT) return false;
+ if(child[0].getKind() != CONST_RATIONAL) return false;
+ for(unsigned j=1; j<child.getNumChildren(); ++j){
+ TNode var = child[j];
+ if(var.getMetaKind() != metakind::VARIABLE) return false;
+ }
+ }
+ return true;
+}
+
+bool isNormalAtom(TNode n){
+
+ if(!(n.getKind() == LEQ|| n.getKind() == GEQ || n.getKind() == EQUAL)){
+ return false;
+ }
+ TNode left = n[0];
+ TNode right = n[1];
+ if(right.getKind() != CONST_RATIONAL){
+ return false;
+ }
+ if(left.getMetaKind() == metakind::VARIABLE){
+ return true;
+ }else if(isBasicSum(left)){
+ return true;
+ }else{
+ return false;
+ }
+
+}
void TheoryArith::preRegisterTerm(TNode n) {
Debug("arith_preregister") << "arith: begin TheoryArith::preRegisterTerm("
<< n << ")" << endl;
setupVariable(n);
}
- Debug("arith_preregister") << "arith: end TheoryArith::preRegisterTerm("
- << n << ")" << endl;
-}
+ //TODO is an atom
+ if(isRelationOperator(n.getKind())){
-bool isBasicSum(TNode n){
- if(n.getKind() != kind::PLUS) return false;
+ Assert(isNormalAtom(n));
+ Node normalForm(n);
- for(TNode::const_iterator i=n.begin(); i!=n.end(); ++i){
- TNode child = *i;
- if(child.getKind() != MULT) return false;
- if(child[0].getKind() != CONST_RATIONAL) return false;
- for(unsigned j=1; j<child.getNumChildren(); ++j){
- TNode var = child[j];
- if(var.getMetaKind() != metakind::VARIABLE) return false;
+ if(normalForm.getKind() == NOT){
+ normalForm = pushInNegation(normalForm);
+ }
+ Kind k = normalForm.getKind();
+
+ if(k != kind::CONST_BOOLEAN){
+ Assert(isRelationOperator(k));
+ TNode left = normalForm[0];
+ TNode right = normalForm[1];
+ if(left.getKind() == PLUS){
+ //We may need to introduce a slack variable.
+ Assert(left.getNumChildren() >= 2);
+ Assert(isBasicSum(left));
+ Node slack;
+ if(!left.getAttribute(Slack(), slack)){
+ //TODO
+ TypeNode real_type = NodeManager::currentNM()->realType();
+ slack = NodeManager::currentNM()->mkVar(real_type);
+
+ left.setAttribute(Slack(), slack);
+ makeBasic(slack);
+
+
+
+ Node slackEqLeft = NodeManager::currentNM()->mkNode(EQUAL,slack,left);
+ slackEqLeft.setAttribute(TheoryArithPropagated(), true);
+ //TODO this has to be wrong no? YES (dejan)
+ // d_out->lemma(slackEqLeft);
+
+ Debug("slack") << "slack " << slackEqLeft << endl;
+
+ d_tableau.addRow(slackEqLeft);
+
+ setupVariable(slack);
+ }
+ }
}
}
- return true;
+
+ Debug("arith_preregister") << "arith: end TheoryArith::preRegisterTerm("
+ << n << ")" << endl;
}
-void registerAtom(TNode rel){
- //addBound(rel);
- //Anything else?
+void TheoryArith::checkBasicVariable(TNode basic){
+ Assert(isBasic(basic));
+ if(!d_partialModel.assignmentIsConsistent(basic)){
+ d_possiblyInconsistent.push(basic);
+ }
}
/* Requirements:
Debug("arith_setup") << "setup("<<x<< " " <<q<<")"<<std::endl;
}
d_partialModel.setAssignment(x,q);
+
+ checkBasicVariable(x);
}
Debug("arithgc") << "setupVariable("<<x<<")"<<std::endl;
};
for(std::set<TNode>::iterator i = row->begin(); i != row->end();++i){
TNode nonbasic = *i;
Rational& coeff = row->lookup(nonbasic);
- DeltaRational assignment = d_partialModel.getSavedAssignment(nonbasic);
+ DeltaRational assignment = d_partialModel.getSafeAssignment(nonbasic);
sum = sum + (assignment * coeff);
}
return sum;
if(tn.getKind() == kind::BUILTIN) return;
- //TODO is an atom
- if(isRelationOperator(tn.getKind())){
-
- Node normalForm = (isNormalized(tn)) ? Node(tn) : rewrite(tn);
- normalForm = (normalForm.getKind() == NOT) ? pushInNegation(normalForm):normalForm;
- Kind k = normalForm.getKind();
-
- if(k != kind::CONST_BOOLEAN){
- Assert(isRelationOperator(k));
- TNode left = normalForm[0];
- TNode right = normalForm[1];
- if(left.getKind() == PLUS){
- //We may need to introduce a slack variable.
- Assert(left.getNumChildren() >= 2);
- Assert(isBasicSum(left));
- Node slack;
- if(!left.getAttribute(Slack(), slack)){
- //TODO
- TypeNode real_type = NodeManager::currentNM()->realType();
- slack = NodeManager::currentNM()->mkVar(real_type);
-
- left.setAttribute(Slack(), slack);
- makeBasic(slack);
-
-
-
- Node slackEqLeft = NodeManager::currentNM()->mkNode(EQUAL,slack,left);
- slackEqLeft.setAttribute(TheoryArithPropagated(), true);
- //TODO this has to be wrong no? YES (dejan)
- // d_out->lemma(slackEqLeft);
-
- Debug("slack") << "slack " << slackEqLeft << endl;
-
- d_tableau.addRow(slackEqLeft);
-
- setupVariable(slack);
-
- Node rewritten = NodeManager::currentNM()->mkNode(k,slack,right);
- registerAtom(rewritten);
- }else{
- Node rewritten = NodeManager::currentNM()->mkNode(k,slack,right);
- registerAtom(rewritten);
- }
- }else{
- Assert(left.getMetaKind() == metakind::VARIABLE);
- Assert(right.getKind() == CONST_RATIONAL);
- registerAtom(normalForm);
- }
- }
- }
}
/* procedure AssertUpper( x_i <= c_i) */
if(d_partialModel.getAssignment(x_i) > c_i){
update(x_i, c_i);
}
+ }else{
+ checkBasicVariable(x_i);
}
d_partialModel.printModel(x_i);
return false;
if(d_partialModel.getAssignment(x_i) < c_i){
update(x_i, c_i);
}
+ }else{
+ checkBasicVariable(x_i);
}
//d_partialModel.printModel(x_i);
}
void TheoryArith::update(TNode x_i, DeltaRational& v){
-
+ Assert(!isBasic(x_i));
DeltaRational assignment_x_i = d_partialModel.getAssignment(x_i);
Debug("arith") <<"update " << x_i << ": "
DeltaRational assignment = d_partialModel.getAssignment(x_j);
DeltaRational nAssignment = assignment+(diff * a_ji);
d_partialModel.setAssignment(x_j, nAssignment);
+ checkBasicVariable(x_j);
}
}
Rational a_kj = row_k->lookup(x_j);
DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj);
d_partialModel.setAssignment(x_k, nextAssignment);
+ checkBasicVariable(x_k);
}
}
d_tableau.pivot(x_i, x_j);
+ checkBasicVariable(x_j);
+
if(debugTagIsOn("tableau")){
d_tableau.printTableau();
}
}
TNode TheoryArith::selectSmallestInconsistentVar(){
+ Debug("arith_update") << "selectSmallestInconsistentVar()" << endl;
+ Debug("arith_update") << "possiblyInconsistent.size()"
+ << d_possiblyInconsistent.size() << endl;
+
+ while(!d_possiblyInconsistent.empty()){
+ TNode var = d_possiblyInconsistent.top();
+ Debug("arith_update") << "possiblyInconsistent var" << var << endl;
+ if(isBasic(var)){
+ if(!d_partialModel.assignmentIsConsistent(var)){
+ return var;
+ }
+ }
+ d_possiblyInconsistent.pop();
+ }
- for(Tableau::VarSet::iterator basicIter = d_tableau.begin();
- basicIter != d_tableau.end();
- ++basicIter){
+ if(debugTagIsOn("paranoid:variables")){
+ for(Tableau::VarSet::iterator basicIter = d_tableau.begin();
+ basicIter != d_tableau.end();
+ ++basicIter){
- TNode basic = *basicIter;
- if(!d_partialModel.assignmentIsConsistent(basic)){
- return basic;
+ TNode basic = *basicIter;
+ Assert(d_partialModel.assignmentIsConsistent(basic));
+ if(!d_partialModel.assignmentIsConsistent(basic)){
+ return basic;
+ }
}
}
Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
Debug("arith") << "updateInconsistentVars" << endl;
+ d_partialModel.turnOnUnsafeMode();
while(true){
if(debugTagIsOn("paranoid:check_tableau")){
checkTableau();
}
- d_partialModel.stopRecordingAssignments(false);
- d_partialModel.beginRecordingAssignments();
+ d_partialModel.commitAssignmentChanges();
+ d_partialModel.turnOffUnsafeMode();
if(debugTagIsOn("paranoid:check_tableau")){
checkTableau();
checkTableau();
}
- d_partialModel.stopRecordingAssignments(true);
- d_partialModel.beginRecordingAssignments();
+ d_partialModel.revertAssignmentChanges();
+ d_partialModel.turnOffUnsafeMode();
+ //d_partialModel.stopRecordingAssignments(true);
+ //d_partialModel.beginRecordingAssignments();
if(debugTagIsOn("paranoid:check_tableau")){
checkTableau();
checkTableau();
}
- d_partialModel.stopRecordingAssignments(true);
- d_partialModel.beginRecordingAssignments();
+ d_partialModel.revertAssignmentChanges();
+ d_partialModel.turnOffUnsafeMode();
+ //d_partialModel.stopRecordingAssignments(true);
+ //d_partialModel.beginRecordingAssignments();
if(debugTagIsOn("paranoid:check_tableau")){
checkTableau();
return conflict;
}
+
//TODO get rid of this!
Node TheoryArith::simulatePreprocessing(TNode n){
if(n.getKind() == NOT){
return NodeManager::currentNM()->mkNode(NOT,sub);
}
}else{
- Node rewritten = rewrite(n);
+ Assert(isNormalAtom(n));
+ Node rewritten = n;
Kind k = rewritten.getKind();
- if(rewritten.getKind() == NOT){
- Node sub = simulatePreprocessing(rewritten[0]);
- if(sub.getKind() == NOT){
- return sub[0];
- }else{
- return NodeManager::currentNM()->mkNode(NOT,sub);
- }
- } else if(!isRelationOperator(k)){
+// if(rewritten.getKind() == NOT){
+// Node sub = simulatePreprocessing(rewritten[0]);
+// if(sub.getKind() == NOT){
+// return sub[0];
+// }else{
+// return NodeManager::currentNM()->mkNode(NOT,sub);
+// }
+// } else
+ if(!isRelationOperator(k)){
if(rewritten.getKind() == CONST_BOOLEAN){
Warning() << "How did I get a const boolean here" << endl;
Warning() << "offending node has id " << n.getId() << endl;
}
}
- if(fullEffort(level)){
- bool enqueuedCaseSplit = false;
- typedef context::CDList<Node>::const_iterator diseq_iterator;
- for(diseq_iterator i = d_diseq.begin(); i!= d_diseq.end(); ++i){
-
- Node assertion = *i;
- Debug("arith") << "splitting" << assertion << endl;
- TNode eq = assertion[0];
- TNode x_i = eq[0];
- TNode c_i = eq[1];
- DeltaRational constant = c_i.getConst<Rational>();
- Debug("arith") << "broken apart" << endl;
- if(d_partialModel.getAssignment(x_i) == constant){
- Debug("arith") << "here" << endl;
- enqueuedCaseSplit = true;
- Node lt = NodeManager::currentNM()->mkNode(LT,x_i,c_i);
- Node gt = NodeManager::currentNM()->mkNode(GT,x_i,c_i);
- Node caseSplit = NodeManager::currentNM()->mkNode(OR, eq, lt, gt);
- //d_out->enqueueCaseSplits(caseSplit);
- Debug("arith") << "finished" << caseSplit << endl;
- }
- Debug("arith") << "end of for loop" << endl;
-
- }
- Debug("arith") << "finished" << endl;
-
- if(enqueuedCaseSplit){
- //d_out->caseSplit();
- //Warning() << "Outstanding case split in theory arith" << endl;
- }
- }
+ // if(fullEffort(level)){
+// bool enqueuedCaseSplit = false;
+// typedef context::CDList<Node>::const_iterator diseq_iterator;
+// for(diseq_iterator i = d_diseq.begin(); i!= d_diseq.end(); ++i){
+
+// Node assertion = *i;
+// Debug("arith") << "splitting" << assertion << endl;
+// TNode eq = assertion[0];
+// TNode x_i = eq[0];
+// TNode c_i = eq[1];
+// DeltaRational constant = c_i.getConst<Rational>();
+// Debug("arith") << "broken apart" << endl;
+// if(d_partialModel.getAssignment(x_i) == constant){
+// Debug("arith") << "here" << endl;
+// enqueuedCaseSplit = true;
+// Node lt = NodeManager::currentNM()->mkNode(LT,x_i,c_i);
+// Node gt = NodeManager::currentNM()->mkNode(GT,x_i,c_i);
+// Node caseSplit = NodeManager::currentNM()->mkNode(OR, eq, lt, gt);
+// //d_out->enqueueCaseSplits(caseSplit);
+// Debug("arith") << "finished" << caseSplit << endl;
+// }
+// Debug("arith") << "end of for loop" << endl;
+
+// }
+// Debug("arith") << "finished" << endl;
+
+// if(enqueuedCaseSplit){
+// //d_out->caseSplit();
+// //Warning() << "Outstanding case split in theory arith" << endl;
+// }
+// }
Debug("arith") << "TheoryArith::check end" << std::endl;
projects / cvc5.git / commitdiff