mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-02 20:31:21 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-05-23 10:30:22 -07:00
commit a9b1966ff2
3 changed files with 7 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/c++/z3++.h
View file

@ -187,7 +187,7 @@ namespace z3 {
\brief The C++ API uses by defaults exceptions on errors. \brief The C++ API uses by defaults exceptions on errors.
For applications that don't work well with exceptions (there should be only few) 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 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. erroneous state.
*/ */
void set_enable_exceptions(bool f) { m_enable_exceptions = f; } void set_enable_exceptions(bool f) { m_enable_exceptions = f; }

7
src/api/ml/z3.mli
View file

@ -2362,7 +2362,7 @@ sig
(** Indicates whether the term is a proof by condensed transitivity of a relation (** 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. It combines several symmetry and transitivity proofs.
Example: Example:
T1: (R a b) T1: (R a b)
@ -2443,14 +2443,11 @@ sig
(** Indicates whether the term is a proof by rewriting (** Indicates whether the term is a proof by rewriting
A proof for rewriting an expression t into an expression s. 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. This proof object can have n antecedents.
The antecedents are proofs for equalities used as substitution rules. 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 object is also used in a few cases. The cases are:
The cases are:
- When applying contextual simplification (CONTEXT_SIMPLIFIER=true) - When applying contextual simplification (CONTEXT_SIMPLIFIER=true)
- When converting bit-vectors to Booleans (BIT2BOOL=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 val is_rewrite_star : Expr.expr -> bool
(** Indicates whether the term is a proof for pulling quantifiers out. (** Indicates whether the term is a proof for pulling quantifiers out.

8
src/api/z3_api.h
View file

@ -83,14 +83,14 @@ typedef const char * Z3_string;
typedef Z3_string * Z3_string_ptr; 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. \brief Lifted Boolean type: \c false, \c undefined, \c true.