From 510cb5ee6e9e8e7120b2112707e0ad3535e2f896 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Wed, 23 May 2018 23:51:36 +0700 Subject: [PATCH 1/3] Z3_TRUE/Z3_FALSE should be true/false, not 1/0. Now that Z3_bool is a C bool, the associated constants should be as well. --- src/api/z3_api.h | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 0825f27a0..d5c279d63 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -83,14 +83,14 @@ typedef const char * Z3_string; typedef Z3_string * Z3_string_ptr; /** - \brief True value. It is just an alias for \c 1. + \brief True value. It is just an alias for \c true. */ -#define Z3_TRUE 1 +#define Z3_TRUE true /** - \brief False value. It is just an alias for \c 0. + \brief False value. It is just an alias for \c false. */ -#define Z3_FALSE 0 +#define Z3_FALSE false /** \brief Lifted Boolean type: \c false, \c undefined, \c true. From a3facc82fb61888557980b392431e298c9add8e3 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Wed, 23 May 2018 23:52:51 +0700 Subject: [PATCH 2/3] Update OCaml docs for changes made elsewhere. This removes references to the PROOF_MODE that have been removed elsewhere. --- src/api/ml/z3.mli | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 14d2ceac4..0fd1242ee 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -2362,7 +2362,7 @@ sig (** Indicates whether the term is a proof by condensed transitivity of a relation - Condensed transitivity proof. This proof object is only used if the parameter PROOF_MODE is 1. + Condensed transitivity proof. It combines several symmetry and transitivity proofs. Example: T1: (R a b) @@ -2443,14 +2443,11 @@ sig (** Indicates whether the term is a proof by rewriting A proof for rewriting an expression t into an expression s. - This proof object is used if the parameter PROOF_MODE is 1. This proof object can have n antecedents. The antecedents are proofs for equalities used as substitution rules. - The object is also used in a few cases if the parameter PROOF_MODE is 2. - The cases are: + The object is also used in a few cases. The cases are: - When applying contextual simplification (CONTEXT_SIMPLIFIER=true) - When converting bit-vectors to Booleans (BIT2BOOL=true) - - When pulling ite expression up (PULL_CHEAP_ITE_TREES=true) *) val is_rewrite_star : Expr.expr -> bool (** Indicates whether the term is a proof for pulling quantifiers out. From 6db90a9333c0e44fca53cfb4d463c1a5189de6cb Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Wed, 23 May 2018 23:58:08 +0700 Subject: [PATCH 3/3] Fix missing word in C++ API docs. --- src/api/c++/z3++.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 8d7825335..eef5d7904 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -187,7 +187,7 @@ namespace z3 { \brief The C++ API uses by defaults exceptions on errors. For applications that don't work well with exceptions (there should be only few) you have the ability to turn off exceptions. The tradeoffs are that applications - have to very careful about using check_error() after calls that may result in an + have to be very careful about using check_error() after calls that may result in an erroneous state. */ void set_enable_exceptions(bool f) { m_enable_exceptions = f; }