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