Make nonlinear solver intercept model assignments from the linear arithmetic solver (#3525)

10 files changed, 201 insertions, 68 deletions

diff --git a/src/theory/arith/nl_model.cpp b/src/theory/arith/nl_model.cpp
index 762e8b141..fe756e5f7 100644
--- a/src/theory/arith/nl_model.cpp
+++ b/src/theory/arith/nl_model.cpp
@@ -15,6 +15,7 @@
 #include "theory/arith/nl_model.h"
 
 #include "expr/node_algorithm.h"
+#include "options/arith_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/rewriter.h"
@@ -36,11 +37,18 @@ NlModel::NlModel(context::Context* c) : d_used_approx(false)
 
 NlModel::~NlModel() {}
 
-void NlModel::reset(TheoryModel* m)
+void NlModel::reset(TheoryModel* m, std::map<Node, Node>& arithModel)
 {
   d_model = m;
   d_mv[0].clear();
   d_mv[1].clear();
+  d_arithVal.clear();
+  // process arithModel
+  std::map<Node, Node>::iterator it;
+  for (const std::pair<const Node, Node>& m : arithModel)
+  {
+    d_arithVal[m.first] = m.second;
+  }
 }
 
 void NlModel::resetCheck()
@@ -127,21 +135,42 @@ Node NlModel::computeModelValue(Node n, bool isConcrete)
   return ret;
 }
 
-Node NlModel::getValueInternal(Node n) const
-{
-  return d_model->getValue(n);
-}
-
 bool NlModel::hasTerm(Node n) const
 {
-  return d_model->hasTerm(n);
+  return d_arithVal.find(n) != d_arithVal.end();
 }
 
 Node NlModel::getRepresentative(Node n) const
 {
+  if (n.isConst())
+  {
+    return n;
+  }
+  std::map<Node, Node>::const_iterator it = d_arithVal.find(n);
+  if (it != d_arithVal.end())
+  {
+    AlwaysAssert(it->second.isConst());
+    return it->second;
+  }
   return d_model->getRepresentative(n);
 }
 
