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

working on pdr gen

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-02-08 16:54:05 -08:00
parent 2e2fa84d40
commit 3ad43c60a9
3 changed files with 93 additions and 41 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/ast/ast.cpp
View file

@ -1836,14 +1836,17 @@ func_decl * ast_manager::mk_func_decl(symbol const & name, unsigned arity, sort
} }
void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * const * args) const { void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * const * args) const {
ast_manager& m = const_cast<ast_manager&>(*this);
if (decl->is_associative()) { if (decl->is_associative()) {
sort * expected = decl->get_domain(0); sort * expected = decl->get_domain(0);
for (unsigned i = 0; i < num_args; i++) { for (unsigned i = 0; i < num_args; i++) {
sort * given = get_sort(args[i]); sort * given = get_sort(args[i]);
if (!compatible_sorts(expected, given)) { if (!compatible_sorts(expected, given)) {
string_buffer<> buff; std::ostringstream buff;
buff << "invalid function application, sort mismatch on argument at position " << (i+1); buff << "Invalid function application for " << decl->get_name() << ". ";
throw ast_exception(buff.c_str()); buff << "Sort mismatch on argument at position " << (i+1) << ". ";
buff << "Expected: " << mk_pp(expected, m) << " but given " << mk_pp(given, m);
throw ast_exception(buff.str().c_str());
} }
} }
} }
@ -1855,9 +1858,11 @@ void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * c
sort * expected = decl->get_domain(i); sort * expected = decl->get_domain(i);
sort * given = get_sort(args[i]); sort * given = get_sort(args[i]);
if (!compatible_sorts(expected, given)) { if (!compatible_sorts(expected, given)) {
string_buffer<> buff; std::ostringstream buff;
buff << "invalid function application, sort mismatch on argument at position " << (i+1); buff << "Invalid function application for " << decl->get_name() << ". ";
throw ast_exception(buff.c_str()); buff << "Sort mismatch on argument at position " << (i+1) << ". ";
buff << "Expected: " << mk_pp(expected, m) << " but given " << mk_pp(given, m);
throw ast_exception(buff.str().c_str());
} }
} }
} }

22
src/ast/ast_ll_pp.cpp
View file

