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

fix #3020

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-06 16:42:01 -07:00
parent 6761bf1495
commit d2ec661ec6
3 changed files with 10 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -766,6 +766,7 @@ namespace datalog {
arith_util a;
datatype_util dt;
bv_util bv;
array_util ar;
DL_ENGINE m_engine_type;
bool is_large_bv(sort* s) {
@ -773,7 +774,7 @@ namespace datalog {
}
public:
engine_type_proc(ast_manager& m): m(m), a(m), dt(m), bv(m), m_engine_type(DATALOG_ENGINE) {}
engine_type_proc(ast_manager& m): m(m), a(m), dt(m), bv(m), ar(m), m_engine_type(DATALOG_ENGINE) {}
DL_ENGINE get_engine() const { return m_engine_type; }
@ -793,6 +794,9 @@ namespace datalog {
else if (!m.get_sort(e)->get_num_elements().is_finite()) {
m_engine_type = SPACER_ENGINE;
}
else if (ar.is_array(e)) {
m_engine_type = SPACER_ENGINE;
}
}
};

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

@ -26,16 +26,14 @@ 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_bv(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_ar(m), m_generate_proof(false) {}
rule_properties::~rule_properties() {}
void rule_properties::collect(rule_set const& rules) {
reset();
rule_set::iterator it = rules.begin(), end = rules.end();
expr_sparse_mark visited;
for (; it != end; ++it) {
rule* r = *it;
for (rule* r : rules) {
m_rule = r;
unsigned ut_size = r->get_uninterpreted_tail_size();
unsigned t_size = r->get_tail_size();
@ -51,7 +49,7 @@ void rule_properties::collect(rule_set const& rules) {
for (unsigned i = 0; m_inf_sort.empty() && i < r->get_decl()->get_arity(); ++i) {
sort* d = r->get_decl()->get_domain(i);
sort_size sz = d->get_num_elements();
if (!sz.is_finite() && !m_dl.is_rule_sort(d)) {
if (m_ar.is_array(d) || (!sz.is_finite() && !m_dl.is_rule_sort(d))) {
TRACE("dl", tout << "sort " << mk_pp(d, m) << " is not finite " << sz << "\n";);
m_inf_sort.push_back(m_rule);
}

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

@ -24,6 +24,7 @@ Notes:
#include "ast/ast.h"
#include "ast/datatype_decl_plugin.h"
#include "ast/bv_decl_plugin.h"
#include "ast/array_decl_plugin.h"
#include "muz/base/dl_rule.h"
namespace datalog {
@ -35,6 +36,7 @@ namespace datalog {
datatype_util m_dt;
dl_decl_util m_dl;
bv_util m_bv;
array_util m_ar;
bool m_generate_proof;
rule* m_rule;
obj_map<quantifier, rule*> m_quantifiers;