mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

Allow building AC functions without requiring arity check from API

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-01-22 14:39:58 -08:00
parent 806a4772bc
commit 7d364bf786
2 changed files with 5 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/api/api_ast.cpp
View file

@ -660,11 +660,14 @@ extern "C" {
LOG_Z3_get_domain(c, d, i); LOG_Z3_get_domain(c, d, i);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
CHECK_VALID_AST(d, nullptr); CHECK_VALID_AST(d, nullptr);
if (i >= to_func_decl(d)->get_arity()) { func_decl* _d = to_func_decl(d);
if (_d->is_associative())
i = 0;
if (i >= _d->get_arity()) {
SET_ERROR_CODE(Z3_IOB, nullptr); SET_ERROR_CODE(Z3_IOB, nullptr);
RETURN_Z3(nullptr); RETURN_Z3(nullptr);
} }
Z3_sort r = of_sort(to_func_decl(d)->get_domain(i)); Z3_sort r = of_sort(_d->get_domain(i));
RETURN_Z3(r); RETURN_Z3(r);
Z3_CATCH_RETURN(nullptr); Z3_CATCH_RETURN(nullptr);
} }

4
src/api/python/z3/z3.py
View file

@ -763,8 +763,6 @@ class FuncDeclRef(AstRef):
>>> f.domain(1) >>> f.domain(1)
Real Real
""" """
if z3_debug():
_z3_assert(i < self.arity(), "Index out of bounds")
return _to_sort_ref(Z3_get_domain(self.ctx_ref(), self.ast, i), self.ctx) return _to_sort_ref(Z3_get_domain(self.ctx_ref(), self.ast, i), self.ctx)
def range(self): def range(self):
@ -834,8 +832,6 @@ class FuncDeclRef(AstRef):
""" """
args = _get_args(args) args = _get_args(args)
num = len(args) num = len(args)
if z3_debug():
_z3_assert(num == self.arity(), "Incorrect number of arguments to %s" % self)
_args = (Ast * num)() _args = (Ast * num)()
saved = [] saved = []
for i in range(num): for i in range(num):