src/theory/arith/nl/ext_theory_callback.h

   1 /*********************                                                        */
   2 /*! \file ext_theory_callback.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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.\endverbatim
  11  **
  12  ** \brief The extended theory callback for non-linear arithmetic
  13  **/
  14
  15 #ifndef CVC4__THEORY__ARITH__NL__EXT_THEORY_CALLBACK_H
  16 #define CVC4__THEORY__ARITH__NL__EXT_THEORY_CALLBACK_H
  17
  18 #include "expr/node.h"
  19 #include "theory/ext_theory.h"
  20
  21 namespace CVC4 {
  22 namespace theory {
  23 namespace arith {
  24 namespace nl {
  25
  26 class NlExtTheoryCallback : public ExtTheoryCallback
  27 {
  28  public:
  29   NlExtTheoryCallback(eq::EqualityEngine* ee);
  30   ~NlExtTheoryCallback() {}
  31   /** Get current substitution
  32    *
  33    * This function and the one below are
  34    * used for context-dependent
  35    * simplification, see Section 3.1 of
  36    * "Designing Theory Solvers with Extensions"
  37    * by Reynolds et al. FroCoS 2017.
  38    *
  39    * effort : an identifier indicating the stage where
  40    *          we are performing context-dependent simplification,
  41    * vars : a set of arithmetic variables.
  42    *
  43    * This function populates subs and exp, such that for 0 <= i < vars.size():
  44    *   ( exp[vars[i]] ) => vars[i] = subs[i]
  45    * where exp[vars[i]] is a set of assertions
  46    * that hold in the current context. We call { vars -> subs } a "derivable
  47    * substituion" (see Reynolds et al. FroCoS 2017).
  48    */
  49   bool getCurrentSubstitution(int effort,
  50                               const std::vector<Node>& vars,
  51                               std::vector<Node>& subs,
  52                               std::map<Node, std::vector<Node>>& exp) override;
  53   /** Is the term n in reduced form?
  54    *
  55    * Used for context-dependent simplification.
  56    *
  57    * effort : an identifier indicating the stage where
  58    *          we are performing context-dependent simplification,
  59    * on : the original term that we reduced to n,
  60    * exp : an explanation such that ( exp => on = n ).
  61    *
  62    * We return a pair ( b, exp' ) such that
  63    *   if b is true, then:
  64    *     n is in reduced form
  65    *     if exp' is non-null, then ( exp' => on = n )
  66    * The second part of the pair is used for constructing
  67    * minimal explanations for context-dependent simplifications.
  68    */
  69   bool isExtfReduced(int effort,
  70                      Node n,
  71                      Node on,
  72                      std::vector<Node>& exp) override;
  73
  74  private:
  75   /** The underlying equality engine. */
  76   eq::EqualityEngine* d_ee;
  77   /** Commonly used nodes */
  78   Node d_zero;
  79 };
  80
  81 }  // namespace nl
  82 }  // namespace arith
  83 }  // namespace theory
  84 }  // namespace CVC4
  85
  86 #endif /* CVC4__THEORY__ARITH__NL__EXT_THEORY_CALLBACK_H */