From 89989627d08f8d48e96d9968943e7e04a74248fa Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 4 Nov 2013 13:33:02 -0800
Subject: [PATCH] add blast method for ite terms
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
scripts/mk_project.py | 2 +-
src/muz/pdr/pdr_context.cpp | 3 +-
src/muz/pdr/pdr_util.cpp | 63 ------
src/muz/pdr/pdr_util.h | 6 -
src/opt/fu_malik.cpp | 44 +++--
src/smt/diff_logic.h | 10 +-
src/smt/network_flow.h | 5 +-
src/smt/network_flow_def.h | 80 +++++++-
src/tactic/core/blast_term_ite_tactic.cpp | 221 ++++++++++++++++++++++
src/tactic/core/blast_term_ite_tactic.h | 38 ++++
10 files changed, 369 insertions(+), 103 deletions(-)
create mode 100644 src/tactic/core/blast_term_ite_tactic.cpp
create mode 100644 src/tactic/core/blast_term_ite_tactic.h
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index ccae41dcb..e92899436 100644
--- a/scripts/mk_project.py
+++ b/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')
diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index aab7b1388..d2ac29689 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/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));
diff --git a/src/muz/pdr/pdr_util.cpp b/src/muz/pdr/pdr_util.cpp
index f122f1e2c..33c98fae4 100644
--- a/src/muz/pdr/pdr_util.cpp
+++ b/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>;
diff --git a/src/muz/pdr/pdr_util.h b/src/muz/pdr/pdr_util.h
index 446bde8aa..150cf2bb5 100644
--- a/src/muz/pdr/pdr_util.h
+++ b/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.
*/
diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp
index 07d256d9e..10fbc05c5 100644
--- a/src/opt/fu_malik.cpp
+++ b/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());
-
- // Get a list of satisfying soft_constraints
- model_ref model;
- s.get_model(model);
-
- 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);
+ lbool is_sat = l_true;
+ do {
+ is_sat = fm.step();
+ }
+ while (is_sat == l_false);
+
+ if (is_sat == l_true) {
+ // Get a list of satisfying soft_constraints
+ model_ref model;
+ s.get_model(model);
+ 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
diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h
index cf0d5f5a6..ff01a4792 100644
--- a/src/smt/diff_logic.h
+++ b/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) {
- edge_id_vector & edges = m_out_edges[source];
- typename edge_id_vector::iterator it = edges.begin();
- typename edge_id_vector::iterator end = edges.end();
+ bool get_edge_id(dl_var source, dl_var target, edge_id & id) const {
+ edge_id_vector const & edges = m_out_edges[source];
+ typename edge_id_vector::const_iterator it = edges.begin();
+ 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;
}
diff --git a/src/smt/network_flow.h b/src/smt/network_flow.h
index a19cae0a2..8d3a9a75b 100644
--- a/src/smt/network_flow.h
+++ b/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:
diff --git a/src/smt/network_flow_def.h b/src/smt/network_flow_def.h
index 3b4b93d51..25ff6ee0c 100644
--- a/src/smt/network_flow_def.h
+++ b/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
diff --git a/src/tactic/core/blast_term_ite_tactic.cpp b/src/tactic/core/blast_term_ite_tactic.cpp
new file mode 100644
index 000000000..c69849253
--- /dev/null
+++ b/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);
+}
diff --git a/src/tactic/core/blast_term_ite_tactic.h b/src/tactic/core/blast_term_ite_tactic.h
new file mode 100644
index 000000000..6756b29d3
--- /dev/null
+++ b/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