mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-20 07:36:38 +00:00
Code Activity

update slicing to fix unbound variables. test datatype realizer

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-11-04 14:15:24 +02:00
parent bfbdad3ce6
commit 37a13b1d09
3 changed files with 59 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/muz_qe/dl_mk_slice.cpp
View file

@ -732,7 +732,7 @@ namespace datalog {
void mk_slice::update_rule(rule& r, rule_set& dst) {
rule* new_rule;
rule_ref new_rule(rm);
if (rule_updated(r)) {
init_vars(r);
app_ref_vector tail(m);
@ -794,16 +794,20 @@ namespace datalog {
}
new_rule = rm.mk(head.get(), tail.size(), tail.c_ptr(), (const bool*) 0);
rm.fix_unbound_vars(new_rule, false);
TRACE("dl", r.display(m_ctx, tout << "replacing:\n"); new_rule->display(m_ctx, tout << "by:\n"););
}
else {
new_rule = &r;
}
dst.add_rule(new_rule);
dst.add_rule(new_rule.get());
if (m_pc) {
m_pc->insert(&r, new_rule, 0, 0);
m_pc->insert(&r, new_rule.get(), 0, 0);
}
}

47
src/muz_qe/qe_datatype_plugin.cpp
View file

@ -133,7 +133,7 @@ namespace qe {
func_decl* f = a->get_decl();
if (m_util.is_recognizer(f) && a->get_arg(0) == x) {
m_recognizers.push_back(a);
TRACE("quant_elim", tout << "add recognizer:" << mk_pp(a, m) << "\n";);
TRACE("qe", tout << "add recognizer:" << mk_pp(a, m) << "\n";);
return true;
}
if (!m.is_eq(a)) {
@ -161,6 +161,10 @@ namespace qe {
unsigned num_neqs() { return m_neq_atoms.size(); }
app* neq_atom(unsigned i) { return m_neq_atoms[i].get(); }
unsigned num_neq_terms() const { return m_neqs.size(); }
expr* neq_term(unsigned i) const { return m_neqs[i]; }
expr* const* neq_terms() const { return m_neqs.c_ptr(); }
unsigned num_recognizers() { return m_recognizers.size(); }
app* recognizer(unsigned i) { return m_recognizers[i].get(); }
@ -212,7 +216,7 @@ namespace qe {
}
void add_atom(app* a, bool is_pos) {
TRACE("quant_elim", tout << "add atom:" << mk_pp(a, m) << " " << (is_pos?"pos":"neg") << "\n";);
TRACE("qe", tout << "add atom:" << mk_pp(a, m) << " " << (is_pos?"pos":"neg") << "\n";);
if (is_pos) {
m_eq_atoms.push_back(a);
}
@ -326,7 +330,7 @@ namespace qe {
for_each_expr(*this, fml.get());
if (m_change) {
fml = get_expr(fml.get());
TRACE("quant_elim", tout << "lift:\n" << mk_pp(fml.get(), m) << "\n";);
TRACE("qe", tout << "lift:\n" << mk_pp(fml.get(), m) << "\n";);
}
return m_change;
}
@ -380,7 +384,7 @@ namespace qe {
}
expr* e = m.mk_and(conj.size(), conj.c_ptr());
m_map.insert(a, e, 0);
TRACE("quant_elim", tout << "replace: " << mk_pp(a, m) << " ==> \n" << mk_pp(e, m) << "\n";);
TRACE("qe", tout << "replace: " << mk_pp(a, m) << " ==> \n" << mk_pp(e, m) << "\n";);
return true;
}
@ -456,7 +460,7 @@ namespace qe {
virtual void assign(contains_app& x, expr* fml, rational const& vl) {
sort* s = x.x()->get_decl()->get_range();
SASSERT(m_datatype_util.is_datatype(s));
TRACE("quant_elim", tout << mk_pp(x.x(), m) << " " << vl << "\n";);
TRACE("qe", tout << mk_pp(x.x(), m) << " " << vl << "\n";);
if (m_datatype_util.is_recursive(s)) {
assign_rec(x, fml, vl);
}
@ -468,16 +472,13 @@ namespace qe {
virtual void subst(contains_app& x, rational const& vl, expr_ref& fml, expr_ref* def) {
sort* s = x.x()->get_decl()->get_range();
SASSERT(m_datatype_util.is_datatype(s));
TRACE("quant_elim", tout << mk_pp(x.x(), m) << " " << vl << "\n";);
TRACE("qe", tout << mk_pp(x.x(), m) << " " << vl << "\n";);
if (m_datatype_util.is_recursive(s)) {
subst_rec(x, vl, fml, def);
}
else {
subst_nonrec(x, vl, fml, def);
}
if (def) {
*def = 0; // TBD
}
}
virtual unsigned get_weight( contains_app& x, expr* fml) {
@ -605,7 +606,7 @@ namespace qe {
num_branches = rational(eqs.num_eqs() + 1);
return true;
}
TRACE("quant_elim", tout << "could not get number of branches " << mk_pp(x.x(), m) << "\n";);
TRACE("qe", tout << "could not get number of branches " << mk_pp(x.x(), m) << "\n";);
return false;
}
@ -660,6 +661,7 @@ namespace qe {
SASSERT(m_datatype_util.is_datatype(s));
func_decl* c = 0, *r = 0;
TRACE("qe", tout << mk_pp(x, m) << " " << vl << " " << mk_pp(fml, m) << " " << (def != 0) << "\n";);
//
// Add recognizer to formula.
// Introduce auxiliary variable to eliminate.
@ -673,13 +675,13 @@ namespace qe {
m_ctx.add_var(fresh_x);
m_replace->apply_substitution(x, fresh_x, 0, fml);
add_def(fresh_x, def);
TRACE("quant_elim", tout << "Add recognizer " << mk_pp(is_c, m) << "\n";);
TRACE("qe", tout << "Add recognizer " << mk_pp(is_c, m) << "\n";);
return;
}
if (has_selector(contains_x, fml, c)) {
TRACE("quant_elim", tout << "Eliminate selector " << mk_ll_pp(c, m) << "\n";);
TRACE("qe", tout << "Eliminate selector " << mk_ll_pp(c, m) << "\n";);
subst_constructor(contains_x, c, fml, def);
return;
}
@ -721,14 +723,19 @@ namespace qe {
}
for (unsigned i = 0; i < eqs.num_neqs(); ++i) {
m_replace->apply_substitution(eqs.neq_atom(i), m.mk_true(), fml);
m_replace->apply_substitution(eqs.neq_atom(i), m.mk_false(), fml);
}
if (def) {
NOT_IMPLEMENTED_YET();
// you need to create a diagonal term
sort* s = m.get_sort(x);
ptr_vector<sort> sorts;
sorts.resize(eqs.num_neq_terms(), s);
func_decl* diag = m.mk_func_decl(symbol("diag"), sorts.size(), sorts.c_ptr(), s);
expr_ref t(m);
t = m.mk_app(diag, eqs.num_neq_terms(), eqs.neq_terms());
add_def(t, def);
}
}
TRACE("quant_elim", tout << "reduced " << mk_pp(fml.get(), m) << "\n";);
TRACE("qe", tout << "reduced " << mk_pp(fml.get(), m) << "\n";);
}
bool get_num_branches_nonrec( contains_app& x, expr* fml, rational& num_branches) {
@ -738,10 +745,10 @@ namespace qe {
func_decl* c = 0, *r = 0;
if (sz != 1 && has_recognizer(x.x(), fml, r, c)) {
TRACE("quant_elim", tout << mk_pp(x.x(), m) << " has a recognizer\n";);
TRACE("qe", tout << mk_pp(x.x(), m) << " has a recognizer\n";);
num_branches = rational(1);
}
TRACE("quant_elim", tout << mk_pp(x.x(), m) << " branches: " << sz << "\n";);
TRACE("qe", tout << mk_pp(x.x(), m) << " branches: " << sz << "\n";);
return true;
}
@ -757,7 +764,7 @@ namespace qe {
}
func_decl* c = 0, *r = 0;
if (has_recognizer(x, fml, r, c)) {
TRACE("quant_elim", tout << mk_pp(x, m) << " has a recognizer\n";);
TRACE("qe", tout << mk_pp(x, m) << " has a recognizer\n";);
return;
}
@ -776,7 +783,7 @@ namespace qe {
SASSERT(!m_datatype_util.is_recursive(s));
func_decl* c = 0, *r = 0;
if (has_recognizer(x.x(), fml, r, c)) {
TRACE("quant_elim", tout << mk_pp(x.x(), m) << " has a recognizer\n";);
TRACE("qe", tout << mk_pp(x.x(), m) << " has a recognizer\n";);
}
else {
unsigned sz = m_datatype_util.get_datatype_num_constructors(s);

36
src/test/quant_solve.cpp
View file

@ -77,7 +77,7 @@ static void validate_quant_solutions(app* x, expr* fml, expr_ref_vector& guards)
#endif
static void test_quant_solver(ast_manager& m, unsigned sz, app*const* xs, expr* fml) {
static void test_quant_solver(ast_manager& m, unsigned sz, app*const* xs, expr* fml, bool validate) {
front_end_params params;
qe::expr_quant_elim qe(m, params);
qe::guarded_defs defs(m);
@ -86,7 +86,8 @@ static void test_quant_solver(ast_manager& m, unsigned sz, app*const* xs, expr*
std::cout << mk_pp(fml, m) << "\n";
if (success) {
defs.display(std::cout);
for (unsigned i = 0; i < defs.size(); ++i) {
for (unsigned i = 0; validate && i < defs.size(); ++i) {
validate_quant_solution(m, fml, defs.guard(i), defs.defs(i));
}
}
@ -106,6 +107,10 @@ static expr_ref parse_fml(ast_manager& m, char const* str) {
<< "(declare-const z Int)\n"
<< "(declare-const a Int)\n"
<< "(declare-const b Int)\n"
<< "(declare-const P Bool)\n"
<< "(declare-const Q Bool)\n"
<< "(declare-const r1 Real)\n"
<< "(declare-const r2 Real)\n"
<< "(declare-datatypes () ((IList (nil) (cons (car Int) (cdr IList)))))\n"
<< "(declare-const l1 IList)\n"
<< "(declare-const l2 IList)\n"
@ -140,21 +145,21 @@ static void parse_fml(char const* str, app_ref_vector& vars, expr_ref& fml) {
}
}
static void test_quant_solver(ast_manager& m, app* x, char const* str) {
static void test_quant_solver(ast_manager& m, app* x, char const* str, bool validate = true) {
expr_ref fml = parse_fml(m, str);
test_quant_solver(m, 1, &x, fml);
test_quant_solver(m, 1, &x, fml, validate);
}
static void test_quant_solver(ast_manager& m, unsigned sz, app*const* xs, char const* str) {
static void test_quant_solver(ast_manager& m, unsigned sz, app*const* xs, char const* str, bool validate = true) {
expr_ref fml = parse_fml(m, str);
test_quant_solver(m, sz, xs, fml);
test_quant_solver(m, sz, xs, fml, validate);
}
static void test_quant_solver(ast_manager& m, char const* str) {
static void test_quant_solver(ast_manager& m, char const* str, bool validate = true) {
expr_ref fml(m);
app_ref_vector vars(m);
parse_fml(str, vars, fml);
test_quant_solver(m, vars.size(), vars.c_ptr(), fml);
test_quant_solver(m, vars.size(), vars.c_ptr(), fml, validate);
}
@ -222,9 +227,18 @@ static void test_quant_solve1() {
test_quant_solver(m, "(exists ((c Cell)) (= c null))");
test_quant_solver(m, "(exists ((c Cell)) (= c (cell null c1)))");
//TBD:
//test_quant_solver(m, "(exists ((c Cell)) (= (cell c c) c1))");
//test_quant_solver(m, "(exists ((c Cell)) (not (= c null)))");
test_quant_solver(m, "(exists ((c Cell)) (not (= c null)))", false);
test_quant_solver(m, "(exists ((c Cell)) (= (cell c c) c1))", false);
test_quant_solver(m, "(exists ((c Cell)) (= (cell c (cdr c1)) c1))", false);
test_quant_solver(m, "(exists ((t Tuple)) (= (tuple a P r1) t))");
test_quant_solver(m, "(exists ((t Tuple)) (= a (first t)))");
test_quant_solver(m, "(exists ((t Tuple)) (= P (second t)))");
test_quant_solver(m, "(exists ((t Tuple)) (= r2 (third t)))");
test_quant_solver(m, "(exists ((t Tuple)) (not (= a (first t))))");
test_quant_solver(m, "(exists ((t Tuple)) (not (= P (second t))))");
test_quant_solver(m, "(exists ((t Tuple)) (not (= r2 (third t))))");
}