#include "util/rational.h"
#include "util/integer.h"
+#include "util/boolean_simplification.h"
+
#include "theory/rewriter.h"
#include "theory/arith/theory_arith.h"
#include "theory/arith/normal_form.h"
+#include "theory/arith/arith_prop_manager.h"
#include <stdint.h>
static const uint32_t RESET_START = 2;
struct SlackAttrID;
-typedef expr::Attribute<SlackAttrID, Node> Slack;
+typedef expr::Attribute<SlackAttrID, bool> Slack;
TheoryArith::TheoryArith(context::Context* c, OutputChannel& out, Valuation valuation) :
Theory(THEORY_ARITH, c, out, valuation),
d_tableauResetDensity(1.6),
d_tableauResetPeriod(10),
d_propagator(c, out),
- d_simplex(d_partialModel, d_tableau),
+ d_propManager(c, d_arithvarNodeMap, d_propagator, valuation),
+ d_simplex(d_propManager, d_partialModel, d_tableau),
d_DELTA_ZERO(0),
d_statistics()
{}
if(isRelationOperator(k)){
Assert(Comparison::isNormalAtom(n));
+ //cout << n << endl;
d_propagator.addAtom(n);
if(left.getKind() == PLUS){
//We may need to introduce a slack variable.
Assert(left.getNumChildren() >= 2);
- if(!left.hasAttribute(Slack())){
+ if(!left.getAttribute(Slack())){
setupSlack(left);
}
}
ArithVar TheoryArith::requestArithVar(TNode x, bool basic){
- Assert(isLeaf(x));
- Assert(!hasArithVar(x));
+ Assert(isLeaf(x) || x.getKind() == PLUS);
+ Assert(!d_arithvarNodeMap.hasArithVar(x));
ArithVar varX = d_variables.size();
d_variables.push_back(Node(x));
d_simplex.increaseMax();
- setArithVar(x,varX);
+ d_arithvarNodeMap.setArithVar(x,varX);
d_userVariables.init(varX, !basic);
d_tableau.increaseSize();
Debug("rewriter") << "should be var: " << n << endl;
Assert(isLeaf(n));
- Assert(hasArithVar(n));
+ Assert(d_arithvarNodeMap.hasArithVar(n));
- ArithVar av = asArithVar(n);
+ ArithVar av = d_arithvarNodeMap.asArithVar(n);
coeffs.push_back(constant.getValue());
variables.push_back(av);
}
void TheoryArith::setupSlack(TNode left){
+ Assert(!left.getAttribute(Slack()));
++(d_statistics.d_statSlackVariables);
- TypeNode real_type = NodeManager::currentNM()->realType();
- Node slack = NodeManager::currentNM()->mkVar(real_type);
- left.setAttribute(Slack(), slack);
+ left.setAttribute(Slack(), true);
- ArithVar varSlack = requestArithVar(slack, true);
+ ArithVar varSlack = requestArithVar(left, true);
Polynomial polyLeft = Polynomial::parsePolynomial(left);
Debug("arith") << "registerTerm(" << tn << ")" << endl;
}
-template <bool selectLeft>
-TNode getSide(TNode assertion, Kind simpleKind){
- switch(simpleKind){
- case LT:
- case GT:
- case DISTINCT:
- return selectLeft ? (assertion[0])[0] : (assertion[0])[1];
- case LEQ:
- case GEQ:
- case EQUAL:
- return selectLeft ? assertion[0] : assertion[1];
- default:
- Unreachable();
- return TNode::null();
- }
-}
ArithVar TheoryArith::determineLeftVariable(TNode assertion, Kind simpleKind){
TNode left = getSide<true>(assertion, simpleKind);
if(isLeaf(left)){
- return asArithVar(left);
+ return d_arithvarNodeMap.asArithVar(left);
}else{
Assert(left.hasAttribute(Slack()));
- TNode slack = left.getAttribute(Slack());
- return asArithVar(slack);
+ return d_arithvarNodeMap.asArithVar(left);
}
}
-DeltaRational determineRightConstant(TNode assertion, Kind simpleKind){
- TNode right = getSide<false>(assertion, simpleKind);
-
- Assert(right.getKind() == CONST_RATIONAL);
- const Rational& noninf = right.getConst<Rational>();
-
- Rational inf = Rational(Integer(deltaCoeff(simpleKind)));
- return DeltaRational(noninf, inf);
-}
Node TheoryArith::disequalityConflict(TNode eq, TNode lb, TNode ub){
NodeBuilder<3> conflict(kind::AND);
if(!possibleConflict.isNull()){
d_partialModel.revertAssignmentChanges();
+ //Node simpleConflict = BooleanSimplification::simplifyConflict(possibleConflict);
+
+ Debug("arith::conflict") << "conflict " << possibleConflict << endl;
+
+ d_simplex.clearUpdates();
d_out->conflict(possibleConflict);
return;
}
}
- if(Debug.isOn("arith::print_assertions") && fullEffort(effortLevel)) {
+ if(Debug.isOn("arith::print_assertions")) {
debugPrintAssertions();
}
Node possibleConflict = d_simplex.updateInconsistentVars();
if(possibleConflict != Node::null()){
-
d_partialModel.revertAssignmentChanges();
+ d_simplex.clearUpdates();
+
+ //Node simpleConflict = BooleanSimplification::simplifyConflict(possibleConflict);
+
+ Debug("arith::conflict") << "conflict " << possibleConflict << endl;
d_out->conflict(possibleConflict);
}else{
}
}
+/*
+bool TheoryArith::isImpliedUpperBound(ArithVar var, Node exp){
+ Node varAsNode = asNode(var);
+ const DeltaRational& ub = d_partialModel.getUpperBound(var);
+ Assert(ub.getInfinitesimalPart() <= 0 );
+ Kind kind = ub.getInfinitesimalPart() < 0 ? LT : LEQ;
+ Node ubAsNode = NodeBuilder<2>(kind) << varAsNode << mkRationalNode(ub.getNoninfinitesimalPart());
+ Node bestImplied = d_propagator.getBestImpliedUpperBound(ubAsNode);
+
+ return bestImplied == exp;
+}
+
+bool TheoryArith::isImpliedLowerBound(ArithVar var, Node exp){
+ Node varAsNode = asNode(var);
+ const DeltaRational& lb = d_partialModel.getLowerBound(var);
+ Assert(lb.getInfinitesimalPart() >= 0 );
+ Kind kind = lb.getInfinitesimalPart() > 0 ? GT : GEQ;
+ Node lbAsIneq = NodeBuilder<2>(kind) << varAsNode << mkRationalNode(lb.getNoninfinitesimalPart());
+ Node bestImplied = d_propagator.getBestImpliedLowerBound(lbAsIneq);
+ return bestImplied == exp;
+}
+*/
+
void TheoryArith::explain(TNode n) {
+ Debug("explain") << "explain @" << getContext()->getLevel() << ": " << n << endl;
+ //Assert(n.hasAttribute(Propagated()));
+
+ //NodeBuilder<> explainBuilder(AND);
+ //internalExplain(n,explainBuilder);
+ Assert(d_propManager.isPropagated(n));
+ Node explanation = d_propManager.explain(n);
+ //Node flatExplanation = BooleanSimplification::simplifyConflict(explanation);
+
+ d_out->explanation(explanation, true);
+}
+/*
+void TheoryArith::internalExplain(TNode n, NodeBuilder<>& explainBuilder){
+ Assert(n.hasAttribute(Propagated()));
+ Node bound = n.getAttribute(Propagated());
+
+ AlwaysAssert(bound.getKind() == kind::AND);
+
+ for(Node::iterator i = bound.begin(), end = bound.end(); i != end; ++i){
+ Node lit = *i;
+ if(lit.hasAttribute(Propagated())){
+ cout << "hoop the sadjklasdj" << endl;
+ internalExplain(lit, explainBuilder);
+ }else{
+ explainBuilder << lit;
+ }
+ }
+}
+*/
+/*
+static const bool EXPORT_LEMMA_INSTEAD_OF_PROPAGATE = false;
+void TheoryArith::propagateArithVar(bool upperbound, ArithVar var ){
+ Node varAsNode = asNode(var);
+ const DeltaRational& b = upperbound ?
+ d_partialModel.getUpperBound(var) : d_partialModel.getLowerBound(var);
+
+ Assert((!upperbound) || (b.getInfinitesimalPart() <= 0) );
+ Assert(upperbound || (b.getInfinitesimalPart() >= 0) );
+ Kind kind;
+ if(upperbound){
+ kind = b.getInfinitesimalPart() < 0 ? LT : LEQ;
+ } else{
+ kind = b.getInfinitesimalPart() > 0 ? GT : GEQ;
+ }
+
+ Node bAsNode = NodeBuilder<2>(kind) << varAsNode
+ << mkRationalNode(b.getNoninfinitesimalPart());
+
+ Node bestImplied = upperbound ?
+ d_propagator.getBestImpliedUpperBound(bAsNode):
+ d_propagator.getBestImpliedLowerBound(bAsNode);
+
+ if(!bestImplied.isNull()){
+ Node satValue = d_valuation.getSatValue(bestImplied);
+ if(satValue.isNull()){
+
+ Node reason = upperbound ?
+ d_partialModel.getUpperConstraint(var) :
+ d_partialModel.getLowerConstraint(var);
+
+ //cout << getContext()->getLevel() << " " << bestImplied << " " << reason << endl;
+ if(EXPORT_LEMMA_INSTEAD_OF_PROPAGATE){
+ Node lemma = NodeBuilder<2>(IMPLIES) << reason
+ << bestImplied;
+
+ //Temporary
+ Node clause = BooleanSimplification::simplifyHornClause(lemma);
+ d_out->lemma(clause);
+ }else{
+ Assert(!bestImplied.hasAttribute(Propagated()));
+ bestImplied.setAttribute(Propagated(), reason);
+ d_reasons.push_back(reason);
+ d_out->propagate(bestImplied);
+ }
+ }else{
+ Assert(!satValue.isNull());
+ Assert(satValue.getKind() == CONST_BOOLEAN);
+ Assert(satValue.getConst<bool>());
+ }
+ }
}
+*/
void TheoryArith::propagate(Effort e) {
if(quickCheckOrMore(e)){
- while(d_simplex.hasMoreLemmas()){
- Node lemma = d_simplex.popLemma();
- d_out->lemma(lemma);
+ bool propagated = false;
+ if(Options::current()->arithPropagation && d_simplex.hasAnyUpdates()){
+ d_simplex.propagateCandidates();
+ }else{
+ d_simplex.clearUpdates();
+ }
+
+ while(d_propManager.hasMorePropagations()){
+ TNode toProp = d_propManager.getPropagation();
+ Node satValue = d_valuation.getSatValue(toProp);
+ AlwaysAssert(satValue.isNull());
+ TNode exp = d_propManager.explain(toProp);
+ propagated = true;
+ d_out->propagate(toProp);
+ }
+
+ if(!propagated){
+ //Opportunistically export previous conflicts
+ while(d_simplex.hasMoreLemmas()){
+ Node lemma = d_simplex.popLemma();
+ d_out->lemma(lemma);
+ }
}
}
}
switch(n.getKind()) {
case kind::VARIABLE: {
- ArithVar var = asArithVar(n);
+ ArithVar var = d_arithvarNodeMap.asArithVar(n);
if(d_removedRows.find(var) != d_removedRows.end()){
Node eq = d_removedRows.find(var)->second;
bool TheoryArith::entireStateIsConsistent(){
typedef std::vector<Node>::const_iterator VarIter;
for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){
- ArithVar var = asArithVar(*i);
+ ArithVar var = d_arithvarNodeMap.asArithVar(*i);
if(!d_partialModel.assignmentIsConsistent(var)){
d_partialModel.printModel(var);
cerr << "Assignment is not consistent for " << var << *i << endl;
Assert(!noRow);
//remove the row from the tableau
- Node eq = d_tableau.rowAsEquality(v, d_arithVarToNodeMap);
+ Node eq = d_tableau.rowAsEquality(v, d_arithvarNodeMap.getArithVarToNodeMap());
d_tableau.removeRow(v);
if(Debug.isOn("tableau")) d_tableau.printTableau();
d_removedRows[v] = eq;
}
- Debug("arith::permanentlyRemoveVariable") << "Permanently removed variable "
- << v << ":" << asNode(v) << endl;
+ Debug("arith::permanentlyRemoveVariable") << "Permanently removed variable " << v
+ << ":" << d_arithvarNodeMap.asNode(v) <<endl;
++(d_statistics.d_permanentlyRemovedVariables);
}
typedef std::vector<Node>::const_iterator VarIter;
for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){
Node variableNode = *i;
- ArithVar var = asArithVar(variableNode);
+ ArithVar var = d_arithvarNodeMap.asArithVar(variableNode);
if(d_userVariables.isMember(var) && !d_propagator.hasAnyAtoms(variableNode)){
//The user variable is unconstrained.
//Remove this variable permanently
projects / cvc5.git / blobdiff