mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-30 04:15:51 +00:00
Code Activity

disable hybrid relations pending overhaul/deletion of product relations

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
This commit is contained in:
Nikolaj Bjorner 2015-05-20 09:21:55 -07:00
parent 15e1c84592
commit 28f6adf79e
9 changed files with 84 additions and 34 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -558,6 +558,7 @@ namespace datalog {
m_rule_properties.check_quantifier_free();
m_rule_properties.check_uninterpreted_free();
m_rule_properties.check_nested_free();
m_rule_properties.check_infinite_sorts();
break;
case PDR_ENGINE:
m_rule_properties.collect(r);

27
src/muz/base/rule_properties.cpp
View file

@ -26,7 +26,7 @@ Notes:
using namespace datalog;
rule_properties::rule_properties(ast_manager & m, rule_manager& rm, context& ctx, i_expr_pred& p):
m(m), rm(rm), m_ctx(ctx), m_is_predicate(p), m_dt(m), m_dl(m), m_generate_proof(false) {}
m(m), rm(rm), m_ctx(ctx), m_is_predicate(p), m_dt(m), m_dl(m), m_bv(m), m_generate_proof(false) {}
rule_properties::~rule_properties() {}
@ -48,6 +48,12 @@ void rule_properties::collect(rule_set const& rules) {
if (m_generate_proof && !r->get_proof()) {
rm.mk_rule_asserted_proof(*r);
}
for (unsigned i = 0; m_inf_sort.empty() && i < r->get_decl()->get_arity(); ++i) {
sort* d = r->get_decl()->get_domain(i);
if (!m.is_bool(d) && !m_dl.is_finite_sort(d) && !m_bv.is_bv_sort(d)) {
m_inf_sort.push_back(m_rule);
}
}
}
}
@ -85,6 +91,16 @@ void rule_properties::check_uninterpreted_free() {
}
}
void rule_properties::check_infinite_sorts() {
if (!m_inf_sort.empty()) {
std::stringstream stm;
rule* r = m_inf_sort.back();
stm << "Rule contains infinite sorts in rule ";
r->display(m_ctx, stm);
throw default_exception(stm.str());
}
}
void rule_properties::check_nested_free() {
if (!m_interp_pred.empty()) {
std::stringstream stm;
@ -92,7 +108,6 @@ void rule_properties::check_nested_free() {
stm << "Rule contains nested predicates ";
r->display(m_ctx, stm);
throw default_exception(stm.str());
}
}
@ -158,7 +173,8 @@ void rule_properties::insert(ptr_vector<rule>& rules, rule* r) {
}
}
void rule_properties::operator()(var* n) { }
void rule_properties::operator()(var* n) {
}
void rule_properties::operator()(quantifier* n) {
m_quantifiers.insert(n, m_rule);
@ -177,6 +193,10 @@ void rule_properties::operator()(app* n) {
m_uninterp_funs.insert(n->get_decl(), m_rule);
}
}
else {
std::cout << mk_pp(n, m) << "\n";
}
}
void rule_properties::reset() {
@ -184,5 +204,6 @@ void rule_properties::reset() {
m_uninterp_funs.reset();
m_interp_pred.reset();
m_negative_rules.reset();
m_inf_sort.reset();
}

4
src/muz/base/rule_properties.h
View file

@ -23,6 +23,7 @@ Notes:
#include"ast.h"
#include"datatype_decl_plugin.h"
#include"bv_decl_plugin.h"
#include"dl_rule.h"
namespace datalog {
@ -33,12 +34,14 @@ namespace datalog {
i_expr_pred& m_is_predicate;
datatype_util m_dt;
dl_decl_util m_dl;
bv_util m_bv;
bool m_generate_proof;
rule* m_rule;
obj_map<quantifier, rule*> m_quantifiers;
obj_map<func_decl, rule*> m_uninterp_funs;
ptr_vector<rule> m_interp_pred;
ptr_vector<rule> m_negative_rules;
ptr_vector<rule> m_inf_sort;
void insert(ptr_vector<rule>& rules, rule* r);
public:
@ -51,6 +54,7 @@ namespace datalog {
void check_existential_tail();
void check_for_negated_predicates();
void check_nested_free();
void check_infinite_sorts();
void operator()(var* n);
void operator()(quantifier* n);
void operator()(app* n);