From 629824db3911ab11ae286e4b14151a537602ba5a Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 10 Jun 2014 17:32:57 -0400 Subject: [PATCH] Merging Tim's pseudoboolean work from his fmcad14 branch. Signed-off-by: Morgan Deters --- src/Makefile.am | 2 + src/smt/smt_engine.cpp | 14 + src/theory/arith/options | 12 +- src/theory/arith/pseudoboolean_proc.cpp | 325 ++++++++++++++++++++++++ src/theory/arith/pseudoboolean_proc.h | 110 ++++++++ 5 files changed, 462 insertions(+), 1 deletion(-) create mode 100644 src/theory/arith/pseudoboolean_proc.cpp create mode 100644 src/theory/arith/pseudoboolean_proc.h diff --git a/src/Makefile.am b/src/Makefile.am index f3bd85825..34fa20c1d 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -389,6 +389,8 @@ libcvc4_la_SOURCES = \ theory/arith/arith_unate_lemma_mode.cpp \ theory/arith/arith_propagation_mode.h \ theory/arith/arith_propagation_mode.cpp \ + theory/arith/pseudoboolean_proc.h \ + theory/arith/pseudoboolean_proc.cpp \ theory/arith/cut_log.h \ theory/arith/cut_log.cpp \ theory/arith/options_handlers.h \ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6dbef4fe3..b71969d15 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -88,6 +88,8 @@ #include "theory/strings/theory_strings_preprocess.h" #include "printer/options.h" +#include "theory/arith/pseudoboolean_proc.h" + using namespace std; using namespace CVC4; using namespace CVC4::smt; @@ -325,6 +327,9 @@ public: RemoveITE d_iteRemover; private: + + theory::arith::PseudoBooleanProcessor d_pbsProcessor; + /** The top level substitutions */ SubstitutionMap d_topLevelSubstitutions; @@ -419,6 +424,7 @@ public: d_simplifyAssertionsDepth(0), d_iteSkolemMap(), d_iteRemover(smt.d_userContext), + d_pbsProcessor(smt.d_userContext), d_topLevelSubstitutions(smt.d_userContext) { d_smt.d_nodeManager->subscribeEvents(this); @@ -1693,6 +1699,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { TimerStat::CodeTimer nonclausalTimer(d_smt.d_stats->d_nonclausalSimplificationTime); + Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify()" << endl; if(d_propagatorNeedsFinish) { @@ -3014,6 +3021,13 @@ void SmtEnginePrivate::processAssertions() { // d_smt.d_theoryEngine->getQuantConflictFind()->registerAssertions( d_assertionsToPreprocess ); //} + if( options::pbRewrites() ){ + d_pbsProcessor.learn(d_assertionsToPreprocess); + if(d_pbsProcessor.likelyToHelp()){ + d_pbsProcessor.applyReplacements(d_assertionsToPreprocess); + } + } + dumpAssertions("pre-simplify", d_assertionsToPreprocess); Chat() << "simplifying assertions..." << endl; bool noConflict = simplifyAssertions(); diff --git a/src/theory/arith/options b/src/theory/arith/options index 6a9005a9a..ea9658eb3 100644 --- a/src/theory/arith/options +++ b/src/theory/arith/options @@ -149,6 +149,16 @@ option soiApproxMinorFailurePen --replay-soi-minor-threshold-pen int :default 10 threshold for a minor tolerance failure by the approximate solver option ppAssertMaxSubSize --pp-assert-max-sub-size unsigned :default 2 - threshold threshold for substituting an equality in ppAssert + threshold for substituting an equality in ppAssert + +option maxReplayTree --max-replay-tree int :default 512 + threshold for attempting to replay a tree + + +option pbRewrites --pb-rewrites bool :default false + apply pseudo boolean rewrites + +option pbRewriteThreshold --pb-rewrite-threshold int :default 256 + threshold of number of pseudoboolean variables to have before doing rewrites endmodule diff --git a/src/theory/arith/pseudoboolean_proc.cpp b/src/theory/arith/pseudoboolean_proc.cpp new file mode 100644 index 000000000..829952c5e --- /dev/null +++ b/src/theory/arith/pseudoboolean_proc.cpp @@ -0,0 +1,325 @@ +/********************* */ +/*! \file pseudoboolean_proc.cpp + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** 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 + **/ + +#include "theory/arith/pseudoboolean_proc.h" +#include "theory/arith/normal_form.h" +#include "theory/arith/arith_utilities.h" +#include "theory/rewriter.h" + +namespace CVC4 { +namespace theory { +namespace arith { + + +PseudoBooleanProcessor::PseudoBooleanProcessor(context::Context* user_context) + : d_pbBounds(user_context) + , d_subCache(user_context) + , d_pbs(user_context, 0) +{} + +bool PseudoBooleanProcessor::decomposeAssertion(Node assertion, bool negated){ + if (assertion.getKind() != kind::GEQ){ return false; } + Assert(assertion.getKind() == kind::GEQ); + + Debug("pbs::rewrites") << "decomposeAssertion" << assertion << std::endl; + + Node l = assertion[0]; + Node r = assertion[1]; + + if( r.getKind() != kind::CONST_RATIONAL ){ + Debug("pbs::rewrites") << "not rhs constant" << assertion << std::endl; + return false; + } + // don't bother matching on anything other than + on the left hand side + if( l.getKind() != kind::PLUS){ + Debug("pbs::rewrites") << "not plus" << assertion << std::endl; + return false; + } + + if(!Polynomial::isMember(l)){ + Debug("pbs::rewrites") << "not polynomial" << assertion << std::endl; + return false; + } + + Polynomial p = Polynomial::parsePolynomial(l); + clear(); + if(negated){ + // (not (>= p r)) + // (< p r) + // (> (-p) (-r)) + // (>= (-p) (-r +1)) + d_off = (-r.getConst()); + + if(d_off.constValue().isIntegral()){ + d_off = d_off.constValue() + Rational(1) ; + }else{ + d_off = Rational(d_off.constValue().ceiling()); + } + }else{ + // (>= p r) + d_off = r.getConst(); + d_off = Rational(d_off.constValue().ceiling()); + } + Assert(d_off.constValue().isIntegral()); + + int adj = negated ? -1 : 1; + for(Polynomial::iterator i=p.begin(), end=p.end(); i != end; ++i){ + Monomial m = *i; + const Rational& coeff = m.getConstant().getValue(); + if(!(coeff.isOne() || coeff.isNegativeOne())){ return false; } + Assert(coeff.sgn() != 0); + + const VarList& vl = m.getVarList(); + Node v = vl.getNode(); + + if(!isPseudoBoolean(v)){ return false; } + int sgn = adj * coeff.sgn(); + if(sgn > 0){ + d_pos.push_back(v); + }else{ + d_neg.push_back(v); + } + } + // all of the variables are pseudoboolean + // with coefficients +/- and the offsetoff + return true; +} + +bool PseudoBooleanProcessor::isPseudoBoolean(Node v) const{ + CDNode2PairMap::const_iterator ci = d_pbBounds.find(v); + if(ci != d_pbBounds.end()){ + const PairNode& p = (*ci).second; + return !(p.first).isNull() && !(p.second).isNull(); + } + return false; +} + +void PseudoBooleanProcessor::addGeqZero(Node v, Node exp){ + Assert(isIntVar(v)); + Assert(!exp.isNull()); + CDNode2PairMap::const_iterator ci = d_pbBounds.find(v); + + Debug("pbs::rewrites") << "addGeqZero " << v << std::endl; + + if(ci == d_pbBounds.end()){ + d_pbBounds.insert(v, std::make_pair(exp, Node::null())); + }else{ + const PairNode& p = (*ci).second; + if(p.first.isNull()){ + Assert(!p.second.isNull()); + d_pbBounds.insert(v, std::make_pair(exp, p.second)); + Debug("pbs::rewrites") << "add pbs " << v << std::endl; + Assert(isPseudoBoolean(v)); + d_pbs = d_pbs + 1; + } + } +} + +void PseudoBooleanProcessor::addLeqOne(Node v, Node exp){ + Assert(isIntVar(v)); + Assert(!exp.isNull()); + Debug("pbs::rewrites") << "addLeqOne " << v << std::endl; + CDNode2PairMap::const_iterator ci = d_pbBounds.find(v); + if(ci == d_pbBounds.end()){ + d_pbBounds.insert(v, std::make_pair(Node::null(), exp)); + }else{ + const PairNode& p = (*ci).second; + if(p.second.isNull()){ + Assert(!p.first.isNull()); + d_pbBounds.insert(v, std::make_pair(p.first, exp)); + Debug("pbs::rewrites") << "add pbs " << v << std::endl; + Assert(isPseudoBoolean(v)); + d_pbs = d_pbs + 1; + } + } +} + +void PseudoBooleanProcessor::learnRewrittenGeq(Node assertion, bool negated, Node orig){ + Assert(assertion.getKind() == kind::GEQ); + Assert(assertion == Rewriter::rewrite(assertion)); + + // assume assertion is rewritten + Node l = assertion[0]; + Node r = assertion[1]; + + + if(r.getKind() == kind::CONST_RATIONAL){ + const Rational& rc = r.getConst(); + if(isIntVar(l)){ + if(!negated && rc.isZero()){ // (>= x 0) + addGeqZero(l, orig); + }else if(negated && rc == Rational(2)){ + addLeqOne(l, orig); + } + }else if(l.getKind() == kind::MULT && l.getNumChildren() == 2){ + Node c = l[0], v = l[1]; + if(c.getKind() == kind::CONST_RATIONAL && c.getConst().isNegativeOne()){ + if(isIntVar(v)){ + if(!negated && rc.isNegativeOne()){ // (>= (* -1 x) -1) + addLeqOne(v, orig); + } + } + } + } + } + + if(!negated){ + learnGeqSub(assertion); + } +} + +void PseudoBooleanProcessor::learnInternal(Node assertion, bool negated, Node orig){ + switch(assertion.getKind()){ + case kind::GEQ: + case kind::GT: + case kind::LEQ: + case kind::LT: + { + Node rw = Rewriter::rewrite(assertion); + if(assertion == rw){ + if(assertion.getKind() == kind::GEQ){ + learnRewrittenGeq(assertion, negated, orig); + } + }else{ + learnInternal(rw, negated, orig); + } + } + break; + case kind::NOT: + learnInternal(assertion[0], !negated, orig); + break; + default: + break; // do nothing + } +} + +void PseudoBooleanProcessor::learn(Node assertion){ + if(assertion.getKind() == kind::AND){ + Node::iterator ci=assertion.begin(), cend = assertion.end(); + for(; ci != cend; ++ci){ + learn(*ci); + } + }else{ + learnInternal(assertion, false, assertion); + } +} + +Node PseudoBooleanProcessor::mkGeqOne(Node v){ + NodeManager* nm = NodeManager::currentNM(); + return nm->mkNode(kind::GEQ, v, mkRationalNode(Rational(1))); +} + +void PseudoBooleanProcessor::learn(const NodeVec& assertions){ + NodeVec::const_iterator ci, cend; + ci = assertions.begin(); cend=assertions.end(); + for(; ci != cend; ++ci ){ + learn(*ci); + } +} + +void PseudoBooleanProcessor::addSub(Node from, Node to){ + if(!d_subCache.hasSubstitution(from)){ + Node rw_to = Rewriter::rewrite(to); + d_subCache.addSubstitution(from, rw_to); + } +} + +void PseudoBooleanProcessor::learnGeqSub(Node geq){ + Assert(geq.getKind() == kind::GEQ); + const bool negated = false; + bool success = decomposeAssertion(geq, negated); + if(!success){ + Debug("pbs::rewrites") << "failed " << std::endl; + return; + } + Assert(d_off.constValue().isIntegral()); + Integer off = d_off.constValue().ceiling(); + + // \sum pos >= \sum neg + off + + // for now special case everything we want + // target easy clauses + if( d_pos.size() == 1 && d_neg.size() == 1 && off.isZero() ){ + // x >= y + // |- (y >= 1) => (x >= 1) + Node x = d_pos.front(); + Node y = d_neg.front(); + + Node xGeq1 = mkGeqOne(x); + Node yGeq1 = mkGeqOne(y); + Node imp = yGeq1.impNode(xGeq1); + addSub(geq, imp); + }else if( d_pos.size() == 0 && d_neg.size() == 2 && off.isNegativeOne()){ + // 0 >= (x + y -1) + // |- 1 >= x + y + // |- (or (not (x >= 1)) (not (y >= 1))) + Node x = d_neg[0]; + Node y = d_neg[1]; + + Node xGeq1 = mkGeqOne(x); + Node yGeq1 = mkGeqOne(y); + Node cases = (xGeq1.notNode()).orNode(yGeq1.notNode()); + addSub(geq, cases); + }else if( d_pos.size() == 2 && d_neg.size() == 1 && off.isZero() ){ + // (x + y) >= z + // |- (z >= 1) => (or (x >= 1) (y >=1 )) + Node x = d_pos[0]; + Node y = d_pos[1]; + Node z = d_neg[0]; + + Node xGeq1 = mkGeqOne(x); + Node yGeq1 = mkGeqOne(y); + Node zGeq1 = mkGeqOne(z); + NodeManager* nm =NodeManager::currentNM(); + Node dis = nm->mkNode(kind::OR, zGeq1.notNode(), xGeq1, yGeq1); + addSub(geq, dis); + } +} + +Node PseudoBooleanProcessor::applyReplacements(Node pre){ + Node assertion = Rewriter::rewrite(pre); + + Node result = d_subCache.apply(assertion); + if(Debug.isOn("pbs::rewrites") && result != assertion ){ + Debug("pbs::rewrites") << "applyReplacements" < " << result << std::endl; + } + return result; +} + +bool PseudoBooleanProcessor::likelyToHelp() const{ + return d_pbs >= 100; +} + +void PseudoBooleanProcessor::applyReplacements(NodeVec& assertions){ + for(size_t i=0, N=assertions.size(); i < N; ++i){ + Node assertion = assertions[i]; + Node res = applyReplacements(assertion); + assertions[i] = res; + } +} + +void PseudoBooleanProcessor::clear() { + d_off.clear(); + d_pos.clear(); + d_neg.clear(); +} + + +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + diff --git a/src/theory/arith/pseudoboolean_proc.h b/src/theory/arith/pseudoboolean_proc.h new file mode 100644 index 000000000..665f1aa06 --- /dev/null +++ b/src/theory/arith/pseudoboolean_proc.h @@ -0,0 +1,110 @@ +/********************* */ +/*! \file pseudoboolean_proc.h + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** 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 + **/ + +#include "cvc4_private.h" + +#pragma once + +#include +#include "util/rational.h" +#include "util/maybe.h" +#include "expr/node.h" + +#include "context/context.h" +#include "context/cdo.h" +#include "context/cdhashmap.h" + +#include "theory/substitutions.h" +#include + +namespace CVC4 { +namespace theory { +namespace arith { + +class PseudoBooleanProcessor { +private: + // x -> + typedef std::pair PairNode; + typedef std::vector NodeVec; + typedef context::CDHashMap CDNode2PairMap; + CDNode2PairMap d_pbBounds; + SubstitutionMap d_subCache; + + typedef __gnu_cxx::hash_set NodeSet; + NodeSet d_learningCache; + + context::CDO d_pbs; + + // decompose into \sum pos >= neg + off + Maybe d_off; + NodeVec d_pos; + NodeVec d_neg; + void clear(); + /** Returns true if successful. */ + bool decomposeAssertion(Node assertion, bool negated); + +public: + PseudoBooleanProcessor(context::Context* user_context); + + /** Assumes that the assertions have been rewritten. */ + void learn(const NodeVec& assertions); + + /** Assumes that the assertions have been rewritten. */ + void applyReplacements(NodeVec& assertions); + + bool likelyToHelp() const; + + bool isPseudoBoolean(Node v) const; + + // Adds the fact the that integert typed variable v + // must be >= 0 to the context. + // This is explained by the explanation exp. + // exp cannot be null. + void addGeqZero(Node v, Node exp); + + + // Adds the fact the that integert typed variable v + // must be <= 1 to the context. + // This is explained by the explanation exp. + // exp cannot be null. + void addLeqOne(Node v, Node exp); + + static inline bool isIntVar(Node v){ + return v.isVar() && v.getType().isInteger(); + } + +private: + /** Assumes that the assertion has been rewritten. */ + void learn(Node assertion); + + /** Rewrites a node */ + Node applyReplacements(Node assertion); + + void learnInternal(Node assertion, bool negated, Node orig); + void learnRewrittenGeq(Node assertion, bool negated, Node orig); + + void addSub(Node from, Node to); + void learnGeqSub(Node geq); + + static Node mkGeqOne(Node v); +}; + + +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + -- 2.30.2