@ -126,7 +126,21 @@ public:
m_autil(m) { m_autil(m) {
} }
void operator()(sort * n) { void pp(ast* n) {
ast_mark visited;
pp(n, visited);
}
void pp(ast* n, ast_mark& visited) {
if (is_sort(n)) {
display_sort(to_sort(n));
}
else {
for_each_ast(*this, visited, n, true);
}
}
void operator()(sort* n) {
} }
void operator()(func_decl * n) { void operator()(func_decl * n) {
@ -296,17 +310,17 @@ public:
void ast_ll_pp(std::ostream & out, ast_manager & m, ast * n, bool only_exprs, bool compact) { void ast_ll_pp(std::ostream & out, ast_manager & m, ast * n, bool only_exprs, bool compact) {
ll_printer p(out, m, n, only_exprs, compact); ll_printer p(out, m, n, only_exprs, compact);
for_each_ast(p, n, true); p.pp(n);
} }
void ast_ll_pp(std::ostream & out, ast_manager & m, ast * n, ast_mark & visited, bool only_exprs, bool compact) { void ast_ll_pp(std::ostream & out, ast_manager & m, ast * n, ast_mark & visited, bool only_exprs, bool compact) {
ll_printer p(out, m, n, only_exprs, compact); ll_printer p(out, m, n, only_exprs, compact);
for_each_ast(p, visited, n, true); p.pp(n, visited);
} }
void ast_def_ll_pp(std::ostream & out, ast_manager & m, ast * n, ast_mark & visited, bool only_exprs, bool compact) { void ast_def_ll_pp(std::ostream & out, ast_manager & m, ast * n, ast_mark & visited, bool only_exprs, bool compact) {
ll_printer p(out, m, 0, only_exprs, compact); ll_printer p(out, m, 0, only_exprs, compact);
for_each_ast(p, visited, n, true); p.pp(n, visited);
} }
void ast_ll_bounded_pp(std::ostream & out, ast_manager & m, ast * n, unsigned depth) { void ast_ll_bounded_pp(std::ostream & out, ast_manager & m, ast * n, unsigned depth) {

95
src/muz_qe/pdr_generalizers.cpp
View file

@ -147,8 +147,12 @@ namespace pdr {
} }
// ----------------------------- // ---------------------------------
// core_arith_inductive_generalizer // core_arith_inductive_generalizer
// NB. this is trying out some ideas for generalization in
// an ad hoc specialized way. arith_inductive_generalizer should
// not be used by default. It is a place-holder for a general purpose
// extrapolator of a lattice basis.
core_arith_inductive_generalizer::core_arith_inductive_generalizer(context& ctx): core_arith_inductive_generalizer::core_arith_inductive_generalizer(context& ctx):
core_generalizer(ctx), core_generalizer(ctx),
@ -168,42 +172,50 @@ namespace pdr {
svector<eq> eqs; svector<eq> eqs;
get_eqs(core, eqs); get_eqs(core, eqs);
if (eqs.empty()) {
return;
}
expr_ref_vector new_core(m);
new_core.append(core);
for (unsigned eq = 0; eq < eqs.size(); ++eq) { for (unsigned eq = 0; eq < eqs.size(); ++eq) {
rational r = eqs[eq].m_value; rational r = eqs[eq].m_value;
expr* x = eqs[eq].m_term; expr* x = eqs[eq].m_term;
unsigned k = eqs[eq].m_i; unsigned k = eqs[eq].m_i;
unsigned l = eqs[eq].m_j; unsigned l = eqs[eq].m_j;
expr_ref_vector new_core(m); new_core[l] = m.mk_true();
for (unsigned i = 0; i < core.size(); ++i) { new_core[k] = m.mk_true();
if (i == k || k == l) {
new_core.push_back(m.mk_true()); for (unsigned i = 0; i < new_core.size(); ++i) {
} if (substitute_alias(r, x, new_core[i].get(), e)) {
else { new_core[i] = e;
if (!substitute_alias(r, x, core[i].get(), e)) {
e = core[i].get();
}
new_core.push_back(e);
} }
} }
if (abs(r) >= rational(2) && a.is_int(x)) { if (abs(r) >= rational(2) && a.is_int(x)) {
new_core[k] = m.mk_eq(a.mk_mod(x, a.mk_numeral(abs(r), true)), a.mk_numeral(rational(0), true)); new_core[k] = m.mk_eq(a.mk_mod(x, a.mk_numeral(rational(2), true)), a.mk_numeral(rational(0), true));
new_core[l] = a.mk_ge(x, a.mk_numeral(r, true)); new_core[l] = a.mk_le(x, a.mk_numeral(rational(0), true));
} }
}
bool inductive = n.pt().check_inductive(n.level(), new_core, uses_level); bool inductive = n.pt().check_inductive(n.level(), new_core, uses_level);
IF_VERBOSE(1, IF_VERBOSE(1,
verbose_stream() << (inductive?"":"non") << "inductive\n"; verbose_stream() << (inductive?"":"non") << "inductive\n";
for (unsigned j = 0; j < new_core.size(); ++j) { verbose_stream() << "old\n";
verbose_stream() << mk_pp(new_core[j].get(), m) << "\n"; for (unsigned j = 0; j < core.size(); ++j) {
}); verbose_stream() << mk_pp(core[j].get(), m) << "\n";
}
if (inductive) { verbose_stream() << "new\n";
core.reset(); for (unsigned j = 0; j < new_core.size(); ++j) {
core.append(new_core); verbose_stream() << mk_pp(new_core[j].get(), m) << "\n";
} });
if (inductive) {
core.reset();
core.append(new_core);
} }
} }
@ -289,13 +301,34 @@ namespace pdr {
result = m.mk_not(result); result = m.mk_not(result);
return true; return true;
} }
if (a.is_le(e, y, z) && a.is_numeral(z, r2) && r == r2) { if (a.is_le(e, y, z) && a.is_numeral(z, r2)) {
result = a.mk_le(y, x); if (r == r2) {
return true; result = a.mk_le(y, x);
return true;
}
if (r == r2 + rational(1)) {
result = a.mk_lt(y, x);
return true;
}
if (r == r2 - rational(1)) {
result = a.mk_le(y, a.mk_sub(x, a.mk_numeral(rational(1), a.is_int(x))));
return true;
}
} }
if (a.is_ge(e, y, z) && a.is_numeral(z, r2) && r == r2) { if (a.is_ge(e, y, z) && a.is_numeral(z, r2)) {
result = a.mk_ge(y, x); if (r == r2) {
return true; result = a.mk_ge(y, x);
return true;
}
if (r2 == r + rational(1)) {
result = a.mk_gt(y, x);
return true;
}
if (r2 == r - rational(1)) {
result = a.mk_ge(y, a.mk_sub(x, a.mk_numeral(rational(1), a.is_int(x))));
return true;
}
} }
return false; return false;
} }