mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

Update OCaml docs for changes made elsewhere.

Browse source 
This removes references to the PROOF_MODE that have been removed
elsewhere.
This commit is contained in:
Bruce Mitchener 2018-05-23 23:52:51 +07:00
parent f5775f265a
commit a3facc82fb
1 changed files with 2 additions and 5 deletions
Show stats 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
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.