fast path for antecedent extraction in smt_context

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

contrib/cmake/src/smt/CMakeLists.txt

@@ -18,6 +18,7 @@ z3_add_component(smt
     smt_checker.cpp
     smt_clause.cpp
     smt_conflict_resolution.cpp
+    smt_consequences.cpp
     smt_context.cpp
     smt_context_inv.cpp
     smt_context_pp.cpp

src/smt/smt_consequences.cpp

@@ -0,0 +1,189 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    smt_consequences.cpp
+
+Abstract:
+
+    Tuned consequence finding for smt_context.
+
+Author:
+
+    nbjorner 2016-07-28.
+
+Revision History:
+
+--*/
+#include "smt_context.h"
+#include "ast_util.h"
+
+namespace smt {
+
+    expr_ref context::antecedent2fml(uint_set const& vars) {
+        expr_ref_vector premises(m_manager);
+        uint_set::iterator it = vars.begin(), end = vars.end();
+        for (; it != end; ++it) {
+            premises.push_back(bool_var2expr(*it));
+        }
+        return mk_and(premises);
+    }
+
+    void context::extract_fixed_consequences(unsigned start, obj_map<expr, expr*>& vars, obj_hashtable<expr> const& assumptions, expr_ref_vector& conseq) {
+        ast_manager& m = m_manager;
+        pop_to_search_lvl();
+        literal_vector const& lits = assigned_literals();
+        unsigned sz = lits.size();
+        expr* e1, *e2;       
+        expr_ref fml(m);
+        for (unsigned i = start; i < sz; ++i) {            
+            literal lit = lits[i];
+            if (lit == true_literal) continue;
+            expr* e = bool_var2expr(lit.var());
+            uint_set s;
+            if (assumptions.contains(e)) {
+                s.insert(get_literal(e).var());
+            }
+            else {
+                b_justification js = get_justification(lit.var());
+                switch (js.get_kind()) {
+                case b_justification::CLAUSE: {
+                    clause * cls      = js.get_clause();
+                    unsigned num_lits = cls->get_num_literals();
+                    for (unsigned j = 0; j < num_lits; ++j) {
+                        literal lit2 = cls->get_literal(j);
+                        if (lit2.var() != lit.var()) {
+                            s |= m_antecedents.find(lit2.var());
+                        }
+                    }
+                    break;
+                }
+                case b_justification::BIN_CLAUSE: {
+                    s |= m_antecedents.find(js.get_literal().var());
+                    break;
+                }
+                case b_justification::AXIOM: {
+                    break;
+                }
+                case b_justification::JUSTIFICATION: 
+                    justification* j = js.get_justification();
+                    // warning_msg("TODO: extract antecedents from theory justification");
+                    // std::cout << "TODO: justification\n";
+                    break;
+                }                
+            }       
+            m_antecedents.insert(lit.var(), s);
+            bool found = false;
+            if (vars.contains(e)) {
+                found = true;
+                fml = lit.sign()?m.mk_not(e):e;
+                vars.erase(e);
+            }
+            else if (!lit.sign() && m.is_eq(e, e1, e2)) {
+                if (vars.contains(e2)) {
+                    std::swap(e1, e2);
+                }
+                if (vars.contains(e1) && m.is_value(e2)) {
+                    found = true;
+                    fml = e;
+                    vars.erase(e1);                    
+                }
+            }
+            if (found) {
+                fml = m.mk_implies(antecedent2fml(s), fml);
+                conseq.push_back(fml);
+            }
+        }
+    }
+
+    lbool context::get_consequences(expr_ref_vector const& assumptions, 
+                                    expr_ref_vector const& vars, expr_ref_vector& conseq) {
+
+        lbool is_sat = check(assumptions.size(), assumptions.c_ptr());
+        if (is_sat != l_true) {
+            return is_sat;
+        }
+        obj_map<expr, expr*> var2val;
+        obj_hashtable<expr> _assumptions;
+        for (unsigned i = 0; i < assumptions.size(); ++i) {
+            _assumptions.insert(assumptions[i]);
+        }
+        model_ref mdl;
+        get_model(mdl);
+        expr_ref_vector trail(m_manager);
+        model_evaluator eval(*mdl.get());
+        expr_ref val(m_manager);
+        for (unsigned i = 0; i < vars.size(); ++i) {
+            eval(vars[i], val);
+            if (m_manager.is_value(val)) {
+                trail.push_back(val);
+                var2val.insert(vars[i], val);
+            } 
+        }
+        extract_fixed_consequences(0, var2val, _assumptions, conseq);
+        unsigned num_units = assigned_literals().size();
+        app_ref eq(m_manager);
+        TRACE("context", 
+              tout << "pop:  " << num_levels << "\n";
+              tout << "vars: " << vars.size() << "\n";
+              tout << "lits: " << num_units << "\n";);
+        m_case_split_queue->init_search_eh();
+        while (!var2val.empty()) {
+            obj_map<expr,expr*>::iterator it = var2val.begin();
+            expr* e = it->m_key;
+            expr* val = it->m_value;
+            push_scope();
+            unsigned current_level = m_scope_lvl;
+
+            literal lit;
+            if (m_manager.is_bool(e)) {
+                lit = literal(get_bool_var(e), m_manager.is_true(val));
+            }
+            else {
+                eq = mk_eq_atom(e, val);
+                internalize_formula(eq, false);
+                lit = literal(get_bool_var(eq), true);
+            }
+            assign(lit, b_justification::mk_axiom(), true);
+            flet<bool> l(m_searching, true);
+            while (true) {
+                is_sat = bounded_search();
+                TRACE("context", tout << "search result: " << is_sat << "\n";);
+                if (is_sat != l_true && m_last_search_failure != OK) {
+                    return is_sat;
+                }
+                if (is_sat == l_undef) {
+                    TRACE("context", tout << "restart\n";);
+                    inc_limits();
+                    continue;
+                }
+                break;
+            }
+            if (get_assignment(lit) == l_true) {
+                var2val.erase(e);
+            }
+            else if (get_assign_level(lit) > get_search_level()) {
+                TRACE("context", tout << "Retry fixing: " << mk_pp(e, m_manager) << "\n";);
+                pop_to_search_lvl();
+                continue;
+            }
+            else {
+                TRACE("context", tout << "Fixed: " << mk_pp(e, m_manager) << "\n";);
+            }
+            extract_fixed_consequences(num_units, var2val, _assumptions, conseq);
+            num_units = assigned_literals().size();
+            if (var2val.contains(e)) {
+                TRACE("context", tout << "TBD: Fixed value to " << mk_pp(e, m_manager) << " was not retrieved\n";);
+                var2val.erase(e);
+                SASSERT(get_assignment(lit) == l_false);
+            }
+        
+            // repeat until we either have a model with negated literal or 
+            // the literal is implied at base.
+            TRACE("context", tout << "Unfixed variables: " << var2val.size() << "\n";);
+        }
+        return l_true;
+    }
+
+}

src/smt/smt_context.cpp

@@ -2460,6 +2460,13 @@ namespace smt {
         SASSERT(m_scope_lvl == m_base_lvl);
     }
 
+    void context::pop_to_search_lvl() {
+        unsigned num_levels = m_scope_lvl - get_search_level();
+        if (num_levels > 0) {
+            pop_scope(num_levels);
+        }
+    }
+
     /**
        \brief Simplify the given clause using the assignment.  Return
        true if the clause was already satisfied, and false otherwise.

src/smt/smt_context.h

@@ -1322,6 +1322,7 @@ namespace smt {
         virtual void setup_context(bool use_static_features);
         void setup_components(void);
         void pop_to_base_lvl();
+        void pop_to_search_lvl();
 #ifdef Z3DEBUG
         bool already_internalized_theory(theory * th) const;
         bool already_internalized_theory_core(theory * th, expr_ref_vector const & s) const;
@@ -1343,6 +1344,11 @@ namespace smt {
             literal lit, context& src_ctx, context& dst_ctx,
             vector<bool_var> b2v, ast_translation& tr);
 
+        u_map<uint_set> m_antecedents;
+        void extract_fixed_consequences(unsigned idx, obj_map<expr, expr*>& vars, obj_hashtable<expr> const& assumptions, expr_ref_vector& conseq);
+
+        expr_ref antecedent2fml(uint_set const& ante);
+
 
     public:
         context(ast_manager & m, smt_params & fp, params_ref const & p = params_ref());
@@ -1383,6 +1389,8 @@ namespace smt {
 
         lbool check(unsigned num_assumptions = 0, expr * const * assumptions = 0, bool reset_cancel = true);        
 
+        lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq);
+        
         lbool setup_and_check(bool reset_cancel = true);
         
         // return 'true' if assertions are inconsistent.

src/smt/smt_kernel.cpp

@@ -99,6 +99,10 @@ namespace smt {
             return m_kernel.check(num_assumptions, assumptions);
         }
 
+        lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq) {
+            return m_kernel.get_consequences(assumptions, vars, conseq);
+        }
+        
         void get_model(model_ref & m) const {
             m_kernel.get_model(m);
         }
@@ -264,6 +268,10 @@ namespace smt {
         return r;
     }
 
+    lbool kernel::get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq) {
+        return m_imp->get_consequences(assumptions, vars, conseq);
+    }
+
     void kernel::get_model(model_ref & m) const {
         m_imp->get_model(m);
     }

src/smt/smt_kernel.h

@@ -126,6 +126,11 @@ namespace smt {
 
         lbool check(app_ref_vector const& asms) { return check(asms.size(), (expr* const*)asms.c_ptr()); }
 
+        /**
+           \brief extract consequences among variables.
+        */
+        lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq);
+
         /**
            \brief Return the model associated with the last check command.
         */

