Improve flexibility of lemma output in non-linear solver (#3518)

1 files changed, 40 insertions, 21 deletions

diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h
index 1690c9334..20357b722 100644
--- a/src/theory/arith/nonlinear_extension.h
+++ b/src/theory/arith/nonlinear_extension.h
@@ -138,13 +138,13 @@ class NonlinearExtension {
    * described in Reynolds et al. FroCoS 2017 that are based on ruling out
    * the current candidate model.
    *
-   * This function returns true if a lemma was sent out on the output
-   * channel of the theory of arithmetic. 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.
+   * This function returns true if a lemma was added to the vector lems/lemsPp.
+   * 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.
    */
-  bool modelBasedRefinement();
+  bool modelBasedRefinement(std::vector<Node>& mlems,
+                            std::vector<Node>& mlemsPp);
   /** returns true if the multiset containing the
    * factors of monomial a is a subset of the multiset
    * containing the factors of monomial b.
@@ -181,12 +181,26 @@ class NonlinearExtension {
    *
    * xts : the list of (non-reduced) extended terms in the current context.
    *
-   * This method returns the number of lemmas added on the output channel of
-   * TheoryArith.
+   * This method adds lemmas to arguments lems, lemsPp, and wlems, each of
+   * which are intended to be sent out on the output channel of TheoryArith
+   * under certain conditions.
+   *
+   * If the set lems or lemsPp is non-empty, then no further processing is
+   * necessary. The last call effort check should terminate and these
+   * lemmas should be sent. The set lemsPp is distinguished from lems since
+   * the preprocess flag on the lemma(...) call should be set to true.
+   *
+   * The "waiting" lemmas wlems contain lemmas that should be sent on the
+   * 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.
    */
   int checkLastCall(const std::vector<Node>& assertions,
                     const std::vector<Node>& false_asserts,
-                    const std::vector<Node>& xts);
+                    const std::vector<Node>& xts,
+                    std::vector<Node>& lems,
+                    std::vector<Node>& lemsPp,
+                    std::vector<Node>& wlems);
   //---------------------------------------term utilities
   static bool isArithKind(Kind k);
   static Node mkLit(Node a, Node b, int status, bool isAbsolute = false);
@@ -240,9 +254,15 @@ class NonlinearExtension {
    *
    * For details, see Section 3 of Cimatti et al CADE 2017 under the heading
    * "Detecting Satisfiable Formulas".
+   *
+   * The arguments lemmas and gs store the lemmas and guard literals to be sent
+   * out on the output channel of TheoryArith as lemmas and calls to
+   * ensureLiteral respectively.
    */
   bool checkModel(const std::vector<Node>& assertions,
-                  const std::vector<Node>& false_asserts);
+                  const std::vector<Node>& false_asserts,
+                  std::vector<Node>& lemmas,
+                  std::vector<Node>& gs);
   //---------------------------end check model
 
   /** In the following functions, status states a relationship
@@ -327,18 +347,19 @@ class NonlinearExtension {
   /** Is n entailed with polarity pol in the current context? */
   bool isEntailed(Node n, bool pol);
 
-  /** flush lemmas
-   *
-   * Potentially sends lem on the output channel if lem has not been sent on the
-   * output channel in this context. Returns the number of lemmas sent on the
-   * output channel of TheoryArith.
+  /**
+   * Potentially adds lemmas to the set out and clears lemmas. Returns
+   * the number of lemmas added to out. We do not add lemmas that have already
+   * been sent on the output channel of TheoryArith.
    */
-  int flushLemma(Node lem);
+  unsigned filterLemmas(std::vector<Node>& lemmas, std::vector<Node>& out);
+  /** singleton version of above */
+  unsigned filterLemma(Node lem, std::vector<Node>& out);
 
-  /** Potentially sends lemmas to the output channel and clears lemmas. Returns
-   * the number of lemmas sent to the output channel.
+  /**
+   * Send lemmas in out on the output channel of theory of arithmetic.
    */
-  int flushLemmas(std::vector<Node>& lemmas);
+  void sendLemmas(const std::vector<Node>& out, bool preprocess = false);
 
   // Returns the NodeMultiset for an existing monomial.
   const NodeMultiset& getMonomialExponentMap(Node monomial) const;
@@ -439,8 +460,6 @@ class NonlinearExtension {
   /** Stores skolems in the range of the above map */
   std::map<Node, bool> d_tr_is_base;
   std::map< Node, bool > d_tf_initial_refine;
-  /** the list of lemmas we are waiting to flush until after check model */
-  std::vector<Node> d_waiting_lemmas;
 
   void mkPi();
   void getCurrentPiBounds( std::vector< Node >& lemmas );