Merge branch 'master' of https://github.com/Z3Prover/z3

# Conflicts:
#	CMakeLists.txt

CMakeLists.txt

@@ -296,10 +296,9 @@ else()
   # Tracing is always enabled in debug builds
   list(APPEND Z3_COMPONENT_CXX_DEFINES $<$<CONFIG:Debug>:_TRACE>)
 endif()
-# Should we always enable tracing when doing a debug build?
 
 ################################################################################
-# Postion indepdent code
+# Postion independent code
 ################################################################################
 # This is required because code built in the components will end up in a shared
 # library. If not building a shared library ``-fPIC`` isn't needed and would add

src/ast/rewriter/rewriter_def.h

@@ -595,6 +595,9 @@ void rewriter_tpl<Config>::set_inv_bindings(unsigned num_bindings, expr * const
 template<typename Config>
 template<bool ProofGen>
 void rewriter_tpl<Config>::main_loop(expr * t, expr_ref & result, proof_ref & result_pr) {
+    if (m().canceled()) {
+        throw rewriter_exception(m().limit().get_cancel_msg());
+    }
     SASSERT(!ProofGen || result_stack().size() == result_pr_stack().size());
     SASSERT(not_rewriting());
     m_root      = t;

src/nlsat/nlsat_solver.cpp

@@ -460,7 +460,7 @@ namespace nlsat {
 
         void del(bool_var b) {
             SASSERT(m_bwatches[b].empty());
-            SASSERT(m_bvalues[b] == l_undef);
+            //SASSERT(m_bvalues[b] == l_undef);
             m_num_bool_vars--;
             m_dead[b]  = true;
             m_atoms[b] = 0;

src/qe/nlqsat.cpp

@@ -31,6 +31,10 @@ Revision History:
 #include "tseitin_cnf_tactic.h"
 #include "expr_safe_replace.h"
 #include "ast_pp.h"
+#include "for_each_expr.h"
+#include "rewriter.h"
+#include "rewriter_def.h"
+
 
 namespace qe {
 
@@ -76,6 +80,7 @@ namespace qe {
         stats                                m_stats;
         statistics                           m_st;
         obj_hashtable<expr>                  m_free_vars;
+        obj_hashtable<expr>                  m_aux_vars;
         expr_ref_vector                      m_answer;
         expr_safe_replace                    m_answer_simplify;
         nlsat::literal_vector                m_assumptions;
@@ -423,6 +428,115 @@ namespace qe {
             }
         }
 
+        struct div {
+            expr_ref num, den, name;
+            div(ast_manager& m, expr* n, expr* d, expr* nm):
+                num(n, m), den(d, m), name(nm, m) {}            
+        };
+
+        class div_rewriter_cfg : public default_rewriter_cfg {
+            nlqsat&       s;
+            ast_manager&  m;
+            arith_util    a;
+            vector<div>   m_divs;
+        public:
+            div_rewriter_cfg(nlqsat& s): s(s), m(s.m), a(s.m) {}
+            ~div_rewriter_cfg() {}
+            br_status reduce_app(func_decl* f, unsigned sz, expr* const* args, expr_ref& result, proof_ref& pr) {
+                if (is_decl_of(f, a.get_family_id(), OP_DIV) && sz == 2 && !a.is_numeral(args[1]) && is_ground(args[0]) && is_ground(args[1])) {
+                    result = m.mk_fresh_const("div", a.mk_real());
+                    m_divs.push_back(div(m, args[0], args[1], result));
+                    return BR_DONE;
+                }
+                return BR_FAILED;
+            }
+            vector<div> const& divs() const { return m_divs; }
+        };
+
+        //template class rewriter_tpl<div_rewriter_cfg>;
+        
+        
+        class div_rewriter_star : public rewriter_tpl<div_rewriter_cfg> {
+            div_rewriter_cfg m_cfg;
+        public:
+            div_rewriter_star(nlqsat& s):
+                rewriter_tpl<div_rewriter_cfg>(s.m, false, m_cfg),
+                m_cfg(s)
+            {}
+            vector<div> const& divs() const { return m_cfg.divs(); }
+        };
+
+        class is_pure_proc {
+            nlqsat&    s;
+            arith_util a;
+            bool       m_has_divs;
+        public:
+            is_pure_proc(nlqsat& s): s(s), a(s.m), m_has_divs(false) {}
+
+            void operator()(::var * n) {
+                if (!a.is_real(n) && !s.m.is_bool(n)) {
+                    throw tactic_exception("not NRA");
+                }
+            }
+            void operator()(app * n) { 
+                if (n->get_family_id() == s.m.get_basic_family_id()) {
+                    return;
+                }
+                if (is_uninterp_const(n) && (a.is_real(n) || s.m.is_bool(n))) {
+                    return;
+                }
+                if (a.is_mul(n) || a.is_add(n) || a.is_sub(n) || a.is_uminus(n) || a.is_numeral(n) ||
+                    a.is_le(n) || a.is_ge(n) || a.is_lt(n) || a.is_gt(n)) {
+                    return;
+                }
+                expr* n1, *n2;
+                if (a.is_div(n, n1, n2) && a.is_numeral(n2)) {
+                    return;
+                }
+                rational r;
+                if (a.is_power(n, n1, n2) && a.is_numeral(n2, r) && r.is_unsigned()) {
+                    return;
+                }
+                if (a.is_div(n, n1, n2) && is_ground(n1) && is_ground(n2) && s.m_mode == qsat_t) {
+                    m_has_divs = true;
+                    return;
+                }
+                TRACE("qe", tout << "not NRA: " << mk_pp(n, s.m) << "\n";);
+                throw tactic_exception("not NRA");
+            }
+            void operator()(quantifier * n) {}
+
+            bool has_divs() const { return m_has_divs; }
+        };
+
+        void purify(expr_ref& fml) {
+            is_pure_proc  is_pure(*this);
+            {
+                expr_fast_mark1 visited;
+                quick_for_each_expr(is_pure, visited, fml);
+            }
+            if (is_pure.has_divs()) {
+                arith_util arith(m);
+                div_rewriter_star rw(*this);
+                proof_ref pr(m);
+                rw(fml, fml, pr);
+                vector<div> const& divs = rw.divs();
+                expr_ref_vector axioms(m);
+                for (unsigned i = 0; i < divs.size(); ++i) {
+                    axioms.push_back(
+                        m.mk_or(m.mk_eq(divs[i].den, arith.mk_numeral(rational(0), false)), 
+                                m.mk_eq(divs[i].num, arith.mk_mul(divs[i].den, divs[i].name))));                    
+                    for (unsigned j = i + 1; j < divs.size(); ++j) {
+                        axioms.push_back(m.mk_or(m.mk_not(m.mk_eq(divs[i].den, divs[j].den)),
+                                                 m.mk_not(m.mk_eq(divs[i].num, divs[j].num)), 
+                                                 m.mk_eq(divs[i].name, divs[j].name)));
+                    }
+                }
+                axioms.push_back(fml);
+                fml = mk_and(axioms);
+            }
+        }
+
         void reset() {
             //m_solver.reset();
             m_asms.reset();
@@ -444,6 +558,7 @@ namespace qe {
             m_st.reset();        
             m_solver.collect_statistics(m_st);
             m_free_vars.reset();
+            m_aux_vars.reset();
             m_answer.reset();
             m_answer_simplify.reset();
             m_assumptions.reset();
@@ -488,10 +603,11 @@ namespace qe {
             app_ref_vector vars(m);
             bool is_forall = false;   
             pred_abs abs(m);
+            purify(fml);
             abs.get_free_vars(fml, vars);
             insert_set(m_free_vars, vars);
             qvars.push_back(vars); 
-            vars.reset();    
+            vars.reset();  
             if (m_mode == elim_t) {
                 is_forall = true;
                 hoist.pull_quantifier(is_forall, fml, vars);
@@ -607,7 +723,7 @@ namespace qe {
             for (; it != end; ++it) {
                 nlsat::var x = it->m_value;
                 expr * t = it->m_key;
-                if (!is_uninterp_const(t) || !m_free_vars.contains(t))
+                if (!is_uninterp_const(t) || !m_free_vars.contains(t) || m_aux_vars.contains(t))
                     continue;
                 expr * v;
                 try {
@@ -626,7 +742,7 @@ namespace qe {
             for (; it != end; ++it) {
                 expr * a = it->m_key;
                 nlsat::bool_var b = it->m_value;
-                if (a == 0 || !is_uninterp_const(a) || b == m_is_true.var() || !m_free_vars.contains(a))
+                if (a == 0 || !is_uninterp_const(a) || b == m_is_true.var() || !m_free_vars.contains(a) || m_aux_vars.contains(a))
                     continue;
                 lbool val = m_bmodel0.get(b, l_undef);
                 if (val == l_undef)

src/qe/qe_lite.cpp

@@ -21,7 +21,6 @@ Revision History:
 #include "expr_abstract.h"
 #include "used_vars.h"
 #include "occurs.h"
-#include "for_each_expr.h"
 #include "rewriter_def.h"
 #include "ast_pp.h"
 #include "ast_ll_pp.h"
@@ -492,6 +491,10 @@ namespace eq {
                     m_new_args.push_back(args[i]);
                 }
             }
+            if (m_new_args.size() == num_args) {
+                r = q;
+                return;
+            }
             
             expr_ref t(m);
             if (q->is_forall()) {
@@ -772,7 +775,7 @@ namespace eq {
                 proof_ref curr_pr(m);
                 q  = to_quantifier(r);
                 reduce_quantifier1(q, r, curr_pr);
-                if (m.proofs_enabled()) {
+                if (m.proofs_enabled() && r != q) {
                     pr = m.mk_transitivity(pr, curr_pr);
                 }
             } while (q != r && is_quantifier(r));
@@ -2298,7 +2301,7 @@ public:
             }
             m_imp(indices, true, result);          
             if (is_forall(q)) {
-                result = m.mk_not(result);
+                result = push_not(result);
             }
             result = m.update_quantifier(
                 q, 
@@ -2423,9 +2426,6 @@ public:
         TRACE("qe_lite", for (unsigned i = 0; i < fmls.size(); ++i) {
                 tout << mk_pp(fmls[i].get(), m) << "\n";
             });
-        IF_VERBOSE(3, for (unsigned i = 0; i < fmls.size(); ++i) {
-                verbose_stream() << mk_pp(fmls[i].get(), m) << "\n";
-            });
         is_variable_test is_var(index_set, index_of_bound);
         m_der.set_is_variable_proc(is_var);
         m_fm.set_is_variable_proc(is_var);
@@ -2480,6 +2480,41 @@ class qe_lite_tactic : public tactic {
             cooperate("qe-lite");
         }
         
+        void debug_diff(expr* a, expr* b) {
+            ptr_vector<expr> as, bs;
+            as.push_back(a);
+            bs.push_back(b);
+            expr* a1, *a2, *b1, *b2;
+            while (!as.empty()) {
+                a = as.back();
+                b = bs.back();
+                as.pop_back();
+                bs.pop_back();
+                if (a == b) {
+                    continue;
+                }
+                else if (is_forall(a) && is_forall(b)) {
+                    as.push_back(to_quantifier(a)->get_expr());
+                    bs.push_back(to_quantifier(b)->get_expr());
+                }
+                else if (m.is_and(a, a1, a2) && m.is_and(b, b1, b2)) {
+                    as.push_back(a1);
+                    as.push_back(a2);
+                    bs.push_back(b1);
+                    bs.push_back(b2);
+                }
+                else if (m.is_eq(a, a1, a2) && m.is_eq(b, b1, b2)) {
+                    as.push_back(a1);
+                    as.push_back(a2);
+                    bs.push_back(b1);
+                    bs.push_back(b2);
+                }
+                else {
+                    TRACE("qe", tout << mk_pp(a, m) << " != " << mk_pp(b, m) << "\n";);
+                }
+            }
+        }
+
         void operator()(goal_ref const & g, 
                         goal_ref_buffer & result, 
                         model_converter_ref & mc, 
@@ -2511,7 +2546,10 @@ class qe_lite_tactic : public tactic {
                         new_pr = g->pr(i);
                     }
                 }
-                g->update(i, new_f, new_pr, g->dep(i));                
+                if (f != new_f) {
+                    TRACE("qe", tout << mk_pp(f, m) << "\n" << new_f << "\n";);
+                    g->update(i, new_f, new_pr, g->dep(i));                
+                }
             }
             g->inc_depth();
             result.push_back(g.get());

src/qe/qsat.cpp

@@ -499,15 +499,7 @@ namespace qe {
             }
         }
     }
-    
+
-    class qsat : public tactic {
-        
-        struct stats {
-            unsigned m_num_rounds;        
-            stats() { reset(); }
-            void reset() { memset(this, 0, sizeof(*this)); }
-        };
-        
         class kernel {
             ast_manager& m;
             smt_params   m_smtp;
@@ -542,6 +534,15 @@ namespace qe {
                       );
             }
         };
+    
+    class qsat : public tactic {
+        
+        struct stats {
+            unsigned m_num_rounds;        
+            stats() { reset(); }
+            void reset() { memset(this, 0, sizeof(*this)); }
+        };
+        
         
         ast_manager&               m;
         params_ref                 m_params;
@@ -1155,10 +1156,67 @@ namespace qe {
         
         tactic * translate(ast_manager & m) {
             return alloc(qsat, m, m_params, m_qelim, m_force_elim);
-        }
+        }               
-        
-        
     };
+
+   
+
+
+    struct min_max_opt::imp {
+        ast_manager&    m;
+        expr_ref_vector m_fmls;
+        pred_abs        m_pred_abs;
+        qe::mbp         m_mbp;
+        kernel          m_kernel;
+
+        imp(ast_manager& m): 
+            m(m), 
+            m_fmls(m), 
+            m_pred_abs(m), 
+            m_mbp(m),
+            m_kernel(m) {}
+
+        void add(expr* e) {
+            m_fmls.push_back(e);
+        }
+
+        lbool check(svector<bool> const& is_max, func_decl_ref_vector const& vars, app* t) {
+            // Assume this is the only call to check.
+            expr_ref_vector defs(m);
+            expr_ref fml = mk_and(m_fmls);
+            m_pred_abs.abstract_atoms(fml, defs);
+            fml = m_pred_abs.mk_abstract(fml);
+            m_kernel.assert_expr(mk_and(defs));
+            m_kernel.assert_expr(fml);
+            // TBD
+            
+            return l_undef;
+        }
+    };
+
+    min_max_opt::min_max_opt(ast_manager& m) {
+        m_imp = alloc(imp, m);
+    }
+
+    min_max_opt::~min_max_opt() {
+        dealloc(m_imp);
+    }
+
+    void min_max_opt::add(expr* e) {
+        m_imp->add(e);
+    }
+
+    void min_max_opt::add(expr_ref_vector const& fmls) {
+        for (unsigned i = 0; i < fmls.size(); ++i) {
+            add(fmls[i]);
+        }
+    }
+
+    lbool min_max_opt::check(svector<bool> const& is_max, func_decl_ref_vector const& vars, app* t) {
+        return m_imp->check(is_max, vars, t);
+    }
+
+
     
 };
 

src/qe/qsat.h

@@ -113,6 +113,17 @@ namespace qe {
         void collect_statistics(statistics& st) const;
     };
 
+    class min_max_opt {
+        struct imp;
+        imp* m_imp;
+    public:
+        min_max_opt(ast_manager& m);
+        ~min_max_opt();
+        void add(expr* e);
+        void add(expr_ref_vector const& fmls);
+        lbool check(svector<bool> const& is_max, func_decl_ref_vector const& vars, app* t);
+    };
+
 
 }
 

src/smt/smt_context_inv.cpp

@@ -420,14 +420,14 @@ namespace smt {
             case l_undef:
                 break;
             case l_true:
-                m_proto_model->eval(n, res, false);
+                if (!m_proto_model->eval(n, res, false)) return true;
                 CTRACE("mbqi_bug", !m.is_true(res), tout << n << " evaluates to " << res << "\n";); 
                 if (m.is_false(res)) {
                     return false;
                 }
                 break;
             case l_false:
-                m_proto_model->eval(n, res, false);
+                if (!m_proto_model->eval(n, res, false)) return true;
                 CTRACE("mbqi_bug", !m.is_false(res), tout << n << " evaluates to " << res << "\n";); 
                 if (m.is_true(res)) {
                     return false;

src/smt/smt_model_finder.cpp

@@ -149,6 +149,7 @@ namespace smt {
                     SASSERT(!contains_model_value(t));
                     unsigned gen = (*it).m_value;
                     expr * t_val = ev.eval(t, true);
+                    if (!t_val) break;
                     TRACE("model_finder", tout << mk_pp(t, m_manager) << " " << mk_pp(t_val, m_manager) << "\n";);
 
                     expr * old_t = 0;
@@ -828,7 +829,7 @@ namespace smt {
                 for (; it != end; ++it) {
                     expr *     t = (*it).m_key;
                     expr * t_val = eval(t, true);
-                    if (!already_found.contains(t_val)) {
+                    if (t_val && !already_found.contains(t_val)) {
                         values.push_back(t_val);
                         already_found.insert(t_val);
                     }
@@ -891,6 +892,7 @@ namespace smt {
                 add_mono_exceptions(n);
                 ptr_buffer<expr> values;
                 get_instantiation_set_values(n, values);
+                if (values.empty()) return;
                 sort_values(n, values);
                 sort * s = n->get_sort();
                 arith_simplifier_plugin * as = get_arith_simp();

src/tactic/smtlogics/nra_tactic.cpp

@@ -35,22 +35,17 @@ tactic * mk_nra_tactic(ast_manager & m, params_ref const& p) {
     p2.set_uint("seed", 13);
     p2.set_bool("factor", false);
 
-    return and_then(mk_simplify_tactic(m, p),
+    return and_then(
-                    mk_nnf_tactic(m, p),
+        mk_simplify_tactic(m, p),
-                    mk_propagate_values_tactic(m, p),
+        mk_propagate_values_tactic(m, p),
-                    //mk_qe_lite_tactic(m), 
+        mk_qe_lite_tactic(m),
-                    mk_qe_tactic(m, p),
+        cond(mk_is_qfnra_probe(),
-                    cond(mk_is_qfnra_probe(),
+             or_else(try_for(mk_qfnra_nlsat_tactic(m, p), 5000),
-                         or_else(try_for(mk_qfnra_nlsat_tactic(m, p), 5000),
+                     try_for(mk_qfnra_nlsat_tactic(m, p1), 10000),
-                                 try_for(mk_qfnra_nlsat_tactic(m, p1), 10000),
+                     mk_qfnra_nlsat_tactic(m, p2)),
-                                 mk_qfnra_nlsat_tactic(m, p2)),
+             or_else(mk_nlqsat_tactic(m, p),
-#if 0
+                     mk_smt_tactic(p))
-                         or_else(mk_nlqsat_tactic(m, p),
+             ));
-                                 mk_smt_tactic(p))
-#else
-                         mk_smt_tactic(p)
-#endif
-                         ));
 }
 
 

src/tactic/smtlogics/quant_tactics.cpp

@@ -22,8 +22,6 @@ Revision History:
 #include"solve_eqs_tactic.h"
 #include"elim_uncnstr_tactic.h"
 #include"qe_tactic.h"
-#include"qe_sat_tactic.h"
-#include"qe_lite.h"
 #include"qsat.h"
 #include"nlqsat.h"
 #include"ctx_simplify_tactic.h"
@@ -54,7 +52,6 @@ static tactic * mk_quant_preprocessor(ast_manager & m, bool disable_gaussian = f
                     using_params(mk_simplify_tactic(m), pull_ite_p),
                     solve_eqs,
                     mk_elim_uncnstr_tactic(m),
-                    mk_qe_lite_tactic(m),
                     mk_simplify_tactic(m));    
 }