From e968ea45fd46ce6837d50b2893568872378171f1 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 1 Jul 2020 14:54:41 -0500 Subject: [PATCH] Add solver for integer AND (#4681) This omits certain inference schemas (sum and bitwise lemmas) which depends on an option that will be added later. --- src/CMakeLists.txt | 2 + src/options/smt_options.toml | 19 ++ src/theory/arith/nl/iand_solver.cpp | 258 ++++++++++++++++++++ src/theory/arith/nl/iand_solver.h | 127 ++++++++++ src/theory/arith/nl/nonlinear_extension.cpp | 25 +- src/theory/arith/nl/nonlinear_extension.h | 7 + 6 files changed, 435 insertions(+), 3 deletions(-) create mode 100644 src/theory/arith/nl/iand_solver.cpp create mode 100644 src/theory/arith/nl/iand_solver.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 0774d60af..5cddccc58 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -300,6 +300,8 @@ libcvc4_add_sources( theory/arith/linear_equality.h theory/arith/matrix.cpp theory/arith/matrix.h + theory/arith/nl/iand_solver.cpp + theory/arith/nl/iand_solver.h theory/arith/nl/nl_constraint.cpp theory/arith/nl/nl_constraint.h theory/arith/nl/nl_lemma_utils.cpp diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index c104cb3e7..c09f8bbf3 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -650,6 +650,25 @@ header = "options/smt_options.h" read_only = true help = "attempt to solve BV formulas by translation to integer arithmetic (experimental)" +[[option]] + name = "iandMode" + category = "undocumented" + long = "iand-mode=mode" + type = "IandMode" + default = "VALUE" + read_only = true + help = "Set the refinement scheme for integer AND" + help_mode = "Refinement modes for integer AND" + [[option.mode.VALUE]] + name = "value" + help = "value-based refinement" + [[option.mode.SUM]] + name = "sum" + help = "use sum to represent integer AND in refinement" + [[option.mode.BITWISE]] + name = "bitwise" + help = "use bitwise comparisons on binary representation of integer for refinement (experimental)" + [[option]] name = "solveIntAsBV" category = "undocumented" diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp new file mode 100644 index 000000000..fd6eedc5a --- /dev/null +++ b/src/theory/arith/nl/iand_solver.cpp @@ -0,0 +1,258 @@ +/********************* */ +/*! \file iand_solver.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of integer and (IAND) solver + **/ + +#include "theory/arith/nl/iand_solver.h" + +#include "options/arith_options.h" +#include "options/smt_options.h" +#include "preprocessing/passes/bv_to_int.h" +#include "theory/arith/arith_msum.h" +#include "theory/arith/arith_utilities.h" +#include "util/iand.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { + +IAndSolver::IAndSolver(TheoryArith& containing, NlModel& model) + : d_containing(containing), + d_model(model), + d_initRefine(containing.getUserContext()) +{ + NodeManager* nm = NodeManager::currentNM(); + d_true = nm->mkConst(true); + d_false = nm->mkConst(false); + d_zero = nm->mkConst(Rational(0)); + d_one = nm->mkConst(Rational(1)); + d_two = nm->mkConst(Rational(2)); + d_neg_one = nm->mkConst(Rational(-1)); +} + +IAndSolver::~IAndSolver() {} + +void IAndSolver::initLastCall(const std::vector& assertions, + const std::vector& false_asserts, + const std::vector& xts) +{ + d_iands.clear(); + + Trace("iand-mv") << "IAND terms : " << std::endl; + for (const Node& a : xts) + { + Kind ak = a.getKind(); + if (ak != IAND) + { + // don't care about other terms + continue; + } + size_t bsize = a.getOperator().getConst().d_size; + d_iands[bsize].push_back(a); + } + + Trace("iand") << "We have " << d_iands.size() << " IAND terms." << std::endl; +} + +std::vector IAndSolver::checkInitialRefine() +{ + Trace("iand-check") << "IAndSolver::checkInitialRefine" << std::endl; + std::vector lems; + NodeManager* nm = NodeManager::currentNM(); + for (const std::pair >& is : d_iands) + { + // the reference bitwidth + unsigned k = is.first; + for (const Node& i : is.second) + { + if (d_initRefine.find(i) != d_initRefine.end()) + { + // already sent initial axioms for i in this user context + continue; + } + d_initRefine.insert(i); + Node op = i.getOperator(); + // initial refinement lemmas + std::vector conj; + // iand(x,y)=iand(y,x) is guaranteed by rewriting + Assert(i[0] <= i[1]); + // conj.push_back(i.eqNode(nm->mkNode(IAND, op, i[1], i[0]))); + // 0 <= iand(x,y) < 2^k + conj.push_back(nm->mkNode(LEQ, d_zero, i)); + conj.push_back(nm->mkNode(LT, i, twoToK(k))); + // iand(x,y)<=x + conj.push_back(nm->mkNode(LEQ, i, i[0])); + // iand(x,y)<=y + conj.push_back(nm->mkNode(LEQ, i, i[1])); + // x=y => iand(x,y)=x + conj.push_back(nm->mkNode(IMPLIES, i[0].eqNode(i[1]), i.eqNode(i[0]))); + Node lem = conj.size() == 1 ? conj[0] : nm->mkNode(AND, conj); + Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; INIT_REFINE" + << std::endl; + lems.push_back(lem); + } + } + return lems; +} + +std::vector IAndSolver::checkFullRefine() +{ + Trace("iand-check") << "IAndSolver::checkFullRefine"; + Trace("iand-check") << "IAND terms: " << std::endl; + std::vector lems; + for (const std::pair >& is : d_iands) + { + // the reference bitwidth + unsigned k = is.first; + for (const Node& i : is.second) + { + Node valAndXY = d_model.computeAbstractModelValue(i); + Node valAndXYC = d_model.computeConcreteModelValue(i); + if (Trace.isOn("iand-check")) + { + Node x = i[0]; + Node y = i[1]; + + Node valX = d_model.computeConcreteModelValue(x); + Node valY = d_model.computeConcreteModelValue(y); + + Trace("iand-check") + << "* " << i << ", value = " << valAndXY << std::endl; + Trace("iand-check") << " actual (" << valX << ", " << valY + << ") = " << valAndXYC << std::endl; + // print the bit-vector versions + Node bvalX = convertToBvK(k, valX); + Node bvalY = convertToBvK(k, valY); + Node bvalAndXY = convertToBvK(k, valAndXY); + Node bvalAndXYC = convertToBvK(k, valAndXYC); + + Trace("iand-check") << " bv-value = " << bvalAndXY << std::endl; + Trace("iand-check") << " bv-actual (" << bvalX << ", " << bvalY + << ") = " << bvalAndXYC << std::endl; + } + if (valAndXY == valAndXYC) + { + Trace("iand-check") << "...already correct" << std::endl; + continue; + } + + // ************* additional lemma schemas go here + if (options::iandMode() == options::IandMode::SUM) + { + // add lemmas based on sum mode + } + else if (options::iandMode() == options::IandMode::BITWISE) + { + // add lemmas based on sum mode + } + else + { + // this is the most naive model-based schema based on model values + Node lem = valueBasedLemma(i); + Trace("iand-lemma") + << "IAndSolver::Lemma: " << lem << " ; VALUE_REFINE" << std::endl; + lems.push_back(lem); + } + } + } + + return lems; +} + +Node IAndSolver::convertToBvK(unsigned k, Node n) const +{ + Assert(n.isConst() && n.getType().isInteger()); + NodeManager* nm = NodeManager::currentNM(); + Node iToBvOp = nm->mkConst(IntToBitVector(k)); + Node bn = nm->mkNode(kind::INT_TO_BITVECTOR, iToBvOp, n); + return Rewriter::rewrite(bn); +} + +Node IAndSolver::twoToK(unsigned k) const +{ + // could be faster + NodeManager* nm = NodeManager::currentNM(); + Node ret = nm->mkNode(POW, d_two, nm->mkConst(Rational(k))); + ret = Rewriter::rewrite(ret); + return ret; +} + +Node IAndSolver::twoToKMinusOne(unsigned k) const +{ + // could be faster + NodeManager* nm = NodeManager::currentNM(); + Node ret = nm->mkNode(MINUS, twoToK(k), d_one); + ret = Rewriter::rewrite(ret); + return ret; +} + +Node IAndSolver::mkIAnd(unsigned k, Node x, Node y) const +{ + NodeManager* nm = NodeManager::currentNM(); + Node iAndOp = nm->mkConst(IntAnd(k)); + Node ret = nm->mkNode(IAND, iAndOp, x, y); + ret = Rewriter::rewrite(ret); + return ret; +} + +Node IAndSolver::mkIOr(unsigned k, Node x, Node y) const +{ + Node ret = mkINot(k, mkIAnd(k, mkINot(k, x), mkINot(k, y))); + ret = Rewriter::rewrite(ret); + return ret; +} + +Node IAndSolver::mkINot(unsigned k, Node x) const +{ + NodeManager* nm = NodeManager::currentNM(); + Node ret = nm->mkNode(MINUS, twoToKMinusOne(k), x); + ret = Rewriter::rewrite(ret); + return ret; +} + +Node IAndSolver::iextract(unsigned i, unsigned j, Node n) const +{ + NodeManager* nm = NodeManager::currentNM(); + // ((_ extract i j) n) is n / 2^j mod 2^{i-j+1} + Node n2j = nm->mkNode(INTS_DIVISION_TOTAL, n, twoToK(j)); + Node ret = nm->mkNode(INTS_MODULUS_TOTAL, n2j, twoToK(i - j + 1)); + ret = Rewriter::rewrite(ret); + return ret; +} + +Node IAndSolver::valueBasedLemma(Node i) +{ + Assert(i.getKind() == IAND); + Node x = i[0]; + Node y = i[1]; + + Node valX = d_model.computeConcreteModelValue(x); + Node valY = d_model.computeConcreteModelValue(y); + + NodeManager* nm = NodeManager::currentNM(); + Node valC = nm->mkNode(IAND, i.getOperator(), valX, valY); + valC = Rewriter::rewrite(valC); + + Node lem = nm->mkNode( + IMPLIES, nm->mkNode(AND, x.eqNode(valX), y.eqNode(valY)), i.eqNode(valC)); + return lem; +} + +bool oneBitAnd(bool a, bool b) { return (a && b); } + +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h new file mode 100644 index 000000000..b526dac57 --- /dev/null +++ b/src/theory/arith/nl/iand_solver.h @@ -0,0 +1,127 @@ +/********************* */ +/*! \file iand_solver.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Solver for integer and (IAND) constraints + **/ + +#ifndef CVC4__THEORY__ARITH__NL__IAND_SOLVER_H +#define CVC4__THEORY__ARITH__NL__IAND_SOLVER_H + +#include +#include + +#include "context/cdhashset.h" +#include "expr/node.h" +#include "theory/arith/nl/nl_lemma_utils.h" +#include "theory/arith/nl/nl_model.h" +#include "theory/arith/theory_arith.h" + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { + +/** Integer and solver class + * + */ +class IAndSolver +{ + typedef context::CDHashSet NodeSet; + + public: + IAndSolver(TheoryArith& containing, NlModel& model); + ~IAndSolver(); + + /** init last call + * + * This is called at the beginning of last call effort check, where + * assertions are the set of assertions belonging to arithmetic, + * false_asserts is the subset of assertions that are false in the current + * model, and xts is the set of extended function terms that are active in + * the current context. + */ + void initLastCall(const std::vector& assertions, + const std::vector& false_asserts, + const std::vector& xts); + //-------------------------------------------- lemma schemas + /** check initial refine + * + * Returns a set of valid theory lemmas, based on simple facts about IAND. + * + * Examples where iand is shorthand for (_ iand k): + * + * 0 <= iand(x,y) < 2^k + * iand(x,y) <= x + * iand(x,y) <= y + * x=y => iand(x,y)=x + * + * This should be a heuristic incomplete check that only introduces a + * small number of new terms in the lemmas it returns. + */ + std::vector checkInitialRefine(); + /** check full refine + * + * This should be a complete check that returns at least one lemma to + * rule out the current model. + */ + std::vector checkFullRefine(); + + //-------------------------------------------- end lemma schemas + private: + // The theory of arithmetic containing this extension. + TheoryArith& d_containing; + /** Reference to the non-linear model object */ + NlModel& d_model; + /** commonly used terms */ + Node d_zero; + Node d_one; + Node d_neg_one; + Node d_two; + Node d_true; + Node d_false; + /** IAND terms that have been given initial refinement lemmas */ + NodeSet d_initRefine; + /** all IAND terms, for each bit-width */ + std::map > d_iands; + + /** + * convert integer value to bitvector value of bitwidth k, + * equivalent to Rewriter::rewrite( ((_ intToBv k) n) ). + */ + Node convertToBvK(unsigned k, Node n) const; + /** 2^k */ + Node twoToK(unsigned k) const; + /** 2^k-1 */ + Node twoToKMinusOne(unsigned k) const; + /** make iand */ + Node mkIAnd(unsigned k, Node x, Node y) const; + /** make ior */ + Node mkIOr(unsigned k, Node x, Node y) const; + /** make inot */ + Node mkINot(unsigned k, Node i) const; + /** extract from integer + * ((_ extract i j) n) is n / 2^j mod 2^{i-j+1} + */ + Node iextract(unsigned i, unsigned j, Node n) const; + /** + * Value-based refinement lemma for i of the form ((_ iand k) x y). Returns: + * x = M(x) ^ y = M(y) => + * ((_ iand k) x y) = Rewriter::rewrite(((_ iand k) M(x) M(y))) + */ + Node valueBasedLemma(Node i); +}; /* class IAndSolver */ + +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__ARITH__IAND_SOLVER_H */ diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 5ded7d3d0..bd48a726a 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -40,6 +40,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing, d_model(containing.getSatContext()), d_trSlv(d_model), d_nlSlv(containing, d_model), + d_iandSlv(containing, d_model), d_builtModel(containing.getSatContext(), false) { d_true = NodeManager::currentNM()->mkConst(true); @@ -96,8 +97,9 @@ std::pair NonlinearExtension::isExtfReduced( if (n != d_zero) { Kind k = n.getKind(); - return std::make_pair(k != NONLINEAR_MULT && !isTranscendentalKind(k), - Node::null()); + return std::make_pair( + k != NONLINEAR_MULT && !isTranscendentalKind(k) && k != IAND, + Node::null()); } Assert(n == d_zero); if (on.getKind() == NONLINEAR_MULT) @@ -402,6 +404,7 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, std::vector& wlems) { std::vector lemmas; + if (options::nlExt()) { // initialize the non-linear solver @@ -411,6 +414,10 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, // process lemmas that may have been generated by the transcendental solver filterLemmas(lemmas, lems); } + + // init last call with IAND + d_iandSlv.initLastCall(assertions, false_asserts, xts); + if (!lems.empty()) { Trace("nl-ext") << " ...finished with " << lems.size() @@ -445,7 +452,16 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, return lems.size(); } } - + //-----------------------------------initial lemmas for iand + lemmas = d_iandSlv.checkInitialRefine(); + filterLemmas(lemmas, lems); + if (!lems.empty()) + { + Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas." + << std::endl; + return lems.size(); + } + // main calls to nlExt if (options::nlExt()) { @@ -559,6 +575,9 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, filterLemmas(lemmas, wlems); } } + // run the full refinement in the IAND solver + lemmas = d_iandSlv.checkFullRefine(); + filterLemmas(lemmas, wlems); Trace("nl-ext") << " ...finished with " << wlems.size() << " waiting lemmas." << std::endl; diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index cb436bda7..ed1838b4b 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -25,6 +25,7 @@ #include "context/cdlist.h" #include "expr/kind.h" #include "expr/node.h" +#include "theory/arith/nl/iand_solver.h" #include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/nl_solver.h" @@ -303,6 +304,12 @@ class NonlinearExtension * constraints involving nonlinear mulitplication, Cimatti et al., TACAS 2017. */ NlSolver d_nlSlv; + /** The integer and solver + * + * This is the subsolver responsible for running the procedure for + * constraints involving integer and. + */ + IAndSolver d_iandSlv; /** * The lemmas we computed during collectModelInfo, to be sent out on the * output channel of TheoryArith. -- 2.30.2