mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-29 02:39:24 +00:00
Code Activity

test hilbert-basis with fdds and checked integers

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-03-26 17:33:44 -07:00
commit c9109132da
15 changed files with 55 additions and 36 deletions
Download patch file Download diff file Expand all files Collapse all files

29
src/muz_qe/dl_mk_bit_blast.cpp
View file

@ -23,6 +23,7 @@ Revision History:
#include "ast_pp.h"
#include "expr_safe_replace.h"
#include "filter_model_converter.h"
#include "dl_mk_interp_tail_simplifier.h"
namespace datalog {
@ -212,18 +213,23 @@ namespace datalog {
ast_manager & m;
params_ref m_params;
rule_ref_vector m_rules;
mk_interp_tail_simplifier m_simplifier;
bit_blaster_rewriter m_blaster;
expand_mkbv m_rewriter;
bool blast(expr_ref& fml) {
bool blast(rule *r, expr_ref& fml) {
proof_ref pr(m);
expr_ref fml1(m), fml2(m);
m_blaster(fml, fml1, pr);
m_rewriter(fml1, fml2);
TRACE("dl", tout << mk_pp(fml, m) << " -> " << mk_pp(fml1, m) << " -> " << mk_pp(fml2, m) << "\n";);
if (fml2 != fml) {
fml = fml2;
expr_ref fml1(m), fml2(m), fml3(m);
rule_ref r2(m_context.get_rule_manager());
// We need to simplify rule before bit-blasting.
m_simplifier.transform_rule(r, r2);
r2->to_formula(fml1);
m_blaster(fml1, fml2, pr);
m_rewriter(fml2, fml3);
TRACE("dl", tout << mk_pp(fml, m) << " -> " << mk_pp(fml2, m) << " -> " << mk_pp(fml3, m) << "\n";);
if (fml3 != fml) {
fml = fml3;
return true;
}
else {
@ -241,8 +247,9 @@ namespace datalog {
m(ctx.get_manager()),
m_params(ctx.get_params().p),
m_rules(ctx.get_rule_manager()),
m_blaster(m, m_params),
m_rewriter(m, ctx, m_rules) {
m_simplifier(ctx),
m_blaster(ctx.get_manager(), m_params),
m_rewriter(ctx.get_manager(), ctx, m_rules) {
m_params.set_bool("blast_full", true);
m_params.set_bool("blast_quant", true);
m_blaster.updt_params(m_params);
@ -261,12 +268,12 @@ namespace datalog {
for (unsigned i = 0; i < sz; ++i) {
rule * r = source.get_rule(i);
r->to_formula(fml);
if (blast(fml)) {
if (blast(r, fml)) {
proof_ref pr(m);
if (m_context.generate_proof_trace()) {
pr = m.mk_asserted(fml); // loses original proof of r.
}
rm.mk_rule(fml, pr, m_rules, r->name());
rm.mk_rule(fml, pr, m_rules, r->name());
}
else {
m_rules.push_back(r);

1
src/muz_qe/dl_rule.cpp
View file

@ -502,6 +502,7 @@ namespace datalog {
r->m_tail_size = n;
r->m_positive_cnt = source->m_positive_cnt;
r->m_uninterp_cnt = source->m_uninterp_cnt;
r->m_proof = 0;
m.inc_ref(r->m_head);
for (unsigned i = 0; i < n; i++) {
r->m_tail[i] = source->m_tail[i];

21
src/muz_qe/qe_lite.cpp
View file

@ -201,9 +201,15 @@ namespace eq {
return (*m_is_variable)(e);
}
bool is_neg_var(ast_manager & m, expr * e) {
bool is_neg_var(ast_manager & m, expr * e, var*& v) {
expr* e1;
return m.is_not(e, e1) && is_variable(e1);
if (m.is_not(e, e1) && is_variable(e1)) {
v = to_var(e1);
return true;
}
else {
return false;
}
}
@ -328,18 +334,19 @@ namespace eq {
bool is_var_eq(expr * e, ptr_vector<var>& vs, expr_ref_vector & ts) {
expr* lhs, *rhs;
var* v;
// (= VAR t), (iff VAR t), (iff (not VAR) t), (iff t (not VAR)) cases
if (m.is_eq(e, lhs, rhs) || m.is_iff(e, lhs, rhs)) {
// (iff (not VAR) t) (iff t (not VAR)) cases
if (!is_variable(lhs) && !is_variable(rhs) && m.is_bool(lhs)) {
if (!is_neg_var(m, lhs)) {
if (!is_neg_var(m, lhs, v)) {
std::swap(lhs, rhs);
}
if (!is_neg_var(m, lhs)) {
if (!is_neg_var(m, lhs, v)) {
return false;
}
vs.push_back(to_var(lhs));
vs.push_back(v);
ts.push_back(m.mk_not(rhs));
TRACE("qe_lite", tout << mk_pp(e, m) << "\n";);
return true;
@ -378,9 +385,9 @@ namespace eq {
}
// VAR = false case
if (is_neg_var(m, e)) {
if (is_neg_var(m, e, v)) {
ts.push_back(m.mk_false());
vs.push_back(to_var(to_app(e)->get_arg(0)));
vs.push_back(v);
TRACE("qe_lite", tout << mk_pp(e, m) << "\n";);
return true;
}