From 0e22528f5d249e301b2a5dc1f14849a7f8e25439 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 17 Mar 2011 21:20:28 +0000 Subject: [PATCH] SimplexDecisionProcedure no longer takes an OutputChannel as a parameter. --- src/theory/arith/simplex.cpp | 47 +++++++++++++++++++------------ src/theory/arith/simplex.h | 23 ++++++--------- src/theory/arith/theory_arith.cpp | 32 ++++++++++----------- src/theory/arith/theory_arith.h | 7 +++-- 4 files changed, 57 insertions(+), 52 deletions(-) diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 1e7b5c028..bfa2d56d3 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -85,19 +85,19 @@ SimplexDecisionProcedure::Statistics::~Statistics(){ } /* procedure AssertLower( x_i >= c_i ) */ -bool SimplexDecisionProcedure::AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode original){ +Node SimplexDecisionProcedure::AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode original){ Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl; if(d_partialModel.belowLowerBound(x_i, c_i, false)){ - return false; //sat + return Node::null(); } if(d_partialModel.aboveUpperBound(x_i, c_i, true)){ Node ubc = d_partialModel.getUpperConstraint(x_i); Node conflict = NodeManager::currentNM()->mkNode(AND, ubc, original); - d_out->conflict(conflict); + //d_out->conflict(conflict); Debug("arith") << "AssertLower conflict " << conflict << endl; ++(d_statistics.d_statAssertLowerConflicts); - return true; + return conflict; } d_partialModel.setLowerConstraint(x_i,original); @@ -111,24 +111,28 @@ bool SimplexDecisionProcedure::AssertLower(ArithVar x_i, const DeltaRational& c_ d_queue.enqueueIfInconsistent(x_i); } - return false; + if(Debug.isOn("model")) { d_partialModel.printModel(x_i); } + + return Node::null(); } /* procedure AssertUpper( x_i <= c_i) */ -bool SimplexDecisionProcedure::AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode original){ +Node SimplexDecisionProcedure::AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode original){ Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl; if(d_partialModel.aboveUpperBound(x_i, c_i, false) ){ // \upperbound(x_i) <= c_i - return false; //sat + //return false; //sat + return Node::null(); } if(d_partialModel.belowLowerBound(x_i, c_i, true)){// \lowerbound(x_i) > c_i Node lbc = d_partialModel.getLowerConstraint(x_i); Node conflict = NodeManager::currentNM()->mkNode(AND, lbc, original); Debug("arith") << "AssertUpper conflict " << conflict << endl; ++(d_statistics.d_statAssertUpperConflicts); - d_out->conflict(conflict); - return true; + //d_out->conflict(conflict); + return conflict; + //return true; } d_partialModel.setUpperConstraint(x_i,original); @@ -141,13 +145,16 @@ bool SimplexDecisionProcedure::AssertUpper(ArithVar x_i, const DeltaRational& c_ }else{ d_queue.enqueueIfInconsistent(x_i); } - d_partialModel.printModel(x_i); - return false; + + if(Debug.isOn("model")) { d_partialModel.printModel(x_i); } + + return Node::null(); + //return false; } /* procedure AssertLower( x_i == c_i ) */ -bool SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational& c_i, TNode original){ +Node SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational& c_i, TNode original){ Debug("arith") << "AssertEquality(" << x_i << " " << c_i << ")"<< std::endl; @@ -155,23 +162,26 @@ bool SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational& // This can happen if both c_i <= x_i and x_i <= c_i are in the system. if(d_partialModel.belowLowerBound(x_i, c_i, false) && d_partialModel.aboveUpperBound(x_i, c_i, false)){ - return false; //sat + //return false; //sat + return Node::null(); } if(d_partialModel.aboveUpperBound(x_i, c_i, true)){ Node ubc = d_partialModel.getUpperConstraint(x_i); Node conflict = NodeManager::currentNM()->mkNode(AND, ubc, original); - d_out->conflict(conflict); + //d_out->conflict(conflict); Debug("arith") << "AssertLower conflict " << conflict << endl; - return true; + //return true; + return conflict; } if(d_partialModel.belowLowerBound(x_i, c_i, true)){ Node lbc = d_partialModel.getLowerConstraint(x_i); Node conflict = NodeManager::currentNM()->mkNode(AND, lbc, original); Debug("arith") << "AssertUpper conflict " << conflict << endl; - d_out->conflict(conflict); - return true; + //d_out->conflict(conflict); + //return true; + return conflict; } d_partialModel.setLowerConstraint(x_i,original); @@ -189,7 +199,8 @@ bool SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational& //checkBasicVariable(x_i); } - return false; + //return false; + return Node::null(); } set tableauAndHasSet(Tableau& tab, ArithVar v){ diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index 6f3ff073f..968275ae5 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -10,7 +10,6 @@ #include "theory/arith/delta_rational.h" #include "theory/arith/tableau.h" #include "theory/arith/partial_model.h" -#include "theory/output_channel.h" #include "util/options.h" @@ -31,8 +30,6 @@ private: */ ArithPartialModel& d_partialModel; - OutputChannel* d_out; - Tableau& d_tableau; ArithPriorityQueue d_queue; @@ -45,10 +42,8 @@ private: public: SimplexDecisionProcedure(ArithPartialModel& pm, - OutputChannel* out, Tableau& tableau) : d_partialModel(pm), - d_out(out), d_tableau(tableau), d_queue(pm, tableau), d_numVariables(0), @@ -61,20 +56,20 @@ public: * Assert*(n, orig) takes an bound n that is implied by orig. * and asserts that as a new bound if it is tighter than the current bound * and updates the value of a basic variable if needed. - * If this new bound is in conflict with the other bound, - * a conflict is created and asserted to the output channel. * - * orig must be an atom in the SAT solver so that it can be used for + * orig must be a literal in the SAT solver so that it can be used for * conflict analysis. * - * n is of the form (x =?= c) where x is a variable, - * c is a constant and =?= is either LT, LEQ, EQ, GEQ, or GT. + * x is the variable getting the new bound, + * c is the value of the new bound. * - * returns true if a conflict was asserted. + * If this new bound is in conflict with the other bound, + * a node describing this conflict is returned. + * If this new bound is not in conflict, Node::null() is returned. */ - bool AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode orig); - bool AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode orig); - bool AssertEquality(ArithVar x_i, const DeltaRational& c_i, TNode orig); + Node AssertLower(ArithVar x, const DeltaRational& c, TNode orig); + Node AssertUpper(ArithVar x, const DeltaRational& c, TNode orig); + Node AssertEquality(ArithVar x, const DeltaRational& c, TNode orig); private: /** diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 726bfc210..dfa81cb3f 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -66,7 +66,7 @@ TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) : d_tableauResetDensity(2.0), d_tableauResetPeriod(10), d_propagator(c, out), - d_simplex(d_partialModel, d_out, d_tableau), + d_simplex(d_partialModel, d_tableau), d_DELTA_ZERO(0), d_statistics() {} @@ -308,16 +308,14 @@ DeltaRational determineRightConstant(TNode assertion, Kind simpleKind){ return DeltaRational(noninf, inf); } -void TheoryArith::disequalityConflict(TNode eq, TNode lb, TNode ub){ - +Node TheoryArith::disequalityConflict(TNode eq, TNode lb, TNode ub){ NodeBuilder<3> conflict(kind::AND); conflict << eq << lb << ub; ++(d_statistics.d_statDisequalityConflicts); - d_out->conflict((TNode)conflict); - + return conflict; } -bool TheoryArith::assertionCases(TNode assertion){ +Node TheoryArith::assertionCases(TNode assertion){ Kind simpKind = simplifiedKind(assertion); Assert(simpKind != UNDEFINED_KIND); ArithVar x_i = determineLeftVariable(assertion, simpKind); @@ -331,18 +329,18 @@ bool TheoryArith::assertionCases(TNode assertion){ if (d_partialModel.hasLowerBound(x_i) && d_partialModel.getLowerBound(x_i) == c_i) { Node diseq = assertion[0].eqNode(assertion[1]).notNode(); if (d_diseq.find(diseq) != d_diseq.end()) { - disequalityConflict(diseq, d_partialModel.getLowerConstraint(x_i) , assertion); - return true; + Node lb = d_partialModel.getLowerConstraint(x_i); + return disequalityConflict(diseq, lb , assertion); } } case LT: - return d_simplex.AssertUpper(x_i, c_i, assertion); + return d_simplex.AssertUpper(x_i, c_i, assertion); case GEQ: if (d_partialModel.hasUpperBound(x_i) && d_partialModel.getUpperBound(x_i) == c_i) { Node diseq = assertion[0].eqNode(assertion[1]).notNode(); if (d_diseq.find(diseq) != d_diseq.end()) { - disequalityConflict(diseq, assertion, d_partialModel.getUpperConstraint(x_i)); - return true; + Node ub = d_partialModel.getUpperConstraint(x_i); + return disequalityConflict(diseq, assertion, ub); } } case GT: @@ -366,14 +364,13 @@ bool TheoryArith::assertionCases(TNode assertion){ d_partialModel.getUpperBound(lhsVar) == rhsValue) { Node lb = d_partialModel.getLowerConstraint(lhsVar); Node ub = d_partialModel.getUpperConstraint(lhsVar); - disequalityConflict(assertion, lb, ub); - return true; + return disequalityConflict(assertion, lb, ub); } } - return false; + return Node::null(); default: Unreachable(); - return false; + return Node::null(); } } @@ -385,10 +382,11 @@ void TheoryArith::check(Effort effortLevel){ while(!done()){ Node assertion = get(); - bool conflictDuringAnAssert = assertionCases(assertion); + Node possibleConflict = assertionCases(assertion); - if(conflictDuringAnAssert){ + if(!possibleConflict.isNull()){ d_partialModel.revertAssignmentChanges(); + d_out->conflict(possibleConflict); return; } } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index ef93b7d64..07ba08e9c 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -203,14 +203,15 @@ private: /** * Handles the case splitting for check() for a new assertion. - * returns true if their is a conflict. + * Returns a conflict if one was found. + * Returns Node::null if no conflict was found. */ - bool assertionCases(TNode assertion); + Node assertionCases(TNode assertion); /** * This is used for reporting conflicts caused by disequalities during assertionCases. */ - void disequalityConflict(TNode eq, TNode lb, TNode ub); + Node disequalityConflict(TNode eq, TNode lb, TNode ub); /** * Returns the basic variable with the shorted row containg a non-basic variable. -- 2.30.2