--- /dev/null
+/********************* */
+/*! \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<Node>& assertions,
+ const std::vector<Node>& false_asserts,
+ const std::vector<Node>& 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<IntAnd>().d_size;
+ d_iands[bsize].push_back(a);
+ }
+
+ Trace("iand") << "We have " << d_iands.size() << " IAND terms." << std::endl;
+}
+
+std::vector<NlLemma> IAndSolver::checkInitialRefine()
+{
+ Trace("iand-check") << "IAndSolver::checkInitialRefine" << std::endl;
+ std::vector<NlLemma> lems;
+ NodeManager* nm = NodeManager::currentNM();
+ for (const std::pair<const unsigned, std::vector<Node> >& 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<Node> 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<NlLemma> IAndSolver::checkFullRefine()
+{
+ Trace("iand-check") << "IAndSolver::checkFullRefine";
+ Trace("iand-check") << "IAND terms: " << std::endl;
+ std::vector<NlLemma> lems;
+ for (const std::pair<const unsigned, std::vector<Node> >& 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
--- /dev/null
+/********************* */
+/*! \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 <map>
+#include <vector>
+
+#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<Node, NodeHashFunction> 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<Node>& assertions,
+ const std::vector<Node>& false_asserts,
+ const std::vector<Node>& 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<NlLemma> checkInitialRefine();
+ /** check full refine
+ *
+ * This should be a complete check that returns at least one lemma to
+ * rule out the current model.
+ */
+ std::vector<NlLemma> 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<unsigned, std::vector<Node> > 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 */
projects / cvc5.git / commitdiff