Fix getModelValue for arithmetic (#8316)

[cvc5.git] / src / theory / arith / nl / iand_solver.h

diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h
index e00cb92a9b483a81789c302d874019a4cc9d1088..997112fee2c50bb787f0683440552e2e390ae5cb 100644 (file)
--- a/src/theory/arith/nl/iand_solver.h
+++ b/src/theory/arith/nl/iand_solver.h
@@ -1,45 +1,49 @@
-/*********************                                                        */
-/*! \file iand_solver.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King, Tianyi Liang
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Makai Mann, Gereon Kremer
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Solver for integer and (IAND) constraints.
+ */
 
-#ifndef CVC4__THEORY__ARITH__NL__IAND_SOLVER_H
-#define CVC4__THEORY__ARITH__NL__IAND_SOLVER_H
+#ifndef CVC5__THEORY__ARITH__NL__IAND_SOLVER_H
+#define CVC5__THEORY__ARITH__NL__IAND_SOLVER_H
 
 #include <map>
 #include <vector>
 
 #include "context/cdhashset.h"
 #include "expr/node.h"
-#include "theory/arith/arith_state.h"
-#include "theory/arith/inference_manager.h"
-#include "theory/arith/nl/iand_table.h"
-#include "theory/arith/nl/nl_lemma_utils.h"
-#include "theory/arith/nl/nl_model.h"
+#include "smt/env_obj.h"
+#include "theory/arith/nl/iand_utils.h"
 
-namespace CVC4 {
+namespace cvc5 {
 namespace theory {
 namespace arith {
+
+class ArithState;
+class InferenceManager;
+
 namespace nl {
 
+class NlModel;
+
 /** Integer and solver class
  *
  */
-class IAndSolver
+class IAndSolver : protected EnvObj
 {
-  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+  typedef context::CDHashSet<Node> NodeSet;
 
  public:
-  IAndSolver(InferenceManager& im, ArithState& state, NlModel& model);
+  IAndSolver(Env& env, InferenceManager& im, ArithState& state, NlModel& model);
   ~IAndSolver();
 
   /** init last call
@@ -82,14 +86,16 @@ class IAndSolver
   InferenceManager& d_im;
   /** Reference to the non-linear model object */
   NlModel& d_model;
+  /** Reference to the arithmetic state */
+  ArithState& d_astate;
   /** commonly used terms */
+  Node d_false;
+  Node d_true;
   Node d_zero;
   Node d_one;
-  Node d_neg_one;
   Node d_two;
-  Node d_true;
-  Node d_false;
-  IAndTable d_iandTable;
+
+  IAndUtils d_iandUtils;
   /** IAND terms that have been given initial refinement lemmas */
   NodeSet d_initRefine;
   /** all IAND terms, for each bit-width */
@@ -97,27 +103,19 @@ class IAndSolver
 
   /**
    * convert integer value to bitvector value of bitwidth k,
-   * equivalent to Rewriter::rewrite( ((_ intToBv k) n) ).
+   * equivalent to 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)))
+   *     ((_ iand k) x y) = rewrite(((_ iand k) M(x) M(y)))
    */
   Node valueBasedLemma(Node i);
   /**
@@ -127,11 +125,17 @@ class IAndSolver
    * and min is defined with an ite.
    */
   Node sumBasedLemma(Node i);
+  /** Bitwise refinement lemma for i of the form ((_ iand k) x y). Returns:
+   *   x[j] & y[j] == ite(x[j] == 1 /\ y[j] == 1, 1, 0)
+   *   for all j where M(x)[j] ^ M(y)[j]
+   *   does not match M(((_ iand k) x y))
+   */
+  Node bitwiseLemma(Node i);
 }; /* class IAndSolver */
 
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__IAND_SOLVER_H */
+#endif /* CVC5__THEORY__ARITH__IAND_SOLVER_H */