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

src/opt/opt_solver.cpp

@@ -42,7 +42,7 @@ namespace opt {
         m_context(mgr, m_params),
         m(mgr),
         m_fm(fm),
-        m_objective_sorts(m),
+        m_objective_terms(m),
         m_dump_benchmarks(false),
         m_first(true) {
         m_params.updt_params(p);
@@ -213,11 +213,13 @@ namespace opt {
         }
         else {
             SASSERT(has_shared);
-            decrement_value(i, val);            
+            decrement_value(i, val);
         }
         m_objective_values[i] = val;
-        TRACE("opt", { tout << val << "\n"; 
+        TRACE("opt", { 
-                tout << blocker << "\n";
+                tout << "objective:     " << mk_pp(m_objective_terms[i].get(), m) << "\n";
+                tout << "maximal value: " << val << "\n"; 
+                tout << "new condition: " << blocker << "\n";
                 model_smt2_pp(tout << "update model:\n", m, *m_models[i], 0); });
     }
 
@@ -240,7 +242,7 @@ namespace opt {
         TRACE("opt", tout << is_sat << "\n";);
         if (is_sat != l_true) {
             // cop-out approximation
-            if (arith_util(m).is_real(m_objective_sorts[i].get())) {
+            if (arith_util(m).is_real(m_objective_terms[i].get())) {
                 val -= inf_eps(inf_rational(rational(0), true));
             }
             else {
@@ -304,7 +306,7 @@ namespace opt {
         smt::theory_var v = get_optimizer().add_objective(term);
         m_objective_vars.push_back(v);
         m_objective_values.push_back(inf_eps(rational(-1), inf_rational()));
-        m_objective_sorts.push_back(m.get_sort(term));
+        m_objective_terms.push_back(term);
         m_valid_objectives.push_back(true);
         m_models.push_back(0);
         return v;
@@ -363,7 +365,7 @@ namespace opt {
     void opt_solver::reset_objectives() {
         m_objective_vars.reset();
         m_objective_values.reset();
-        m_objective_sorts.reset();
+        m_objective_terms.reset();
         m_valid_objectives.reset();
     }
 

src/opt/opt_solver.h

@@ -76,7 +76,7 @@ namespace opt {
         svector<smt::theory_var>  m_objective_vars;
         vector<inf_eps>     m_objective_values;
         sref_vector<model>  m_models;
-        sort_ref_vector     m_objective_sorts;
+        expr_ref_vector     m_objective_terms;
         svector<bool>       m_valid_objectives;
         bool                m_dump_benchmarks;
         static unsigned     m_dump_count;

src/qe/qe_mbp.h

@@ -1,48 +0,0 @@
-/*++
-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

@@ -1,281 +0,0 @@
-/*++
-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

@@ -1,52 +0,0 @@
-/*++
-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/tactic/arith/card2bv_tactic.cpp

@@ -488,7 +488,7 @@ public:
         unsigned size = g->size();
         expr_ref new_f1(m), new_f2(m);
         proof_ref new_pr1(m), new_pr2(m);
-        for (unsigned idx = 0; idx < size; idx++) {
+        for (unsigned idx = 0; !g->inconsistent() && idx < g->size(); idx++) {
             m_rw1(g->form(idx), new_f1, new_pr1);
             TRACE("card2bv", tout << "Rewriting " << mk_ismt2_pp(new_f1.get(), m) << std::endl;);
             m_rw2.rewrite(new_f1, new_f2);