add blast method for ite terms

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

scripts/mk_project.py

@@ -58,7 +58,7 @@ def init_project_def():
     add_lib('muz', ['smt', 'sat', 'smt2parser', 'aig_tactic', 'qe'], 'muz/base')
     add_lib('transforms', ['muz', 'hilbert'], 'muz/transforms')
     add_lib('rel', ['muz', 'transforms'], 'muz/rel')
-    add_lib('pdr', ['muz', 'transforms', 'arith_tactics', 'smt_tactic'], 'muz/pdr')
+    add_lib('pdr', ['muz', 'transforms', 'arith_tactics', 'core_tactics', 'smt_tactic'], 'muz/pdr')
     add_lib('clp', ['muz', 'transforms'], 'muz/clp')
     add_lib('tab', ['muz', 'transforms'], 'muz/tab')
     add_lib('bmc', ['muz', 'transforms'], 'muz/bmc')

src/muz/pdr/pdr_context.cpp

@@ -47,6 +47,7 @@ Notes:
 #include "dl_boogie_proof.h"
 #include "qe_util.h"
 #include "scoped_proof.h"
+#include "blast_term_ite_tactic.h"
 
 namespace pdr {
 
@@ -601,7 +602,7 @@ namespace pdr {
         th_rewriter rw(m);
         rw(fml);
         if (ctx.is_dl() || ctx.is_utvpi()) {
-            hoist_non_bool_if(fml);
+            blast_term_ite(fml);
         }
         TRACE("pdr", tout << mk_pp(fml, m) << "\n";);
         SASSERT(is_ground(fml));

src/muz/pdr/pdr_util.cpp

@@ -1030,68 +1030,6 @@ namespace pdr {
         fml = m.mk_and(conjs.size(), conjs.c_ptr());        
     }
 
-    // 
-    // (f (if c1 (if c2 e1 e2) e3) b c) -> 
-    // (if c1 (if c2 (f e1 b c)
-
-    class ite_hoister {
-        ast_manager& m;
-    public:
-        ite_hoister(ast_manager& m): m(m) {}
-
-        br_status mk_app_core(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result) {
-            if (m.is_ite(f)) {
-                return BR_FAILED;
-            }
-            for (unsigned i = 0; i < num_args; ++i) {
-                expr* c, *t, *e;
-                if (!m.is_bool(args[i]) && m.is_ite(args[i], c, t, e)) {
-                    expr_ref e1(m), e2(m);
-                    ptr_vector<expr> args1(num_args, args);
-                    args1[i] = t;
-                    e1 = m.mk_app(f, num_args, args1.c_ptr());
-                    if (t == e) {
-                        result = e1;
-                        return BR_REWRITE1;
-                    }
-                    args1[i] = e;
-                    e2 = m.mk_app(f, num_args, args1.c_ptr());
-                    result = m.mk_app(f, num_args, args);
-                    result = m.mk_ite(c, e1, e2);
-                    return BR_REWRITE3;
-                }
-            }
-            return BR_FAILED;
-        }
-    };
-
-    struct ite_hoister_cfg: public default_rewriter_cfg {
-        ite_hoister m_r;
-        bool rewrite_patterns() const { return false; }
-        br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
-            return m_r.mk_app_core(f, num, args, result);
-        }
-        ite_hoister_cfg(ast_manager & m, params_ref const & p):m_r(m) {}        
-    };
-
-    class ite_hoister_star : public rewriter_tpl<ite_hoister_cfg> {
-        ite_hoister_cfg m_cfg;
-    public:
-        ite_hoister_star(ast_manager & m, params_ref const & p):
-            rewriter_tpl<ite_hoister_cfg>(m, false, m_cfg),
-            m_cfg(m, p) {}
-    };
-
-    void hoist_non_bool_if(expr_ref& fml) {
-        ast_manager& m = fml.get_manager();
-        scoped_no_proof _sp(m);
-        params_ref p;
-        ite_hoister_star ite_rw(m, p);
-        expr_ref tmp(m);
-        ite_rw(fml, tmp);
-        fml = tmp;        
-    }
-
     class test_diff_logic {
         ast_manager& m;
         arith_util a;
@@ -1441,7 +1379,6 @@ namespace pdr {
 
 }
 
-template class rewriter_tpl<pdr::ite_hoister_cfg>;
 template class rewriter_tpl<pdr::arith_normalizer_cfg>;
 
 

src/muz/pdr/pdr_util.h

@@ -143,12 +143,6 @@ namespace pdr {
      */
     void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml);
 
-    /**
-       \brief hoist non-boolean if expressions.
-     */
-    void hoist_non_bool_if(expr_ref& fml);
-
-
     /**
        \brief normalize coefficients in polynomials so that least coefficient is 1.
      */

src/opt/fu_malik.cpp

@@ -71,14 +71,15 @@ namespace opt {
            * add at-most-one constraint with blocking 
         */
 
-        bool step() {
+        lbool step() {
+            IF_VERBOSE(1, verbose_stream() << "(opt.max_sat step)\n";);
             expr_ref_vector assumptions(m), block_vars(m);
             for (unsigned i = 0; i < m_soft.size(); ++i) {
                 assumptions.push_back(m.mk_not(m_aux[i].get()));
             }
             lbool is_sat = s.check_sat(assumptions.size(), assumptions.c_ptr());
             if (is_sat != l_false) {
-                return true;
+                return is_sat;
             }
 
             ptr_vector<expr> core;
@@ -102,7 +103,7 @@ namespace opt {
                 s.assert_expr(m.mk_or(m_soft[i].get(), m_aux[i].get()));
             }
             assert_at_most_one(block_vars);
-            return false;
+            return l_false;
         }
 
     private:
@@ -139,23 +140,28 @@ namespace opt {
             s.push();
 
             fu_malik fm(m, s, soft_constraints);
-            while (!fm.step());
+			lbool is_sat = l_true;
-
+            do {
-            // Get a list of satisfying soft_constraints
+				is_sat = fm.step();
-            model_ref model;
+			}
-            s.get_model(model);
+			while (is_sat == l_false);
-
+			
-            expr_ref_vector result(m);
+			if (is_sat == l_true) {
-            for (unsigned i = 0; i < soft_constraints.size(); ++i) {
+				// Get a list of satisfying soft_constraints
-                expr_ref val(m);
+				model_ref model;
-                VERIFY(model->eval(soft_constraints[i].get(), val));
+				s.get_model(model);
-                if (!m.is_false(val)) {
-                    result.push_back(soft_constraints[i].get());
-                }
-            }
-            soft_constraints.reset();
-            soft_constraints.append(result);
 
+				expr_ref_vector result(m);
+				for (unsigned i = 0; i < soft_constraints.size(); ++i) {
+					expr_ref val(m);
+					VERIFY(model->eval(soft_constraints[i].get(), val));
+					if (!m.is_false(val)) {
+						result.push_back(soft_constraints[i].get());
+					}
+				}
+				soft_constraints.reset();
+				soft_constraints.append(result);
+			}
             s.pop(1);
         }
         // We are done and soft_constraints has 

src/smt/diff_logic.h

@@ -935,13 +935,13 @@ public:
 
     // Return true if there is an edge source --> target (also counting disabled edges).
     // If there is such edge, return its edge_id in parameter id.
-    bool get_edge_id(dl_var source, dl_var target, edge_id & id) {
+    bool get_edge_id(dl_var source, dl_var target, edge_id & id) const {
-        edge_id_vector & edges = m_out_edges[source];
+        edge_id_vector const & edges = m_out_edges[source];
-        typename edge_id_vector::iterator it  = edges.begin();
+        typename edge_id_vector::const_iterator it  = edges.begin();
-        typename edge_id_vector::iterator end = edges.end();
+        typename edge_id_vector::const_iterator end = edges.end();
         for (; it != end; ++it) {
             id = *it;
-            edge & e = m_edges[id];
+            edge const & e = m_edges[id];
             if (e.get_target() == target) {
                 return true;
             }

src/smt/network_flow.h

@@ -93,7 +93,7 @@ namespace smt {
         // Initialize the network with a feasible spanning tree
         void initialize();
 
-        edge_id get_edge_id(dl_var source, dl_var target);
+        edge_id get_edge_id(dl_var source, dl_var target) const;
 
 
         void update_potentials();
@@ -112,6 +112,9 @@ namespace smt {
 
         std::string display_spanning_tree();
 
+        bool edge_in_tree(edge_id id) const;
+        bool edge_in_tree(node src, node dst) const;
+
         bool check_well_formed();
 
     public:

src/smt/network_flow_def.h

@@ -137,7 +137,7 @@ namespace smt {
     }
 
     template<typename Ext>
-    edge_id network_flow<Ext>::get_edge_id(dl_var source, dl_var target) {
+    edge_id network_flow<Ext>::get_edge_id(dl_var source, dl_var target) const {
         // m_upwards[source] decides which node is the real source
         edge_id id;
         VERIFY(m_upwards[source] ? m_graph.get_edge_id(source, target, id) : m_graph.get_edge_id(target, source, id));
@@ -234,6 +234,7 @@ namespace smt {
                 m_delta = m_flows[e_id];
                 src = u;
                 tgt = m_pred[u];
+                SASSERT(edge_in_tree(src,tgt));
                 m_in_edge_dir = true;
             }
         }
@@ -245,6 +246,7 @@ namespace smt {
                 m_delta = m_flows[e_id];
                 src = u;
                 tgt = m_pred[u];
+                SASSERT(edge_in_tree(src,tgt));
                 m_in_edge_dir = false;
             }
         }
@@ -267,10 +269,12 @@ namespace smt {
         node q = m_graph.get_target(m_entering_edge);        
         node u = m_graph.get_source(m_leaving_edge);
         node v = m_graph.get_target(m_leaving_edge);
+
         // v is parent of u so T_u does not contain root node
         if (m_pred[u] == v) {
             std::swap(u, v);
         }  
+        SASSERT(m_pred[v] == u);
 
         for (node n = p; n != -1; n = m_pred[n]) {
             // q should be in T_v so swap p and q
@@ -285,13 +289,10 @@ namespace smt {
             tout << u << ", " << v << ") leaves\n";
         });
 
-        node x = m_final[p];
-        node y = m_thread[x];
-        node z = m_final[q];
 
         // Update m_pred (for nodes in the stem from q to v)
         node n = q;
-        node last = m_pred[v];
+        node last = m_pred[v]; // review: m_pred[v] == u holds, so why not 'u'?
         node prev = p;
         while (n != last && n != -1) {
             node next = m_pred[n];  
@@ -303,6 +304,11 @@ namespace smt {
 
         TRACE("network_flow", tout << pp_vector("Predecessors", m_pred, true) << pp_vector("Upwards", m_upwards););
 
+        node x = m_final[p];
+        node y = m_thread[x];
+        node z = m_final[q];
+
+
         // Do this before updating data structures
         node gamma_p = m_pred[m_thread[m_final[p]]];
         node gamma_v = m_pred[m_thread[m_final[v]]];
@@ -430,6 +436,8 @@ namespace smt {
             if (!bounded) return false;
             update_flows();
             if (m_entering_edge != m_leaving_edge) {
+				SASSERT(edge_in_tree(m_leaving_edge));
+				SASSERT(!edge_in_tree(m_entering_edge));
                 m_states[m_entering_edge] = BASIS;
                 m_states[m_leaving_edge] = (m_flows[m_leaving_edge].is_zero()) ? LOWER : UPPER;
                 update_spanning_tree();
@@ -494,6 +502,7 @@ namespace smt {
     }
 
     static int get_final(int root, svector<int> const & thread, svector<int> const & depth) {
+        // really final or should one take into account connected tree?
         int n = root;
         while (depth[thread[n]] > depth[root]) {
             n = thread[n];
@@ -501,19 +510,76 @@ namespace smt {
         return n;
     }
 
+    template<typename Ext>
+    bool network_flow<Ext>::edge_in_tree(edge_id id) const {
+        return m_states[id] == BASIS;
+    }
+
+    template<typename Ext>
+    bool network_flow<Ext>::edge_in_tree(node src, node dst) const {
+        return edge_in_tree(get_edge_id(src,dst));
+    }
+
+    /**
+       \brief Check invariants of main data-structures.
+
+       Spanning tree of m_graph + root is represented using:
+        
+        svector<edge_state> m_states;      edge_id |-> edge_state
+        svector<bool> m_upwards;           node |-> bool
+        svector<node> m_pred;              node |-> node
+        svector<int>  m_depth;             node |-> int
+        svector<node> m_thread;            node |-> node
+        svector<node> m_rev_thread;        node |-> node
+        svector<node> m_final;             node |-> node
+
+        m_thread[m_rev_thread[n]] == n  for each node n
+
+        Tree is determined by m_pred:
+        - m_pred[root] == -1
+        - m_pred[n] = m != n     for each node n, acyclic until reaching root.
+        - m_depth[m_pred[n]] + 1 == m_depth[n] for each n != root        
+
+        m_thread is a linked list traversing all nodes.
+        Furthermore, the nodes linked in m_thread follows a 
+        depth-first traversal order.
+
+        m_final[n] is deepest most node in a sub-tree rooted at n.
+                
+    */
+
     template<typename Ext>
     bool network_flow<Ext>::check_well_formed() {
         node root = m_pred.size()-1;
 
+        // Check that m_thread traverses each node.
+        // This gets checked using union-find as well.
+        svector<bool> found(m_thread.size(), false);
+        found[root] = true;
+        for (node x = m_thread[root]; x != root; x = m_thread[x]) {
+            found[x] = true;
+        }
+        for (unsigned i = 0; i < found.size(); ++i) {
+            SASSERT(found[i]);
+        }
+
+        // m_pred is acyclic, and points to root.
+        SASSERT(m_pred[root] == -1);
+        SASSERT(m_depth[root] == 0);
+        for (node i = 0; i < root; ++i) {
+            SASSERT(m_depth[m_pred[i]] < m_depth[i]);
+        }
+
         // m_upwards show correct direction
         for (unsigned i = 0; i < m_upwards.size(); ++i) {
             node p = m_pred[i];
             edge_id id;
-            SASSERT(m_upwards[i] == m_graph.get_edge_id(i, p, id));            
+            SASSERT(!m_upwards[i] || m_graph.get_edge_id(i, p, id));            
         }
 
         // m_depth[x] denotes distance from x to the root node
         for (node x = m_thread[root]; x != root; x = m_thread[x]) {
+            SASSERT(m_depth[x] > 0);
             SASSERT(m_depth[x] == m_depth[m_pred[x]] + 1);
         }
 
@@ -540,7 +606,7 @@ namespace smt {
         
         // All nodes belong to the same spanning tree
         for (unsigned i = 0; i < roots.size(); ++i) {            
-            SASSERT(i == 0 ? roots[i] + roots.size() == 0 : roots[i] == 0);            
+            SASSERT(roots[i] + roots.size() == 0 || roots[i] >= 0);            
         }        
 
         // m_flows are zero on non-basic edges

src/tactic/core/blast_term_ite_tactic.cpp

@@ -0,0 +1,221 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    blast_term_ite_tactic.cpp
+
+Abstract:
+
+    Blast term if-then-else by hoisting them up.
+
+Author:
+ 
+    Nikolaj Bjorner (nbjorner) 2013-11-4
+
+Notes:
+
+--*/
+#include"tactical.h"
+#include"defined_names.h"
+#include"rewriter_def.h"
+#include"filter_model_converter.h"
+#include"cooperate.h"
+#include"scoped_proof.h"
+
+
+
+// 
+// (f (if c1 (if c2 e1 e2) e3) b c) -> 
+// (if c1 (if c2 (f e1 b c)
+//
+
+
+class blast_term_ite_tactic : public tactic {
+
+    struct rw_cfg : public default_rewriter_cfg {
+        ast_manager& m;
+        unsigned long long          m_max_memory; // in bytes
+        unsigned m_num_fresh; // number of expansions
+
+        rw_cfg(ast_manager & _m, params_ref const & p):
+            m(_m),
+            m_num_fresh(0) {
+            updt_params(p);
+        }
+
+        void updt_params(params_ref const & p) {
+            m_max_memory     = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
+        }
+
+        bool max_steps_exceeded(unsigned num_steps) const { 
+            cooperate("blast term ite");
+            if (memory::get_allocation_size() > m_max_memory)
+                throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
+            return false;
+        }
+        
+        br_status mk_app_core(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result) {
+            if (m.is_ite(f)) {
+                return BR_FAILED;
+            }
+            for (unsigned i = 0; i < num_args; ++i) {
+                expr* c, *t, *e;
+                if (!m.is_bool(args[i]) && m.is_ite(args[i], c, t, e)) {
+                    expr_ref e1(m), e2(m);
+                    ptr_vector<expr> args1(num_args, args);
+                    args1[i] = t;
+                    ++m_num_fresh;
+                    e1 = m.mk_app(f, num_args, args1.c_ptr());
+                    if (t == e) {
+                        result = e1;
+                        return BR_REWRITE1;
+                    }
+                    args1[i] = e;
+                    e2 = m.mk_app(f, num_args, args1.c_ptr());
+                    result = m.mk_app(f, num_args, args);
+                    result = m.mk_ite(c, e1, e2);
+                    return BR_REWRITE3;
+                }
+            }
+            return BR_FAILED;
+        }
+
+        bool rewrite_patterns() const { return false; }
+
+        br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
+            return mk_app_core(f, num, args, result);
+        }
+
+    };
+                
+    struct rw : public rewriter_tpl<rw_cfg> {
+        rw_cfg m_cfg;
+        
+        rw(ast_manager & m, params_ref const & p):
+            rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg),
+            m_cfg(m, p) {
+        }
+    };
+
+    struct imp {
+        ast_manager & m;
+        rw            m_rw;
+        
+        imp(ast_manager & _m, params_ref const & p):
+            m(_m),
+            m_rw(m, p) {
+        }
+        
+        void set_cancel(bool f) {
+            m_rw.set_cancel(f);
+        }
+        
+        void updt_params(params_ref const & p) {
+            m_rw.cfg().updt_params(p);
+        }
+        
+        void operator()(goal_ref const & g, 
+                        goal_ref_buffer & result, 
+                        model_converter_ref & mc, 
+                        proof_converter_ref & pc,
+                        expr_dependency_ref & core) {
+            SASSERT(g->is_well_sorted());
+            mc = 0; pc = 0; core = 0;
+            tactic_report report("blast-term-ite", *g);
+            bool produce_proofs = g->proofs_enabled();
+
+            expr_ref   new_curr(m);
+            proof_ref  new_pr(m);
+            unsigned   size = g->size();
+            for (unsigned idx = 0; idx < size; idx++) {
+                expr * curr = g->form(idx);
+                m_rw(curr, new_curr, new_pr);
+                if (produce_proofs) {
+                    proof * pr = g->pr(idx);
+                    new_pr     = m.mk_modus_ponens(pr, new_pr);
+                }
+                g->update(idx, new_curr, new_pr, g->dep(idx));
+            }
+            report_tactic_progress(":blast-term-ite-consts", m_rw.m_cfg.m_num_fresh);
+            g->inc_depth();
+            result.push_back(g.get());
+            TRACE("blast_term_ite", g->display(tout););
+            SASSERT(g->is_well_sorted());
+        }
+    };
+    
+    imp *      m_imp;
+    params_ref m_params;
+public:
+    blast_term_ite_tactic(ast_manager & m, params_ref const & p):
+        m_params(p) {
+        m_imp = alloc(imp, m, p);
+    }
+
+    virtual tactic * translate(ast_manager & m) {
+        return alloc(blast_term_ite_tactic, m, m_params);
+    }
+        
+    virtual ~blast_term_ite_tactic() {
+        dealloc(m_imp);
+    }
+
+    virtual void updt_params(params_ref const & p) {
+        m_params = p;
+        m_imp->m_rw.cfg().updt_params(p);
+    }
+
+    virtual void collect_param_descrs(param_descrs & r) {
+        insert_max_memory(r);
+        insert_max_steps(r);
+        r.insert("max_args", CPK_UINT, 
+                 "(default: 128) maximum number of arguments (per application) that will be considered by the greedy (quadratic) heuristic.");
+    }
+    
+    virtual void operator()(goal_ref const & in, 
+                            goal_ref_buffer & result, 
+                            model_converter_ref & mc, 
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core) {
+        (*m_imp)(in, result, mc, pc, core);
+    }
+    
+    virtual void cleanup() {
+        ast_manager & m = m_imp->m;
+        imp * d = m_imp;
+        #pragma omp critical (tactic_cancel)
+        {
+            m_imp = 0;
+        }
+        dealloc(d);
+        d = alloc(imp, m, m_params);
+        #pragma omp critical (tactic_cancel)
+        {
+            m_imp = d;
+        }
+    }
+
+    virtual void set_cancel(bool f) {
+        if (m_imp)
+            m_imp->set_cancel(f);
+    }
+
+    static void blast_term_ite(expr_ref& fml) {
+        ast_manager& m = fml.get_manager();
+        scoped_no_proof _sp(m);
+        params_ref p;
+        rw ite_rw(m, p);
+        expr_ref tmp(m);
+        ite_rw(fml, tmp);
+        fml = tmp;        
+    }
+};
+
+tactic * mk_blast_term_ite_tactic(ast_manager & m, params_ref const & p) {
+    return clean(alloc(blast_term_ite_tactic, m, p));
+}
+
+void blast_term_ite(expr_ref& fml) {
+    blast_term_ite_tactic::blast_term_ite(fml);
+}

src/tactic/core/blast_term_ite_tactic.h

@@ -0,0 +1,38 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    blast_term_ite_tactic.h
+
+Abstract:
+
+    Blast term if-then-else by hoisting them up.
+    This is expensive but useful in some cases, such as
+    for enforcing constraints being in difference logic.
+    Use elim-term-ite elsewhere when possible.
+   
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-11-4
+
+Notes:
+
+--*/
+#ifndef _BLAST_TERM_ITE_TACTIC_H_
+#define _BLAST_TERM_ITE_TACTIC_H_
+
+#include"params.h"
+class ast_manager;
+class tactic;
+
+tactic * mk_blast_term_ite_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+/*
+    ADD_TACTIC("blast-term-ite", "blast term if-then-else by hoisting them.", "mk_blast_term_ite_tactic(m, p)")
+*/
+
+void blast_term_ite(expr_ref& fml);
+
+#endif