+Node NlModel::getValueInternal(Node n) const
+{
+  if (n.isConst())
+  {
+    return n;
+  }
+  std::map<Node, Node>::const_iterator it = d_arithVal.find(n);
+  if (it != d_arithVal.end())
+  {
+    AlwaysAssert(it->second.isConst());
+    return it->second;
+  }
+  // It is unconstrained in the model, return 0.
+  return d_zero;
+}
+
 int NlModel::compare(Node i, Node j, bool isConcrete, bool isAbsolute)
 {
   Node ci = computeModelValue(i, isConcrete);
diff --git a/src/theory/arith/nl_model.h b/src/theory/arith/nl_model.h
index ed13327cc..66c5d89c1 100644
--- a/src/theory/arith/nl_model.h
+++ b/src/theory/arith/nl_model.h
@@ -52,7 +52,7 @@ class NlModel
    * where m is the model of the theory of arithmetic. This method resets the
    * cache of computed model values.
    */
-  void reset(TheoryModel* m);
+  void reset(TheoryModel* m, std::map<Node, Node>& arithModel);
   /** reset check
    *
    * This method is called when the non-linear arithmetic solver restarts
@@ -265,6 +265,12 @@ class NlModel
   Node d_true;
   Node d_false;
   Node d_null;
+  /**
+   * The values that the arithmetic theory solver assigned in the model. This
+   * corresponds to exactly the set of equalities that TheoryArith is currently
+   * sending to TheoryModel during collectModelInfo.
+   */
+  std::map<Node, Node> d_arithVal;
   /** cache of model values
    *
    * Stores the the concrete/abstract model values. This is a cache of the
diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index 287acbc36..6e8e7623d 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -185,7 +185,6 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing,
                                        eq::EqualityEngine* ee)
     : d_lemmas(containing.getUserContext()),
       d_zero_split(containing.getUserContext()),
-      d_skolem_atoms(containing.getUserContext()),
       d_containing(containing),
       d_ee(ee),
       d_needsLastCall(false),
@@ -735,16 +734,16 @@ std::vector<Node> NonlinearExtension::checkModelEval(
   for (size_t i = 0; i < assertions.size(); ++i) {
     Node lit = assertions[i];
     Node atom = lit.getKind()==NOT ? lit[0] : lit;
-    if( d_skolem_atoms.find( atom )==d_skolem_atoms.end() ){
-      Node litv = d_model.computeConcreteModelValue(lit);
-      Trace("nl-ext-mv-assert") << "M[[ " << lit << " ]] -> " << litv;
-      if (litv != d_true) {
-        Trace("nl-ext-mv-assert") << " [model-false]" << std::endl;
-        //Assert(litv == d_false);
-        false_asserts.push_back(lit);
-      } else {
-        Trace("nl-ext-mv-assert") << std::endl;
-      }
+    Node litv = d_model.computeConcreteModelValue(lit);
+    Trace("nl-ext-mv-assert") << "M[[ " << lit << " ]] -> " << litv;
+    if (litv != d_true)
+    {
+      Trace("nl-ext-mv-assert") << " [model-false]" << std::endl;
+      false_asserts.push_back(lit);
+    }
+    else
+    {
+      Trace("nl-ext-mv-assert") << std::endl;
     }
   }
   return false_asserts;
@@ -1271,32 +1270,17 @@ void NonlinearExtension::check(Theory::Effort e) {
   }
   else
   {
-    std::map<Node, Node> approximations;
-    std::map<Node, Node> arithModel;
-    TheoryModel* tm = d_containing.getValuation().getModel();
-    if (!d_builtModel.get())
+    // If we computed lemmas during collectModelInfo, send them now.
+    if (!d_cmiLemmas.empty() || !d_cmiLemmasPp.empty())
     {
-      // run a last call effort check
-      std::vector<Node> mlems;
-      std::vector<Node> mlemsPp;
-      if (modelBasedRefinement(mlems, mlemsPp))
-      {
-        sendLemmas(mlems);
-        sendLemmas(mlemsPp, true);
-        return;
-      }
+      sendLemmas(d_cmiLemmas);
+      sendLemmas(d_cmiLemmasPp, true);
+      return;
     }
-    // get the values that should be replaced in the model
-    d_model.getModelValueRepair(arithModel, approximations);
-    // those that are exact are written as exact approximations to the model
-    for (std::pair<const Node, Node>& r : arithModel)
-    {
-      Node eq = r.first.eqNode(r.second);
-      eq = Rewriter::rewrite(eq);
-      tm->recordApproximation(r.first, eq);
-    }
-    // those that are approximate are recorded as approximations
-    for (std::pair<const Node, Node>& a : approximations)
+    // Otherwise, we will answer SAT. The values that we approximated are
+    // recorded as approximations here.
+    TheoryModel* tm = d_containing.getValuation().getModel();
+    for (std::pair<const Node, Node>& a : d_approximations)
     {
       tm->recordApproximation(a.first, a.second);
     }
@@ -1306,8 +1290,6 @@ void NonlinearExtension::check(Theory::Effort e) {
 bool NonlinearExtension::modelBasedRefinement(std::vector<Node>& mlems,
                                               std::vector<Node>& mlemsPp)
 {
-  // reset the model object
-  d_model.reset(d_containing.getValuation().getModel());
   // get the assertions
   std::vector<Node> assertions;
   getAssertions(assertions);
@@ -1497,6 +1479,29 @@ bool NonlinearExtension::modelBasedRefinement(std::vector<Node>& mlems,
   return false;
 }
 
+void NonlinearExtension::interceptModel(std::map<Node, Node>& arithModel)
+{
+  if (!needsCheckLastEffort())
+  {
+    // no non-linear constraints, we are done
+    return;
+  }
+  d_model.reset(d_containing.getValuation().getModel(), arithModel);
+  // run a last call effort check
+  d_cmiLemmas.clear();
+  d_cmiLemmasPp.clear();
+  if (!d_builtModel.get())
+  {
+    modelBasedRefinement(d_cmiLemmas, d_cmiLemmasPp);
+  }
+  if (d_builtModel.get())
+  {
+    d_approximations.clear();
+    // modify the model values
+    d_model.getModelValueRepair(arithModel, d_approximations);
+  }
+}
+
 void NonlinearExtension::presolve()
 {
   Trace("nl-ext") << "NonlinearExtension::presolve" << std::endl;
@@ -2453,17 +2458,9 @@ std::vector<Node> NonlinearExtension::checkFactoring(
     Node atom = lit.getKind() == NOT ? lit[0] : lit;
     Node litv = d_model.computeConcreteModelValue(lit);
     bool considerLit = false;
-    if( d_skolem_atoms.find(atom) != d_skolem_atoms.end() )
-    {
-      //always consider skolem literals
-      considerLit = true;
-    }
-    else
-    {
-      // Only consider literals that are in false_asserts.
-      considerLit = std::find(false_asserts.begin(), false_asserts.end(), lit)
-                    != false_asserts.end();
-    }
+    // Only consider literals that are in false_asserts.
+    considerLit = std::find(false_asserts.begin(), false_asserts.end(), lit)
+                  != false_asserts.end();
 
     if (considerLit)
     {
@@ -2538,7 +2535,6 @@ std::vector<Node> NonlinearExtension::checkFactoring(
             Trace("nl-ext-factor") << "...factored polynomial : " << polyn << std::endl;
             Node conc_lit = NodeManager::currentNM()->mkNode( atom.getKind(), polyn, d_zero );
             conc_lit = Rewriter::rewrite( conc_lit );
-            d_skolem_atoms.insert( conc_lit );
             if( !polarity ){
               conc_lit = conc_lit.negate();
             }
@@ -2562,7 +2558,6 @@ Node NonlinearExtension::getFactorSkolem( Node n, std::vector< Node >& lemmas )
   if( itf==d_factor_skolem.end() ){
     Node k = NodeManager::currentNM()->mkSkolem( "kf", n.getType() );
     Node k_eq = Rewriter::rewrite( k.eqNode( n ) );
-    d_skolem_atoms.insert( k_eq );
     lemmas.push_back( k_eq );
     d_factor_skolem[n] = k;
     return k;
diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h
index 20357b722..ddca284a4 100644
--- a/src/theory/arith/nonlinear_extension.h
+++ b/src/theory/arith/nonlinear_extension.h
@@ -116,8 +116,44 @@ class NonlinearExtension {
    *
    * This call may result in (possibly multiple) calls to d_out->lemma(...)
    * where d_out is the output channel of TheoryArith.
+   *
+   * If e is FULL, then we add lemmas based on context-depedent
+   * simplification (see Reynolds et al FroCoS 2017).
+   *
+   * If e is LAST_CALL, we add lemmas based on model-based refinement
+   * (see additionally Cimatti et al., TACAS 2017). The lemmas added at this
+   * effort may be computed during a call to interceptModel as described below.
    */
   void check(Theory::Effort e);
+  /** intercept model
+   *
+   * This method is called during TheoryArith::collectModelInfo, which is
+   * invoked after the linear arithmetic solver passes a full effort check
+   * with no lemmas.
+   *
+   * The argument arithModel is a map of the form { v1 -> c1, ..., vn -> cn }
+   * which represents the linear arithmetic theory solver's contribution to the
+   * current candidate model. That is, its collectModelInfo method is requesting
+   * that equalities v1 = c1, ..., vn = cn be added to the current model, where
+   * v1, ..., vn are arithmetic variables and c1, ..., cn are constants. Notice
+   * arithmetic variables may be real-valued terms belonging to other theories,
+   * or abstractions of applications of multiplication (kind NONLINEAR_MULT).
+   *
+   * This method requests that the non-linear solver inspect this model and
+   * do any number of the following:
+   * (1) Construct lemmas based on a model-based refinement procedure inspired
+   * by Cimatti et al., TACAS 2017.,
+   * (2) In the case that the nonlinear solver finds that the current
+   * constraints are satisfiable, it may "repair" the values in the argument
+   * arithModel so that it satisfies certain nonlinear constraints. This may
+   * involve e.g. solving for variables in nonlinear equations.
+   *
+   * Notice that in the former case, the lemmas it constructs are not sent out
+   * immediately. Instead, they are put in temporary vectors d_cmiLemmas
+   * and d_cmiLemmasPp, which are then sent out (if necessary) when a last call
+   * effort check is issued to this class.
+   */
+  void interceptModel(std::map<Node, Node>& arithModel);
   /** Does this class need a call to check(...) at last call effort? */
   bool needsCheckLastEffort() const { return d_needsLastCall; }
   /** presolve
@@ -390,12 +426,6 @@ class NonlinearExtension {
   NodeSet d_lemmas;
   /** cache of terms t for which we have added the lemma ( t = 0 V t != 0 ). */
   NodeSet d_zero_split;
-  
-  /** 
-   * The set of atoms with Skolems that this solver introduced. We do not
-   * require that models satisfy literals over Skolem atoms.
-   */
-  NodeSet d_skolem_atoms;
 
   /** commonly used terms */
   Node d_zero;
@@ -443,6 +473,15 @@ class NonlinearExtension {
    * and for establishing when we are able to answer "SAT".
    */
   NlModel d_model;
+  /**
+   * The lemmas we computed during collectModelInfo. We store two vectors of
+   * lemmas to be sent out on the output channel of TheoryArith. The first
+   * is not preprocessed, the second is.
+   */
+  std::vector<Node> d_cmiLemmas;
+  std::vector<Node> d_cmiLemmasPp;
+  /** The approximations computed during collectModelInfo. */
+  std::map<Node, Node> d_approximations;
   /** have we successfully built the model in this SAT context? */
   context::CDO<bool> d_builtModel;
 
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index bc4d7db02..58636a10b 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -3550,7 +3550,7 @@ void TheoryArithPrivate::check(Theory::Effort effortLevel){
 
   if(effortLevel == Theory::EFFORT_LAST_CALL){
     if( options::nlExt() ){
-      d_nonlinearExtension->check( effortLevel );
+      d_nonlinearExtension->check(effortLevel);
     }
     return;
   }
@@ -4321,6 +4321,8 @@ bool TheoryArithPrivate::collectModelInfo(TheoryModel* m)
   // TODO:
   // This is not very good for user push/pop....
   // Revisit when implementing push/pop
+  // Map of terms to values, constructed when non-linear arithmetic is active.
+  std::map<Node, Node> arithModel;
   for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
     ArithVar v = *vi;
 
@@ -4335,10 +4337,18 @@ bool TheoryArithPrivate::collectModelInfo(TheoryModel* m)
 
         Node qNode = mkRationalNode(qmodel);
         Debug("arith::collectModelInfo") << "m->assertEquality(" << term << ", " << qmodel << ", true)" << endl;
-
-        if (!m->assertEquality(term, qNode, true))
+        if (options::nlExt())
         {
-          return false;
+          // Let non-linear extension inspect the values before they are sent
+          // to the theory model.
+          arithModel[term] = qNode;
+        }
+        else
+        {
+          if (!m->assertEquality(term, qNode, true))
+          {
+            return false;
+          }
         }
       }else{
         Debug("arith::collectModelInfo") << "Skipping m->assertEquality(" << term << ", true)" << endl;
@@ -4346,6 +4356,20 @@ bool TheoryArithPrivate::collectModelInfo(TheoryModel* m)
       }
     }
   }
