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

support for legacy datatype test

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-09-05 10:28:11 -07:00
parent aac7773a52
commit 06087c17be
12 changed files with 100 additions and 98 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/datatype_decl_plugin.h
View file

@ -16,7 +16,7 @@ Author:
Revision History:
--*/
// define DATATYPE_V2
#define DATATYPE_V2
#ifdef DATATYPE_V2
#include "ast/datatype_decl_plugin2.h"
#else

60
src/ast/datatype_decl_plugin2.cpp
View file

@ -236,7 +236,7 @@ namespace datatype {
return m.mk_func_decl(symbol("update-field"), arity, domain, range, info);
}
#define VALIDATE_PARAM(_pred_) if (!(_pred_)) m_manager->raise_exception("invalid parameter to datatype function");
#define VALIDATE_PARAM(_pred_) if (!(_pred_)) m_manager->raise_exception("invalid parameter to datatype function " #_pred_);
func_decl * decl::plugin::mk_constructor(unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
@ -252,13 +252,26 @@ namespace datatype {
func_decl * decl::plugin::mk_recognizer(unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort *) {
ast_manager& m = *m_manager;
VALIDATE_PARAM(arity == 1 && num_parameters == 1 && parameters[0].is_ast() && is_func_decl(parameters[0].get_ast()));
VALIDATE_PARAM(arity == 1 && num_parameters == 2 && parameters[1].is_symbol() && parameters[0].is_ast() && is_func_decl(parameters[0].get_ast()));
VALIDATE_PARAM(u().is_datatype(domain[0]));
// blindly trust that parameter is a constructor
sort* range = m_manager->mk_bool_sort();
func_decl* f = to_func_decl(parameters[0].get_ast());
func_decl_info info(m_family_id, OP_DT_RECOGNISER, num_parameters, parameters);
info.m_private_parameters = true;
return m.mk_func_decl(symbol(parameters[1].get_symbol()), arity, domain, range, info);
}
func_decl * decl::plugin::mk_is(unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort *) {
ast_manager& m = *m_manager;
VALIDATE_PARAM(arity == 1 && num_parameters == 1 && parameters[0].is_ast() && is_func_decl(parameters[0].get_ast()));
VALIDATE_PARAM(u().is_datatype(domain[0]));
// blindly trust that parameter is a constructor
sort* range = m_manager->mk_bool_sort();
func_decl* f = to_func_decl(parameters[0].get_ast());
func_decl_info info(m_family_id, OP_DT_IS, num_parameters, parameters);
info.m_private_parameters = true;
return m.mk_func_decl(symbol("is"), arity, domain, range, info);
}
@ -282,6 +295,8 @@ namespace datatype {
return mk_constructor(num_parameters, parameters, arity, domain, range);
case OP_DT_RECOGNISER:
return mk_recognizer(num_parameters, parameters, arity, domain, range);
case OP_DT_IS:
return mk_is(num_parameters, parameters, arity, domain, range);
case OP_DT_ACCESSOR:
return mk_accessor(num_parameters, parameters, arity, domain, range);
case OP_DT_UPDATE_FIELD:
@ -297,20 +312,6 @@ namespace datatype {
return alloc(def, m, u(), name, m_class_id, n, params);
}
#if 0
def& plugin::add(symbol const& name, unsigned n, sort * const * params) {
ast_manager& m = *m_manager;
def* d = 0;
if (m_defs.find(name, d)) {
TRACE("datatype", tout << "delete previous version for " << name << "\n";);
dealloc(d);
}
d = alloc(def, m, u(), name, m_class_id, n, params);
m_defs.insert(name, d);
m_def_block.push_back(name);
return *d;
}
#endif
void plugin::end_def_block() {
ast_manager& m = *m_manager;
@ -407,7 +408,7 @@ namespace datatype {
}
void plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
op_names.push_back(builtin_name("is", OP_DT_RECOGNISER));
op_names.push_back(builtin_name("is", OP_DT_IS));
if (logic == symbol::null) {
op_names.push_back(builtin_name("update-field", OP_DT_UPDATE_FIELD));
}
@ -739,18 +740,25 @@ namespace datatype {
return res;
}
func_decl * util::get_constructor_recognizer(func_decl * constructor) {
SASSERT(is_constructor(constructor));
func_decl * util::get_constructor_recognizer(func_decl * con) {
SASSERT(is_constructor(con));
func_decl * d = 0;
if (m_constructor2recognizer.find(constructor, d))
if (m_constructor2recognizer.find(con, d))
return d;
sort * datatype = constructor->get_range();
parameter ps[1] = { parameter(constructor) };
d = m.mk_func_decl(m_family_id, OP_DT_RECOGNISER, 1, ps, 1, &datatype);
sort * datatype = con->get_range();
def const& dd = get_def(datatype);
symbol r;
for (constructor const* c : dd) {
if (c->name() == con->get_name()) {
r = c->recognizer();
}
}
parameter ps[2] = { parameter(con), parameter(r) };
d = m.mk_func_decl(m_family_id, OP_DT_RECOGNISER, 2, ps, 1, &datatype);
SASSERT(d);
m_asts.push_back(constructor);
m_asts.push_back(con);
m_asts.push_back(d);
m_constructor2recognizer.insert(constructor, d);
m_constructor2recognizer.insert(con, d);
return d;
}
@ -917,11 +925,11 @@ namespace datatype {
UNREACHABLE();
return 0;
}
unsigned util::get_recognizer_constructor_idx(func_decl * f) const {
return get_constructor_idx(get_recognizer_constructor(f));
}
/**
\brief Two datatype sorts s1 and s2 are siblings if they were
defined together in the same mutually recursive definition.

21
src/ast/datatype_decl_plugin2.h
View file

@ -36,7 +36,8 @@ Revision History:
enum op_kind {
OP_DT_CONSTRUCTOR,
OP_DT_RECOGNISER,
OP_DT_ACCESSOR,
OP_DT_IS,
OP_DT_ACCESSOR,
OP_DT_UPDATE_FIELD,
LAST_DT_OP
};
@ -78,13 +79,15 @@ namespace datatype {
class constructor {
symbol m_name;
symbol m_recognizer;
ptr_vector<accessor> m_accessors;
def* m_def;
public:
constructor(symbol n): m_name(n) {}
constructor(symbol n, symbol const& r): m_name(n), m_recognizer(r) {}
~constructor();
void add(accessor* a) { m_accessors.push_back(a); a->attach(this); }
symbol const& name() const { return m_name; }
symbol const& recognizer() const { return m_recognizer; }
ptr_vector<accessor> const& accessors() const { return m_accessors; }
ptr_vector<accessor>::const_iterator begin() const { return m_accessors.begin(); }
ptr_vector<accessor>::const_iterator end() const { return m_accessors.end(); }
@ -290,6 +293,10 @@ namespace datatype {
unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_is(
unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
symbol datatype_name(sort * s) const {
//SASSERT(u().is_datatype(s));
return s->get_parameter(0).get_symbol();
@ -340,11 +347,15 @@ namespace datatype {
bool is_enum_sort(sort* s);
bool is_recursive(sort * ty);
bool is_constructor(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_CONSTRUCTOR); }
bool is_recognizer(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_RECOGNISER); }
bool is_recognizer(func_decl * f) const { return is_recognizer0(f) || is_is(f); }
bool is_recognizer0(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_RECOGNISER); }
bool is_is(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_IS); }
bool is_accessor(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_ACCESSOR); }
bool is_update_field(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_UPDATE_FIELD); }
bool is_constructor(app * f) const { return is_app_of(f, m_family_id, OP_DT_CONSTRUCTOR); }
bool is_recognizer(app * f) const { return is_app_of(f, m_family_id, OP_DT_RECOGNISER); }
bool is_recognizer0(app * f) const { return is_app_of(f, m_family_id, OP_DT_RECOGNISER);}
bool is_is(app * f) const { return is_app_of(f, m_family_id, OP_DT_IS);}
bool is_recognizer(app * f) const { return is_recognizer0(f) || is_is(f); }
bool is_accessor(app * f) const { return is_app_of(f, m_family_id, OP_DT_ACCESSOR); }
bool is_update_field(app * f) const { return is_app_of(f, m_family_id, OP_DT_UPDATE_FIELD); }
ptr_vector<func_decl> const * get_datatype_constructors(sort * ty);
@ -401,7 +412,7 @@ inline accessor_decl * mk_accessor_decl(ast_manager& m, symbol const & n, type_r
}
inline constructor_decl * mk_constructor_decl(symbol const & n, symbol const & r, unsigned num_accessors, accessor_decl * * acs) {
constructor_decl* c = alloc(constructor_decl, n);
constructor_decl* c = alloc(constructor_decl, n, r);
for (unsigned i = 0; i < num_accessors; ++i) {
c->add(acs[i]);
}

1
src/ast/rewriter/datatype_rewriter.cpp
View file

@ -23,6 +23,7 @@ br_status datatype_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr
switch(f->get_decl_kind()) {
case OP_DT_CONSTRUCTOR: return BR_FAILED;
case OP_DT_RECOGNISER:
case OP_DT_IS:
//
// simplify is_cons(cons(x,y)) -> true
// simplify is_cons(nil) -> false

4
src/ast/rewriter/poly_rewriter_def.h
View file

@ -753,18 +753,14 @@ br_status poly_rewriter<Config>::cancel_monomials(expr * lhs, expr * rhs, bool m
normalize(c);
TRACE("mk_le_bug", tout << c << "\n";);
if (!has_multiple && num_coeffs <= 1) {
if (move) {
if (is_numeral(rhs)) {
TRACE("mk_le_bug", tout << "rhs is numeral\n";);
return BR_FAILED;
}
}
else {
if (num_coeffs == 0 || is_numeral(rhs)) {
TRACE("mk_le_bug", tout << "rhs is numeral or no coeffs\n";);
return BR_FAILED;
}
}

13
src/ast/static_features.cpp
View file

@ -145,18 +145,19 @@ bool static_features::is_diff_atom(expr const * e) const {
return true;
if (!is_numeral(rhs))
return false;
// lhs can be 'x' or '(+ x (* -1 y))'
// lhs can be 'x' or '(+ x (* -1 y))' or '(+ (* -1 x) y)'
if (!is_arith_expr(lhs))
return true;
expr* arg1, *arg2;
if (!m_autil.is_add(lhs, arg1, arg2))
return false;
// x
if (is_arith_expr(arg1))
return false;
// arg2: (* -1 y)
expr* m1, *m2;
return m_autil.is_mul(arg2, m1, m2) && is_minus_one(m1) && !is_arith_expr(m2);
if (!is_arith_expr(arg1) && m_autil.is_mul(arg2, m1, m2) && is_minus_one(m1) && !is_arith_expr(m2))
return true;
if (!is_arith_expr(arg2) && m_autil.is_mul(arg1, m1, m2) && is_minus_one(m1) && !is_arith_expr(m2))
return true;
return false;
}
bool static_features::is_gate(expr const * e) const {