mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
This commit is contained in:
commit
fc84461e31
|
@ -1,9 +1,11 @@
|
|||
#include<vector>
|
||||
#include"z3++.h"
|
||||
|
||||
|
||||
using namespace z3;
|
||||
|
||||
|
||||
|
||||
|
||||
/**
|
||||
Demonstration of how Z3 can be used to prove validity of
|
||||
De Morgan's Duality Law: {e not(x and y) <-> (not x) or ( not y) }
|
||||
|
@ -985,6 +987,7 @@ void extract_example() {
|
|||
}
|
||||
|
||||
int main() {
|
||||
|
||||
try {
|
||||
demorgan(); std::cout << "\n";
|
||||
find_model_example1(); std::cout << "\n";
|
||||
|
|
|
@ -89,6 +89,7 @@ namespace api {
|
|||
m_bv_util(m()),
|
||||
m_datalog_util(m()),
|
||||
m_fpa_util(m()),
|
||||
m_dtutil(m()),
|
||||
m_last_result(m()),
|
||||
m_ast_trail(m()),
|
||||
m_replay_stack() {
|
||||
|
|
|
@ -58,6 +58,7 @@ namespace api {
|
|||
bv_util m_bv_util;
|
||||
datalog::dl_decl_util m_datalog_util;
|
||||
fpa_util m_fpa_util;
|
||||
datatype_util m_dtutil;
|
||||
|
||||
// Support for old solver API
|
||||
smt_params m_fparams;
|
||||
|
@ -119,6 +120,7 @@ namespace api {
|
|||
bv_util & bvutil() { return m_bv_util; }
|
||||
datalog::dl_decl_util & datalog_util() { return m_datalog_util; }
|
||||
fpa_util & fpautil() { return m_fpa_util; }
|
||||
datatype_util& dtutil() { return m_dtutil; }
|
||||
family_id get_basic_fid() const { return m_basic_fid; }
|
||||
family_id get_array_fid() const { return m_array_fid; }
|
||||
family_id get_arith_fid() const { return m_arith_fid; }
|
||||
|
|
|
@ -36,7 +36,7 @@ extern "C" {
|
|||
RESET_ERROR_CODE();
|
||||
mk_c(c)->reset_last_result();
|
||||
ast_manager& m = mk_c(c)->m();
|
||||
datatype_util dt_util(m);
|
||||
datatype_util& dt_util = mk_c(c)->dtutil();
|
||||
|
||||
sort_ref_vector tuples(m);
|
||||
sort* tuple;
|
||||
|
@ -102,7 +102,7 @@ extern "C" {
|
|||
RESET_ERROR_CODE();
|
||||
mk_c(c)->reset_last_result();
|
||||
ast_manager& m = mk_c(c)->m();
|
||||
datatype_util dt_util(m);
|
||||
datatype_util& dt_util = mk_c(c)->dtutil();
|
||||
|
||||
sort_ref_vector sorts(m);
|
||||
sort* e;
|
||||
|
@ -451,7 +451,7 @@ extern "C" {
|
|||
RESET_ERROR_CODE();
|
||||
CHECK_VALID_AST(t, 0);
|
||||
sort * _t = to_sort(t);
|
||||
datatype_util dt_util(mk_c(c)->m());
|
||||
datatype_util& dt_util = mk_c(c)->dtutil();
|
||||
|
||||
if (!dt_util.is_datatype(_t)) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
|
@ -470,17 +470,17 @@ extern "C" {
|
|||
RESET_ERROR_CODE();
|
||||
CHECK_VALID_AST(t, 0);
|
||||
sort * _t = to_sort(t);
|
||||
datatype_util dt_util(mk_c(c)->m());
|
||||
datatype_util& dt_util = mk_c(c)->dtutil();
|
||||
if (!dt_util.is_datatype(_t)) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
unsigned n = dt_util.get_datatype_num_constructors(_t);
|
||||
if (idx >= n) {
|
||||
ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t);
|
||||
if (idx >= decls->size()) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
func_decl* decl = dt_util.get_constructor(_t, idx);
|
||||
func_decl* decl = (*decls)[idx];
|
||||
mk_c(c)->save_ast_trail(decl);
|
||||
return of_func_decl(decl);
|
||||
}
|
||||
|
@ -499,18 +499,18 @@ extern "C" {
|
|||
LOG_Z3_get_datatype_sort_recognizer(c, t, idx);
|
||||
RESET_ERROR_CODE();
|
||||
sort * _t = to_sort(t);
|
||||
datatype_util dt_util(mk_c(c)->m());
|
||||
datatype_util& dt_util = mk_c(c)->dtutil();
|
||||
|
||||
if (!dt_util.is_datatype(_t)) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
RETURN_Z3(0);
|
||||
}
|
||||
unsigned n = dt_util.get_datatype_num_constructors(_t);
|
||||
if (idx >= n) {
|
||||
ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t);
|
||||
if (idx >= decls->size()) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
func_decl* decl = dt_util.get_constructor(_t, idx);
|
||||
func_decl* decl = (*decls)[idx];
|
||||
decl = dt_util.get_constructor_recognizer(decl);
|
||||
mk_c(c)->save_ast_trail(decl);
|
||||
RETURN_Z3(of_func_decl(decl));
|
||||
|
@ -522,18 +522,18 @@ extern "C" {
|
|||
LOG_Z3_get_datatype_sort_constructor_accessor(c, t, idx_c, idx_a);
|
||||
RESET_ERROR_CODE();
|
||||
sort * _t = to_sort(t);
|
||||
datatype_util dt_util(mk_c(c)->m());
|
||||
datatype_util& dt_util = mk_c(c)->dtutil();
|
||||
|
||||
if (!dt_util.is_datatype(_t)) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
RETURN_Z3(0);
|
||||
}
|
||||
unsigned n = dt_util.get_datatype_num_constructors(_t);
|
||||
if (idx_c >= n) {
|
||||
ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t);
|
||||
if (idx_c >= decls->size()) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
func_decl* decl = dt_util.get_constructor(_t, idx_c);
|
||||
func_decl* decl = (*decls)[idx_c];
|
||||
if (decl->get_arity() <= idx_a) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
RETURN_Z3(0);
|
||||
|
@ -555,7 +555,7 @@ extern "C" {
|
|||
LOG_Z3_get_tuple_sort_mk_decl(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
sort * tuple = to_sort(t);
|
||||
datatype_util dt_util(mk_c(c)->m());
|
||||
datatype_util& dt_util = mk_c(c)->dtutil();
|
||||
if (!dt_util.is_datatype(tuple) || dt_util.is_recursive(tuple) || dt_util.get_datatype_num_constructors(tuple) != 1) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
RETURN_Z3(0);
|
||||
|
@ -570,7 +570,7 @@ extern "C" {
|
|||
LOG_Z3_get_tuple_sort_num_fields(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
sort * tuple = to_sort(t);
|
||||
datatype_util dt_util(mk_c(c)->m());
|
||||
datatype_util& dt_util = mk_c(c)->dtutil();
|
||||
if (!dt_util.is_datatype(tuple) || dt_util.is_recursive(tuple) || dt_util.get_datatype_num_constructors(tuple) != 1) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
|
@ -593,7 +593,7 @@ extern "C" {
|
|||
LOG_Z3_get_tuple_sort_field_decl(c, t, i);
|
||||
RESET_ERROR_CODE();
|
||||
sort * tuple = to_sort(t);
|
||||
datatype_util dt_util(mk_c(c)->m());
|
||||
datatype_util& dt_util = mk_c(c)->dtutil();
|
||||
if (!dt_util.is_datatype(tuple) || dt_util.is_recursive(tuple) || dt_util.get_datatype_num_constructors(tuple) != 1) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
RETURN_Z3(0);
|
||||
|
|
|
@ -170,6 +170,7 @@ class datatype_util {
|
|||
ptr_vector<ptr_vector<func_decl> > m_vectors;
|
||||
|
||||
func_decl * get_non_rec_constructor_core(sort * ty, ptr_vector<sort> & forbidden_set);
|
||||
func_decl * get_constructor(sort * ty, unsigned c_id);
|
||||
|
||||
public:
|
||||
datatype_util(ast_manager & m);
|
||||
|
@ -202,7 +203,6 @@ public:
|
|||
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