mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

add slicing

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-03-02 21:24:21 -08:00
parent 352912c6b5
commit 523dc0fb36
1 changed files with 14 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/muz_qe/horn_tactic.cpp
View file

@ -22,6 +22,8 @@ Revision History:
#include"horn_tactic.h" #include"horn_tactic.h"
#include"dl_context.h" #include"dl_context.h"
#include"expr_replacer.h" #include"expr_replacer.h"
#include"dl_rule_transformer.h"
#include"dl_mk_slice.h"
class horn_tactic : public tactic { class horn_tactic : public tactic {
struct imp { struct imp {
@ -30,9 +32,9 @@ class horn_tactic : public tactic {
datalog::context m_ctx; datalog::context m_ctx;
smt_params m_fparams; smt_params m_fparams;
imp(bool is_simplify, ast_manager & m, params_ref const & p): imp(bool t, ast_manager & m, params_ref const & p):
m(m), m(m),
m_is_simplify(is_simplify), m_is_simplify(t),
m_ctx(m, m_fparams) { m_ctx(m, m_fparams) {
updt_params(p); updt_params(p);
} }
@ -283,6 +285,13 @@ class horn_tactic : public tactic {
m_ctx.set_output_predicate(query_pred); m_ctx.set_output_predicate(query_pred);
m_ctx.get_rules(); // flush adding rules. m_ctx.get_rules(); // flush adding rules.
m_ctx.apply_default_transformation(mc, pc); m_ctx.apply_default_transformation(mc, pc);
if (m_ctx.get_params().slice()) {
datalog::rule_transformer transformer(m_ctx);
datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx);
transformer.register_plugin(slice);
m_ctx.transform_rules(transformer, mc, pc);
}
expr_substitution sub(m); expr_substitution sub(m);
sub.insert(q, m.mk_false()); sub.insert(q, m.mk_false());
@ -308,10 +317,10 @@ class horn_tactic : public tactic {
statistics m_stats; statistics m_stats;
imp * m_imp; imp * m_imp;
public: public:
horn_tactic(bool is_simplify, ast_manager & m, params_ref const & p): horn_tactic(bool t, ast_manager & m, params_ref const & p):
m_is_simplify(is_simplify), m_is_simplify(t),
m_params(p) { m_params(p) {
m_imp = alloc(imp, is_simplify, m, p); m_imp = alloc(imp, t, m, p);
} }
virtual tactic * translate(ast_manager & m) { virtual tactic * translate(ast_manager & m) {