fix mixed integer/real bugs for maximization exposed by non-termination in slow.smt. partially fixes issue #56

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/smt/tactic/smt_tactic.cpp

@@ -27,10 +27,8 @@ Notes:
 
 typedef obj_map<expr, expr *> expr2expr_map;
 
-void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clauses, ptr_vector<expr>& assumptions, scoped_ptr<expr2expr_map>& bool2dep, ref<filter_model_converter>& fmc) {
+void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clauses, ptr_vector<expr>& assumptions, expr2expr_map& bool2dep, ref<filter_model_converter>& fmc) {
-    scoped_ptr<expr2expr_map> dep2bool;
+    expr2expr_map dep2bool;
-    dep2bool = alloc(expr2expr_map);
-    bool2dep = alloc(expr2expr_map);
     ptr_vector<expr> deps;
     ast_manager& m = g->m();
     expr_ref_vector clause(m);
@@ -38,7 +36,7 @@ void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clause
     for (unsigned i = 0; i < sz; i++) {
         expr * f            = g->form(i);
         expr_dependency * d = g->dep(i);
-        if (d == 0) {
+        if (d == 0 || !g->unsat_core_enabled()) {
             clauses.push_back(f);
         }
         else {
@@ -54,19 +52,19 @@ void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clause
                 expr * d = *it;
                 if (is_uninterp_const(d) && m.is_bool(d)) {
                     // no need to create a fresh boolean variable for d
-                    if (!bool2dep->contains(d)) {
+                    if (!bool2dep.contains(d)) {
                         assumptions.push_back(d);
-                        bool2dep->insert(d, d);
+                        bool2dep.insert(d, d);
                     }
                     clause.push_back(m.mk_not(d));
                 }
                 else {
                     // must normalize assumption 
                     expr * b = 0;
-                    if (!dep2bool->find(d, b)) {
+                    if (!dep2bool.find(d, b)) {
                         b = m.mk_fresh_const(0, m.mk_bool_sort());
-                        dep2bool->insert(d, b);
+                        dep2bool.insert(d, b);
-                        bool2dep->insert(b, d);
+                        bool2dep.insert(b, d);
                         assumptions.push_back(b);
                         if (!fmc) {
                             fmc = alloc(filter_model_converter, m);
@@ -78,7 +76,7 @@ void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clause
             }
             SASSERT(clause.size() > 1);
             expr_ref cls(m);
-            cls = mk_or(m, clauses.size(), clauses.c_ptr());
+            cls = mk_or(m, clause.size(), clause.c_ptr());
             clauses.push_back(cls);
         }
     }    
@@ -208,7 +206,7 @@ public:
             SASSERT(m_ctx != 0);
 
             expr_ref_vector clauses(m);
-            scoped_ptr<expr2expr_map>   bool2dep; 
+            expr2expr_map               bool2dep; 
             ptr_vector<expr>            assumptions;       
             ref<filter_model_converter> fmc;
             if (in->unsat_core_enabled()) {
@@ -273,7 +271,7 @@ public:
                     for (unsigned i = 0; i < sz; i++) {
                         expr * b = m_ctx->get_unsat_core_expr(i);
                         SASSERT(is_uninterp_const(b) && m.is_bool(b));
-                        expr * d = bool2dep->find(b);
+                        expr * d = bool2dep.find(b);
                         lcore = m.mk_join(lcore, m.mk_leaf(d));
                     }
                 }

src/smt/tactic/smt_tactic.h

@@ -32,7 +32,7 @@ tactic * mk_smt_tactic(params_ref const & p = params_ref());
 tactic * mk_smt_tactic_using(bool auto_config = true, params_ref const & p = params_ref());
 
 
-void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clauses, ptr_vector<expr>& assumptions, scoped_ptr<obj_map<expr, expr*> >& bool2dep, ref<filter_model_converter>& fmc);
+void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clauses, ptr_vector<expr>& assumptions, obj_map<expr, expr*>& bool2dep, ref<filter_model_converter>& fmc);
 
 /*
   ADD_TACTIC("smt", "apply a SAT based SMT solver.", "mk_smt_tactic(p)") 

src/smt/theory_arith.h

@@ -879,7 +879,6 @@ namespace smt {
         row               m_tmp_row;
 
         void add_tmp_row(row & r1, numeral const & coeff, row const & r2);
-        theory_var pick_var_to_leave(bool has_int, theory_var x_j, bool inc, numeral & a_ij, inf_numeral & gain, bool& skiped_row);
         bool is_safe_to_leave(theory_var x, bool inc, bool& has_int, bool& is_shared);
         template<bool invert>
         void add_tmp_row_entry(row & r, numeral const & coeff, theory_var v);

src/smt/theory_arith_aux.h

@@ -989,83 +989,6 @@ namespace smt {
     }
 
 
-    /**
-       \brief Select tightest variable x_i to pivot with x_j. The goal
-       is to select a x_i such that the value of x_j is increased
-       (decreased) if inc = true (inc = false), and the tableau
-       remains feasible. Store the gain in x_j of the pivoting
-       operation in 'gain'. Note the gain can be too much. That is,
-       it may make x_i infeasible. In this case, instead of pivoting
-       we move x_j to its upper bound (lower bound) when inc = true (inc = false).
-       
-       If no x_i imposes a restriction on x_j, then return null_theory_var.
-       That is, x_j is free to move to its upper bound (lower bound).
-
-       Get the equations for x_j:
-
-       x_i1 = coeff_1 * x_j + rest_1
-       ...
-       x_in = coeff_n * x_j + rest_n
-
-       gain_k := (upper_bound(x_ik) - value(x_ik))/coeff_k
-
-    */
-
-    template<typename Ext>
-    theory_var theory_arith<Ext>::pick_var_to_leave(
-        bool has_int, theory_var x_j, bool inc, 
-        numeral & a_ij, inf_numeral & gain, bool& skipped_row) {
-        TRACE("opt", tout << "selecting variable to replace v" << x_j << ", inc: " << inc << "\n";);
-        theory_var x_i  = null_theory_var;
-        inf_numeral curr_gain; 
-        column & c      = m_columns[x_j];
-        typename svector<col_entry>::iterator it  = c.begin_entries();
-        typename svector<col_entry>::iterator end = c.end_entries();
-        for (; it != end; ++it) {
-            if (!it->is_dead()) {
-                row & r        = m_rows[it->m_row_id];
-                theory_var s = r.get_base_var();
-                if (s != null_theory_var && !is_quasi_base(s)) {
-                    numeral const & coeff = r[it->m_row_idx].m_coeff;
-                    bool inc_s = coeff.is_neg() ? inc : !inc;
-                    bound * b  = get_bound(s, inc_s);
-                    if (b) {
-                        curr_gain  = get_value(s);
-                        curr_gain -= b->get_value();
-                        curr_gain /= coeff;
-                        if (curr_gain.is_neg())
-                            curr_gain.neg();
-                        if (x_i == null_theory_var || (curr_gain < gain) || (gain.is_zero() && curr_gain.is_zero() && s < x_i)) {
-                            if (is_int(s) && !curr_gain.is_int()) {
-                                skipped_row = true;
-                                continue;
-                            }
-                            if (is_int(x_j) && !curr_gain.is_int()) {
-                                skipped_row = true;
-                                continue;
-                            }
-                            if (!curr_gain.is_int() && has_int) {
-                                skipped_row = true;
-                                continue;
-                            }
-                            x_i  = s;
-                            a_ij = coeff;
-                            gain = curr_gain;
-                            TRACE("opt", 
-                                  tout << "x_i: v" << x_i << ", gain: " << gain << "\n";
-                                  tout << "value(s): (" << get_value(s) << " - " << b->get_value() << ")/" << coeff << "\n";
-                                  display_row(tout, r, true);
-                                  );
-                        }
-                    }
-                }
-                TRACE("opt", tout << "x_i: v" << x_i << ", gain: " << gain << "\n";);
-            }
-        }
-        TRACE("opt", tout << "x_i v" << x_i << "\n";);
-        return x_i;
-    }
-
     template<typename Ext>
     bool theory_arith<Ext>::get_theory_vars(expr * n, uint_set & vars) {
         rational r;
@@ -1388,6 +1311,9 @@ namespace smt {
         bool& has_shared,      // determine if pivot involves shared variable
         theory_var& x_i) {     // base variable to pivot with x_j
         
+        if (is_int(x_j) && !get_value(x_j).is_int()) {
+            return false;
+        }
         x_i = null_theory_var;
         context& ctx = get_context();
         column & c   = m_columns[x_j];
@@ -1447,8 +1373,7 @@ namespace smt {
     template<typename Ext>
     void theory_arith<Ext>::normalize_gain(numeral const& divisor, inf_numeral & max_gain) const {
         SASSERT(divisor.is_int());
-        SASSERT(divisor.is_pos());
+        if (!divisor.is_minus_one() && !divisor.is_one() && !max_gain.is_minus_one()) {
-        if (!divisor.is_one() && !max_gain.is_minus_one()) {
             max_gain = floor(max_gain/divisor)*divisor;
         }
     }
@@ -1473,14 +1398,15 @@ namespace smt {
         if (is_int(x)) {
             min_gain = inf_numeral::one();
         }
+        TRACE("opt",
+              tout << "v" << x << " := " << get_value(x) << " "
+              << "min gain: " << min_gain << " " 
+              << "max gain: " << max_gain << "\n";);              
+
         SASSERT(max_gain.is_minus_one() || !max_gain.is_neg());
         SASSERT(min_gain.is_minus_one() || min_gain.is_one());
         SASSERT(!is_int(x) || max_gain.is_int());
         SASSERT(is_int(x) == min_gain.is_one());
-        TRACE("opt",
-              tout << "v" << x << " "
-              << "min gain: " << min_gain << " " 
-              << "max gain: " << max_gain << "\n";);              
 
     }
 
@@ -1512,14 +1438,18 @@ namespace smt {
         if (is_int(x_i)) den_aij = denominator(a_ij);
         SASSERT(den_aij.is_pos() && den_aij.is_int());
 
-        if (is_int(x_i) && !den_aij.is_one()) {
+        if (is_int(x_i) && !den_aij.is_one() && min_gain.is_pos()) {
-            SASSERT(min_gain.is_pos());
             min_gain = inf_numeral(lcm(min_gain.get_rational(), den_aij));
             normalize_gain(min_gain.get_rational(), max_gain);
         }
 
         if (!max_inc.is_minus_one()) {
             if (is_int(x_i)) {
+                TRACE("opt",
+                      tout << "v" << x_i << " a_ij " << a_ij << " "
+                      << "min gain: " << min_gain << " " 
+                      << "max gain: " << max_gain << "\n";);
+
                 max_inc = floor(max_inc);
                 normalize_gain(min_gain.get_rational(), max_inc);
             }
@@ -1539,9 +1469,9 @@ namespace smt {
               << (is_tighter?"true":"false") << "\n";);
         SASSERT(max_gain.is_minus_one() || !max_gain.is_neg());
         SASSERT(min_gain.is_minus_one() || !min_gain.is_neg());
-        SASSERT(!is_int(x_i) || min_gain.is_pos());
+        //SASSERT(!is_int(x_i) || min_gain.is_pos());
-        SASSERT(!is_int(x_i) || min_gain.is_int());
+        //SASSERT(!is_int(x_i) || min_gain.is_int());
-        SASSERT(!is_int(x_i) || max_gain.is_int());
+        //SASSERT(!is_int(x_i) || max_gain.is_int());
         return is_tighter;
     }
 
@@ -1759,6 +1689,10 @@ namespace smt {
         unsigned& best_efforts, // is bound move a best effort?
         bool& has_shared) {     // does move include shared variables?
         inf_numeral min_gain, max_gain;
+        if (is_int(x_i) && !get_value(x_i).is_int()) {
+            ++best_efforts;
+            return false;
+        }
         init_gains(x_i, inc, min_gain, max_gain);        
         column & c   = m_columns[x_i];
         typename svector<col_entry>::iterator it  = c.begin_entries();

src/tactic/nlsat_smt/nl_purify_tactic.cpp

@@ -58,6 +58,7 @@ Revision History:
 #include "solver.h"
 #include "model_smt2_pp.h"
 #include "expr_safe_replace.h"
+#include "ast_util.h"
 
 class nl_purify_tactic : public tactic {
 
@@ -81,6 +82,10 @@ class nl_purify_tactic : public tactic {
     app_ref_vector  m_new_reals;    // interface real variables
     app_ref_vector  m_new_preds;    // abstraction predicates for smt_solver (hide real constraints)
     expr_ref_vector m_asms;         // assumptions to pass to SMT solver
+    ptr_vector<expr> m_ctx_asms;     // assumptions passed by context
+    obj_hashtable<expr>   m_ctx_asms_set; // assumptions passed by context
+    obj_hashtable<expr> m_used_asms;
+    obj_map<expr, expr*> m_bool2dep; 
     obj_pair_map<expr,expr,expr*> m_eq_pairs;  // map pairs of interface variables to auxiliary predicates
     obj_map<expr,expr*> m_interface_cache;     // map of compound real expression to interface variable.
     obj_map<expr, polarity_t> m_polarities;    // polarities of sub-expressions
@@ -98,6 +103,7 @@ public:
         obj_map<expr, polarity_t>& m_polarities;
         obj_map<expr,expr*>& m_interface_cache;
         expr_ref_vector      m_args;
+        proof_ref_vector     m_proofs;
         mode_t               m_mode;
 
         rw_cfg(nl_purify_tactic & o):
@@ -108,6 +114,7 @@ public:
             m_polarities(o.m_polarities),
             m_interface_cache(o.m_interface_cache),
             m_args(m),
+            m_proofs(m),
             m_mode(mode_interface_var) {
         }
 
@@ -115,8 +122,8 @@ public:
 
         arith_util & u() { return m_owner.m_util; }
 
-        expr * mk_interface_var(expr* arg) {
+        expr * mk_interface_var(expr* arg, proof_ref& arg_pr) {
-            expr* r;
+            expr* r;            
             if (m_interface_cache.find(arg, r)) {
                 return r;
             }
@@ -136,6 +143,9 @@ public:
             else {
                 m_owner.m_solver->assert_expr(eq);
             }
+            if (m_owner.m_produce_proofs) {
+                arg_pr = m.mk_oeq(arg, r);
+            }
             return r;
         }
 
@@ -225,24 +235,29 @@ public:
                 }
             }
             m_args.reset();
+            m_proofs.reset();
             for (unsigned i = 0; i < num; ++i) {
                 expr* arg = args[i];
+                proof_ref arg_pr(m);
                 if (is_arith && !is_arith_op(arg)) {
                     has_interface = true;
-                    m_args.push_back(mk_interface_var(arg));
+                    m_args.push_back(mk_interface_var(arg, arg_pr));
                 }
                 else if (!is_arith && u().is_real(arg)) {
                     has_interface = true;
-                    m_args.push_back(mk_interface_var(arg));
+                    m_args.push_back(mk_interface_var(arg, arg_pr));
                 }
                 else {
                     m_args.push_back(arg);
                 }
+                if (arg_pr) {
+                    m_proofs.push_back(arg_pr);
+                }
             }
             if (has_interface) {
                 result = m.mk_app(f, num, m_args.c_ptr());
                 if (m_owner.m_produce_proofs) {
-                    pr = m.mk_oeq(m.mk_app(f, num, args), result); // push proof object to mk_interface_var?
+                    pr = m.mk_oeq_congruence(m.mk_app(f, num, args), to_app(result), m_proofs.size(), m_proofs.c_ptr());
                 }
                 TRACE("nlsat_smt", tout << result << "\n";);
                 return BR_DONE;
@@ -281,7 +296,7 @@ private:
 
     void display_result(std::ostream& out, goal_ref_buffer const& result) {
         for (unsigned i = 0; i < result.size(); ++i) {
-            result[i]->display(out << "goal\n");
+            result[i]->display_with_dependencies(out << "goal\n");
         }        
     }
 
@@ -301,8 +316,11 @@ private:
         }
     }
 
-    void solve(goal_ref_buffer&     result, 
+    void solve(
-               model_converter_ref& mc) {        
+        goal_ref const&       g,
+        goal_ref_buffer&      result, 
+        expr_dependency_ref&  core,
+        model_converter_ref&  mc) {        
 
         while (true) {
             check_point();
@@ -316,6 +334,7 @@ private:
             (*m_nl_tac)(tmp_nl, result, nl_mc, nl_pc, nl_core);
 
             if (is_decided_unsat(result)) {
+                core2result(core, g, result);
                 TRACE("nlsat_smt", tout << "unsat\n";);
                 break;
             }
@@ -328,7 +347,7 @@ private:
             // assert equalities between equal interface real variables.
 
             model_ref mdl_nl, mdl_smt;
-            if (mdl_nl.get()) {
+            if (nl_mc.get()) {
                 model_converter2model(m, nl_mc.get(), mdl_nl);
                 update_eq_values(mdl_nl);
                 enforce_equalities(mdl_nl, m_nl_g);
@@ -343,21 +362,28 @@ private:
             lbool r = m_solver->check_sat(m_asms.size(), m_asms.c_ptr());
             if (r == l_false) {
                 // extract the core from the result 
-                ptr_vector<expr> core;
+                ptr_vector<expr> ecore, asms;
-                m_solver->get_unsat_core(core);
-                if (core.empty()) {
-                    goal_ref g = alloc(goal, m);
-                    g->assert_expr(m.mk_false());
-                    result.push_back(g.get());
-                    break;
-                }
                 expr_ref_vector clause(m);
                 expr_ref fml(m);
-                expr* e;
+                get_unsat_core(ecore, asms);
-                for (unsigned i = 0; i < core.size(); ++i) {
+
-                    clause.push_back(m.is_not(core[i], e)?e:m.mk_not(core[i]));
+                //
+                // assumptions should also be used for the nlsat tactic,
+                // but since it does not support assumptions at this time
+                // we overapproximate the necessary core and accumulate 
+                // all assumptions that are ever used.
+                //
+                for (unsigned i = 0; i < asms.size(); ++i) {
+                    m_used_asms.insert(asms[i]);
                 }
-                fml = m.mk_or(clause.size(), clause.c_ptr());
+                if (ecore.empty()) {
+                    core2result(core, g, result);
+                    break;
+                }
+                for (unsigned i = 0; i < ecore.size(); ++i) {
+                    clause.push_back(mk_not(m, ecore[i]));
+                }
+                fml = mk_or(m, clause.size(), clause.c_ptr());
                 m_nl_g->assert_expr(fml);
                 continue;
             }
@@ -386,9 +412,35 @@ private:
         TRACE("nlsat_smt", display_result(tout, result););
     }
 
+    void get_unsat_core(ptr_vector<expr>& core, ptr_vector<expr>& asms) {
+        m_solver->get_unsat_core(core);
+        for (unsigned i = 0; i < core.size(); ++i) {
+            if (m_ctx_asms_set.contains(core[i])) {
+                asms.push_back(core[i]);
+                core[i] = core.back();
+                core.pop_back();
+                --i;
+            }
+        }
+    }
+
+    void core2result(expr_dependency_ref & lcore, goal_ref const& g, goal_ref_buffer& result) {
+        result.reset();
+        proof * pr = 0;
+        lcore = 0;
+        g->reset();
+        obj_hashtable<expr>::iterator it = m_used_asms.begin(), end = m_used_asms.end();
+        for (; it != end; ++it) {
+            lcore = m.mk_join(lcore, m.mk_leaf(m_bool2dep.find(*it)));
+        }
+        g->assert_expr(m.mk_false(), pr, lcore);
+        TRACE("nlsat_smt", g->display_with_dependencies(tout););
+        result.push_back(g.get());
+    }
 
     void setup_assumptions(model_ref& mdl) {
         m_asms.reset();
+        m_asms.append(m_ctx_asms.size(), m_ctx_asms.c_ptr());
         app_ref_vector const& fresh_preds = m_new_preds;
         expr_ref tmp(m);
         for (unsigned i = 0; i < fresh_preds.size(); ++i) {
@@ -419,10 +471,7 @@ private:
             }
         }
         TRACE("nlsat_smt", 
-              tout << "assumptions:\n";
+              tout << "assumptions:\n" << m_asms << "\n";);
-              for (unsigned i = 0; i < m_asms.size(); ++i) {
-                  tout << mk_pp(m_asms[i].get(), m) << "\n";
-              });
     }
 
     bool enforce_equalities(model_ref& mdl, goal_ref const& nl_g) {
@@ -602,7 +651,7 @@ private:
             expr * curr = g->form(i);
             if (is_pure_arithmetic(is_pure, curr)) {
                 m_nl_g->assert_expr(curr, g->pr(i), g->dep(i));
-                g->update(i, m.mk_true());
+                g->update(i, m.mk_true(), g->pr(i), g->dep(i));
             }
         }        
     }
@@ -702,6 +751,10 @@ public:
         m_new_preds.reset();
         m_eq_pairs.reset();
         m_polarities.reset();
+        m_ctx_asms.reset();
+        m_ctx_asms_set.reset();
+        m_used_asms.reset();
+        m_bool2dep.reset();
     }
     
     virtual void operator()(goal_ref const & g, 
@@ -717,8 +770,9 @@ public:
         mc = 0; pc = 0; core = 0;
 
         fail_if_proof_generation("qfufnra-purify", g);
-        fail_if_unsat_core_generation("qfufnra-purify", g);        
+        // fail_if_unsat_core_generation("qfufnra-purify", g);        
         rw r(*this);
+        expr_ref_vector clauses(m);
         m_nl_g = alloc(goal, m, true, false);
         m_fmc = alloc(filter_model_converter, m);                
 
@@ -728,17 +782,27 @@ public:
         // creating a place-holder predicate inside the
         // original goal and extracing pure nlsat clauses.
         r.set_interface_var_mode();
-        rewrite_goal(r, g);       
+        rewrite_goal(r, g); 
-        remove_pure_arith(g);
+        if (!g->unsat_core_enabled()) {
+            remove_pure_arith(g);
+        }
         get_polarities(*g.get());
         r.set_bool_mode();
         rewrite_goal(r, g);        
 
-        for (unsigned i = 0; i < g->size(); ++i) {
+        extract_clauses_and_dependencies(g, clauses, m_ctx_asms, m_bool2dep, m_fmc);
-            m_solver->assert_expr(g->form(i));
+
+        TRACE("nlsat_smt", tout << clauses << "\n";);
+
+        for (unsigned i = 0; i < m_ctx_asms.size(); ++i) {
+            m_ctx_asms_set.insert(m_ctx_asms[i]);
+        }
+
+        for (unsigned i = 0; i < clauses.size(); ++i) {
+            m_solver->assert_expr(clauses[i].get());
         }
         g->inc_depth();
-        solve(result, mc);        
+        solve(g, result, core, mc);
     }
 };
 
@@ -746,43 +810,3 @@ public:
 tactic * mk_nl_purify_tactic(ast_manager& m, params_ref const& p) {
     return alloc(nl_purify_tactic, m, p);
 }
-
-#if 0
-    void mark_interface_vars(goal_ref const& g) {
-        expr_mark visited;
-        ptr_vector<expr> todo;
-        unsigned sz = g->size();
-        for (unsigned i = 0; i < sz; i++) {
-            todo.push_back(g->form(i));
-        }
-        while (!todo.empty()) {
-            expr* e = todo.back();
-            todo.pop_back();
-            if (visited.is_marked(e)) {
-                continue;
-            }
-            visited.mark(e);
-            if (is_quantifier(e)) {
-                todo.push_back(to_quantifier(e)->get_expr());
-                continue;
-            }
-            if (is_var(e)) {
-                continue;
-            }
-            app* ap = to_app(e);
-            sz = ap->get_num_args();
-            bool is_arith = is_arith_op(e);
-            for (unsigned i = 0; i < sz; ++i) {
-                expr* arg = ap->get_arg(i);
-                todo.push_back(arg);
-                if (is_arith && !is_arith_op(arg)) {
-                    m_interface_vars.mark(arg);
-                }
-                else if (!is_arith && is_arith_op(arg) && ap->get_family_id() != m.get_basic_family_id()) {
-                    m_interface_vars.mark(arg);
-                }
-            }
-        }
-
-    }
-#endif