call nlsat

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

src/math/lp/monic.h

@@ -74,6 +74,9 @@ public:
     void reset_rfields() { m_rsign = false; m_rvars.reset(); SASSERT(m_rvars.size() == 0); }
     void push_rvar(signed_var sv) { m_rsign ^= sv.sign(); m_rvars.push_back(sv.var()); }
     void sort_rvars() { std::sort(m_rvars.begin(), m_rvars.end()); }
+    
+    svector<lpvar>::const_iterator begin() const { return vars().begin(); }
+    svector<lpvar>::const_iterator end() const { return vars().end(); }
 };
 
 inline std::ostream& operator<<(std::ostream& out, monic const& m) {

src/math/lp/nla_basics_lemmas.cpp

@@ -359,8 +359,7 @@ bool basics::basic_lemma_for_mon_neutral_derived(const monic& rm, const factoriz
 
 // x != 0 or y = 0 => |xy| >= |y|
 void basics::proportion_lemma_model_based(const monic& rm, const factorization& factorization) {
-    if (c().has_real(factorization)) // todo: handle the situaiton when all factors are greater than 1,        
-        return;     // or smaller than 1
+    if (c().factorization_has_real(factorization)) // todo: handle the situaiton when all factors are greater than 1,           return;     // or smaller than 1
     rational rmv = abs(var_val(rm));
     if (rmv.is_zero()) {
         SASSERT(c().has_zero_factor(factorization));
@@ -486,8 +485,6 @@ bool basics::is_separated_from_zero(const factorization& f) const {
     return true;
 }
 
-
-
 // here we use the fact xy = 0 -> x = 0 or y = 0
 void basics::basic_lemma_for_mon_zero_model_based(const monic& rm, const factorization& f) {        
     TRACE("nla_solver",  c().trace_print_monic_and_factorization(rm, f, tout););

src/math/lp/nla_core.cpp

@@ -1895,4 +1895,23 @@ bool core::influences_nl_var(lpvar j) const {
     return false;
 }
 
+bool core::factorization_has_real(const factorization& f) const {
+    for (const factor& fc: f) {
+        lpvar j = var(fc);
+        if (!var_is_int(j))
+            return true;
+    }
+    return false;
+}
+
+bool core::monic_has_real(const monic& m) const {
+    if (!var_is_int(m.var()))
+        return true;
+    for (lpvar j : m) {
+        if (!var_is_int(j))
+            return true;
+    }
+    return false;
+}
+
 } // end of nla

src/math/lp/nla_core.h

@@ -153,7 +153,7 @@ public:
 
     void insert_to_refine(lpvar j);
     void erase_from_to_refine(lpvar j);
-    
+    const lp::u_set& to_refine() const { return m_to_refine; }         
     const lp::u_set&  active_var_set () const { return m_active_var_set;}
     bool active_var_set_contains(unsigned j) const { return m_active_var_set.contains(j); }
 
@@ -441,9 +441,8 @@ public:
     bool patch_blocker(lpvar u, const monic& m) const;
     bool has_big_num(const monic&) const;
     bool var_is_big(lpvar) const;
-    bool has_real(const factorization&) const;
-    bool has_real(const monic& m) const;
-
+    bool factorization_has_real(const factorization&) const;
+    bool monic_has_real(const monic&) const;
 };  // end of core
 
 struct pp_mon {

src/math/lp/nla_monotone_lemmas.cpp

@@ -11,13 +11,25 @@ namespace nla {
 
 monotone::monotone(core * c) : common(c) {}
 
+// return false if at least one variable, including the monic var, is real,
+// or one of the variable from m.vars() is zero
+bool monotone::monotonicity_lemma_candidate(const monic & m) const {
+    if (!c().var_is_int(m.var()))
+        return false;
+    for (lpvar j : m) {
+        if (!c().var_is_int(j) || val(j).is_zero())
+            return false;        
+    }
+    return true;
+}
     
 void monotone::monotonicity_lemma() {
     unsigned shift = random();
     unsigned size = c().m_to_refine.size();
     for (unsigned i = 0; i < size && !done(); i++) { 
         lpvar v = c().m_to_refine[(i + shift) % size];
-        monotonicity_lemma(c().emons()[v]);
+        if (monotonicity_lemma_candidate(c().emons()[v]))
+            monotonicity_lemma(c().emons()[v]);
     }
 }
    
@@ -33,6 +45,9 @@ void monotone::monotonicity_lemma(monic const& m) {
         monotonicity_lemma_lt(m, prod_val);
     else if (m_val > prod_val)
         monotonicity_lemma_gt(m, prod_val);
+    else {
+        TRACE("nla_solver", tout << "equal\n";);
+    }
 }
 
 void monotone::monotonicity_lemma_gt(const monic& m, const rational& prod_val) {

src/math/lp/nla_monotone_lemmas.h

@@ -18,5 +18,6 @@ private:
     void monotonicity_lemma_lt(const monic& m, const rational& prod_val);    
     std::vector<rational> get_sorted_key(const monic& rm) const;
     vector<std::pair<rational, lpvar>> get_sorted_key_with_rvars(const monic& a) const;
+    bool monotonicity_lemma_candidate(const monic& m) const;
 };
 }

src/math/lp/nla_order_lemmas.cpp

@@ -40,7 +40,6 @@ void order::order_lemma() {
 void order::order_lemma_on_monic(const monic& m) {
     TRACE("nla_solver_details",
           tout << "m = " << pp_mon(c(), m););
-
     if (c().has_real(m))
         return;
     for (auto ac : factorization_factory_imp(m, _())) {

src/math/lp/nla_solver.cpp

@@ -28,10 +28,23 @@ bool solver::is_monic_var(lpvar v) const {
 
 bool solver::need_check() { return true; }
 
-lbool solver::check(vector<lemma>& l) {
-    return m_core->check(l);
+lbool solver::run_nra(lp::explanation & expl) {
+    return m_nra.check(expl);
 }
 
+
+lbool solver::check(vector<lemma>& l, lp::explanation& expl) {    
+    set_use_nra_model(false);
+    lbool ret = m_core->check(l);
+    if (ret == l_undef) {
+        ret = run_nra(expl);
+        if (ret == l_true) {
+            set_use_nra_model(true);
+        }            
+    }
+    return ret;
+}
+ 
 void solver::push(){
     m_core->push();
 }

src/math/lp/nla_solver.h

@@ -26,6 +26,9 @@ class solver {
     reslimit m_res_limit;
     core* m_core;
     nra::solver m_nra;
+    bool m_use_nra_model;
+    lbool run_nra(lp::explanation&);
+    void set_use_nra_model(bool m) { m_use_nra_model = m; }
 public:
     void add_monic(lpvar v, unsigned sz, lpvar const* vs);
     
@@ -35,11 +38,11 @@ public:
     void push();
     void pop(unsigned scopes);
     bool need_check();
-    lbool check(vector<lemma>&);
+    lbool check(vector<lemma>&, lp::explanation& lp);
     bool is_monic_var(lpvar) const;
     bool influences_nl_var(lpvar) const;
     std::ostream& display(std::ostream& out) const;
-
+    bool use_nra_model() const { return m_use_nra_model; }
     core& get_core() { return *m_core; }
 };
 }

src/math/lp/nra_solver.cpp

@@ -24,8 +24,6 @@ struct solver::imp {
     u_map<polynomial::var> m_lp2nl;  // map from lar_solver variables to nlsat::solver variables        
     scoped_ptr<nlsat::solver> m_nlsat;
     scoped_ptr<scoped_anum>   m_zero;
-    vector<mon_eq>            m_monics;
-    unsigned_vector           m_monics_lim;
     mutable variable_map_type m_variable_values; // current model        
     nla::core&                m_nla_core;    
     imp(lp::lar_solver& s, reslimit& lim, params_ref const& p, nla::core& nla_core): 
@@ -35,22 +33,9 @@ struct solver::imp {
         m_nla_core(nla_core) {}
 
     bool need_check() {
-        return !m_monics.empty() && !check_assignments(m_monics, s, m_variable_values);
+        return m_nla_core.to_refine().size() != 0;
     }
 
-    void add(lp::var_index v, unsigned sz, lp::var_index const* vs) {
-        m_monics.push_back(mon_eq(v, sz, vs));
-    }
-
-    void push() {
-        m_monics_lim.push_back(m_monics.size());
-    }
-
-    void pop(unsigned n) {
-        if (n == 0) return;
-        m_monics.shrink(m_monics_lim[m_monics_lim.size() - n]);
-        m_monics_lim.shrink(m_monics_lim.size() - n);       
-    }
 
     /*
       \brief Check if polynomials are well defined.
@@ -85,8 +70,8 @@ struct solver::imp {
        TBD: use partial model from lra_solver to prime the state of nlsat_solver.
        TBD: explore more incremental ways of applying nlsat (using assumptions)
     */
-    lbool check(lp::explanation& ex) {
-        SASSERT(need_check());
+    lbool check(lp::explanation& ex) {        
+        SASSERT(need_check() && ex.size() == 0);
         m_nlsat = alloc(nlsat::solver, m_limit, m_params, false);
         m_zero = alloc(scoped_anum, am());
         m_lp2nl.reset();
@@ -97,10 +82,10 @@ struct solver::imp {
             add_constraint(ci);
         }
 
-        // add polynomial definitions.
-        for (auto const& m : m_monics) {
-            add_monic_eq(m);
-        }
+        // // add polynomial definitions.
+        // for (auto const& m : m_monics) {
+        //     add_monic_eq(m);
+        // }
         // TBD: add variable bounds?
 
         lbool r = l_undef;
@@ -227,7 +212,7 @@ struct solver::imp {
     }
 
     std::ostream& display(std::ostream& out) const {
-        for (auto m : m_monics) {
+        for (auto m : m_nla_core.emons()) {
             out << "j" << m.var() << " = ";
             for (auto v : m.vars()) {
                 out << "j" << v << " ";
@@ -246,9 +231,6 @@ solver::~solver() {
     dealloc(m_imp);
 }
 
-void solver::add_monic(lp::var_index v, unsigned sz, lp::var_index const* vs) {
-    m_imp->add(v, sz, vs);
-}
 
 lbool solver::check(lp::explanation& ex) {
     return m_imp->check(ex);
@@ -258,14 +240,6 @@ bool solver::need_check() {
     return m_imp->need_check();
 }
 
-void solver::push() {
-    m_imp->push();
-}
-
-void solver::pop(unsigned n) {
-    m_imp->pop(n);
-}
-
 std::ostream& solver::display(std::ostream& out) const {
     return m_imp->display(out);
 }

src/math/lp/nra_solver.h

@@ -29,11 +29,6 @@ namespace nra {
         
         ~solver();
 
-        /*
-          \brief Add a definition v = vs[0]*vs[1]*...*vs[sz-1]
-          The variable v is equal to the product of variables vs.
-        */
-        void add_monic(lp::var_index v, unsigned sz, lp::var_index const* vs);
 
         /*
           \brief Check feasiblity of linear constraints augmented by polynomial definitions
@@ -53,13 +48,6 @@ namespace nra {
 
         nlsat::anum_manager& am();        
 
-        /*
-          \brief push and pop scope. 
-          Monomial definitions are retraced when popping scope.
-        */
-        void push();
-        
-        void pop(unsigned n);
 
         /*
           \brief display state

src/smt/theory_lra.cpp

@@ -632,7 +632,8 @@ class theory_lra::imp {
                 vars.push_back(register_theory_var_in_lar_solver(v));
             }
             TRACE("arith", tout << "v" << v << " := " << mk_pp(t, m) << "\n" << vars << "\n";);
-            m_solver->register_existing_terms();            
+            m_solver->register_existing_terms();
+            ensure_nla();
             m_nla->add_monic(register_theory_var_in_lar_solver(v), vars.size(), vars.c_ptr());
         }
         return v;
@@ -2138,7 +2139,11 @@ public:
     lbool check_nla_continue() {
         m_a1 = nullptr; m_a2 = nullptr;
         auto & lv = m_nla_lemma_vector;
-        lbool r = m_nla->check(lv);
+        lbool r = m_nla->check(lv, m_explanation);
+        if (m_explanation.size()) {
+            NOT_IMPLEMENTED_YET(); // the nra_solver worked
+        }
+    
         switch (r) {
         case l_false: {
             m_stats.m_nla_lemmas += lv.size();

src/tactic/smtlogics/qfnra_tactic.cpp

@@ -44,12 +44,14 @@ tactic * mk_qfnra_tactic(ast_manager & m, params_ref const& p) {
 
     return and_then(mk_simplify_tactic(m, p), 
                     mk_propagate_values_tactic(m, p),
-                    or_else(try_for(mk_qfnra_nlsat_tactic(m, p0), 5000),
-                            try_for(mk_qfnra_nlsat_tactic(m, p1), 10000),
-                            mk_qfnra_sat_solver(m, p, 4),
-                            and_then(try_for(mk_smt_tactic(m), 5000), mk_fail_if_undecided_tactic()),
-                            mk_qfnra_sat_solver(m, p, 6),
-                            mk_qfnra_nlsat_tactic(m, p2)));
+                    //or_else(//try_for(mk_qfnra_nlsat_tactic(m, p0), 5000),
+                            //try_for(mk_qfnra_nlsat_tactic(m, p1), 10000),
+                            //mk_qfnra_sat_solver(m, p, 4),
+                            //and_then(try_for(mk_smt_tactic(m), 5000), mk_fail_if_undecided_tactic()),
+                            mk_qfnra_sat_solver(m, p, 6)
+                            //mk_qfnra_nlsat_tactic(m, p2)
+                            //)
+        );
 }