src/smt/smt_solver.cpp

@@ -67,6 +67,10 @@ namespace smt {
             m_context.collect_statistics(st);
         }
 
+        virtual lbool get_consequences_core(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq) {
+            return m_context.get_consequences(assumptions, vars, conseq);
+        }
+
         virtual void assert_expr(expr * t) {
             m_context.assert_expr(t);
         }

src/solver/solver.cpp

@@ -48,6 +48,10 @@ struct scoped_assumption_push {
 };
 
 lbool solver::get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
+    return get_consequences_core(asms, vars, consequences);
+}
+
+lbool solver::get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
     ast_manager& m = asms.get_manager();
     lbool is_sat = check_sat(asms);
     if (is_sat != l_true) {

src/solver/solver.h

@@ -171,6 +171,11 @@ public:
         ~scoped_push() { if (!m_nopop) s.pop(1); }
         void disable_pop() { m_nopop = true; }
     };
+ 
+protected:
+
+    virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences);
+
 };
 
 #endif

src/solver/solver_na2as.cpp

@@ -65,6 +65,11 @@ lbool solver_na2as::check_sat(unsigned num_assumptions, expr * const * assumptio
     return check_sat_core(m_assumptions.size(), m_assumptions.c_ptr());
 }
 
+lbool solver_na2as::get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
+    append_assumptions app(m_assumptions, asms.size(), asms.c_ptr());
+    return get_consequences_core(m_assumptions, vars, consequences);
+}
+
 void solver_na2as::push() {
     m_scopes.push_back(m_assumptions.size());
     push_core();

src/solver/solver_na2as.h

@@ -45,6 +45,7 @@ public:
     
     virtual unsigned get_num_assumptions() const { return m_assumptions.size(); }
     virtual expr * get_assumption(unsigned idx) const { return m_assumptions[idx]; }
+    virtual lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences);
 protected:
     virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) = 0;
     virtual void push_core() = 0;