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