}
/** is k \in {LT, LEQ, EQ, GEQ, GT} */
-inline Kind negateRelationKind(Kind k){
+inline Kind reverseRelationKind(Kind k){
using namespace kind;
switch(k){
Unreachable();
}
}
+
inline bool evaluateConstantPredicate(Kind k, const Rational& left, const Rational& right){
using namespace kind;
}
/**
- * Given a rewritten predicate to TheoryArith return a single kind to
+ * Given a literal to TheoryArith return a single kind to
* to indicate its underlying structure.
* The function returns the following in each case:
- * - (K left right) -> K where is a wildcard for EQUAL, LEQ, or GEQ:
+ * - (K left right) -> K where is a wildcard for EQUAL, LT, GT, LEQ, or GEQ:
* - (NOT (EQUAL left right)) -> DISTINCT
* - (NOT (LEQ left right)) -> GT
* - (NOT (GEQ left right)) -> LT
+ * - (NOT (LT left right)) -> GEQ
+ * - (NOT (GT left right)) -> LEQ
* If none of these match, it returns UNDEFINED_KIND.
*/
inline Kind simplifiedKind(TNode assertion){
switch(assertion.getKind()){
+ case kind::LT:
+ case kind::GT:
case kind::LEQ:
- case kind::GEQ:
- case kind::EQUAL:
+ case kind::GEQ:
+ case kind::EQUAL:
return assertion.getKind();
case kind::NOT:
{
switch(atom.getKind()){
case kind::LEQ: //(not (LEQ x c)) <=> (GT x c)
return kind::GT;
- case kind::GEQ: //(not (GEQ x c) <=> (LT x c)
+ case kind::GEQ: //(not (GEQ x c)) <=> (LT x c)
return kind::LT;
+ case kind::LT: //(not (LT x c)) <=> (GEQ x c)
+ return kind::GEQ;
+ case kind::GT: //(not (GT x c) <=> (LEQ x c)
+ return kind::LEQ;
case kind::EQUAL:
return kind::DISTINCT;
default:
Comparison Comparison::multiplyConstant(const Constant& constant) const {
Assert(!isBoolean());
- Kind newOper = (constant.getValue() < 0) ? negateRelationKind(oper) : oper;
+ Kind newOper = (constant.getValue() < 0) ? reverseRelationKind(oper) : oper;
return mkComparison(newOper, left*Monomial(constant), right*constant);
}
d_statAssertLowerConflicts("theory::arith::AssertLowerConflicts", 0),
d_statUpdateConflicts("theory::arith::UpdateConflicts", 0),
d_statEjections("theory::arith::Ejections", 0),
- d_statUnEjections("theory::arith::UnEjections", 0)
+ d_statUnEjections("theory::arith::UnEjections", 0),
+ d_statEarlyConflicts("theory::arith::EarlyConflicts", 0),
+ d_statEarlyConflictImprovements("theory::arith::EarlyConflictImprovements", 0),
+ d_selectInitialConflictTime("theory::arith::selectInitialConflictTime")
{
StatisticsRegistry::registerStat(&d_statPivots);
StatisticsRegistry::registerStat(&d_statUpdates);
StatisticsRegistry::registerStat(&d_statUpdateConflicts);
StatisticsRegistry::registerStat(&d_statEjections);
StatisticsRegistry::registerStat(&d_statUnEjections);
+ StatisticsRegistry::registerStat(&d_statEarlyConflicts);
+ StatisticsRegistry::registerStat(&d_statEarlyConflictImprovements);
+ StatisticsRegistry::registerStat(&d_selectInitialConflictTime);
}
SimplexDecisionProcedure::Statistics::~Statistics(){
StatisticsRegistry::unregisterStat(&d_statUpdateConflicts);
StatisticsRegistry::unregisterStat(&d_statEjections);
StatisticsRegistry::unregisterStat(&d_statUnEjections);
+ StatisticsRegistry::unregisterStat(&d_statEarlyConflicts);
+ StatisticsRegistry::unregisterStat(&d_statEarlyConflictImprovements);
+ StatisticsRegistry::unregisterStat(&d_selectInitialConflictTime);
}
return slack;
}
+Node betterConflict(TNode x, TNode y){
+ if(x.isNull()) return y;
+ else if(y.isNull()) return x;
+ else if(x.getNumChildren() <= y.getNumChildren()) return x;
+ else return y;
+}
+
+Node SimplexDecisionProcedure::selectInitialConflict() {
+ Node bestConflict = Node::null();
+
+ TimerStat::CodeTimer codeTimer(d_statistics.d_selectInitialConflictTime);
+
+ vector<VarDRatPair> init;
+
+ while( !d_griggioRuleQueue.empty()){
+ ArithVar var = d_griggioRuleQueue.top().first;
+ if(d_basicManager.isMember(var)){
+ if(!d_partialModel.assignmentIsConsistent(var)){
+ init.push_back( d_griggioRuleQueue.top());
+ }
+ }
+ d_griggioRuleQueue.pop();
+ }
+
+ int conflictChanges = 0;
+
+ for(vector<VarDRatPair>::iterator i=init.begin(), end=init.end(); i != end; ++i){
+ ArithVar x_i = (*i).first;
+ d_griggioRuleQueue.push(*i);
+
+ DeltaRational beta_i = d_partialModel.getAssignment(x_i);
+
+ if(d_partialModel.belowLowerBound(x_i, beta_i, true)){
+ DeltaRational l_i = d_partialModel.getLowerBound(x_i);
+ ArithVar x_j = selectSlackBelow(x_i);
+ if(x_j == ARITHVAR_SENTINEL ){
+ Node better = betterConflict(bestConflict, generateConflictBelow(x_i));
+ if(better != bestConflict) ++conflictChanges;
+ bestConflict = better;
+ ++(d_statistics.d_statEarlyConflicts);
+ }
+ }else if(d_partialModel.aboveUpperBound(x_i, beta_i, true)){
+ DeltaRational u_i = d_partialModel.getUpperBound(x_i);
+ ArithVar x_j = selectSlackAbove(x_i);
+ if(x_j == ARITHVAR_SENTINEL ){
+ Node better = betterConflict(bestConflict, generateConflictAbove(x_i));
+ if(better != bestConflict) ++conflictChanges;
+ bestConflict = better;
+ ++(d_statistics.d_statEarlyConflicts);
+ }
+ }
+ }
+ if(conflictChanges > 1) ++(d_statistics.d_statEarlyConflictImprovements);
+ return bestConflict;
+}
+
Node SimplexDecisionProcedure::updateInconsistentVars(){
- Node possibleConflict = privateUpdateInconsistentVars();
+ if(d_griggioRuleQueue.empty()) return Node::null();
+
+ Node possibleConflict = selectInitialConflict();
+ if(possibleConflict.isNull()){
+ possibleConflict = privateUpdateInconsistentVars();
+ }
+
Assert(!possibleConflict.isNull() || d_griggioRuleQueue.empty());
Assert(!possibleConflict.isNull() || d_possiblyInconsistent.empty());
d_pivotStage = true;
private:
Node privateUpdateInconsistentVars();
+ Node selectInitialConflict();
+
private:
/**
* Given the basic variable x_i,
IntStat d_statAssertLowerConflicts, d_statUpdateConflicts;
IntStat d_statEjections, d_statUnEjections;
+
+ IntStat d_statEarlyConflicts, d_statEarlyConflictImprovements;
+ TimerStat d_selectInitialConflictTime;
Statistics();
~Statistics();
};
d_statUserVariables("theory::arith::UserVariables", 0),
d_statSlackVariables("theory::arith::SlackVariables", 0),
d_statDisequalitySplits("theory::arith::DisequalitySplits", 0),
- d_statDisequalityConflicts("theory::arith::DisequalityConflicts", 0)
+ d_statDisequalityConflicts("theory::arith::DisequalityConflicts", 0),
+ d_staticLearningTimer("theory::arith::staticLearningTimer")
{
StatisticsRegistry::registerStat(&d_statUserVariables);
StatisticsRegistry::registerStat(&d_statSlackVariables);
StatisticsRegistry::registerStat(&d_statDisequalitySplits);
StatisticsRegistry::registerStat(&d_statDisequalityConflicts);
+ StatisticsRegistry::registerStat(&d_staticLearningTimer);
}
TheoryArith::Statistics::~Statistics(){
StatisticsRegistry::unregisterStat(&d_statSlackVariables);
StatisticsRegistry::unregisterStat(&d_statDisequalitySplits);
StatisticsRegistry::unregisterStat(&d_statDisequalityConflicts);
+ StatisticsRegistry::unregisterStat(&d_staticLearningTimer);
}
+void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) {
+ TimerStat::CodeTimer codeTimer(d_statistics.d_staticLearningTimer);
+
+ vector<TNode> workList;
+ workList.push_back(n);
+ __gnu_cxx::hash_set<TNode, TNodeHashFunction> processed;
+
+ while(!workList.empty()) {
+ n = workList.back();
+
+ bool unprocessedChildren = false;
+ for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) {
+ if(processed.find(*i) == processed.end()) {
+ // unprocessed child
+ workList.push_back(*i);
+ unprocessedChildren = true;
+ }
+ }
+
+ if(unprocessedChildren) {
+ continue;
+ }
+
+ workList.pop_back();
+ // has node n been processed in the meantime ?
+ if(processed.find(n) != processed.end()) {
+ continue;
+ }
+ processed.insert(n);
+
+ // == MINS ==
+
+ Debug("mins") << "===================== looking at" << endl << n << endl;
+ if(n.getKind() == kind::ITE && n[0].getKind() != EQUAL && isRelationOperator(n[0].getKind()) ){
+ TNode c = n[0];
+ Kind k = simplifiedKind(c);
+ TNode t = n[1];
+ TNode e = n[2];
+ TNode cleft = (c.getKind() == NOT) ? c[0][0] : c[0];
+ TNode cright = (c.getKind() == NOT) ? c[0][1] : c[1];
+
+ if((t == cright) && (e == cleft)){
+ TNode tmp = t;
+ t = e;
+ e = tmp;
+ k = reverseRelationKind(k);
+ }
+ if(t == cleft && e == cright){
+ // t == cleft && e == cright
+ Assert( t == cleft );
+ Assert( e == cright );
+ switch(k){
+ case LT: // (ite (< x y) x y)
+ case LEQ: { // (ite (<= x y) x y)
+ Node nLeqX = NodeBuilder<2>(LEQ) << n << t;
+ Node nLeqY = NodeBuilder<2>(LEQ) << n << e;
+ Debug("arith::mins") << n << "is a min =>" << nLeqX << nLeqY << endl;
+ learned << nLeqX << nLeqY;
+ break;
+ }
+ case GT: // (ite (> x y) x y)
+ case GEQ: { // (ite (>= x y) x y)
+ Node nGeqX = NodeBuilder<2>(GEQ) << n << t;
+ Node nGeqY = NodeBuilder<2>(GEQ) << n << e;
+ Debug("arith::mins") << n << "is a max =>" << nGeqX << nGeqY << endl;
+ learned << nGeqX << nGeqY;
+ break;
+ }
+ default: Unreachable();
+ }
+ }
+ }
+ // == 2-CONSTANTS ==
+
+ if(n.getKind() == ITE &&
+ (n[1].getKind() == CONST_RATIONAL || n[1].getKind() == CONST_INTEGER) &&
+ (n[2].getKind() == CONST_RATIONAL || n[2].getKind() == CONST_INTEGER)) {
+ Rational t = coerceToRational(n[1]);
+ Rational e = coerceToRational(n[2]);
+ TNode min = (t <= e) ? n[1] : n[2];
+ TNode max = (t >= e) ? n[1] : n[2];
+
+ Node nGeqMin = NodeBuilder<2>(GEQ) << n << min;
+ Node nLeqMax = NodeBuilder<2>(LEQ) << n << max;
+ Debug("arith::mins") << n << " is a constant sandwich" << nGeqMin << nLeqMax << endl;
+ learned << nGeqMin << nLeqMax;
+ }
+
+ // // binary OR of binary ANDs of EQUALities
+ // if(n.getKind() == kind::OR && n.getNumChildren() == 2 &&
+ // n[0].getKind() == kind::AND && n[0].getNumChildren() == 2 &&
+ // n[1].getKind() == kind::AND && n[1].getNumChildren() == 2 &&
+ // (n[0][0].getKind() == kind::EQUAL || n[0][0].getKind() == kind::IFF) &&
+ // (n[0][1].getKind() == kind::EQUAL || n[0][1].getKind() == kind::IFF) &&
+ // (n[1][0].getKind() == kind::EQUAL || n[1][0].getKind() == kind::IFF) &&
+ // (n[1][1].getKind() == kind::EQUAL || n[1][1].getKind() == kind::IFF)) {
+ // // now we have (a = b && c = d) || (e = f && g = h)
+
+ // Debug("diamonds") << "has form of a diamond!" << endl;
+
+ // TNode
+ // a = n[0][0][0], b = n[0][0][1],
+ // c = n[0][1][0], d = n[0][1][1],
+ // e = n[1][0][0], f = n[1][0][1],
+ // g = n[1][1][0], h = n[1][1][1];
+
+ // // test that one of {a, b} = one of {c, d}, and make "b" the
+ // // shared node (i.e. put in the form (a = b && b = d))
+ // // note we don't actually care about the shared ones, so the
+ // // "swaps" below are one-sided, ignoring b and c
+ // if(a == c) {
+ // a = b;
+ // } else if(a == d) {
+ // a = b;
+ // d = c;
+ // } else if(b == c) {
+ // // nothing to do
+ // } else if(b == d) {
+ // d = c;
+ // } else {
+ // // condition not satisfied
+ // Debug("diamonds") << "+ A fails" << endl;
+ // continue;
+ // }
+
+ // Debug("diamonds") << "+ A holds" << endl;
+
+ // // same: one of {e, f} = one of {g, h}, and make "f" the
+ // // shared node (i.e. put in the form (e = f && f = h))
+ // if(e == g) {
+ // e = f;
+ // } else if(e == h) {
+ // e = f;
+ // h = g;
+ // } else if(f == g) {
+ // // nothing to do
+ // } else if(f == h) {
+ // h = g;
+ // } else {
+ // // condition not satisfied
+ // Debug("diamonds") << "+ B fails" << endl;
+ // continue;
+ // }
+
+ // Debug("diamonds") << "+ B holds" << endl;
+
+ // // now we have (a = b && b = d) || (e = f && f = h)
+ // // test that {a, d} == {e, h}
+ // if( (a == e && d == h) ||
+ // (a == h && d == e) ) {
+ // // learn: n implies a == d
+ // Debug("diamonds") << "+ C holds" << endl;
+ // Node newEquality = a.getType().isBoolean() ? a.iffNode(d) : a.eqNode(d);
+ // Debug("diamonds") << " ==> " << newEquality << endl;
+ // learned << n.impNode(newEquality);
+ // } else {
+ // Debug("diamonds") << "+ C fails" << endl;
+ // }
+ // }
+ }
+}
check(FULL_EFFORT);
}
+ void staticLearning(TNode in, NodeBuilder<>& learned);
+
std::string identify() const { return std::string("TheoryArith"); }
private:
IntStat d_statUserVariables, d_statSlackVariables;
IntStat d_statDisequalitySplits;
IntStat d_statDisequalityConflicts;
+ TimerStat d_staticLearningTimer;
Statistics();
~Statistics();
projects / cvc5.git / commitdiff