mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-08 15:13:23 +00:00
Code Activity

working on transforms for duality

Browse source
This commit is contained in:
Ken McMillan 2014-10-04 19:07:14 -07:00
parent e8985ff33d
commit ec48f6d129
2 changed files with 26 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/muz/base/dl_context.cpp
View file

@ -985,6 +985,9 @@ namespace datalog {
flush_add_rules(); flush_add_rules();
break; break;
case DUALITY_ENGINE: case DUALITY_ENGINE:
// this lets us use duality with SAS 2013 abstraction
if(quantify_arrays())
flush_add_rules();
break; break;
default: default:
UNREACHABLE(); UNREACHABLE();

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

@ -37,6 +37,7 @@ Revision History:
#include "fixedpoint_params.hpp" #include "fixedpoint_params.hpp"
#include "used_vars.h" #include "used_vars.h"
#include "func_decl_dependencies.h" #include "func_decl_dependencies.h"
#include "dl_transforms.h"
// template class symbol_table<family_id>; // template class symbol_table<family_id>;
@ -158,22 +159,34 @@ lbool dl_interface::query(::expr * query) {
vector<unsigned> bounds; vector<unsigned> bounds;
// m_ctx.get_rules_as_formulas(rules, names); // m_ctx.get_rules_as_formulas(rules, names);
// If using SAS 2013 abstractiion, we need to perform some transforms
expr_ref query_ref(m_ctx.get_manager()); expr_ref query_ref(m_ctx.get_manager());
if(****){ if(m_ctx.quantify_arrays()){
m_ctx.flush_add_rules();
datalog::rule_manager& rm = m_ctx.get_rule_manager(); datalog::rule_manager& rm = m_ctx.get_rule_manager();
rm.mk_query(query, m_ctx.get_rules()); rm.mk_query(query, m_ctx.get_rules());
apply_default_transformation(m_ctx); apply_default_transformation(m_ctx);
rule_set &rs = m_ctx.get_rules(); datalog::rule_set &rs = m_ctx.get_rules();
if(m_ctx.get_rules().get_output_predicates().empty()) if(m_ctx.get_rules().get_output_predicates().empty())
query_ref = m_ctx.get_manager().mk_true(); query_ref = m_ctx.get_manager().mk_false();
else { else {
query_pred = m_ctx.get_rules().get_output_predicate();
func_decl_ref query_pred(m_ctx.get_manager()); func_decl_ref query_pred(m_ctx.get_manager());
query_pred = m_ctx.get_rules().get_output_predicate(); query_pred = m_ctx.get_rules().get_output_predicate();
ptr_vector<sort> sorts; ptr_vector<sort> sorts;
unsi unsigned nargs = query_pred.get()->get_arity();
expr_ref_vector vars(m_ctx.get_manager());
for(unsigned i = 0; i < nargs; i++){
::sort *s = query_pred.get()->get_domain(i);
vars.push_back(m_ctx.get_manager().mk_var(nargs-1-i,s));
}
query_ref = m_ctx.get_manager().mk_app(query_pred.get(),nargs,vars.c_ptr());
query = query_ref.get();
}
unsigned nrules = rs.get_num_rules();
for(unsigned i = 0; i < nrules; i++){
expr_ref f(m_ctx.get_manager());
rs.get_rule(i)->to_formula(f);
rules.push_back(f);
} }
} }
else else