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

Merge pull request #1773 from NikolajBjorner/master

Browse source 
bug fixes
This commit is contained in:
Nikolaj Bjorner 2018-07-29 08:09:35 -07:00 • committed by GitHub
commit 6bacf09447
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
44 changed files with 425 additions and 339 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/api/api_ast.cpp
View file

@ -384,12 +384,14 @@ extern "C" {
Z3_symbol Z3_API Z3_get_decl_name(Z3_context c, Z3_func_decl d) {
LOG_Z3_get_decl_name(c, d);
RESET_ERROR_CODE();
CHECK_VALID_AST(d, nullptr);
return of_symbol(to_func_decl(d)->get_name());
}
unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d) {
LOG_Z3_get_decl_num_parameters(c, d);
RESET_ERROR_CODE();
CHECK_VALID_AST(d, 0);
return to_func_decl(d)->get_num_parameters();
}
@ -397,6 +399,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_decl_parameter_kind(c, d, idx);
RESET_ERROR_CODE();
CHECK_VALID_AST(d, Z3_PARAMETER_INT);
if (idx >= to_func_decl(d)->get_num_parameters()) {
SET_ERROR_CODE(Z3_IOB, nullptr);
return Z3_PARAMETER_INT;
@ -429,6 +432,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_decl_int_parameter(c, d, idx);
RESET_ERROR_CODE();
CHECK_VALID_AST(d, 0);
if (idx >= to_func_decl(d)->get_num_parameters()) {
SET_ERROR_CODE(Z3_IOB, nullptr);
return 0;
@ -446,6 +450,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_decl_double_parameter(c, d, idx);
RESET_ERROR_CODE();
CHECK_VALID_AST(d, 0);
if (idx >= to_func_decl(d)->get_num_parameters()) {
SET_ERROR_CODE(Z3_IOB, nullptr);
return 0;
@ -463,6 +468,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_decl_symbol_parameter(c, d, idx);
RESET_ERROR_CODE();
CHECK_VALID_AST(d, 0);
if (idx >= to_func_decl(d)->get_num_parameters()) {
SET_ERROR_CODE(Z3_IOB, nullptr);
return nullptr;
@ -480,6 +486,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_decl_sort_parameter(c, d, idx);
RESET_ERROR_CODE();
CHECK_VALID_AST(d, 0);
if (idx >= to_func_decl(d)->get_num_parameters()) {
SET_ERROR_CODE(Z3_IOB, nullptr);
RETURN_Z3(nullptr);
@ -497,6 +504,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_decl_ast_parameter(c, d, idx);
RESET_ERROR_CODE();
CHECK_VALID_AST(d, 0);
if (idx >= to_func_decl(d)->get_num_parameters()) {
SET_ERROR_CODE(Z3_IOB, nullptr);
RETURN_Z3(nullptr);
@ -514,6 +522,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_decl_func_decl_parameter(c, d, idx);
RESET_ERROR_CODE();
CHECK_VALID_AST(d, 0);
if (idx >= to_func_decl(d)->get_num_parameters()) {
SET_ERROR_CODE(Z3_IOB, nullptr);
RETURN_Z3(nullptr);
@ -531,6 +540,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_decl_rational_parameter(c, d, idx);
RESET_ERROR_CODE();
CHECK_VALID_AST(d, "");
if (idx >= to_func_decl(d)->get_num_parameters()) {
SET_ERROR_CODE(Z3_IOB, nullptr);
return "";
@ -549,6 +559,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_sort_name(c, t);
RESET_ERROR_CODE();
CHECK_VALID_AST(t, nullptr);
return of_symbol(to_sort(t)->get_name());
Z3_CATCH_RETURN(nullptr);
}
@ -567,6 +578,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_arity(c, d);
RESET_ERROR_CODE();
CHECK_VALID_AST(d, 0);
return to_func_decl(d)->get_arity();
Z3_CATCH_RETURN(0);
}
@ -575,6 +587,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_domain_size(c, d);
RESET_ERROR_CODE();
CHECK_VALID_AST(d, 0);
return to_func_decl(d)->get_arity();
Z3_CATCH_RETURN(0);
}
@ -583,6 +596,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_domain(c, d, i);
RESET_ERROR_CODE();
CHECK_VALID_AST(d, 0);
if (i >= to_func_decl(d)->get_arity()) {
SET_ERROR_CODE(Z3_IOB, nullptr);
RETURN_Z3(nullptr);

21
src/api/api_numeral.cpp
View file

@ -26,6 +26,7 @@ Revision History:
#include "ast/fpa_decl_plugin.h"
bool is_numeral_sort(Z3_context c, Z3_sort ty) {
if (!ty) return false;
sort * _ty = to_sort(ty);
family_id fid = _ty->get_family_id();
if (fid != mk_c(c)->get_arith_fid() &&
@ -145,7 +146,8 @@ extern "C" {
Z3_bool Z3_API Z3_is_numeral_ast(Z3_context c, Z3_ast a) {
Z3_TRY;
LOG_Z3_is_numeral_ast(c, a);
RESET_ERROR_CODE();
RESET_ERROR_CODE();
CHECK_IS_EXPR(a, Z3_FALSE);
expr* e = to_expr(a);
return
mk_c(c)->autil().is_numeral(e) ||
@ -160,11 +162,8 @@ extern "C" {
Z3_TRY;
// This function is not part of the public API
RESET_ERROR_CODE();
CHECK_IS_EXPR(a, Z3_FALSE);
expr* e = to_expr(a);
if (!e) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return Z3_FALSE;
}
if (mk_c(c)->autil().is_numeral(e, r)) {
return Z3_TRUE;
}
@ -187,6 +186,7 @@ extern "C" {
// This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
LOG_Z3_get_numeral_string(c, a);
RESET_ERROR_CODE();
CHECK_IS_EXPR(a, "");
rational r;
Z3_bool ok = Z3_get_numeral_rational(c, a, r);
if (ok == Z3_TRUE) {
@ -232,11 +232,8 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_numeral_decimal_string(c, a, precision);
RESET_ERROR_CODE();
CHECK_IS_EXPR(a, "");
expr* e = to_expr(a);
if (!e) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return "";
}
rational r;
arith_util & u = mk_c(c)->autil();
if (u.is_numeral(e, r) && !r.is_int()) {
@ -267,6 +264,7 @@ extern "C" {
// This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
LOG_Z3_get_numeral_small(c, a, num, den);
RESET_ERROR_CODE();
CHECK_IS_EXPR(a, Z3_FALSE);
rational r;
Z3_bool ok = Z3_get_numeral_rational(c, a, r);
if (ok == Z3_TRUE) {
@ -292,6 +290,7 @@ extern "C" {
// This function invokes Z3_get_numeral_int64, but it is still ok to add LOG command here because it does not return a Z3 object.
LOG_Z3_get_numeral_int(c, v, i);
RESET_ERROR_CODE();
CHECK_IS_EXPR(v, Z3_FALSE);
if (!i) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return Z3_FALSE;
@ -310,6 +309,7 @@ extern "C" {
// This function invokes Z3_get_numeral_uint64, but it is still ok to add LOG command here because it does not return a Z3 object.
LOG_Z3_get_numeral_uint(c, v, u);
RESET_ERROR_CODE();
CHECK_IS_EXPR(v, Z3_FALSE);
if (!u) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return Z3_FALSE;
@ -328,6 +328,7 @@ extern "C" {
// This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
LOG_Z3_get_numeral_uint64(c, v, u);
RESET_ERROR_CODE();
CHECK_IS_EXPR(v, Z3_FALSE);
if (!u) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return Z3_FALSE;
@ -348,6 +349,7 @@ extern "C" {
// This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
LOG_Z3_get_numeral_int64(c, v, i);
RESET_ERROR_CODE();
CHECK_IS_EXPR(v, Z3_FALSE);
if (!i) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return Z3_FALSE;
@ -367,6 +369,7 @@ extern "C" {
// This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
LOG_Z3_get_numeral_rational_int64(c, v, num, den);
RESET_ERROR_CODE();
CHECK_IS_EXPR(v, Z3_FALSE);
if (!num || !den) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return Z3_FALSE;

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

@ -1675,7 +1675,6 @@ def Or(*args):
class PatternRef(ExprRef):
"""Patterns are hints for quantifier instantiation.
See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
"""
def as_ast(self):
return Z3_pattern_to_ast(self.ctx_ref(), self.ast)
@ -1686,8 +1685,6 @@ class PatternRef(ExprRef):
def is_pattern(a):
"""Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ])
@ -1705,8 +1702,6 @@ def is_pattern(a):
def MultiPattern(*args):
"""Create a Z3 multi-pattern using the given expressions `*args`
See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
>>> f = Function('f', IntSort(), IntSort())
>>> g = Function('g', IntSort(), IntSort())
>>> x = Int('x')
@ -1966,8 +1961,6 @@ def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> x = Int('x')
>>> y = Int('y')
@ -1985,7 +1978,6 @@ def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> x = Int('x')