Use side effect utility for non-linear lemmas (#3780)

Fixes #3647.

Previously, when doing incremental linearization for transcedental functions, we would add points to the list of secant points at the time when linearization lemmas were generated. However, our strategy has been updated such that lemmas may be abandoned (say in the case that a higher priority lemma is found). Thus, our list of secant points had spurious points corresponding to lemmas that weren't sent. This led to assertion failures, and likely led to gaps in our linearization, hindering our ability to say sat/unsat.

This PR introduces a "lemma side effect" class to ensure that modifications to the state of the nonlinear solver are in sync with the lemmas we send out.

1 files changed, 88 insertions, 63 deletions

diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h
index 338ae6611..64a601cc5 100644
--- a/src/theory/arith/nonlinear_extension.h
+++ b/src/theory/arith/nonlinear_extension.h
@@ -34,6 +34,7 @@
 #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/theory_arith.h"
 #include "theory/uf/equality_engine.h"
@@ -178,9 +179,13 @@ class NonlinearExtension {
    * Otherwise, it returns false. In the latter case, the model object d_model
    * may have information regarding how to construct a model, in the case that
    * we determined the problem is satisfiable.
+   *
+   * The argument lemSE is the "side effect" of the lemmas in mlems and mlemsPp
+   * (for details, see checkLastCall).
    */
   bool modelBasedRefinement(std::vector<Node>& mlems,
-                            std::vector<Node>& mlemsPp);
+                            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.
@@ -230,13 +235,19 @@ class NonlinearExtension {
    * output channel as a last resort. In other words, only if we are not
    * able to establish SAT via a call to checkModel(...) should wlems be
    * considered. This set typically contains tangent plane lemmas.
+   *
+   * The argument lemSE is the "side effect" of the lemmas from the previous
+   * three calls. If a lemma is mapping to a side effect, it should be
+   * processed via a call to processSideEffect(...) immediately after the
+   * lemma is sent (if it is indeed sent on this call to check).
    */
   int checkLastCall(const std::vector<Node>& assertions,
                     const std::vector<Node>& false_asserts,
                     const std::vector<Node>& xts,
                     std::vector<Node>& lems,
                     std::vector<Node>& lemsPp,
-                    std::vector<Node>& wlems);
+                    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);
@@ -395,7 +406,11 @@ class NonlinearExtension {
   /**
    * Send lemmas in out on the output channel of theory of arithmetic.
    */
-  void sendLemmas(const std::vector<Node>& out, bool preprocess = false);
+  void sendLemmas(const std::vector<Node>& out,
+                  bool preprocess,
+                  std::map<Node, NlLemmaSideEffect>& lemSE);
+  /** Process side effect se */
+  void processSideEffect(const NlLemmaSideEffect& se);
 
   // Returns the NodeMultiset for an existing monomial.
   const NodeMultiset& getMonomialExponentMap(Node monomial) const;
@@ -480,6 +495,8 @@ class NonlinearExtension {
    */
   std::vector<Node> d_cmiLemmas;
   std::vector<Node> d_cmiLemmasPp;
+  /** the side effects of the above lemmas */
+  std::map<Node, NlLemmaSideEffect> d_cmiLemmasSE;
   /**
    * The approximations computed during collectModelInfo. For details, see
    * NlModel::getModelValueRepair.
@@ -872,64 +889,68 @@ class NonlinearExtension {
   std::vector<Node> checkTranscendentalMonotonic();
 
   /** check transcendental tangent planes
-  *
-  * Returns a set of valid theory lemmas, based on
-  * computing an "incremental linearization" of
-  * transcendental functions based on the model values
-  * of transcendental functions and their arguments.
-  * It is based on Figure 3 of "Satisfiability
-  * Modulo Transcendental Functions via Incremental
-  * Linearization" by Cimatti et al., CADE 2017.
-  * This schema is not terminating in general.
-  * It is not enabled by default, and can
-  * be enabled by --nl-ext-tf-tplanes.
-  *
-  * Example:
-  *
-  * Assume we have a term sin(y) where M( y ) = 1 where M is the current model.
-  * Note that:
-  *   sin(1) ~= .841471
-  *
-  * The Taylor series and remainder of sin(y) of degree 7 is
-  *   P_{7,sin(0)}( x ) = x + (-1/6)*x^3 + (1/20)*x^5
-  *   R_{7,sin(0),b}( x ) = (-1/5040)*x^7
-  *
-  * This gives us lower and upper bounds :
-  *   P_u( x ) = P_{7,sin(0)}( x ) + R_{7,sin(0),b}( x )
-  *     ...where note P_u( 1 ) = 4243/5040 ~= .841865
-  *   P_l( x ) = P_{7,sin(0)}( x ) - R_{7,sin(0),b}( x )
-  *     ...where note P_l( 1 ) = 4241/5040 ~= .841468
-  *
-  * Assume that M( sin(y) ) > P_u( 1 ).
-  * Since the concavity of sine in the region 0 < x < PI/2 is -1,
-  * we add a tangent plane refinement.
-  * The tangent plane at the point 1 in P_u is
-  * given by the formula:
-  *   T( x ) = P_u( 1 ) + ((d/dx)(P_u(x)))( 1 )*( x - 1 )
-  * We add the lemma:
-  *   ( 0 < y < PI/2 ) => sin( y ) <= T( y )
-  * which is:
-  *   ( 0 < y < PI/2 ) => sin( y ) <= (391/720)*(y - 2737/1506)
-  *
-  * Assume that M( sin(y) ) < P_u( 1 ).
-  * Since the concavity of sine in the region 0 < x < PI/2 is -1,
-  * we add a secant plane refinement for some constants ( l, u )
-  * such that 0 <= l < M( y ) < u <= PI/2. Assume we choose
-  * l = 0 and u = M( PI/2 ) = 150517/47912.
-  * The secant planes at point 1 for P_l
-  * are given by the formulas:
-  *   S_l( x ) = (x-l)*(P_l( l )-P_l(c))/(l-1) + P_l( l )
-  *   S_u( x ) = (x-u)*(P_l( u )-P_l(c))/(u-1) + P_l( u )
-  * We add the lemmas:
-  *   ( 0 < y < 1 ) => sin( y ) >= S_l( y )
-  *   ( 1 < y < PI/2 ) => sin( y ) >= S_u( y )
-  * which are:
-  *   ( 0 < y < 1 ) => (sin y) >= 4251/5040*y
-  *   ( 1 < y < PI/2 ) => (sin y) >= c1*(y+c2)
-  *     where c1, c2 are rationals (for brevity, omitted here)
-  *     such that c1 ~= .277 and c2 ~= 2.032.
-  */
-  std::vector<Node> checkTranscendentalTangentPlanes();
+   *
+   * Returns a set of valid theory lemmas, based on
+   * computing an "incremental linearization" of
+   * transcendental functions based on the model values
+   * of transcendental functions and their arguments.
+   * It is based on Figure 3 of "Satisfiability
+   * Modulo Transcendental Functions via Incremental
+   * Linearization" by Cimatti et al., CADE 2017.
+   * This schema is not terminating in general.
+   * It is not enabled by default, and can
+   * be enabled by --nl-ext-tf-tplanes.
+   *
+   * Example:
+   *
+   * Assume we have a term sin(y) where M( y ) = 1 where M is the current model.
+   * Note that:
+   *   sin(1) ~= .841471
+   *
+   * The Taylor series and remainder of sin(y) of degree 7 is
+   *   P_{7,sin(0)}( x ) = x + (-1/6)*x^3 + (1/20)*x^5
+   *   R_{7,sin(0),b}( x ) = (-1/5040)*x^7
+   *
+   * This gives us lower and upper bounds :
+   *   P_u( x ) = P_{7,sin(0)}( x ) + R_{7,sin(0),b}( x )
+   *     ...where note P_u( 1 ) = 4243/5040 ~= .841865
+   *   P_l( x ) = P_{7,sin(0)}( x ) - R_{7,sin(0),b}( x )
+   *     ...where note P_l( 1 ) = 4241/5040 ~= .841468
+   *
+   * Assume that M( sin(y) ) > P_u( 1 ).
+   * Since the concavity of sine in the region 0 < x < PI/2 is -1,
+   * we add a tangent plane refinement.
+   * The tangent plane at the point 1 in P_u is
+   * given by the formula:
+   *   T( x ) = P_u( 1 ) + ((d/dx)(P_u(x)))( 1 )*( x - 1 )
+   * We add the lemma:
+   *   ( 0 < y < PI/2 ) => sin( y ) <= T( y )
+   * which is:
+   *   ( 0 < y < PI/2 ) => sin( y ) <= (391/720)*(y - 2737/1506)
+   *
+   * Assume that M( sin(y) ) < P_u( 1 ).
+   * Since the concavity of sine in the region 0 < x < PI/2 is -1,
+   * we add a secant plane refinement for some constants ( l, u )
+   * such that 0 <= l < M( y ) < u <= PI/2. Assume we choose
+   * l = 0 and u = M( PI/2 ) = 150517/47912.
+   * The secant planes at point 1 for P_l
+   * are given by the formulas:
+   *   S_l( x ) = (x-l)*(P_l( l )-P_l(c))/(l-1) + P_l( l )
+   *   S_u( x ) = (x-u)*(P_l( u )-P_l(c))/(u-1) + P_l( u )
+   * We add the lemmas:
+   *   ( 0 < y < 1 ) => sin( y ) >= S_l( y )
+   *   ( 1 < y < PI/2 ) => sin( y ) >= S_u( y )
+   * which are:
+   *   ( 0 < y < 1 ) => (sin y) >= 4251/5040*y
+   *   ( 1 < y < PI/2 ) => (sin y) >= c1*(y+c2)
+   *     where c1, c2 are rationals (for brevity, omitted here)
+   *     such that c1 ~= .277 and c2 ~= 2.032.
+   *
+   * The argument lemSE is the "side effect" of the lemmas in the return
+   * value of this function (for details, see checkLastCall).
+   */
+  std::vector<Node> checkTranscendentalTangentPlanes(
+      std::map<Node, NlLemmaSideEffect>& lemSE);
   /** check transcendental function refinement for tf
    *
    * This method is called by the above method for each refineable
@@ -938,9 +959,13 @@ class NonlinearExtension {
    *
    * This runs Figure 3 of Cimatti et al., CADE 2017 for transcendental
    * function application tf for Taylor degree d. It may add a secant or
-   * tangent plane lemma to lems.
+   * tangent plane lemma to lems and its side effect (if one exists)
+   * to lemSE.
    */
-  bool checkTfTangentPlanesFun(Node tf, unsigned d, std::vector<Node>& lems);
+  bool checkTfTangentPlanesFun(Node tf,
+                               unsigned d,
+                               std::vector<Node>& lems,
+                               std::map<Node, NlLemmaSideEffect>& lemSE);
   //-------------------------------------------- end lemma schemas
 }; /* class NonlinearExtension */