mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

filter query predicates from models

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-08-18 21:11:14 -07:00
parent 7bbabcdf6d
commit e43383b6a8
4 changed files with 27 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/muz_qe/clp_context.cpp
View file

@ -68,9 +68,13 @@ namespace datalog {
m_goals.reset();
rm.mk_query(query, m_ctx.get_rules());
m_ctx.apply_default_transformation();
func_decl *head_decl = m_ctx.get_rules().get_output_predicate();
expr_ref head(m_ctx.get_rules().get_predicate_rules(head_decl)[0]->get_head(), m);
func_decl* head_decl = m_ctx.get_rules().get_output_predicate();
rule_set& rules = m_ctx.get_rules();
rule_vector const& rv = rules.get_predicate_rules(head_decl);
if (rv.empty()) {
return l_false;
}
expr_ref head(rv[0]->get_head(), m);
ground(head);
m_goals.push_back(to_app(head));
return search(20, 0);

2
src/muz_qe/dl_mk_array_blast.cpp
View file

@ -250,11 +250,11 @@ namespace datalog {
rule_set new_rules(m_ctx);
rm.mk_rule(fml2, p, new_rules, r.name());
TRACE("dl", new_rules.last()->display(m_ctx, tout << "new rule\n"););
rule_ref new_rule(rm);
if (m_simplifier.transform_rule(new_rules.last(), new_rule)) {
rules.add_rule(new_rule.get());
rm.mk_rule_rewrite_proof(r, *new_rule.get());
TRACE("dl", new_rule->display(m_ctx, tout << "new rule\n"););
}
return true;
}

9
src/muz_qe/dl_rule.cpp
View file

@ -41,6 +41,7 @@ Revision History:
#include"expr_replacer.h"
#include"bool_rewriter.h"
#include"expr_safe_replace.h"
#include"filter_model_converter.h"
namespace datalog {
@ -335,8 +336,14 @@ namespace datalog {
vars.reverse();
names.reverse();
func_decl* qpred = m_ctx.mk_fresh_head_predicate(symbol("query"), symbol(), vars.size(), vars.c_ptr(), body_pred);
m_ctx.register_predicate(qpred, false);
m_ctx.register_predicate(qpred, false);
rules.set_output_predicate(qpred);
if (m_ctx.get_model_converter()) {
filter_model_converter* mc = alloc(filter_model_converter, m);
mc->insert(qpred);
m_ctx.add_model_converter(mc);
}
expr_ref_vector qhead_args(m);
for (unsigned i = 0; i < vars.size(); i++) {

12
src/muz_qe/horn_tactic.cpp
View file

@ -24,6 +24,7 @@ Revision History:
#include"expr_replacer.h"
#include"dl_rule_transformer.h"
#include"dl_mk_slice.h"
#include"filter_model_converter.h"
class horn_tactic : public tactic {
struct imp {
@ -226,6 +227,9 @@ class horn_tactic : public tactic {
}
queries.reset();
queries.push_back(q);
filter_model_converter* mc1 = alloc(filter_model_converter, m);
mc1->insert(to_app(q)->get_decl());
mc = mc1;
}
SASSERT(queries.size() == 1);
q = queries[0].get();
@ -276,7 +280,13 @@ class horn_tactic : public tactic {
g->reset();
if (produce_models) {
model_ref md = m_ctx.get_model();
mc = model2model_converter(&*md);
model_converter_ref mc2 = model2model_converter(&*md);
if (mc) {
mc = concat(mc.get(), mc2.get());
}
else {
mc = mc2;
}
}
break;
}