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 |
4914 |
~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 */ |