diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-01 14:54:41 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-01 14:54:41 -0500 |
commit | e968ea45fd46ce6837d50b2893568872378171f1 (patch) | |
tree | 1e9f4e720830562e4bbf77186ca90f85405aea9c /src/theory/arith/nl/iand_solver.h | |
parent | 9ce4c3153d42bc079470b7bd73bf131499b3fcbe (diff) |
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.
Diffstat (limited to 'src/theory/arith/nl/iand_solver.h')
-rw-r--r-- | src/theory/arith/nl/iand_solver.h | 127 |
1 files changed, 127 insertions, 0 deletions
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 <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 */ |