mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

Merge pull request #1641 from waywardmonkeys/remove-proof-mode-from-ocaml-docs

Browse source 
Update OCaml docs for changes made elsewhere.
This commit is contained in:
Nikolaj Bjorner 2018-05-23 10:01:11 -07:00 • committed by GitHub
commit 148ccc93f0
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 2 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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.