diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-20 12:53:12 -0600 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-20 10:53:12 -0800 |
commit | 05a2414a2742ee0c7e5af40ac9c725cb49d1f196 (patch) | |
tree | 8392f1b56aedc1a9ea107790cf7741af64b6607f /src/theory/arith/nonlinear_extension.h | |
parent | 4ef569cfd91bccabb6e704dcc4ecd55a9fa0a8ea (diff) |
Minor fixes and additions for transcendental functions (#1612)
Also adds parsing support for PI in smt2 with syntax "real.pi".
Diffstat (limited to 'src/theory/arith/nonlinear_extension.h')
-rw-r--r-- | src/theory/arith/nonlinear_extension.h | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h index 84acc0269..a37ef97f8 100644 --- a/src/theory/arith/nonlinear_extension.h +++ b/src/theory/arith/nonlinear_extension.h @@ -390,6 +390,10 @@ class NonlinearExtension { typedef std::map<Node, NodeMultiset> MonomialExponentMap; MonomialExponentMap d_m_exp; + /** + * Mapping from monomials to the list of variables that occur in it. For + * example, x*x*y*z -> { x, y, z }. + */ std::map<Node, std::vector<Node> > d_m_vlist; NodeMultiset d_m_degree; // monomial index, by sorted variables @@ -475,7 +479,8 @@ private: std::vector< Node > d_ms; std::vector< Node > d_ms_vars; std::map<Node, bool> d_ms_proc; - std::vector<Node> d_mterms; + std::vector<Node> d_mterms; + //list of monomials with factors whose model value is non-constant in model // e.g. y*cos( x ) std::map<Node, bool> d_m_nconst_factor; @@ -668,6 +673,12 @@ private: * * |x|>|y| => |x*z|>|y*z| * |x|>|y| ^ |z|>|w| ^ |x|>=1 => |x*x*z*u|>|y*w| + * + * Argument c indicates the class of inferences to perform for the (non-linear) + * monomials in the vector d_ms. + * 0 : compare non-linear monomials against 1, + * 1 : compare non-linear monomials against variables, + * 2 : compare non-linear monomials against other non-linear monomials. */ std::vector<Node> checkMonomialMagnitude( unsigned c ); |