mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-05 01:27:41 +00:00
Code Activity

merged

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-11-30 13:17:41 -08:00
commit 124c0339c1
53 changed files with 4995 additions and 4595 deletions
Download patch file Download diff file Expand all files Collapse all files

30
src/muz_qe/dl_context.cpp
View file

@ -995,6 +995,7 @@ namespace datalog {
p.insert("print_with_fixedpoint_extensions", CPK_BOOL, "(default true) use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules");
p.insert("print_low_level_smt2", CPK_BOOL, "(default false) use (faster) low-level SMT2 printer (the printer is scalable but the result may not be as readable)");
p.insert("print_with_variable_declarations", CPK_BOOL, "(default true) use variable declarations when displaying rules (instead of attempting to use original names)");
PRIVATE_PARAMS(
p.insert("dbg_fpr_nonempty_relation_signature", CPK_BOOL,
@ -1625,6 +1626,23 @@ namespace datalog {
void context::get_rules_as_formulas(expr_ref_vector& rules, svector<symbol>& names) {
expr_ref fml(m);
datalog::rule_manager& rm = get_rule_manager();
datalog::rule_ref_vector rule_refs(rm);
// ensure that rules are all using bound variables.
for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
ptr_vector<sort> sorts;
get_free_vars(m_rule_fmls[i].get(), sorts);
if (!sorts.empty()) {
rm.mk_rule(m_rule_fmls[i].get(), rule_refs, m_rule_names[i]);
m_rule_fmls[i] = m_rule_fmls.back();
m_rule_names[i] = m_rule_names.back();
m_rule_fmls.pop_back();
m_rule_names.pop_back();
--i;
}
}
add_rules(rule_refs);
rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end();
for (; it != end; ++it) {
(*it)->to_formula(fml);
@ -1652,6 +1670,7 @@ namespace datalog {
svector<symbol> names;
bool use_fixedpoint_extensions = m_params.get_bool("print_with_fixedpoint_extensions", true);
bool print_low_level = m_params.get_bool("print_low_level_smt2", false);
bool do_declare_vars = m_params.get_bool("print_with_variable_declarations", true);
#define PP(_e_) if (print_low_level) out << mk_smt_pp(_e_, m); else ast_smt2_pp(out, _e_, env, params);
@ -1708,7 +1727,7 @@ namespace datalog {
out << "))\n";
}
if (use_fixedpoint_extensions) {
if (use_fixedpoint_extensions && do_declare_vars) {
declare_vars(rules, fresh_names, out);
}
@ -1730,13 +1749,20 @@ namespace datalog {
}
PP(r);
if (symbol::null != nm) {
out << " :named ";
while (fresh_names.contains(nm)) {
std::ostringstream s;
s << nm << "!";
nm = symbol(s.str().c_str());
}
fresh_names.add(nm);
out << " :named " << nm << ")";
if (is_smt2_quoted_symbol(nm)) {
out << mk_smt2_quoted_symbol(nm);
}
else {
out << nm;
}
out << ")";
}
out << ")\n";
}

5
src/muz_qe/dl_mk_interp_tail_simplifier.cpp
View file

@ -461,6 +461,11 @@ namespace datalog {
{
rule_ref r(r0, m_context.get_rule_manager());
if (r->has_quantifiers()) {
res = r;
return false;
}
start:
unsigned u_len = r->get_uninterpreted_tail_size();
unsigned len = r->get_tail_size();

37
src/muz_qe/horn_tactic.cpp
View file

@ -90,21 +90,30 @@ class horn_tactic : public tactic {
m_ctx.register_predicate(to_app(a)->get_decl(), true);
}
void check_predicate(expr* a) {
expr* a1 = 0;
while (true) {
void check_predicate(ast_mark& mark, expr* a) {
ptr_vector<expr> todo;
todo.push_back(a);
while (!todo.empty()) {
a = todo.back();
todo.pop_back();
if (mark.is_marked(a)) {
continue;
}
mark.mark(a, true);
if (is_quantifier(a)) {
a = to_quantifier(a)->get_expr();
continue;
todo.push_back(a);
}
if (m.is_not(a, a1)) {
a = a1;
continue;
else if (m.is_not(a) || m.is_and(a) || m.is_or(a) || m.is_implies(a)) {
todo.append(to_app(a)->get_num_args(), to_app(a)->get_args());
}
if (is_predicate(a)) {
else if (m.is_ite(a)) {
todo.append(to_app(a)->get_arg(1));
todo.append(to_app(a)->get_arg(2));
}
else if (is_predicate(a)) {
register_predicate(a);
}
break;
}
}
@ -112,14 +121,15 @@ class horn_tactic : public tactic {
formula_kind get_formula_kind(expr_ref& f) {
normalize(f);
ast_mark mark;
expr_ref_vector args(m), body(m);
expr_ref head(m);
expr* a = 0, *a1 = 0;
datalog::flatten_or(f, args);
for (unsigned i = 0; i < args.size(); ++i) {
a = args[i].get();
check_predicate(a);
if (m.is_not(a, a1) && is_predicate(a1)) {
a = args[i].get();
check_predicate(mark, a);
if (m.is_not(a, a1)) {
body.push_back(a1);
}
else if (is_predicate(a)) {
@ -128,9 +138,6 @@ class horn_tactic : public tactic {
}
head = a;
}
else if (m.is_not(a, a1)) {
body.push_back(a1);
}
else {
body.push_back(m.mk_not(a));
}

6
src/muz_qe/pdr_context.cpp
View file

@ -1827,10 +1827,8 @@ namespace pdr {
proof_ref pr(m);
pr = m.mk_asserted(m.mk_true());
for (unsigned i = 0; i < vars.size(); ++i) {
if (smt::is_value_sort(m, vars[i].get())) {
tmp = mev.eval(M, vars[i].get());
sub.insert(vars[i].get(), tmp, pr);
}
tmp = mev.eval(M, vars[i].get());
sub.insert(vars[i].get(), tmp, pr);
}
if (!rep) rep = mk_expr_simp_replacer(m);
rep->set_substitution(&sub);

13
src/muz_qe/pdr_util.cpp
View file

@ -608,6 +608,7 @@ namespace pdr {
best effort evaluator of extensional array equality.
*/
void model_evaluator::eval_array_eq(app* e, expr* arg1, expr* arg2) {
TRACE("pdr", tout << "array equality: " << mk_pp(e, m) << "\n";);
expr_ref v1(m), v2(m);
m_model->eval(arg1, v1);
m_model->eval(arg2, v2);
@ -633,7 +634,10 @@ namespace pdr {
if (else1 != else2) {
if (m.is_value(else1) && m.is_value(else2)) {
set_bool(e, false);
TRACE("pdr", tout
<< "defaults are different: " << mk_pp(e, m) << " "
<< mk_pp(else1, m) << " " << mk_pp(else2, m) << "\n";);
set_false(e);
}
else {
TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";);
@ -659,7 +663,10 @@ namespace pdr {
continue;
}
else if (m.is_value(w1) && m.is_value(w2)) {
set_bool(e, false);
TRACE("pdr", tout << "Equality evaluation: " << mk_pp(e, m) << "\n";
tout << mk_pp(s1, m) << " |-> " << mk_pp(w1, m) << "\n";
tout << mk_pp(s2, m) << " |-> " << mk_pp(w2, m) << "\n";);
set_false(e);
return;
}
else {
@ -668,7 +675,7 @@ namespace pdr {
return;
}
}
set_bool(e, true);
set_true(e);
}
void model_evaluator::eval_eq(app* e, expr* arg1, expr* arg2) {