src/theory/arith/nl/iand_solver.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, Makai Mann, Gereon Kremer
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  * in the top-level source directory and their institutional affiliations.
   9  * All rights reserved.  See the file COPYING in the top-level source
  10  * directory for licensing information.
  11  * ****************************************************************************
  12  *
  13  * Solver for integer and (IAND) constraints.
  14  */
  15
  16 #ifndef CVC5__THEORY__ARITH__NL__IAND_SOLVER_H
  17 #define CVC5__THEORY__ARITH__NL__IAND_SOLVER_H
  18
  19 #include <map>
  20 #include <vector>
  21
  22 #include "context/cdhashset.h"
  23 #include "expr/node.h"
  24 #include "smt/env_obj.h"
  25 #include "theory/arith/nl/iand_utils.h"
  26
  27 namespace cvc5 {
  28 namespace theory {
  29 namespace arith {
  30
  31 class ArithState;
  32 class InferenceManager;
  33
  34 namespace nl {
  35
  36 class NlModel;
  37
  38 /** Integer and solver class
  39  *
  40  */
  41 class IAndSolver : protected EnvObj
  42 {
  43   typedef context::CDHashSet<Node> NodeSet;
  44
  45  public:
  46   IAndSolver(Env& env, InferenceManager& im, ArithState& state, NlModel& model);
  47   ~IAndSolver();
  48
  49   /** init last call
  50    *
  51    * This is called at the beginning of last call effort check, where
  52    * assertions are the set of assertions belonging to arithmetic,
  53    * false_asserts is the subset of assertions that are false in the current
  54    * model, and xts is the set of extended function terms that are active in
  55    * the current context.
  56    */
  57   void initLastCall(const std::vector<Node>& assertions,
  58                     const std::vector<Node>& false_asserts,
  59                     const std::vector<Node>& xts);
  60   //-------------------------------------------- lemma schemas
  61   /** check initial refine
  62    *
  63    * Returns a set of valid theory lemmas, based on simple facts about IAND.
  64    *
  65    * Examples where iand is shorthand for (_ iand k):
  66    *
  67    * 0 <= iand(x,y) < 2^k
  68    * iand(x,y) <= x
  69    * iand(x,y) <= y
  70    * x=y => iand(x,y)=x
  71    *
  72    * This should be a heuristic incomplete check that only introduces a
  73    * small number of new terms in the lemmas it returns.
  74    */
  75   void checkInitialRefine();
  76   /** check full refine
  77    *
  78    * This should be a complete check that returns at least one lemma to
  79    * rule out the current model.
  80    */
  81   void checkFullRefine();
  82
  83   //-------------------------------------------- end lemma schemas
  84  private:
  85   // The inference manager that we push conflicts and lemmas to.
  86   InferenceManager& d_im;
  87   /** Reference to the non-linear model object */
  88   NlModel& d_model;
  89   /** Reference to the arithmetic state */
  90   ArithState& d_astate;
  91   /** commonly used terms */
  92   Node d_false;
  93   Node d_true;
  94   Node d_zero;
  95   Node d_one;
  96   Node d_two;
  97
  98   IAndUtils d_iandUtils;
  99   /** IAND terms that have been given initial refinement lemmas */
 100   NodeSet d_initRefine;
 101   /** all IAND terms, for each bit-width */
 102   std::map<unsigned, std::vector<Node> > d_iands;
 103
 104   /**
 105    * convert integer value to bitvector value of bitwidth k,
 106    * equivalent to rewrite( ((_ intToBv k) n) ).
 107    */
 108   Node convertToBvK(unsigned k, Node n) const;
 109   /** make iand */
 110   Node mkIAnd(unsigned k, Node x, Node y) const;
 111   /** make ior */
 112   Node mkIOr(unsigned k, Node x, Node y) const;
 113   /** make inot */
 114   Node mkINot(unsigned k, Node i) const;
 115   /**
 116    * Value-based refinement lemma for i of the form ((_ iand k) x y). Returns:
 117    *   x = M(x) ^ y = M(y) =>
 118    *     ((_ iand k) x y) = rewrite(((_ iand k) M(x) M(y)))
 119    */
 120   Node valueBasedLemma(Node i);
 121   /**
 122    * Sum-based refinement lemma for i of the form ((_ iand k) x y). Returns:
 123    * i = 2^0*min(x[0],y[0])+...2^{k-1}*min(x[k-1],y[k-1])
 124    * where x[i] is x div i mod 2
 125    * and min is defined with an ite.
 126    */
 127   Node sumBasedLemma(Node i);
 128   /** Bitwise refinement lemma for i of the form ((_ iand k) x y). Returns:
 129    *   x[j] & y[j] == ite(x[j] == 1 /\ y[j] == 1, 1, 0)
 130    *   for all j where M(x)[j] ^ M(y)[j]
 131    *   does not match M(((_ iand k) x y))
 132    */
 133   Node bitwiseLemma(Node i);
 134 }; /* class IAndSolver */
 135
 136 }  // namespace nl
 137 }  // namespace arith
 138 }  // namespace theory
 139 }  // namespace cvc5
 140
 141 #endif /* CVC5__THEORY__ARITH__IAND_SOLVER_H */