exposing facility to extract dependent clauses

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

src/smt/tactic/smt_tactic.cpp

@@ -23,6 +23,66 @@ Notes:
 #include"smt_params_helper.hpp"
 #include"rewriter_types.h"
 #include"filter_model_converter.h"
+#include"ast_util.h"
+
+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) {
+    scoped_ptr<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);
+    unsigned sz = g->size();
+    for (unsigned i = 0; i < sz; i++) {
+        expr * f            = g->form(i);
+        expr_dependency * d = g->dep(i);
+        if (d == 0) {
+            clauses.push_back(f);
+        }
+        else {
+            // create clause (not d1 \/ ... \/ not dn \/ f) when the d's are the assumptions/dependencies of f.
+            clause.reset();
+            clause.push_back(f);
+            deps.reset();
+            m.linearize(d, deps);
+            SASSERT(!deps.empty()); // d != 0, then deps must not be empty
+            ptr_vector<expr>::iterator it  = deps.begin();
+            ptr_vector<expr>::iterator end = deps.end();
+            for (; it != end; ++it) {
+                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)) {
+                        assumptions.push_back(d);
+                        bool2dep->insert(d, d);
+                    }
+                    clause.push_back(m.mk_not(d));
+                }
+                else {
+                    // must normalize assumption 
+                    expr * b = 0;
+                    if (!dep2bool->find(d, b)) {
+                        b = m.mk_fresh_const(0, m.mk_bool_sort());
+                        dep2bool->insert(d, b);
+                        bool2dep->insert(b, d);
+                        assumptions.push_back(b);
+                        if (!fmc) {
+                            fmc = alloc(filter_model_converter, m);
+                        }
+                        fmc->insert(to_app(b)->get_decl());
+                    }
+                    clause.push_back(m.mk_not(b));
+                }
+            }
+            SASSERT(clause.size() > 1);
+            expr_ref cls(m);
+            cls = mk_or(m, clauses.size(), clauses.c_ptr());
+            clauses.push_back(cls);
+        }
+    }    
+}
 
 class smt_tactic : public tactic {
     smt_params                   m_params;
@@ -128,7 +188,6 @@ public:
         }
     };
 
-    typedef obj_map<expr, expr *> expr2expr_map;
 
     virtual void operator()(goal_ref const & in, 
                             goal_ref_buffer & result, 
@@ -148,64 +207,16 @@ public:
             scoped_init_ctx  init(*this, m);
             SASSERT(m_ctx != 0);
 
-            scoped_ptr<expr2expr_map> dep2bool;
+            expr_ref_vector clauses(m);
             scoped_ptr<expr2expr_map>   bool2dep; 
             ptr_vector<expr>            assumptions;       
             ref<filter_model_converter> fmc;
             if (in->unsat_core_enabled()) {
                 if (in->proofs_enabled())
                     throw tactic_exception("smt tactic does not support simultaneous generation of proofs and unsat cores");
-                dep2bool = alloc(expr2expr_map);
+                extract_clauses_and_dependencies(in, clauses, assumptions, bool2dep, fmc);
-                bool2dep = alloc(expr2expr_map);
+                for (unsigned i = 0; i < clauses.size(); ++i) {
-                ptr_vector<expr> deps;
+                    m_ctx->assert_expr(clauses[i].get());
-                ptr_vector<expr> clause;
-                unsigned sz = in->size();
-                for (unsigned i = 0; i < sz; i++) {
-                    expr * f            = in->form(i);
-                    expr_dependency * d = in->dep(i);
-                    if (d == 0) {
-                        m_ctx->assert_expr(f);
-                    }
-                    else {
-                        // create clause (not d1 \/ ... \/ not dn \/ f) when the d's are the assumptions/dependencies of f.
-                        clause.reset();
-                        clause.push_back(f);
-                        deps.reset();
-                        m.linearize(d, deps);
-                        SASSERT(!deps.empty()); // d != 0, then deps must not be empty
-                        ptr_vector<expr>::iterator it  = deps.begin();
-                        ptr_vector<expr>::iterator end = deps.end();
-                        for (; it != end; ++it) {
-                            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)) {
-                                    assumptions.push_back(d);
-                                    bool2dep->insert(d, d);
-                                }
-                                clause.push_back(m.mk_not(d));
-                            }
-                            else {
-                                // must normalize assumption 
-                                expr * b = 0;
-                                if (!dep2bool->find(d, b)) {
-                                    b = m.mk_fresh_const(0, m.mk_bool_sort());
-                                    dep2bool->insert(d, b);
-                                    bool2dep->insert(b, d);
-                                    assumptions.push_back(b);
-                                    if (!fmc) {
-                                        fmc = alloc(filter_model_converter, m);
-                                    }
-                                    fmc->insert(to_app(b)->get_decl());
-                                }
-                                clause.push_back(m.mk_not(b));
-                            }
-                        }
-                        SASSERT(clause.size() > 1);
-                        expr_ref cls(m);
-                        cls = m.mk_or(clause.size(), clause.c_ptr());
-                        m_ctx->assert_expr(cls);
-                    }
                 }
             }
             else if (in->proofs_enabled()) {

src/smt/tactic/smt_tactic.h

@@ -20,15 +20,21 @@ Notes:
 #define _SMT_TACTIC_H_
 
 #include"params.h"
+#include"ast.h"
+#include"obj_hashtable.h"
+#include"goal.h"
 
 class tactic;
+class filter_model_converter;
 
 tactic * mk_smt_tactic(params_ref const & p = params_ref());
 // syntax sugar for using_params(mk_smt_tactic(), p) where p = (:auto_config, auto_config)
 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);
