src/theory/arith/nl/ext_theory_callback.h

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