mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

remove unstable sequence interpolant from doc test

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-09-06 13:34:41 -07:00
parent 7f127cdd5d
commit 2ea9bfaa41
8 changed files with 31 additions and 67 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/api/python/z3/z3.py
View file

@ -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]

2
src/ast/ast_ll_pp.cpp
View file

@ -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++) {

56
src/ast/rewriter/bool_rewriter.cpp
View file

@ -629,6 +629,7 @@ 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);
@ -640,50 +641,11 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & 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<app> 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,27 +659,21 @@ 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;
if (m().is_not(lhs) && m().is_not(rhs)) {

7
src/ast/rewriter/rewriter_def.h
View file

@ -18,6 +18,7 @@ Notes:
--*/
#include "ast/rewriter/rewriter.h"
#include "ast/ast_smt2_pp.h"
#include "ast/ast_ll_pp.h"
template<typename Config>
template<bool ProofGen>
@ -259,10 +260,10 @@ void rewriter_tpl<Config>::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);

1
src/ast/rewriter/th_rewriter.cpp
View file

@ -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) {

4
src/smt/asserted_formulas.cpp
View file

@ -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<justified_ex
}
void asserted_formulas::set_eliminate_and(bool flag) {
if (flag == m_elim_and) return;
m_elim_and = flag;
params_ref p;
p.set_bool("pull_cheap_ite", false);
p.set_bool("elim_and", flag);
p.set_bool("arith_ineq_lhs", true);
p.set_bool("sort_sums", true);

1
src/smt/asserted_formulas.h
View file

@ -52,6 +52,7 @@ class asserted_formulas {
static_features m_static_features;
vector<justified_expr> m_formulas;
unsigned m_qhead;
bool m_elim_and;
macro_manager m_macro_manager;
scoped_ptr<macro_finder> m_macro_finder;
maximize_bv_sharing_rw m_bv_sharing;

1
src/smt/tactic/smt_tactic.cpp
View file

@ -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();