mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

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

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-03-16 07:46:35 -07:00
parent 86d3bbe6cb 3a4a58ecfd
commit b93a04c38f
4 changed files with 2 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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. *) 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 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. (** Indicates whether the term is a proof for pushing quantifiers in.
A proof for: A proof for:
@ -2658,22 +2651,6 @@ sig
(and (or r_1 r_2) (or r_1' r_2'))) *) (and (or r_1 r_2) (or r_1' r_2'))) *)
val is_nnf_neg : Expr.expr -> bool 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 (** Indicates whether the term is a proof for a Skolemization step
Proof for: Proof for:

3
src/api/python/z3/z3.py
View file

@ -368,9 +368,6 @@ class AstRef(Z3PPObject):
def __copy__(self): def __copy__(self):
return self.translate(self.ctx) return self.translate(self.ctx)
def __deepcopy__(self):
return self.translate(self.ctx)
def hash(self): def hash(self):
"""Return a hashcode for the `self`. """Return a hashcode for the `self`.

2
src/api/z3_algebraic.h
View file

@ -31,7 +31,7 @@ extern "C" {
/** @name Algebraic Numbers */ /** @name Algebraic Numbers */
/*@{*/ /*@{*/
/** /**
\brief Return Z3_TRUE if \c can be used as value in the Z3 real algebraic \brief Return Z3_TRUE if \c a can be used as value in the Z3 real algebraic
number package. number package.
def_API('Z3_algebraic_is_value', BOOL, (_in(CONTEXT), _in(AST))) def_API('Z3_algebraic_is_value', BOOL, (_in(CONTEXT), _in(AST)))

2
src/api/z3_api.h
View file

@ -4350,7 +4350,7 @@ extern "C" {
Z3_bool Z3_API Z3_is_numeral_ast(Z3_context c, Z3_ast a); Z3_bool Z3_API Z3_is_numeral_ast(Z3_context c, Z3_ast a);
/** /**
\brief Return true if the give AST is a real algebraic number. \brief Return true if the given AST is a real algebraic number.
def_API('Z3_is_algebraic_number', BOOL, (_in(CONTEXT), _in(AST))) def_API('Z3_is_algebraic_number', BOOL, (_in(CONTEXT), _in(AST)))
*/ */