mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
This commit is contained in:
commit
3c5897eea0
|
@ -475,12 +475,12 @@ extern "C" {
|
|||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t);
|
||||
if (!decls || idx >= decls->size()) {
|
||||
unsigned n = dt_util.get_datatype_num_constructors(_t);
|
||||
if (idx >= n) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
func_decl* decl = (*decls)[idx];
|
||||
func_decl* decl = dt_util.get_constructor(_t, idx);
|
||||
mk_c(c)->save_ast_trail(decl);
|
||||
return of_func_decl(decl);
|
||||
}
|
||||
|
@ -505,12 +505,12 @@ extern "C" {
|
|||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
RETURN_Z3(0);
|
||||
}
|
||||
ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t);
|
||||
if (!decls || idx >= decls->size()) {
|
||||
unsigned n = dt_util.get_datatype_num_constructors(_t);
|
||||
if (idx >= n) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
RETURN_Z3(0);
|
||||
return 0;
|
||||
}
|
||||
func_decl* decl = (*decls)[idx];
|
||||
func_decl* decl = dt_util.get_constructor(_t, idx);
|
||||
decl = dt_util.get_constructor_recognizer(decl);
|
||||
mk_c(c)->save_ast_trail(decl);
|
||||
RETURN_Z3(of_func_decl(decl));
|
||||
|
@ -528,12 +528,12 @@ extern "C" {
|
|||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
RETURN_Z3(0);
|
||||
}
|
||||
ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t);
|
||||
if (!decls || idx_c >= decls->size()) {
|
||||
unsigned n = dt_util.get_datatype_num_constructors(_t);
|
||||
if (idx_c >= n) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
RETURN_Z3(0);
|
||||
return 0;
|
||||
}
|
||||
func_decl* decl = (*decls)[idx_c];
|
||||
func_decl* decl = dt_util.get_constructor(_t, idx_c);
|
||||
if (decl->get_arity() <= idx_a) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
RETURN_Z3(0);
|
||||
|
|
|
@ -168,8 +168,7 @@ class datatype_util {
|
|||
obj_map<sort, bool> m_is_recursive;
|
||||
ast_ref_vector m_asts;
|
||||
ptr_vector<ptr_vector<func_decl> > m_vectors;
|
||||
|
||||
func_decl * get_constructor(sort * ty, unsigned c_id);
|
||||
|
||||
func_decl * get_non_rec_constructor_core(sort * ty, ptr_vector<sort> & forbidden_set);
|
||||
|
||||
public:
|
||||
|
@ -185,7 +184,12 @@ public:
|
|||
bool is_recognizer(app * f) const { return is_app_of(f, m_family_id, OP_DT_RECOGNISER); }
|
||||
bool is_accessor(app * f) const { return is_app_of(f, m_family_id, OP_DT_ACCESSOR); }
|
||||
ptr_vector<func_decl> const * get_datatype_constructors(sort * ty);
|
||||
unsigned get_datatype_num_constructors(sort * ty) { return get_datatype_constructors(ty)->size(); }
|
||||
unsigned get_datatype_num_constructors(sort * ty) {
|
||||
SASSERT(is_datatype(ty));
|
||||
unsigned tid = ty->get_parameter(1).get_int();
|
||||
unsigned o = ty->get_parameter(3 + 2 * tid).get_int();
|
||||
return ty->get_parameter(o).get_int();
|
||||
}
|
||||
unsigned get_constructor_idx(func_decl * f) const { SASSERT(is_constructor(f)); return f->get_parameter(1).get_int(); }
|
||||
unsigned get_recognizer_constructor_idx(func_decl * f) const { SASSERT(is_recognizer(f)); return f->get_parameter(1).get_int(); }
|
||||
func_decl * get_non_rec_constructor(sort * ty);
|
||||
|
@ -197,6 +201,8 @@ public:
|
|||
bool are_siblings(sort * s1, sort * s2);
|
||||
void reset();
|
||||
void display_datatype(sort *s, std::ostream& strm);
|
||||
|
||||
func_decl * get_constructor(sort * ty, unsigned c_id);
|
||||
};
|
||||
|
||||
#endif /* _DATATYPE_DECL_PLUGIN_H_ */
|
||||
|
|
Loading…
Reference in a new issue