summaryrefslogtreecommitdiff
path: root/src/theory/arith/theory_arith.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/theory_arith.cpp')
-rw-r--r--src/theory/arith/theory_arith.cpp294
1 files changed, 172 insertions, 122 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index e99a3e823..92781e0ba 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -30,7 +30,7 @@
#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"
@@ -63,7 +63,6 @@ TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) :
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){
@@ -72,6 +71,40 @@ TheoryArith::~TheoryArith(){
}
}
+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;
@@ -98,31 +131,63 @@ void TheoryArith::preRegisterTerm(TNode n) {
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:
@@ -153,6 +218,8 @@ void TheoryArith::setupVariable(TNode x){
Debug("arith_setup") << "setup("<<x<< " " <<q<<")"<<std::endl;
}
d_partialModel.setAssignment(x,q);
+
+ checkBasicVariable(x);
}
Debug("arithgc") << "setupVariable("<<x<<")"<<std::endl;
};
@@ -185,7 +252,7 @@ DeltaRational TheoryArith::computeRowValueUsingSavedAssignment(TNode x){
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;
@@ -208,56 +275,6 @@ void TheoryArith::registerTerm(TNode tn){
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) */
@@ -288,6 +305,8 @@ bool TheoryArith::AssertUpper(TNode n, TNode original){
if(d_partialModel.getAssignment(x_i) > c_i){
update(x_i, c_i);
}
+ }else{
+ checkBasicVariable(x_i);
}
d_partialModel.printModel(x_i);
return false;
@@ -319,6 +338,8 @@ bool TheoryArith::AssertLower(TNode n, TNode original){
if(d_partialModel.getAssignment(x_i) < c_i){
update(x_i, c_i);
}
+ }else{
+ checkBasicVariable(x_i);
}
//d_partialModel.printModel(x_i);
@@ -326,7 +347,7 @@ bool TheoryArith::AssertLower(TNode n, TNode original){
}
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 << ": "
@@ -345,6 +366,7 @@ void TheoryArith::update(TNode x_i, DeltaRational& v){
DeltaRational assignment = d_partialModel.getAssignment(x_j);
DeltaRational nAssignment = assignment+(diff * a_ji);
d_partialModel.setAssignment(x_j, nAssignment);
+ checkBasicVariable(x_j);
}
}
@@ -383,25 +405,45 @@ void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){
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;
+ }
}
}
@@ -449,6 +491,7 @@ TNode TheoryArith::selectSlackAbove(TNode x_i){ // beta(x_i) > u_i
Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
Debug("arith") << "updateInconsistentVars" << endl;
+ d_partialModel.turnOnUnsafeMode();
while(true){
if(debugTagIsOn("paranoid:check_tableau")){
@@ -464,8 +507,8 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
checkTableau();
}
- d_partialModel.stopRecordingAssignments(false);
- d_partialModel.beginRecordingAssignments();
+ d_partialModel.commitAssignmentChanges();
+ d_partialModel.turnOffUnsafeMode();
if(debugTagIsOn("paranoid:check_tableau")){
checkTableau();
@@ -487,8 +530,10 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
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();
@@ -508,8 +553,10 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
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();
@@ -596,6 +643,7 @@ Node TheoryArith::generateConflictBelow(TNode conflictVar){
return conflict;
}
+
//TODO get rid of this!
Node TheoryArith::simulatePreprocessing(TNode n){
if(n.getKind() == NOT){
@@ -606,17 +654,19 @@ Node TheoryArith::simulatePreprocessing(TNode n){
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;
@@ -719,37 +769,37 @@ void TheoryArith::check(Effort level){
}
}
- 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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback