diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-07 09:12:59 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-02-07 09:12:59 -0600 |
commit | 0533b9009d23a39bcc78ef85d6e98b62ef304351 (patch) | |
tree | e32b823d509e1c9b54dfe4230d075b8396f48b9c /src/theory/arith/nonlinear_extension.h | |
parent | 82066be04ce068b59b24526fbc8c9b4188503cae (diff) |
Add remaining transcendental functions (#1551)
Diffstat (limited to 'src/theory/arith/nonlinear_extension.h')
-rw-r--r-- | src/theory/arith/nonlinear_extension.h | 22 |
1 files changed, 21 insertions, 1 deletions
diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h index 34da28f6c..84acc0269 100644 --- a/src/theory/arith/nonlinear_extension.h +++ b/src/theory/arith/nonlinear_extension.h @@ -121,6 +121,23 @@ class NonlinearExtension { void check(Theory::Effort e); /** Does this class need a call to check(...) at last call effort? */ bool needsCheckLastEffort() const { return d_needsLastCall; } + /** add definition + * + * This function notifies this class that lem is a formula that defines or + * constrains an auxiliary variable. For example, during + * TheoryArith::expandDefinitions, we replace a term like arcsin( x ) with an + * auxiliary variable k. The lemmas 0 <= k < pi and sin( x ) = k are added as + * definitions to this class. + */ + void addDefinition(Node lem); + /** presolve + * + * This function is called during TheoryArith's presolve command. + * In this function, we send lemmas we accumulated during preprocessing, + * for instance, definitional lemmas from expandDefinitions are sent out + * on the output channel of TheoryArith in this function. + */ + void presolve(); /** Compare arithmetic terms i and j based an ordering. * * orderType = 0 : compare concrete model values @@ -387,8 +404,11 @@ class NonlinearExtension { // ( x*y, x*z, y ) for each pair of monomials ( x*y, x*z ) with common factors std::map<Node, std::map<Node, Node> > d_mono_diff; - // cache of all lemmas sent + /** cache of definition lemmas (user-context-dependent) */ + NodeSet d_def_lemmas; + /** cache of all lemmas sent on the output channel (user-context-dependent) */ NodeSet d_lemmas; + /** cache of terms t for which we have added the lemma ( t = 0 V t != 0 ). */ NodeSet d_zero_split; // literals with Skolems (need not be satisfied by model) |