From 2ea9bfaa41652303b50ece8afc5a7af6908ddb08 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 6 Sep 2017 13:34:41 -0700 Subject: [PATCH] remove unstable sequence interpolant from doc test Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 6 +-- src/ast/ast_ll_pp.cpp | 2 +- src/ast/rewriter/bool_rewriter.cpp | 76 +++++++----------------------- src/ast/rewriter/rewriter_def.h | 7 +-- src/ast/rewriter/th_rewriter.cpp | 1 + src/smt/asserted_formulas.cpp | 4 ++ src/smt/asserted_formulas.h | 1 + src/smt/tactic/smt_tactic.cpp | 1 + 8 files changed, 31 insertions(+), 67 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 1452a037e..39af03190 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -8185,9 +8185,9 @@ def sequence_interpolant(v,p=None,ctx=None): If parameters p are supplied, these are used in creating the solver that determines satisfiability. - >>> x = Int('x') - >>> y = Int('y') - >>> print(sequence_interpolant([x < 0, y == x , y > 2])) + x = Int('x') + y = Int('y') + print(sequence_interpolant([x < 0, y == x , y > 2])) [Not(x >= 0), Not(y >= 0)] """ f = v[0] diff --git a/src/ast/ast_ll_pp.cpp b/src/ast/ast_ll_pp.cpp index 6b14b75a8..c00053780 100644 --- a/src/ast/ast_ll_pp.cpp +++ b/src/ast/ast_ll_pp.cpp @@ -284,7 +284,7 @@ public: } unsigned num_args = to_app(n)->get_num_args(); if (num_args > 0) - m_out << "(_ "; + m_out << "("; display_name(to_app(n)->get_decl()); display_params(to_app(n)->get_decl()); for (unsigned i = 0; i < num_args; i++) { diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 44fccb49e..6e99cb23e 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -629,61 +629,23 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result) return BR_REWRITE2; } } - expr* cond2, *t2, *e2; - if (m().is_ite(t, cond2, t2, e2) && m().is_value(t2) && m().is_value(e2)) { - try_ite_value(to_app(t), val, result); - result = m().mk_ite(cond, result, m().mk_eq(e, val)); - return BR_REWRITE2; - } - if (m().is_ite(e, cond2, t2, e2) && m().is_value(t2) && m().is_value(e2)) { - try_ite_value(to_app(e), val, result); - result = m().mk_ite(cond, m().mk_eq(t, val), result); - return BR_REWRITE2; + { + expr* cond2, *t2, *e2; + if (m().is_ite(t, cond2, t2, e2) && m().is_value(t2) && m().is_value(e2)) { + try_ite_value(to_app(t), val, result); + result = m().mk_ite(cond, result, m().mk_eq(e, val)); + return BR_REWRITE2; + } + if (m().is_ite(e, cond2, t2, e2) && m().is_value(t2) && m().is_value(e2)) { + try_ite_value(to_app(e), val, result); + result = m().mk_ite(cond, m().mk_eq(t, val), result); + return BR_REWRITE2; + } } return BR_FAILED; } -#if 0 -// Return true if ite is an if-then-else tree where the leaves are values, -// and they are all different from val -static bool is_ite_value_tree_neq_value(ast_manager & m, app * ite, app * val) { - SASSERT(m.is_ite(ite)); - SASSERT(m.is_value(val)); - - expr_fast_mark1 visited; - ptr_buffer todo; - todo.push_back(ite); - -#define VISIT(ARG) { \ - if (m.is_value(ARG)) { \ - if (ARG == val) \ - return false; \ - } \ - else if (m.is_ite(ARG)) { \ - if (!visited.is_marked(ARG)) { \ - visited.mark(ARG); \ - todo.push_back(to_app(ARG)); \ - } \ - } \ - else { \ - return false; \ - } \ - } - - while (!todo.empty()) { - app * ite = todo.back(); - todo.pop_back(); - SASSERT(m.is_ite(ite)); - expr * t = ite->get_arg(1); - expr * e = ite->get_arg(2); - VISIT(t); - VISIT(e); - } - - return true; -} -#endif br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { if (m().are_equal(lhs, rhs)) { @@ -697,26 +659,20 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { } br_status r = BR_FAILED; + if (m().is_ite(lhs) && m().is_value(rhs)) { - // if (is_ite_value_tree_neq_value(m(), to_app(lhs), to_app(rhs))) { - // result = m().mk_false(); - // return BR_DONE; - // } r = try_ite_value(to_app(lhs), to_app(rhs), result); CTRACE("try_ite_value", r != BR_FAILED, - tout << mk_ismt2_pp(lhs, m()) << "\n" << mk_ismt2_pp(rhs, m()) << "\n--->\n" << mk_ismt2_pp(result, m()) << "\n";); + tout << mk_bounded_pp(lhs, m()) << "\n" << mk_bounded_pp(rhs, m()) << "\n--->\n" << mk_bounded_pp(result, m()) << "\n";); } else if (m().is_ite(rhs) && m().is_value(lhs)) { - // if (is_ite_value_tree_neq_value(m(), to_app(rhs), to_app(lhs))) { - // result = m().mk_false(); - // return BR_DONE; - // } r = try_ite_value(to_app(rhs), to_app(lhs), result); CTRACE("try_ite_value", r != BR_FAILED, - tout << mk_ismt2_pp(lhs, m()) << "\n" << mk_ismt2_pp(rhs, m()) << "\n--->\n" << mk_ismt2_pp(result, m()) << "\n";); + tout << mk_bounded_pp(lhs, m()) << "\n" << mk_bounded_pp(rhs, m()) << "\n--->\n" << mk_bounded_pp(result, m()) << "\n";); } if (r != BR_FAILED) return r; + if (m().is_bool(lhs)) { bool unfolded = false; diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index c511f00d0..42f268379 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -18,6 +18,7 @@ Notes: --*/ #include "ast/rewriter/rewriter.h" #include "ast/ast_smt2_pp.h" +#include "ast/ast_ll_pp.h" template template @@ -259,10 +260,10 @@ void rewriter_tpl::process_app(app * t, frame & fr) { } br_status st = m_cfg.reduce_app(f, new_num_args, new_args, m_r, m_pr2); SASSERT(st != BR_DONE || m().get_sort(m_r) == m().get_sort(t)); - TRACE("reduce_app", - tout << mk_ismt2_pp(t, m()) << "\n"; + CTRACE("reduce_app", st != BR_FAILED, + tout << mk_bounded_pp(t, m()) << "\n"; tout << "st: " << st; - if (m_r) tout << " --->\n" << mk_ismt2_pp(m_r, m()); + if (m_r) tout << " --->\n" << mk_bounded_pp(m_r, m()); tout << "\n";); if (st != BR_FAILED) { result_stack().shrink(fr.m_spos); diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index a2ca12b24..dd431bf85 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -736,6 +736,7 @@ ast_manager & th_rewriter::m() const { void th_rewriter::updt_params(params_ref const & p) { m_params = p; m_imp->cfg().updt_params(p); + IF_VERBOSE(10, verbose_stream() << p << "\n";); } void th_rewriter::get_param_descrs(param_descrs & r) { diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index ebdda73a1..c8670bd36 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -60,6 +60,7 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p): m_macro_finder = alloc(macro_finder, m, m_macro_manager); + m_elim_and = true; set_eliminate_and(false); } @@ -118,7 +119,10 @@ void asserted_formulas::push_assertion(expr * e, proof * pr, vector m_formulas; unsigned m_qhead; + bool m_elim_and; macro_manager m_macro_manager; scoped_ptr m_macro_finder; maximize_bv_sharing_rw m_bv_sharing; diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index f2dc83cfe..57ac7b34b 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -150,6 +150,7 @@ public: proof_converter_ref & pc, expr_dependency_ref & core) { try { + IF_VERBOSE(10, verbose_stream() << "(smt.tactic start)\n";); mc = 0; pc = 0; core = 0; SASSERT(in->is_well_sorted()); ast_manager & m = in->m();