+
 /*
   ADD_TACTIC("smt", "apply a SAT based SMT solver.", "mk_smt_tactic(p)") 
 */
-
 #endif

src/tactic/nlsat_smt/nl_purify_tactic.cpp

@@ -115,8 +115,6 @@ public:
 
         arith_util & u() { return m_owner.m_util; }
 
-        bool produce_proofs() const { return m_owner.m_produce_proofs; }
-
         expr * mk_interface_var(expr* arg) {
             expr* r;
             if (m_interface_cache.find(arg, r)) {
@@ -145,7 +143,7 @@ public:
             return is_app(e) && (to_app(e)->get_family_id() == u().get_family_id());
         }
 
-        void mk_interface_bool(func_decl * f, unsigned num, expr* const* args, expr_ref& result) {
+        void mk_interface_bool(func_decl * f, unsigned num, expr* const* args, expr_ref& result, proof_ref& pr) {
             expr_ref old_pred(m.mk_app(f, num, args), m);
             polarity_t pol;
             VERIFY(m_polarities.find(old_pred, pol));
@@ -154,10 +152,13 @@ public:
             m_new_preds.push_back(to_app(result));
             m_owner.m_fmc->insert(to_app(result)->get_decl());
             if (pol != pol_neg) {
-                m_owner.m_nl_g->assert_expr(m.mk_or(m.mk_not(result), m.mk_app(f, num, args)));
+                m_owner.m_nl_g->assert_expr(m.mk_or(m.mk_not(result), old_pred));
             }
             if (pol != pol_pos) {
-                m_owner.m_nl_g->assert_expr(m.mk_or(result, m.mk_not(m.mk_app(f, num, args))));
+                m_owner.m_nl_g->assert_expr(m.mk_or(result, m.mk_not(old_pred)));
+            }
+            if (m_owner.m_produce_proofs) {
+                pr = m.mk_oeq(old_pred, result);
             }
             TRACE("nlsat_smt", tout << old_pred << " : " << result << "\n";);
         }
@@ -183,7 +184,7 @@ public:
         br_status reduce_app_bool(func_decl * f, unsigned num, expr* const* args, expr_ref& result, proof_ref & pr) {
             if (f->get_family_id() == m.get_basic_family_id()) {
                 if (f->get_decl_kind() == OP_EQ && u().is_real(args[0])) {
-                    mk_interface_bool(f, num, args, result);
+                    mk_interface_bool(f, num, args, result, pr);
                     return BR_DONE;
                 }
                 else {
@@ -194,7 +195,7 @@ public:
                 switch (f->get_decl_kind()) {
                 case OP_LE: case OP_GE: case OP_LT: case OP_GT:
                     // these are the only real cases of non-linear atomic formulas besides equality.
-                    mk_interface_bool(f, num, args, result);
+                    mk_interface_bool(f, num, args, result, pr);
                     return BR_DONE;
                 default:
                     return BR_FAILED;
@@ -209,12 +210,14 @@ public:
         bool is_arith_op(expr* e) {
             return is_app(e) && to_app(e)->get_family_id() == u().get_family_id();
         }
+
         br_status reduce_app_real(func_decl * f, unsigned num, expr* const* args, expr_ref& result, proof_ref & pr) {
             bool has_interface = false;
             bool is_arith = false;
             if (f->get_family_id() == u().get_family_id()) {
                 switch (f->get_decl_kind()) {
-                case OP_NUM: case OP_IRRATIONAL_ALGEBRAIC_NUM:
+                case OP_NUM: 
+                case OP_IRRATIONAL_ALGEBRAIC_NUM:
                     return BR_FAILED;
                 default:
                     is_arith = true;
@@ -238,6 +241,9 @@ public:
             }
             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?
+                }
                 TRACE("nlsat_smt", tout << result << "\n";);
                 return BR_DONE;
             }
@@ -264,6 +270,7 @@ private:
         }
     };
 
+
     arith_util & u() { return m_util; }
 
     void check_point() {
@@ -727,7 +734,6 @@ public:
         r.set_bool_mode();
         rewrite_goal(r, g);        
 
-        g->inc_depth();
         for (unsigned i = 0; i < g->size(); ++i) {
             m_solver->assert_expr(g->form(i));
         }
@@ -740,3 +746,43 @@ 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