mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

fix

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-03-14 18:14:29 -07:00
parent 46048d5150
commit b1f05d8271
1 changed files with 0 additions and 23 deletions

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

@ -2458,13 +2458,6 @@ sig
A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents. *)
val is_pull_quant : Expr.expr -> bool
(** Indicates whether the term is a proof for pulling quantifiers out.
A proof for (iff P Q) where Q is in prenex normal form.
This proof object is only used if the parameter PROOF_MODE is 1.
This proof object has no antecedents *)
val is_pull_quant_star : Expr.expr -> bool
(** Indicates whether the term is a proof for pushing quantifiers in.
A proof for:
@ -2658,22 +2651,6 @@ sig
(and (or r_1 r_2) (or r_1' r_2'))) *)
val is_nnf_neg : Expr.expr -> bool
(** Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form.
A proof for (~ P Q) where Q is in negation normal form.
This proof object is only used if the parameter PROOF_MODE is 1.
This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO. *)
val is_nnf_star : Expr.expr -> bool
(** Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form.
A proof for (~ P Q) where Q is in conjunctive normal form.
This proof object is only used if the parameter PROOF_MODE is 1.
This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO. *)
val is_cnf_star : Expr.expr -> bool
(** Indicates whether the term is a proof for a Skolemization step
Proof for: