From 5b50d98b8961d5d63fc4e169dcaaa1999b9bdb48 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 6 Feb 2016 16:13:31 +0000 Subject: [PATCH] ensure that seq rewriter gets invoked during pre-processing Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bit_blaster/bit_blaster.cpp | 50 +++++++++---------- src/ast/rewriter/bit_blaster/bit_blaster.h | 32 ++++++------ .../bit_blaster/bit_blaster_rewriter.cpp | 1 + .../bit_blaster/bit_blaster_tpl_def.h | 1 + src/ast/rewriter/seq_rewriter.cpp | 4 ++ src/ast/seq_decl_plugin.cpp | 3 ++ src/ast/simplifier/seq_simplifier_plugin.cpp | 39 +++++++++++++++ src/ast/simplifier/seq_simplifier_plugin.h | 39 +++++++++++++++ src/smt/asserted_formulas.cpp | 2 + 9 files changed, 130 insertions(+), 41 deletions(-) create mode 100644 src/ast/simplifier/seq_simplifier_plugin.cpp create mode 100644 src/ast/simplifier/seq_simplifier_plugin.h diff --git a/src/ast/rewriter/bit_blaster/bit_blaster.cpp b/src/ast/rewriter/bit_blaster/bit_blaster.cpp index 153066711..1055ceb58 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster.cpp +++ b/src/ast/rewriter/bit_blaster/bit_blaster.cpp @@ -21,10 +21,10 @@ Revision History: #include"ast_pp.h" #include"bv_decl_plugin.h" -bit_blaster_cfg::bit_blaster_cfg(bv_util & u, bit_blaster_params const & p, basic_simplifier_plugin & _s): +bit_blaster_cfg::bit_blaster_cfg(bv_util & u, bit_blaster_params const & p, bool_rewriter& rw): m_util(u), m_params(p), - s(_s) { + m_rw(rw) { } static void sort_args(expr * & l1, expr * & l2, expr * & l3) { @@ -47,30 +47,30 @@ void bit_blaster_cfg::mk_xor3(expr * l1, expr * l2, expr * l3, expr_ref & r) { else if (l2 == l3) r = l1; else if (m().is_complement(l1, l2)) - s.mk_not(l3, r); + m_rw.mk_not(l3, r); else if (m().is_complement(l1, l3)) - s.mk_not(l2, r); + m_rw.mk_not(l2, r); else if (m().is_complement(l2, l3)) - s.mk_not(l1, r); + m_rw.mk_not(l1, r); else if (m().is_true(l1)) - s.mk_iff(l2, l3, r); + m_rw.mk_iff(l2, l3, r); else if (m().is_false(l1)) - s.mk_xor(l2, l3, r); + m_rw.mk_xor(l2, l3, r); else if (m().is_true(l2)) - s.mk_iff(l1, l3, r); + m_rw.mk_iff(l1, l3, r); else if (m().is_false(l2)) - s.mk_xor(l1, l3, r); + m_rw.mk_xor(l1, l3, r); else if (m().is_true(l3)) - s.mk_iff(l1, l2, r); + m_rw.mk_iff(l1, l2, r); else if (m().is_false(l3)) - s.mk_xor(l1, l2, r); + m_rw.mk_xor(l1, l2, r); else r = m().mk_app(m_util.get_family_id(), OP_XOR3, l1, l2, l3); } else { expr_ref t(m()); - s.mk_xor(l1, l2, t); - s.mk_xor(t, l3, r); + m_rw.mk_xor(l1, l2, t); + m_rw.mk_xor(t, l3, r); } } @@ -90,17 +90,17 @@ void bit_blaster_cfg::mk_carry(expr * l1, expr * l2, expr * l3, expr_ref & r) { else if (l1 == l2 && l1 == l3) r = l1; else if (m().is_false(l1)) - s.mk_and(l2, l3, r); + m_rw.mk_and(l2, l3, r); else if (m().is_false(l2)) - s.mk_and(l1, l3, r); + m_rw.mk_and(l1, l3, r); else if (m().is_false(l3)) - s.mk_and(l1, l2, r); + m_rw.mk_and(l1, l2, r); else if (m().is_true(l1)) - s.mk_or(l2, l3, r); + m_rw.mk_or(l2, l3, r); else if (m().is_true(l2)) - s.mk_or(l1, l3, r); + m_rw.mk_or(l1, l3, r); else if (m().is_true(l3)) - s.mk_or(l1, l2, r); + m_rw.mk_or(l1, l2, r); else if (m().is_complement(l1, l2)) r = l3; else if (m().is_complement(l1, l3)) @@ -112,17 +112,17 @@ void bit_blaster_cfg::mk_carry(expr * l1, expr * l2, expr * l3, expr_ref & r) { } else { expr_ref t1(m()), t2(m()), t3(m()); - s.mk_and(l1, l2, t1); - s.mk_and(l1, l3, t2); - s.mk_and(l2, l3, t3); - s.mk_or(t1, t2, t3, r); + m_rw.mk_and(l1, l2, t1); + m_rw.mk_and(l1, l3, t2); + m_rw.mk_and(l2, l3, t3); + m_rw.mk_or(t1, t2, t3, r); } } template class bit_blaster_tpl; bit_blaster::bit_blaster(ast_manager & m, bit_blaster_params const & params): - bit_blaster_tpl(bit_blaster_cfg(m_util, params, m_simp)), + bit_blaster_tpl(bit_blaster_cfg(m_util, params, m_rw)), m_util(m), - m_simp(m) { + m_rw(m) { } diff --git a/src/ast/rewriter/bit_blaster/bit_blaster.h b/src/ast/rewriter/bit_blaster/bit_blaster.h index 958c79b4d..6221eeaf9 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster.h @@ -19,7 +19,7 @@ Revision History: #ifndef BIT_BLASTER_H_ #define BIT_BLASTER_H_ -#include"basic_simplifier_plugin.h" +#include"bool_rewriter.h" #include"bit_blaster_params.h" #include"bit_blaster_tpl.h" #include"bv_decl_plugin.h" @@ -31,31 +31,31 @@ public: protected: bv_util & m_util; bit_blaster_params const & m_params; - basic_simplifier_plugin & s; + bool_rewriter & m_rw; public: - bit_blaster_cfg(bv_util & u, bit_blaster_params const & p, basic_simplifier_plugin & _s); + bit_blaster_cfg(bv_util & u, bit_blaster_params const & p, bool_rewriter& rw); ast_manager & m() const { return m_util.get_manager(); } numeral power(unsigned n) const { return rational::power_of_two(n); } - void mk_xor(expr * a, expr * b, expr_ref & r) { s.mk_xor(a, b, r); } + void mk_xor(expr * a, expr * b, expr_ref & r) { m_rw.mk_xor(a, b, r); } void mk_xor3(expr * a, expr * b, expr * c, expr_ref & r); void mk_carry(expr * a, expr * b, expr * c, expr_ref & r); - void mk_iff(expr * a, expr * b, expr_ref & r) { s.mk_iff(a, b, r); } - void mk_and(expr * a, expr * b, expr_ref & r) { s.mk_and(a, b, r); } - void mk_and(expr * a, expr * b, expr * c, expr_ref & r) { s.mk_and(a, b, c, r); } - void mk_and(unsigned sz, expr * const * args, expr_ref & r) { s.mk_and(sz, args, r); } - void mk_or(expr * a, expr * b, expr_ref & r) { s.mk_or(a, b, r); } - void mk_or(expr * a, expr * b, expr * c, expr_ref & r) { s.mk_or(a, b, c, r); } - void mk_or(unsigned sz, expr * const * args, expr_ref & r) { s.mk_or(sz, args, r); } - void mk_not(expr * a, expr_ref & r) { s.mk_not(a, r); } - void mk_ite(expr * c, expr * t, expr * e, expr_ref & r) { s.mk_ite(c, t, e, r); } - void mk_nand(expr * a, expr * b, expr_ref & r) { s.mk_nand(a, b, r); } - void mk_nor(expr * a, expr * b, expr_ref & r) { s.mk_nor(a, b, r); } + void mk_iff(expr * a, expr * b, expr_ref & r) { m_rw.mk_iff(a, b, r); } + void mk_and(expr * a, expr * b, expr_ref & r) { m_rw.mk_and(a, b, r); } + void mk_and(expr * a, expr * b, expr * c, expr_ref & r) { m_rw.mk_and(a, b, c, r); } + void mk_and(unsigned sz, expr * const * args, expr_ref & r) { m_rw.mk_and(sz, args, r); } + void mk_or(expr * a, expr * b, expr_ref & r) { m_rw.mk_or(a, b, r); } + void mk_or(expr * a, expr * b, expr * c, expr_ref & r) { m_rw.mk_or(a, b, c, r); } + void mk_or(unsigned sz, expr * const * args, expr_ref & r) { m_rw.mk_or(sz, args, r); } + void mk_not(expr * a, expr_ref & r) { m_rw.mk_not(a, r); } + void mk_ite(expr * c, expr * t, expr * e, expr_ref & r) { m_rw.mk_ite(c, t, e, r); } + void mk_nand(expr * a, expr * b, expr_ref & r) { m_rw.mk_nand(a, b, r); } + void mk_nor(expr * a, expr * b, expr_ref & r) { m_rw.mk_nor(a, b, r); } }; class bit_blaster : public bit_blaster_tpl { bv_util m_util; - basic_simplifier_plugin m_simp; + bool_rewriter m_rw; public: bit_blaster(ast_manager & m, bit_blaster_params const & params); bit_blaster_params const & get_params() const { return this->m_params; } diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp index bf9e7f394..49c68fedf 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp +++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp @@ -362,6 +362,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend); return BR_FAILED; } + if (m().is_ite(f)) { SASSERT(num == 3); if (butil().is_bv(args[1])) { diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h index 813c0cd1c..15b87697f 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h @@ -23,6 +23,7 @@ Revision History: #include"common_msgs.h" #include"rewriter_types.h" + template void bit_blaster_tpl::checkpoint() { if (memory::get_allocation_size() > m_max_memory) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 89b9bb90f..c65f51144 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -875,6 +875,10 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) { if (m().is_false(cond)) { continue; } + if (m().is_true(cond)) { + add_next(next, trail, mv.dst(), acc); + continue; + } expr* args[2] = { cond, acc }; cond = mk_and(m(), 2, args); add_next(next, trail, mv.dst(), cond); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 0eac9d316..f3e696879 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -173,6 +173,9 @@ std::string zstring::encode() const { if (0 <= ch && ch < 32) { strm << esc_table[ch]; } + else if (ch == '\\') { + strm << "\\\\"; + } else { strm << (char)(ch); } diff --git a/src/ast/simplifier/seq_simplifier_plugin.cpp b/src/ast/simplifier/seq_simplifier_plugin.cpp new file mode 100644 index 000000000..e31d6812c --- /dev/null +++ b/src/ast/simplifier/seq_simplifier_plugin.cpp @@ -0,0 +1,39 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + seq_simplifier_plugin.cpp + +Abstract: + + Simplifier for the floating-point theory + +Author: + + Nikolaj Bjorner (nbjorner) 2016-02-05 + +--*/ +#include"seq_simplifier_plugin.h" + +seq_simplifier_plugin::seq_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b) : +simplifier_plugin(symbol("seq"), m), +m_util(m), +m_rw(m) {} + +seq_simplifier_plugin::~seq_simplifier_plugin() {} + +bool seq_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { + set_reduce_invoked(); + + SASSERT(f->get_family_id() == get_family_id()); + + return m_rw.mk_app_core(f, num_args, args, result) != BR_FAILED; +} + +bool seq_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & result) { + set_reduce_invoked(); + + return m_rw.mk_eq_core(lhs, rhs, result) != BR_FAILED; +} + diff --git a/src/ast/simplifier/seq_simplifier_plugin.h b/src/ast/simplifier/seq_simplifier_plugin.h new file mode 100644 index 000000000..45668678c --- /dev/null +++ b/src/ast/simplifier/seq_simplifier_plugin.h @@ -0,0 +1,39 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + seq_simplifier_plugin.h + +Abstract: + + Simplifier for the sequence theory + +Author: + + Nikolaj Bjorner (nbjorner) 2016-02-05 + +--*/ +#ifndef SEQ_SIMPLIFIER_PLUGIN_H_ +#define SEQ_SIMPLIFIER_PLUGIN_H_ + +#include"basic_simplifier_plugin.h" +#include"seq_decl_plugin.h" +#include"seq_rewriter.h" + +class seq_simplifier_plugin : public simplifier_plugin { + seq_util m_util; + seq_rewriter m_rw; + +public: + seq_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b); + ~seq_simplifier_plugin(); + + + virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); + + virtual bool reduce_eq(expr * lhs, expr * rhs, expr_ref & result); + +}; + +#endif /* SEQ_SIMPLIFIER_PLUGIN_H_ */ diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 6543bddad..df4b528fd 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -23,6 +23,7 @@ Revision History: #include"array_simplifier_plugin.h" #include"datatype_simplifier_plugin.h" #include"fpa_simplifier_plugin.h" +#include"seq_simplifier_plugin.h" #include"bv_simplifier_plugin.h" #include"for_each_expr.h" #include"well_sorted.h" @@ -98,6 +99,7 @@ void asserted_formulas::setup_simplifier_plugins(simplifier & s, basic_simplifie s.register_plugin(bvsimp); s.register_plugin(alloc(datatype_simplifier_plugin, m_manager, *bsimp)); s.register_plugin(alloc(fpa_simplifier_plugin, m_manager, *bsimp)); + s.register_plugin(alloc(seq_simplifier_plugin, m_manager, *bsimp)); } void asserted_formulas::init(unsigned num_formulas, expr * const * formulas, proof * const * prs) {