mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

working on transforms in duality

Browse source
This commit is contained in:
Ken McMillan 2014-10-04 17:17:33 -07:00
parent 16445569f1
commit e8985ff33d
1 changed files with 21 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/muz/duality/duality_dl_interface.cpp
View file

@ -157,7 +157,27 @@ lbool dl_interface::query(::expr * query) {
svector< ::symbol> names;
vector<unsigned> bounds;
// m_ctx.get_rules_as_formulas(rules, names);
m_ctx.get_raw_rule_formulas(rules, names, bounds);
expr_ref query_ref(m_ctx.get_manager());
if(****){
m_ctx.flush_add_rules();
datalog::rule_manager& rm = m_ctx.get_rule_manager();
rm.mk_query(query, m_ctx.get_rules());
apply_default_transformation(m_ctx);
rule_set &rs = m_ctx.get_rules();
if(m_ctx.get_rules().get_output_predicates().empty())
query_ref = m_ctx.get_manager().mk_true();
else {
query_pred = m_ctx.get_rules().get_output_predicate();
func_decl_ref query_pred(m_ctx.get_manager());
query_pred = m_ctx.get_rules().get_output_predicate();
ptr_vector<sort> sorts;
unsi
}
}
else
m_ctx.get_raw_rule_formulas(rules, names, bounds);
// get all the rules as clauses
std::vector<expr> &clauses = _d->clauses;