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

add bypass to allow recursive functions from API

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-03-31 16:38:15 -07:00
parent 582880346e
commit c4b26cd691
1 changed files with 10 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/api/api_quant.cpp
View file

@ -69,14 +69,17 @@ extern "C" {
} }
expr * const* ps = reinterpret_cast<expr * const*>(patterns); expr * const* ps = reinterpret_cast<expr * const*>(patterns);
expr * const* no_ps = reinterpret_cast<expr * const*>(no_patterns); expr * const* no_ps = reinterpret_cast<expr * const*>(no_patterns);
pattern_validator v(mk_c(c)->m()); symbol qid = to_symbol(quantifier_id);
for (unsigned i = 0; i < num_patterns; i++) { bool is_rec = mk_c(c)->m().rec_fun_qid() == qid;
if (!v(num_decls, ps[i], 0, 0)) { if (!is_rec) {
SET_ERROR_CODE(Z3_INVALID_PATTERN); pattern_validator v(mk_c(c)->m());
return 0; for (unsigned i = 0; i < num_patterns; i++) {
if (!v(num_decls, ps[i], 0, 0)) {
SET_ERROR_CODE(Z3_INVALID_PATTERN);
return 0;
}
} }
} }
sort* const* ts = reinterpret_cast<sort * const*>(sorts); sort* const* ts = reinterpret_cast<sort * const*>(sorts);
svector<symbol> names; svector<symbol> names;
for (unsigned i = 0; i < num_decls; ++i) { for (unsigned i = 0; i < num_decls; ++i) {
@ -88,7 +91,7 @@ extern "C" {
(0 != is_forall), (0 != is_forall),
names.size(), ts, names.c_ptr(), to_expr(body), names.size(), ts, names.c_ptr(), to_expr(body),
weight, weight,
to_symbol(quantifier_id), qid,
to_symbol(skolem_id), to_symbol(skolem_id),
num_patterns, ps, num_patterns, ps,
num_no_patterns, no_ps num_no_patterns, no_ps