Minor fixes and additions for transcendental functions (#1612)

Also adds parsing support for PI in smt2 with syntax "real.pi".

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 );