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

src/api/api_solver.cpp

@@ -355,6 +355,10 @@ extern "C" {
         init_solver(c, s);
         Z3_stats_ref * st = alloc(Z3_stats_ref);
         to_solver_ref(s)->collect_statistics(st->m_stats);
+        unsigned long long max_mem = memory::get_max_used_memory();
+        unsigned long long mem = memory::get_allocation_size();
+        st->m_stats.update("max memory", static_cast<double>(max_mem)/(1024.0*1024.0));
+        st->m_stats.update("memory", static_cast<double>(mem)/(1024.0*1024.0));
         mk_c(c)->save_object(st);
         Z3_stats r = of_stats(st);
         RETURN_Z3(r);

src/api/python/z3.py

@@ -5617,7 +5617,7 @@ class Statistics:
         sat
         >>> st = s.statistics()
         >>> len(st)
-        2
+        4
         """
         return int(Z3_stats_size(self.ctx.ref(), self.stats))
 
@@ -5631,7 +5631,7 @@ class Statistics:
         sat
         >>> st = s.statistics()
         >>> len(st)
-        2
+        4
         >>> st[0]
         ('nlsat propagations', 2)
         >>> st[1]
@@ -5655,7 +5655,7 @@ class Statistics:
         sat
         >>> st = s.statistics()
         >>> st.keys()
-        ['nlsat propagations', 'nlsat stages']
+        ['nlsat propagations', 'nlsat stages', 'max memory', 'memory']
         """
         return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))]
 
@@ -5692,7 +5692,7 @@ class Statistics:
         sat
         >>> st = s.statistics() 
         >>> st.keys()
-        ['nlsat propagations', 'nlsat stages']
+        ['nlsat propagations', 'nlsat stages', 'max memory', 'memory']
         >>> st.nlsat_propagations
         2
         >>> st.nlsat_stages

src/cmd_context/cmd_context.cpp

@@ -40,6 +40,7 @@ Notes:
 #include"for_each_expr.h"
 #include"scoped_timer.h"
 #include"interpolant_cmds.h"
+#include"model_smt2_pp.h"
 
 func_decls::func_decls(ast_manager & m, func_decl * f):
     m_decls(TAG(func_decl*, f, 0)) {
@@ -1404,6 +1405,15 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
                 was_pareto = true;
                 get_opt()->display_assignment(regular_stream());
                 regular_stream() << "\n";
+                if (get_opt()->print_model()) {
+                    model_ref mdl;
+                    get_opt()->get_model(mdl);
+                    if (mdl) {
+                        regular_stream() << "(model " << std::endl;
+                        model_smt2_pp(regular_stream(), *this, *(mdl.get()), 2);
+                        regular_stream() << ")" << std::endl;                    
+                    }
+                }
                 r = get_opt()->optimize();
             }
         }

src/cmd_context/cmd_context.h

@@ -124,6 +124,7 @@ public:
     virtual void display_assignment(std::ostream& out) = 0;
     virtual bool is_pareto() = 0;
     virtual void set_logic(symbol const& s) = 0;
+    virtual bool print_model() const = 0;
 };
 
 class cmd_context : public progress_callback, public tactic_manager, public ast_printer_context {

src/muz/base/dl_context.cpp

@@ -945,6 +945,10 @@ namespace datalog {
         if (m_engine) {
             m_engine->collect_statistics(st);
         }
+        unsigned long long max_mem = memory::get_max_used_memory();
+        unsigned long long mem = memory::get_allocation_size();
+        st.update("max memory", static_cast<double>(max_mem)/(1024.0*1024.0));
+        st.update("memory", static_cast<double>(mem)/(1024.0*1024.0));        
     }
 
 

src/opt/opt_cmds.cpp

@@ -323,12 +323,8 @@ private:
 
     void display_statistics(cmd_context& ctx) {
         statistics stats;
-        unsigned long long max_mem = memory::get_max_used_memory();
-        unsigned long long mem = memory::get_allocation_size();
-        stats.update("time", ctx.get_seconds());
-        stats.update("memory", static_cast<double>(mem)/static_cast<double>(1024*1024));
-        stats.update("max memory", static_cast<double>(max_mem)/static_cast<double>(1024*1024));
         get_opt(ctx).collect_statistics(stats);
+        stats.update("time", ctx.get_seconds());
         stats.display_smt2(ctx.regular_stream());        
     }
 };

