GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/ext_theory_callback.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
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 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 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
4388
  ~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) override;
76
77
 private:
78
  /** The underlying equality engine. */
79
  eq::EqualityEngine* d_ee;
80
  /** Commonly used nodes */
81
  Node d_zero;
82
};
83
84
}  // namespace nl
85
}  // namespace arith
86
}  // namespace theory
87
}  // namespace CVC4
88
89
#endif /* CVC4__THEORY__ARITH__NL__EXT_THEORY_CALLBACK_H */