+  if (options::nlExt())
+  {
+    // Non-linear may repair values to satisfy non-linear constraints (see
+    // documentation for NonlinearExtension::interceptModel).
+    d_nonlinearExtension->interceptModel(arithModel);
+    // We are now ready to assert the model.
+    for (std::pair<const Node, Node>& p : arithModel)
+    {
+      if (!m->assertEquality(p.first, p.second, true))
+      {
+        return false;
+      }
+    }
+  }
 
   // Iterate over equivalence classes in LinearEqualityModule
   // const eq::EqualityEngine& ee = d_congruenceManager.getEqualityEngine();
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 90038872f..0bcaa049a 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -537,7 +537,9 @@ set(regress_0_tests
   regress0/model-core.smt2
   regress0/nl/coeff-sat.smt2
   regress0/nl/ext-rew-aggr-test.smt2
+  regress0/nl/issue3003.smt2
   regress0/nl/issue3407.smt2
+  regress0/nl/issue3411.smt2
   regress0/nl/issue3475.smt2
   regress0/nl/magnitude-wrong-1020-m.smt2
   regress0/nl/mult-po.smt2
@@ -554,6 +556,7 @@ set(regress_0_tests
   regress0/nl/nta/tan-rewrite.smt2
   regress0/nl/real-as-int.smt2
   regress0/nl/real-div-ufnra.smt2
+  regress0/nl/sin-cos-346-b-chunk-0169.smt2
   regress0/nl/sqrt.smt2
   regress0/nl/sqrt2-value.smt2
   regress0/nl/subs0-unsat-confirm.smt2
@@ -1261,6 +1264,7 @@ set(regress_1_tests
   regress1/nl/exp1-lb.smt2
   regress1/nl/exp_monotone.smt2
   regress1/nl/factor_agg_s.smt2
+  regress1/nl/issue3441.smt2
   regress1/nl/metitarski-1025.smt2
   regress1/nl/metitarski-3-4.smt2
   regress1/nl/metitarski_3_4_2e.smt2
diff --git a/test/regress/regress0/nl/issue3003.smt2 b/test/regress/regress0/nl/issue3003.smt2
new file mode 100644
index 000000000..52bb25963
--- /dev/null
+++ b/test/regress/regress0/nl/issue3003.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic QF_NRA)
+(set-info :status sat)
+(declare-fun _substvar_15_ () Real)                                                                                                                                 
+(declare-fun _substvar_17_ () Real)                                                                                                                                 
+(assert (let ((?v_1 (<= 0.0 _substvar_15_))) (and ?v_1 (and ?v_1 (and ?v_1 (= (* _substvar_15_ _substvar_15_) (+ 1 (* _substvar_17_ (* _substvar_17_ (- 1)))))))))) 
+(check-sat)     
diff --git a/test/regress/regress0/nl/issue3411.smt2 b/test/regress/regress0/nl/issue3411.smt2
new file mode 100644
index 000000000..daf69834b
--- /dev/null
+++ b/test/regress/regress0/nl/issue3411.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic NRA)
+(set-info :status sat)
+(declare-fun a () Real)
+(declare-fun b () Real)
+(assert (= (/ 0 (+ 1 (* a a b))) 0))
+(check-sat)
diff --git a/test/regress/regress0/nl/sin-cos-346-b-chunk-0169.smt2 b/test/regress/regress0/nl/sin-cos-346-b-chunk-0169.smt2
new file mode 100644
index 000000000..65e705fa3
--- /dev/null
+++ b/test/regress/regress0/nl/sin-cos-346-b-chunk-0169.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-info :smt-lib-version 2.6)
+(set-logic QF_NRA)
+(set-info :category "industrial")
+(set-info :status sat)
+(declare-fun skoX () Real)
+(declare-fun skoSQ3 () Real)
+(declare-fun pi () Real)
+(assert (let ((?v_0 (* skoSQ3 skoSQ3))) (and (not (<= (* skoX (* skoX (* skoX (* skoX (+ (/ 1 24) (* skoX (* skoX (+ (/ (- 1) 720) (* skoX (* skoX (/ 1 40320))))))))))) (+ (- 3) ?v_0))) (and (= ?v_0 3) (and (not (<= (+ (/ (- 1) 10000000) (* pi (/ 1 2))) skoX)) (and (not (<= pi (/ 15707963 5000000))) (and (not (<= (/ 31415927 10000000) pi)) (and (not (<= skoX 0)) (not (<= skoSQ3 0))))))))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress1/nl/issue3441.smt2 b/test/regress/regress1/nl/issue3441.smt2
new file mode 100644
index 000000000..19fe98bc5
--- /dev/null
+++ b/test/regress/regress1/nl/issue3441.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_NIA)   
+(set-info :status sat)                                                           
+(declare-fun a () Int)                                                          
+(declare-fun b () Int)                                                          
+(declare-fun c () Int)                                                          
+(declare-fun d () Int)                                                          
+(assert (and (>= (+ (* b c (- (-  4) d)) (- 1)) 0 (div a b))))                  
+(check-sat)