src/opt/opt_context.cpp

@@ -254,6 +254,12 @@ namespace opt {
         }
     }
 
+
+    bool context::print_model() const {
+        opt_params optp(m_params);
+        return optp.print_model();
+    }
+
     void context::get_base_model(model_ref& mdl) {
         mdl = m_model;
     }
@@ -1179,6 +1185,10 @@ namespace opt {
         for (; it != end; ++it) {
             it->m_value->collect_statistics(stats);
         }        
+        unsigned long long max_mem = memory::get_max_used_memory();
+        unsigned long long mem = memory::get_allocation_size();
+        stats.update("memory", static_cast<double>(mem)/static_cast<double>(1024*1024));
+        stats.update("max memory", static_cast<double>(max_mem)/static_cast<double>(1024*1024));
     }
 
     void context::collect_param_descrs(param_descrs & r) {

src/opt/opt_context.h

@@ -180,6 +180,7 @@ namespace opt {
         virtual void cancel() { set_cancel(true); }
         virtual void set_hard_constraints(ptr_vector<expr> & hard);
         virtual lbool optimize();
+        virtual bool print_model() const;
         virtual void get_model(model_ref& _m);
         virtual void set_model(model_ref& _m);
         virtual void fix_model(model_ref& _m);

src/qe/qe_mbp.h

@@ -0,0 +1,48 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    qe_mbp.h
+
+Abstract:
+
+    Model-based projection utilities
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2015-5-28
+
+Revision History:
+
+
+--*/
+
+#ifndef __QE_MBP_H__
+#define __QE_MBP_H__
+
+#include "ast.h"
+#include "params.h"
+
+namespace qe {
+    class mbp {
+        class impl;
+        impl * m_impl;
+    public:
+        mbp(ast_manager& m);
+        
+        ~mbp();
+        
+        /**
+           \brief
+           Apply model-based qe on constants provided as vector of variables. 
+           Return the updated formula and updated set of variables that were not eliminated.
+           
+        */
+        void operator()(app_ref_vector& vars, model_ref& mdl, expr_ref& fml);
+        
+        void set_cancel(bool f);
+    };
+}
+
+#endif 

src/qe/qsat.cpp

@@ -0,0 +1,281 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    qsat.cpp
+
+Abstract:
+
+    Quantifier Satisfiability Solver.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2015-5-28
+
+Revision History:
+
+
+--*/
+
+#include "qsat.h"
+#include "smt_kernel.h"
+#include "qe_mbp.h"
+#include "smt_params.h"
+#include "ast_util.h"
+
+using namespace qe;
+
+struct qdef_t {
+    expr_ref        m_pred;
+    expr_ref        m_expr;
+    expr_ref_vector m_vars;
+    bool            m_is_forall;
+    qdef_t(expr_ref& p, expr_ref& e, expr_ref_vector const& vars, bool is_forall):
+        m_pred(p), 
+        m_expr(e),
+        m_vars(vars),
+        m_is_forall(is_forall) {}
+};
+
+typedef vector<qdef_t> qdefs_t;
+
+struct pdef_t {
+    expr_ref  m_pred;
+    expr_ref  m_atom;
+    pdef_t(expr_ref& p, expr* a):
+        m_pred(p),
+        m_atom(a, p.get_manager())
+    {}
+};
+
+class qsat::impl {
+    ast_manager&      m;
+    qe::mbp           mbp;
+    smt_params        m_smtp;
+    smt::kernel       m_kernel;
+    expr_ref          m_fml_pred;  // predicate that encodes top-level formula
+    expr_ref_vector   m_atoms;     // predicates that encode atomic subformulas
+
+
+    lbool check_sat() {        
+        // TBD main procedure goes here.
+        return l_undef;
+    }
+
+    /**
+       \brief replace quantified sub-formulas by a predicate, introduce definitions for the predicate.
+     */
+    void remove_quantifiers(expr_ref_vector& fmls, qdefs_t& defs) {
+        
+    }
+
+    /** 
+        \brief create propositional abstration of formula by replacing atomic sub-formulas by fresh 
+        propositional variables, and adding definitions for each propositional formula on the side.
+        Assumption is that the formula is quantifier-free.
+    */
+    void mk_abstract(expr_ref& fml, vector<pdef_t>& pdefs) {
+        expr_ref_vector todo(m), trail(m);
+        obj_map<expr,expr*> cache;
+        ptr_vector<expr> args;
+        expr_ref r(m);
+        todo.push_back(fml);
+        while (!todo.empty()) {
+            expr* e = todo.back();
+            if (cache.contains(e)) {
+                todo.pop_back();
+                continue;
+            }
+            SASSERT(is_app(e));
+            app* a = to_app(e);
+            if (a->get_family_id() == m.get_basic_family_id()) {
+                unsigned sz = a->get_num_args();
+                args.reset();
+                for (unsigned i = 0; i < sz; ++i) {
+                    expr* f = a->get_arg(i);
+                    if (cache.find(f, f)) {
+                        args.push_back(f);
+                    }
+                    else {
+                        todo.push_back(f);
+                    }
+                } 
+                if (args.size() == sz) {
+                    r = m.mk_app(a->get_decl(), sz, args.c_ptr());
+                    cache.insert(e, r);
+                    trail.push_back(r);
+                    todo.pop_back();
+                }
+            }
+            else if (is_uninterp_const(a)) {
+                cache.insert(e, e);
+            }
+            else {
+                // TBD: nested Booleans.    
+
+                r = m.mk_fresh_const("p",m.mk_bool_sort());
+                trail.push_back(r);
+                cache.insert(e, r);
+                pdefs.push_back(pdef_t(r, e));
+            }
+        }
+        fml = cache.find(fml);
+    }
+
+    /** 
+        \brief use dual propagation to minimize model.
+    */
+    bool minimize_assignment(expr_ref_vector& assignment, expr* not_fml) {        
+        bool result = false;
+        assignment.push_back(not_fml);
+        lbool res = m_kernel.check(assignment.size(), assignment.c_ptr());
+        switch (res) {
+        case l_true:
+            UNREACHABLE();
+            break;
+        case l_undef:
+            break;
+        case l_false: 
+            result = true;
+            get_core(assignment, not_fml);
+            break;
+        }
+        return result;
+    }
+
+    lbool check_sat(expr_ref_vector& assignment, expr* fml) {
+        assignment.push_back(fml);
+        lbool res = m_kernel.check(assignment.size(), assignment.c_ptr());
+        switch (res) {
+        case l_true: {
+            model_ref mdl;
+            expr_ref tmp(m);
+            assignment.reset();
+            m_kernel.get_model(mdl);
+            for (unsigned i = 0; i < m_atoms.size(); ++i) {
+                expr* p = m_atoms[i].get();
+                if (mdl->eval(p, tmp)) {
+                    if (m.is_true(tmp)) {
+                        assignment.push_back(p);
+                    }
+                    else if (m.is_false(tmp)) {
+                        assignment.push_back(m.mk_not(p));
+                    }
+                }                
+            }
+            expr_ref not_fml = mk_not(fml);
+            if (!minimize_assignment(assignment, not_fml)) {
+                res = l_undef;
+            }
+            break;
+        }
+        case l_undef:            
+            break;
+        case l_false:
+            get_core(assignment, fml);
+            break;
+        }
+        return res;
+    }
+
+    void get_core(expr_ref_vector& core, expr* exclude) {
+        unsigned sz = m_kernel.get_unsat_core_size();
+        core.reset();
+        for (unsigned i = 0; i < sz; ++i) {
+            expr* e = m_kernel.get_unsat_core_expr(i);
+            if (e != exclude) {
+                core.push_back(e);
+            } 
+        }        
+    }
+
+    expr_ref mk_not(expr* e) {
+        return expr_ref(::mk_not(m, e), m);
+    }
+
+public:
+    impl(ast_manager& m):
+        m(m),
+        mbp(m),
+        m_kernel(m, m_smtp),
+        m_fml_pred(m), 
+        m_atoms(m) {}
+    
+    void updt_params(params_ref const & p) {
+    }
+
+    void collect_param_descrs(param_descrs & r) {
+    }
+
+    void operator()(/* in */  goal_ref const & in, 
+                    /* out */ goal_ref_buffer & result, 
+                    /* out */ model_converter_ref & mc, 
+                    /* out */ proof_converter_ref & pc,
+                    /* out */ expr_dependency_ref & core) {
+
+    }
+
+    void collect_statistics(statistics & st) const {
+
+    }
+    void reset_statistics() {
+    }
+
+    void cleanup() {
+    }
+
+    void set_logic(symbol const & l) {
+    }
+
+    void set_progress_callback(progress_callback * callback) {
+    }
+
+    tactic * translate(ast_manager & m) {
+        return 0;
+    }
+
+};
+
+qsat::qsat(ast_manager& m) {
+    m_impl = alloc(impl, m);
+}
+
+qsat::~qsat() {
+    dealloc(m_impl);
+}
+
+void qsat::updt_params(params_ref const & p) {
+    m_impl->updt_params(p);
+}
+void qsat::collect_param_descrs(param_descrs & r) {
+    m_impl->collect_param_descrs(r);
+}
+void qsat::operator()(/* in */  goal_ref const & in, 
+                      /* out */ goal_ref_buffer & result, 
+                      /* out */ model_converter_ref & mc, 
+                      /* out */ proof_converter_ref & pc,
+                      /* out */ expr_dependency_ref & core) {
+    (*m_impl)(in, result, mc, pc, core);
+}
+
+void qsat::collect_statistics(statistics & st) const {
+    m_impl->collect_statistics(st);
+}
+void qsat::reset_statistics() {
+    m_impl->reset_statistics();
+}
+void qsat::cleanup() {
+    m_impl->cleanup();
+}
+void qsat::set_logic(symbol const & l) {
+    m_impl->set_logic(l);
+}
+void qsat::set_progress_callback(progress_callback * callback) {
+    m_impl->set_progress_callback(callback);
+}
+tactic * qsat::translate(ast_manager & m) {
+    return m_impl->translate(m);
+}
+
+

src/qe/qsat.h

@@ -0,0 +1,52 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    qsat.h
+
+Abstract:
+
+    Quantifier Satisfiability Solver.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2015-5-28
+
+Revision History:
+
+
+--*/
+
+#ifndef __QE_QSAT_H__
+#define __QE_QSAT_H__
+
+#include "tactic.h"
+
+namespace qe {
+    class qsat : public tactic {
+        class impl;
+        impl * m_impl;
+    public:
+        qsat(ast_manager& m);
+        ~qsat();
+        
+        virtual void updt_params(params_ref const & p);
+        virtual void collect_param_descrs(param_descrs & r);
+        virtual void operator()(/* in */  goal_ref const & in, 
+                                /* out */ goal_ref_buffer & result, 
+                                /* out */ model_converter_ref & mc, 
+                                /* out */ proof_converter_ref & pc,
+                                /* out */ expr_dependency_ref & core);
+        
+        virtual void collect_statistics(statistics & st) const;
+        virtual void reset_statistics();
+        virtual void cleanup() = 0;
+        virtual void set_logic(symbol const & l);
+        virtual void set_progress_callback(progress_callback * callback);
+        virtual tactic * translate(ast_manager & m);
+        
+    };
+};
+
+#endif 

src/smt/theory_array_full.cpp

@@ -208,6 +208,8 @@ namespace smt {
         theory_array::reset_eh();
         std::for_each(m_var_data_full.begin(), m_var_data_full.end(), delete_proc<var_data_full>());
         m_var_data_full.reset();
+        m_eqs.reset();
+        m_eqsv.reset();
     }
 
     void theory_array_full::display_var(std::ostream & out, theory_var v) const {
@@ -223,7 +225,6 @@ namespace smt {
     }
     
     theory_var theory_array_full::mk_var(enode * n) {
-
         theory_var r = theory_array::mk_var(n);
         SASSERT(r == static_cast<int>(m_var_data_full.size()));
         m_var_data_full.push_back(alloc(var_data_full));
@@ -512,7 +513,7 @@ namespace smt {
         
         TRACE("array_map_bug",
               tout << "select-map axiom\n" << mk_ismt2_pp(sel1, m) << "\n=\n" << mk_ismt2_pp(sel2,m) << "\n";);
-        
+
         return try_assign_eq(sel1, sel2);
     }
 
@@ -760,37 +761,36 @@ namespace smt {
                     r = FC_CONTINUE;
             }
         }
+        while (!m_eqsv.empty()) {
+            literal eq = m_eqsv.back();
+            m_eqsv.pop_back();
+            get_context().mark_as_relevant(eq);            
+            assert_axiom(eq);
+            r = FC_CONTINUE;
+        }
         if (r == FC_DONE && m_found_unsupported_op)
             r = FC_GIVEUP;
         return r;
     }
 
+
     bool theory_array_full::try_assign_eq(expr* v1, expr* v2) {
-        context& ctx = get_context();
-        enode* n1 = ctx.get_enode(v1);
-        enode* n2 = ctx.get_enode(v2);
-        if (n1->get_root() == n2->get_root()) {
-            return false;
-        }
         TRACE("array", 
               tout << mk_bounded_pp(v1, get_manager()) << "\n==\n" 
               << mk_bounded_pp(v2, get_manager()) << "\n";);
-
-#if 0
-        if (m.proofs_enabled()) {
-#endif
-            literal eq(mk_eq(v1,v2,true));
-            ctx.mark_as_relevant(eq);
-            assert_axiom(eq);
-#if 0
+        context& ctx = get_context();
+        if (m_eqs.contains(v1, v2)) {
+            return false;
         }
         else {
-            ctx.mark_as_relevant(n1);
-            ctx.mark_as_relevant(n2);
-            ctx.assign_eq(n1, n2, eq_justification::mk_axiom());
+            m_eqs.insert(v1, v2, true);
+            literal eq(mk_eq(v1, v2, true));
+            get_context().mark_as_relevant(eq);            
+            assert_axiom(eq);
+
+            // m_eqsv.push_back(eq);
+            return true;
         }
-#endif
-        return true;
     }
 
     void theory_array_full::pop_scope_eh(unsigned num_scopes) {
@@ -798,6 +798,8 @@ namespace smt {
         theory_array::pop_scope_eh(num_scopes);
         std::for_each(m_var_data_full.begin() + num_old_vars, m_var_data_full.end(), delete_proc<var_data_full>());
         m_var_data_full.shrink(num_old_vars);        
+        m_eqs.reset();
+        m_eqsv.reset();
     }
 
     void theory_array_full::collect_statistics(::statistics & st) const {

src/smt/theory_array_full.h

@@ -38,12 +38,12 @@ namespace smt {
 
         ast2ast_trailmap<sort,app> m_sort2epsilon;
         simplifier*                m_simp;
+        obj_pair_map<expr,expr,bool> m_eqs;
+        svector<literal>             m_eqsv;
 
     protected:
 
-#if 0
-        virtual final_check_status final_check_eh();
-#endif
+        //virtual final_check_status final_check_eh();
         virtual void reset_eh();
 
         virtual void set_prop_upward(theory_var v);
@@ -84,6 +84,7 @@ namespace smt {
 
 
         bool try_assign_eq(expr* n1, expr* n2);
+        void assign_eqs();
 
         
     public: