From a311ba5ad6b922903fb706c1576d3e5c8eb5c599 Mon Sep 17 00:00:00 2001 From: Tim King Date: Fri, 4 Jun 2010 19:40:33 +0000 Subject: [PATCH] Changed how assignments are saved during check. These are now backed by an attribute. There is now a priority queue for selecting the smallest inconsistent basic variable. normal.h has been removed. A large chunk of the registerTerm() stuff has been moved into preregister. The lazy splitting code is now been commented out so that it stops showing up in profiling. --- src/theory/arith/arith_rewriter.cpp | 10 - src/theory/arith/normal.h | 48 ----- src/theory/arith/partial_model.cpp | 99 ++++++---- src/theory/arith/partial_model.h | 49 +++-- src/theory/arith/theory_arith.cpp | 294 ++++++++++++++++------------ src/theory/arith/theory_arith.h | 5 + 6 files changed, 271 insertions(+), 234 deletions(-) delete mode 100644 src/theory/arith/normal.h diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 19980cd20..5c2a1e996 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -20,7 +20,6 @@ #include "theory/arith/arith_rewriter.h" #include "theory/arith/arith_utilities.h" -#include "theory/arith/normal.h" #include #include @@ -542,10 +541,6 @@ Kind multKind(Kind k, int sgn){ Node ArithRewriter::rewrite(TNode n){ Debug("arithrewriter") << "Trace rewrite:" << n << std::endl; - if(n.getAttribute(IsNormal())){ - return n; - } - Node res; if(isRelationOperator(n.getKind())){ @@ -554,11 +549,6 @@ Node ArithRewriter::rewrite(TNode n){ res = rewriteTerm(n); } - if(n == res){ - n.setAttribute(NormalForm(), Node::null()); - }else{ - n.setAttribute(NormalForm(), res); - } Debug("arithrewriter") << "Trace rewrite:" << n << "|->"<< res << std::endl; return res; diff --git a/src/theory/arith/normal.h b/src/theory/arith/normal.h deleted file mode 100644 index 12b2a5e71..000000000 --- a/src/theory/arith/normal.h +++ /dev/null @@ -1,48 +0,0 @@ -/********************* */ -/*! \file normal.h - ** \verbatim - ** Original author: taking - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - - -#ifndef __CVC4__THEORY__ARITH__NORMAL_H -#define __CVC4__THEORY__ARITH__NORMAL_H - -namespace CVC4 { -namespace theory { -namespace arith { - -struct IsNormalAttrID; - -typedef expr::Attribute IsNormal; - - -inline bool isNormalized(TNode x){ - return x.getAttribute(IsNormal()); -} - -struct NormalFormAttrID; - -typedef expr::Attribute NormalForm; - - - -}; /* namespace arith */ -}; /* namespace theory */ -}; /* namespace CVC4 */ - - -#endif /* __CVC4__THEORY__ARITH__NORMAL_H */ diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index 2d65f0640..d4be75559 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -45,15 +45,21 @@ void ArithPartialModel::setLowerBound(TNode x, const DeltaRational& r){ 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 < curr = *i; - if(curr.first == x){ - return DeltaRational(curr.second); - } - } - } - return getAssignment(x); -} void ArithPartialModel::setLowerConstraint(TNode x, TNode constraint){ @@ -163,7 +170,7 @@ TNode ArithPartialModel::getUpperConstraint(TNode x){ // } -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 @@ -180,7 +187,7 @@ bool ArithPartialModel::belowLowerBound(TNode x, DeltaRational& c, bool strict){ } } -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 @@ -222,7 +229,7 @@ bool ArithPartialModel::strictlyAboveLowerBound(TNode x){ } 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); @@ -231,32 +238,50 @@ bool ArithPartialModel::assignmentIsConsistent(TNode x){ 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& 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) << " "; diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index 36567e86e..d04d8dd8c 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -37,7 +37,9 @@ namespace partial_model { struct DeltaRationalCleanupStrategy{ static void cleanup(DeltaRational* dq){ Debug("arithgc") << "cleaning up " << dq << "\n"; - delete dq; + if(dq != NULL){ + delete dq; + } } }; @@ -46,6 +48,12 @@ typedef expr::Attribute Assignment; + +struct SafeAssignmentAttrID {}; +typedef expr::Attribute SafeAssignment; + /** * This defines a context dependent delta rational map. * This is used to keep track of the current lower and upper bounds on @@ -108,12 +116,11 @@ private: partial_model::CDDRationalMap d_LowerBoundMap; partial_model::CDDRationalMap d_UpperBoundMap; - typedef std::pair HistoryPair; - typedef std::deque< HistoryPair > HistoryStack; - HistoryStack d_history; + typedef std::vector HistoryList; + HistoryList d_history; - bool d_savingAssignments; + bool d_unsafeMode; public: @@ -121,7 +128,7 @@ public: d_LowerBoundMap(c), d_UpperBoundMap(c), d_history(), - d_savingAssignments(false) + d_unsafeMode(false) { } void setLowerConstraint(TNode x, TNode constraint); @@ -130,11 +137,21 @@ public: 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); @@ -143,20 +160,20 @@ public: /** 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); @@ -164,10 +181,8 @@ public: void printModel(TNode x); - void initialize(TNode x, const DeltaRational& r); - - DeltaRational getSavedAssignment(TNode x) const; - +private: + void clearSafeAssignments(bool revert); }; 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::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= 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("<::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::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(); - 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::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(); +// 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; diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index c6b555bf8..cdd73782e 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -32,6 +32,7 @@ #include "theory/arith/partial_model.h" #include +#include namespace CVC4 { namespace theory { @@ -56,6 +57,8 @@ private: //This needs to come before d_partialModel and d_tableau in the file + std::priority_queue d_possiblyInconsistent; + /* Chopping block ends */ ArithConstants d_constants; ArithPartialModel d_partialModel; @@ -98,6 +101,8 @@ private: DeltaRational computeRowValueUsingSavedAssignment(TNode x); void checkTableau(); + void checkBasicVariable(TNode basic); + //TODO get rid of this! Node simulatePreprocessing(TNode n); -- 2.30.2