Split the non-linear solver (#4219)

This splits the "non-linear solver" from "NonlinearExtension". The non-linear solver is the module that implements the inference schemas whereas NonlinearExtension is the glue code that manages the solver(s) for non-linear.

This also involves moving utilities from the non-linear solver to their own file.

1 files changed, 9 insertions, 354 deletions

diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h
index bfc713b12..5aa2070a6 100644
--- a/src/theory/arith/nonlinear_extension.h
+++ b/src/theory/arith/nonlinear_extension.h
@@ -19,23 +19,15 @@
 #define CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H
 
 #include <stdint.h>
-
 #include <map>
-#include <queue>
-#include <set>
-#include <unordered_map>
-#include <utility>
 #include <vector>
 
-#include "context/cdhashset.h"
-#include "context/cdinsert_hashmap.h"
 #include "context/cdlist.h"
-#include "context/cdqueue.h"
-#include "context/context.h"
 #include "expr/kind.h"
 #include "expr/node.h"
 #include "theory/arith/nl_lemma_utils.h"
 #include "theory/arith/nl_model.h"
+#include "theory/arith/nl_solver.h"
 #include "theory/arith/theory_arith.h"
 #include "theory/arith/transcendental_solver.h"
 #include "theory/uf/equality_engine.h"
@@ -44,9 +36,6 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-typedef std::map<Node, unsigned> NodeMultiset;
-
-// TODO : refactor/document this class (#1287)
 /** Non-linear extension class
  *
  * This class implements model-based refinement schemes
@@ -72,6 +61,8 @@ typedef std::map<Node, unsigned> NodeMultiset;
  * where d_out is the output channel of TheoryArith.
  */
 class NonlinearExtension {
+  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+
  public:
   NonlinearExtension(TheoryArith& containing, eq::EqualityEngine* ee);
   ~NonlinearExtension();
@@ -187,34 +178,7 @@ class NonlinearExtension {
   bool modelBasedRefinement(std::vector<Node>& mlems,
                             std::vector<Node>& mlemsPp,
                             std::map<Node, NlLemmaSideEffect>& lemSE);
-  /** returns true if the multiset containing the
-   * factors of monomial a is a subset of the multiset
-   * containing the factors of monomial b.
-   */
-  bool isMonomialSubset(Node a, Node b) const;
-  void registerMonomialSubset(Node a, Node b);
-
-  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
-
-  // monomial information (context-independent)
-  class MonomialIndex {
-   public:
-    // status 0 : n equal, -1 : n superset, 1 : n subset
-    void addTerm(Node n, const std::vector<Node>& reps, NonlinearExtension* nla,
-                 int status = 0, unsigned argIndex = 0);
-
-   private:
-    std::map<Node, MonomialIndex> d_data;
-    std::vector<Node> d_monos;
-  }; /* class MonomialIndex */
 
-  // constraint information (context-independent)
-  struct ConstraintInfo {
-   public:
-    Node d_rhs;
-    Node d_coeff;
-    Kind d_type;
-  }; /* struct ConstraintInfo */
 
   /** check last call
    *
@@ -249,24 +213,6 @@ class NonlinearExtension {
                     std::vector<Node>& lemsPp,
                     std::vector<Node>& wlems,
                     std::map<Node, NlLemmaSideEffect>& lemSE);
-  //---------------------------------------term utilities
-  static bool isArithKind(Kind k);
-  static Node mkLit(Node a, Node b, int status, bool isAbsolute = false);
-  static Node mkAbs(Node a);
-  static Node mkValidPhase(Node a, Node pi);
-  Node mkMonomialRemFactor(Node n, const NodeMultiset& n_exp_rem) const;
-  //---------------------------------------end term utilities
-
-  /** register monomial */
-  void registerMonomial(Node n);
-  void setMonomialFactor(Node a, Node b, const NodeMultiset& common);
-
-  void registerConstraint(Node atom);
-  /** assign order ids */
-  void assignOrderIds(std::vector<Node>& vars,
-                      NodeMultiset& d_order,
-                      bool isConcrete,
-                      bool isAbsolute);
 
   /** get assertions
    *
@@ -312,85 +258,6 @@ class NonlinearExtension {
                   std::vector<Node>& gs);
   //---------------------------end check model
 
-  /** In the following functions, status states a relationship
-  * between two arithmetic terms, where:
-  * 0 : equal
-  * 1 : greater than or equal
-  * 2 : greater than
-  * -X : (greater -> less)
-  * TODO (#1287) make this an enum?
-  */
-  /** compute the sign of a.
-  *
-  * Calls to this function are such that :
-  *    exp => ( oa = a ^ a <status> 0 )
-  *
-  * This function iterates over the factors of a,
-  * where a_index is the index of the factor in a
-  * we are currently looking at.
-  *
-  * This function returns a status, which indicates
-  * a's relationship to 0.
-  * We add lemmas to lem of the form given by the
-  * lemma schema checkSign(...).
-  */
-  int compareSign(Node oa, Node a, unsigned a_index, int status,
-                  std::vector<Node>& exp, std::vector<Node>& lem);
-  /** compare monomials a and b
-  *
-  * Initially, a call to this function is such that :
-  *    exp => ( oa = a ^ ob = b )
-  *
-  * This function returns true if we can infer a valid
-  * arithmetic lemma of the form :
-  *    P => abs( a ) >= abs( b )
-  * where P is true and abs( a ) >= abs( b ) is false in the
-  * current model.
-  *
-  * This function is implemented by "processing" factors
-  * of monomials a and b until an inference of the above
-  * form can be made. For example, if :
-  *   a = x*x*y and b = z*w
-  * Assuming we are trying to show abs( a ) >= abs( c ),
-  * then if abs( M( x ) ) >= abs( M( z ) ) where M is the current model,
-  * then we can add abs( x ) >= abs( z ) to our explanation, and
-  * mark one factor of x as processed in a, and
-  * one factor of z as processed in b. The number of processed factors of a
-  * and b are stored in a_exp_proc and b_exp_proc respectively.
-  *
-  * cmp_infers stores information that is helpful
-  * in discarding redundant inferences.  For example,
-  * we do not want to infer abs( x ) >= abs( z ) if
-  * we have already inferred abs( x ) >= abs( y ) and
-  * abs( y ) >= abs( z ).
-  * It stores entries of the form (status,t1,t2)->F,
-  * which indicates that we constructed a lemma F that
-  * showed t1 <status> t2.
-  *
-  * We add lemmas to lem of the form given by the
-  * lemma schema checkMagnitude(...).
-  */
-  bool compareMonomial(
-      Node oa, Node a, NodeMultiset& a_exp_proc, Node ob, Node b,
-      NodeMultiset& b_exp_proc, std::vector<Node>& exp, std::vector<Node>& lem,
-      std::map<int, std::map<Node, std::map<Node, Node> > >& cmp_infers);
-  /** helper function for above
-   *
-   * The difference is the inputs a_index and b_index, which are the indices of
-   * children (factors) in monomials a and b which we are currently looking at.
-   */
-  bool compareMonomial(
-      Node oa, Node a, unsigned a_index, NodeMultiset& a_exp_proc, Node ob,
-      Node b, unsigned b_index, NodeMultiset& b_exp_proc, int status,
-      std::vector<Node>& exp, std::vector<Node>& lem,
-      std::map<int, std::map<Node, std::map<Node, Node> > >& cmp_infers);
-  /** Check whether we have already inferred a relationship between monomials
-   * x and y based on the information in cmp_infers. This computes the
-   * transitive closure of the relation stored in cmp_infers.
-   */
-  bool cmp_holds(Node x, Node y,
-                 std::map<Node, std::map<Node, Node> >& cmp_infers,
-                 std::vector<Node>& exp, std::map<Node, bool>& visited);
   /** Is n entailed with polarity pol in the current context? */
   bool isEntailed(Node n, bool pol);
 
@@ -412,61 +279,19 @@ class NonlinearExtension {
   /** Process side effect se */
   void processSideEffect(const NlLemmaSideEffect& se);
 
-  // Returns the NodeMultiset for an existing monomial.
-  const NodeMultiset& getMonomialExponentMap(Node monomial) const;
-
-  // Map from monomials to var^index.
-  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
-  MonomialIndex d_m_index;
-  // list of all monomials
-  std::vector<Node> d_monomials;
-  // containment ordering
-  std::map<Node, std::vector<Node> > d_m_contain_children;
-  std::map<Node, std::vector<Node> > d_m_contain_parent;
-  std::map<Node, std::map<Node, Node> > d_m_contain_mult;
-  std::map<Node, std::map<Node, Node> > d_m_contain_umult;
-  // ( 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 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;
-
   /** commonly used terms */
   Node d_zero;
   Node d_one;
   Node d_neg_one;
-  Node d_two;
   Node d_true;
-  Node d_false;
-
   // The theory of arithmetic containing this extension.
   TheoryArith& d_containing;
-
   // pointer to used equality engine
   eq::EqualityEngine* d_ee;
   // needs last call effort
   bool d_needsLastCall;
-
-  // if d_c_info[lit][x] = ( r, coeff, k ), then ( lit <=>  (coeff * x) <k> r )
-  std::map<Node, std::map<Node, ConstraintInfo> > d_c_info;
-  std::map<Node, std::map<Node, bool> > d_c_info_maxm;
-  std::vector<Node> d_constraints;
-
-  // per last-call effort
-
-  // model values/orderings
-
   /** The non-linear model object
    *
    * This class is responsible for computing model values for arithmetic terms
@@ -479,6 +304,12 @@ class NonlinearExtension {
    * transcendental functions.
    */
   TranscendentalSolver d_trSlv;
+  /** The nonlinear extension object
+   *
+   * This is the subsolver responsible for running the procedure for
+   * constraints involving nonlinear mulitplication.
+   */
+  NlSolver d_nlSlv;
   /**
    * The lemmas we computed during collectModelInfo. We store two vectors of
    * lemmas to be sent out on the output channel of TheoryArith. The first
@@ -495,182 +326,6 @@ class NonlinearExtension {
   std::map<Node, std::pair<Node, Node>> d_approximations;
   /** have we successfully built the model in this SAT context? */
   context::CDO<bool> d_builtModel;
-
-  // ordering, stores variables and 0,1,-1
-  std::map<Node, unsigned> d_order_vars;
-  std::vector<Node> d_order_points;
-  
-
- private:
-  //per last-call effort check
-  
-  //information about monomials
-  std::vector< Node > d_ms;
-  std::vector< Node > d_ms_vars;
-  std::map<Node, bool> d_ms_proc;
-  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;
-  /** the set of monomials we should apply tangent planes to */
-  std::unordered_set<Node, NodeHashFunction> d_tplane_refine;
-  // term -> coeff -> rhs -> ( status, exp, b ),
-  //   where we have that : exp =>  ( coeff * term <status> rhs )
-  //   b is true if degree( term ) >= degree( rhs )
-  std::map<Node, std::map<Node, std::map<Node, Kind> > > d_ci;
-  std::map<Node, std::map<Node, std::map<Node, Node> > > d_ci_exp;
-  std::map<Node, std::map<Node, std::map<Node, bool> > > d_ci_max;
-
-  // factor skolems
-  std::map< Node, Node > d_factor_skolem;
-  Node getFactorSkolem( Node n, std::vector< Node >& lemmas );
-
-  // tangent plane bounds
-  std::map< Node, std::map< Node, Node > > d_tangent_val_bound[4];
-
-  /** get approximate sqrt
-   *
-   * This approximates the square root of positive constant c. If this method
-   * returns true, then l and u are updated to constants such that
-   *   l <= sqrt( c ) <= u
-   * The argument iter is the number of iterations in the binary search to
-   * perform. By default, this is set to 15, which is usually enough to be
-   * precise in the majority of simple cases, whereas not prohibitively
-   * expensive to compute.
-   */
-  bool getApproximateSqrt(Node c, Node& l, Node& u, unsigned iter = 15) const;
-
- private:
-  //-------------------------------------------- lemma schemas
-  /** check split zero
-  *
-  * Returns a set of theory lemmas of the form
-  *   t = 0 V t != 0
-  * where t is a term that exists in the current context.
-  */
-  std::vector<Node> checkSplitZero();
-
-  /** check monomial sign
-  *
-  * Returns a set of valid theory lemmas, based on a
-  * lemma schema which ensures that non-linear monomials
-  * respect sign information based on their facts.
-  * For more details, see Section 5 of "Design Theory
-  * Solvers with Extensions" by Reynolds et al., FroCoS 2017,
-  * Figure 5, this is the schema "Sign".
-  *
-  * Examples:
-  *
-  * x > 0 ^ y > 0 => x*y > 0
-  * x < 0 => x*y*y < 0
-  * x = 0 => x*y*z = 0
-  */
-  std::vector<Node> checkMonomialSign();
-
-  /** check monomial magnitude
-  *
-  * Returns a set of valid theory lemmas, based on a
-  * lemma schema which ensures that comparisons between
-  * non-linear monomials respect the magnitude of their
-  * factors.
-  * For more details, see Section 5 of "Design Theory
-  * Solvers with Extensions" by Reynolds et al., FroCoS 2017,
-  * Figure 5, this is the schema "Magnitude".
-  *
-  * Examples:
-  *
-  * |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 );
-
-  /** check monomial inferred bounds
-  *
-  * Returns a set of valid theory lemmas, based on a
-  * lemma schema that infers new constraints about existing
-  * terms based on mulitplying both sides of an existing
-  * constraint by a term.
-  * For more details, see Section 5 of "Design Theory
-  * Solvers with Extensions" by Reynolds et al., FroCoS 2017,
-  * Figure 5, this is the schema "Multiply".
-  *
-  * Examples:
-  *
-  * x > 0 ^ (y > z + w) => x*y > x*(z+w)
-  * x < 0 ^ (y > z + w) => x*y < x*(z+w)
-  *   ...where (y > z + w) and x*y are a constraint and term
-  *      that occur in the current context.
-  */
-  std::vector<Node> checkMonomialInferBounds(
-      std::vector<Node>& nt_lemmas,
-      const std::vector<Node>& asserts,
-      const std::vector<Node>& false_asserts);
-
-  /** check factoring
-  *
-  * Returns a set of valid theory lemmas, based on a
-  * lemma schema that states a relationship betwen monomials
-  * with common factors that occur in the same constraint.
-  *
-  * Examples:
-  *
-  * x*z+y*z > t => ( k = x + y ^ k*z > t )
-  *   ...where k is fresh and x*z + y*z > t is a
-  *      constraint that occurs in the current context.
-  */
-  std::vector<Node> checkFactoring(const std::vector<Node>& asserts,
-                                   const std::vector<Node>& false_asserts);
-
-  /** check monomial infer resolution bounds
-  *
-  * Returns a set of valid theory lemmas, based on a
-  * lemma schema which "resolves" upper bounds
-  * of one inequality with lower bounds for another.
-  * This schema is not enabled by default, and can
-  * be enabled by --nl-ext-rbound.
-  *
-  * Examples:
-  *
-  *  ( y>=0 ^ s <= x*z ^ x*y <= t ) => y*s <= z*t
-  *  ...where s <= x*z and x*y <= t are constraints
-  *     that occur in the current context.
-  */
-  std::vector<Node> checkMonomialInferResBounds();
-
-  /** check tangent planes
-  *
-  * Returns a set of valid theory lemmas, based on an
-  * "incremental linearization" of non-linear monomials.
-  * This linearization is accomplished by adding constraints
-  * corresponding to "tangent planes" at the current
-  * model value of each non-linear monomial. In particular
-  * consider the definition for constants a,b :
-  *   T_{a,b}( x*y ) = b*x + a*y - a*b.
-  * The lemmas added by this function are of the form :
-  *  ( ( x>a ^ y<b) ^ (x<a ^ y>b) ) => x*y < T_{a,b}( x*y )
-  *  ( ( x>a ^ y>b) ^ (x<a ^ y<b) ) => x*y > T_{a,b}( x*y )
-  * It is inspired by "Invariant Checking of NRA Transition
-  * Systems via Incremental Reduction to LRA with EUF" by
-  * Cimatti et al., TACAS 2017.
-  * This schema is not terminating in general.
-  * It is not enabled by default, and can
-  * be enabled by --nl-ext-tplanes.
-  *
-  * Examples:
-  *
-  * ( ( x>2 ^ y>5) ^ (x<2 ^ y<5) ) => x*y > 5*x + 2*y - 10
-  * ( ( x>2 ^ y<5) ^ (x<2 ^ y>5) ) => x*y < 5*x + 2*y - 10
-  */
-  std::vector<Node> checkTangentPlanes();
-
-  //-------------------------------------------- end lemma schemas
 }; /* class NonlinearExtension */
 
 }  // namespace arith