mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

Merge pull request #1431 from waywardmonkeys/typo-fixes

Browse source 
Typo fixes.
This commit is contained in:
Nikolaj Bjorner 2018-01-02 07:56:31 -08:00 • committed by GitHub
commit f5bba63674
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
33 changed files with 120 additions and 120 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/api/dotnet/Context.cs
View file

@ -2262,7 +2262,7 @@ namespace Microsoft.Z3
/// Maps f on the argument arrays.
/// </summary>
/// <remarks>
/// Eeach element of <c>args</c> must be of an array sort <c>[domain_i -> range_i]</c>.
/// Each element of <c>args</c> must be of an array sort <c>[domain_i -> range_i]</c>.
/// The function declaration <c>f</c> must have type <c> range_1 .. range_n -> range</c>.
/// <c>v</c> must have sort range. The sort of the result is <c>[domain_i -> range]</c>.
/// <seealso cref="MkArraySort(Sort, Sort)"/>
@ -2862,7 +2862,7 @@ namespace Microsoft.Z3
}
/// <summary>
/// Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer.
/// Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer.
/// It is slightly faster than <c>MakeNumeral</c> since it is not necessary to parse a string.
/// </summary>
/// <param name="v">Value of the numeral</param>
@ -2878,7 +2878,7 @@ namespace Microsoft.Z3
}
/// <summary>
/// Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer.
/// Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer.
/// It is slightly faster than <c>MakeNumeral</c> since it is not necessary to parse a string.
/// </summary>
/// <param name="v">Value of the numeral</param>
@ -2894,7 +2894,7 @@ namespace Microsoft.Z3
}
/// <summary>
/// Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer.
/// Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer.
/// It is slightly faster than <c>MakeNumeral</c> since it is not necessary to parse a string.
/// </summary>
/// <param name="v">Value of the numeral</param>
@ -2910,7 +2910,7 @@ namespace Microsoft.Z3
}
/// <summary>
/// Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer.
/// Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer.
/// It is slightly faster than <c>MakeNumeral</c> since it is not necessary to parse a string.
/// </summary>
/// <param name="v">Value of the numeral</param>
@ -3211,7 +3211,7 @@ namespace Microsoft.Z3
/// Create an existential Quantifier.
/// </summary>
/// <remarks>
/// Creates an existential quantifier using de-Brujin indexed variables.
/// Creates an existential quantifier using de-Bruijn indexed variables.
/// (<see cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>).
/// </remarks>
public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)

14
src/api/dotnet/Expr.cs
View file

@ -959,7 +959,7 @@ namespace Microsoft.Z3
/// Tn: (R t_n s_n)
/// [monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n))
/// Remark: if t_i == s_i, then the antecedent Ti is suppressed.
/// That is, reflexivity proofs are supressed to save space.
/// That is, reflexivity proofs are suppressed to save space.
/// </remarks>
public bool IsProofMonotonicity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MONOTONICITY; } }
@ -1002,7 +1002,7 @@ namespace Microsoft.Z3
public bool IsProofAndElimination { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_AND_ELIM; } }
/// <summary>
/// Indicates whether the term is a proof by eliminiation of not-or
/// Indicates whether the term is a proof by elimination of not-or
/// </summary>
/// <remarks>
/// Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i).
@ -1112,7 +1112,7 @@ namespace Microsoft.Z3
public bool IsProofQuantInst { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INST; } }
/// <summary>
/// Indicates whether the term is a hypthesis marker.
/// Indicates whether the term is a hypothesis marker.
/// </summary>
/// <remarks>Mark a hypothesis in a natural deduction style proof.</remarks>
public bool IsProofHypothesis { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_HYPOTHESIS; } }
@ -1433,7 +1433,7 @@ namespace Microsoft.Z3
/// <remarks>
/// Filter (restrict) a relation with respect to a predicate.
/// The first argument is a relation.
/// The second argument is a predicate with free de-Brujin indices
/// The second argument is a predicate with free de-Bruijn indices
/// corresponding to the columns of the relation.
/// So the first column in the relation has index 0.
/// </remarks>
@ -1649,7 +1649,7 @@ namespace Microsoft.Z3
public bool IsFPMul { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MUL; } }
/// <summary>
/// Indicates whether the term is a floating-point divison term
/// Indicates whether the term is a floating-point division term
/// </summary>
public bool IsFPDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_DIV; } }
@ -1709,7 +1709,7 @@ namespace Microsoft.Z3
public bool IsFPLe { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_LE; } }
/// <summary>
/// Indicates whether the term is a floating-point greater-than or erqual term
/// Indicates whether the term is a floating-point greater-than or equal term
/// </summary>
public bool IsFPGe { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_GE; } }
@ -1789,7 +1789,7 @@ namespace Microsoft.Z3
#region Bound Variables
/// <summary>
/// The de-Burijn index of a bound variable.
/// The de-Bruijn index of a bound variable.
/// </summary>
/// <remarks>
/// Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain

2
src/api/dotnet/Model.cs
View file

@ -253,7 +253,7 @@ namespace Microsoft.Z3
/// The uninterpreted sorts that the model has an interpretation for.
/// </summary>
/// <remarks>
/// Z3 also provides an intepretation for uninterpreted sorts used in a formula.
/// Z3 also provides an interpretation for uninterpreted sorts used in a formula.
/// The interpretation for a sort is a finite set of distinct values. We say this finite set is
/// the "universe" of the sort.
/// </remarks>

6
src/api/java/Context.java
View file

@ -2234,7 +2234,7 @@ public class Context implements AutoCloseable {
}
/**
* Create a Term of a given sort. This function can be use to create
* Create a Term of a given sort. This function can be used to create
* numerals that fit in a machine integer. It is slightly faster than
* {@code MakeNumeral} since it is not necessary to parse a string.
*
@ -2250,7 +2250,7 @@ public class Context implements AutoCloseable {
}
/**
* Create a Term of a given sort. This function can be use to create
* Create a Term of a given sort. This function can be used to create
* numerals that fit in a machine integer. It is slightly faster than
* {@code MakeNumeral} since it is not necessary to parse a string.
*
@ -2438,7 +2438,7 @@ public class Context implements AutoCloseable {
}
/**
* Creates an existential quantifier using de-Brujin indexed variables.
* Creates an existential quantifier using de-Bruijn indexed variables.
* @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
**/
public Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body,

10
src/api/java/Expr.java
View file

@ -1421,7 +1421,7 @@ public class Expr extends AST
* Remarks: T1:
* (R t_1 s_1) ... Tn: (R t_n s_n) [monotonicity T1 ... Tn]: (R (f t_1 ...
* t_n) (f s_1 ... s_n)) Remark: if t_i == s_i, then the antecedent Ti is
* suppressed. That is, reflexivity proofs are supressed to save space.
* suppressed. That is, reflexivity proofs are suppressed to save space.
*
* @throws Z3Exception on error
* @return a boolean
@ -1473,7 +1473,7 @@ public class Expr extends AST
}
/**
* Indicates whether the term is a proof by eliminiation of not-or
* Indicates whether the term is a proof by elimination of not-or
* Remarks: * Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i). * T1: (not (or l_1 ... l_n)) [not-or-elim T1]: (not l_i)
* @throws Z3Exception on error
* @return a boolean
@ -1605,7 +1605,7 @@ public class Expr extends AST
}
/**
* Indicates whether the term is a hypthesis marker.
* Indicates whether the term is a hypothesis marker.
* Remarks: Mark a
* hypothesis in a natural deduction style proof.
* @throws Z3Exception on error
@ -1987,7 +1987,7 @@ public class Expr extends AST
* Indicates whether the term is a relation filter
* Remarks: Filter
* (restrict) a relation with respect to a predicate. The first argument is
* a relation. The second argument is a predicate with free de-Brujin
* a relation. The second argument is a predicate with free de-Bruijn
* indices corresponding to the columns of the relation. So the first column
* in the relation has index 0.
* @throws Z3Exception on error
@ -2094,7 +2094,7 @@ public class Expr extends AST
}
/**
* The de-Burijn index of a bound variable.
* The de-Bruijn index of a bound variable.
* Remarks: Bound variables are
* indexed by de-Bruijn indices. It is perhaps easiest to explain the
* meaning of de-Bruijn indices by indicating the compilation process from

2
src/api/java/Model.java
View file

@ -239,7 +239,7 @@ public class Model extends Z3Object {
/**
* The uninterpreted sorts that the model has an interpretation for.
* Remarks: Z3 also provides an intepretation for uninterpreted sorts used
* Remarks: Z3 also provides an interpretation for uninterpreted sorts used
* in a formula. The interpretation for a sort is a finite set of distinct
* values. We say this finite set is the "universe" of the sort.
*

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

@ -536,7 +536,7 @@ sig
@return A Term with the given value and sort *)
val mk_numeral_string : context -> string -> Sort.sort -> expr
(** Create a numeral of a given sort. This function can be use to create numerals that fit in a machine integer.
(** Create a numeral of a given sort. This function can be used to create numerals that fit in a machine integer.
It is slightly faster than [MakeNumeral] since it is not necessary to parse a string.
@return A Term with the given value and sort *)
val mk_numeral_int : context -> int -> Sort.sort -> expr
@ -667,7 +667,7 @@ sig
end
(** The de-Burijn index of a bound variable.
(** The de-Bruijn index of a bound variable.
Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain
the meaning of de-Bruijn indices by indicating the compilation process from
@ -830,7 +830,7 @@ sig
(** Maps f on the argument arrays.
Eeach element of [args] must be of an array sort [[domain_i -> range_i]].
Each element of [args] must be of an array sort [[domain_i -> range_i]].
The function declaration [f] must have type [ range_1 .. range_n -> range].
[v] must have sort range. The sort of the result is [[domain_i -> range]].
{!Z3Array.mk_sort}
@ -962,7 +962,7 @@ sig
Filter (restrict) a relation with respect to a predicate.
The first argument is a relation.
The second argument is a predicate with free de-Brujin indices
The second argument is a predicate with free de-Bruijn indices
corresponding to the columns of the relation.
So the first column in the relation has index 0. *)
val is_filter : Expr.expr -> bool
@ -2085,7 +2085,7 @@ sig
(** Indicates whether an expression is a floating-point lt expression *)
val is_lt : Expr.expr -> bool
(** Indicates whether an expression is a floating-point geqexpression *)
(** Indicates whether an expression is a floating-point geq expression *)
val is_geq : Expr.expr -> bool
(** Indicates whether an expression is a floating-point gt expression *)
@ -2233,7 +2233,7 @@ sig
(** Conversion of a 2's complement unsigned bit-vector term into a term of FloatingPoint sort. *)
val mk_to_fp_unsigned : context -> Expr.expr -> Expr.expr -> Sort.sort -> Expr.expr
(** C1onversion of a floating-point term into an unsigned bit-vector. *)
(** Conversion of a floating-point term into an unsigned bit-vector. *)
val mk_to_ubv : context -> Expr.expr -> Expr.expr -> int -> Expr.expr
(** Conversion of a floating-point term into a signed bit-vector. *)
@ -2385,7 +2385,7 @@ sig
Tn: (R t_n s_n)
[monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n))
Remark: if t_i == s_i, then the antecedent Ti is suppressed.
That is, reflexivity proofs are supressed to save space. *)
That is, reflexivity proofs are suppressed to save space. *)
val is_monotonicity : Expr.expr -> bool
(** Indicates whether the term is a quant-intro proof
@ -2417,7 +2417,7 @@ sig
[and-elim T1]: l_i *)
val is_and_elimination : Expr.expr -> bool
(** Indicates whether the term is a proof by eliminiation of not-or
(** Indicates whether the term is a proof by elimination of not-or
Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i).
T1: (not (or l_1 ... l_n))
@ -2500,7 +2500,7 @@ sig
A proof of (or (not (forall (x) (P x))) (P a)) *)
val is_quant_inst : Expr.expr -> bool
(** Indicates whether the term is a hypthesis marker.
(** Indicates whether the term is a hypothesis marker.
Mark a hypothesis in a natural deduction style proof. *)
val is_hypothesis : Expr.expr -> bool
@ -2882,7 +2882,7 @@ sig
(** The uninterpreted sorts that the model has an interpretation for.
Z3 also provides an intepretation for uninterpreted sorts used in a formula.
Z3 also provides an interpretation for uninterpreted sorts used in a formula.
The interpretation for a sort is a finite set of distinct values. We say this finite set is
the "universe" of the sort.
{!get_num_sorts}
@ -3056,7 +3056,7 @@ sig
(** Create a tactic that fails if the probe evaluates to false. *)
val fail_if : context -> Probe.probe -> tactic
(** Create a tactic that fails if the goal is not triviall satisfiable (i.e., empty)
(** Create a tactic that fails if the goal is not trivially satisfiable (i.e., empty)
or trivially unsatisfiable (i.e., contains `false'). *)
val fail_if_not_decided : context -> tactic
@ -3105,7 +3105,7 @@ sig
(** True if the entry is float-valued. *)
val is_float : statistics_entry -> bool
(** The string representation of the the entry's value. *)
(** The string representation of the entry's value. *)
val to_string_value : statistics_entry -> string
(** The string representation of the entry (key and value) *)
@ -3370,7 +3370,7 @@ sig
(** Assert a constraints into the optimize solver. *)
val add : optimize -> Expr.expr list -> unit
(** Asssert a soft constraint.
(** Assert a soft constraint.
Supply integer weight and string that identifies a group
of soft constraints. *)
val add_soft : optimize -> Expr.expr -> string -> Symbol.symbol -> handle

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

@ -182,7 +182,7 @@ class Context:
"""Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions.
This method can be invoked from a thread different from the one executing the
interruptable procedure.
interruptible procedure.
"""
Z3_interrupt(self.ref())
@ -602,7 +602,7 @@ def _sort(ctx, a):
return _to_sort_ref(Z3_get_sort(ctx.ref(), a), ctx)
def DeclareSort(name, ctx=None):
"""Create a new uninterpred sort named `name`.
"""Create a new uninterpreted sort named `name`.
If `ctx=None`, then the new sort is declared in the global Z3Py context.
@ -724,7 +724,7 @@ class FuncDeclRef(AstRef):
The arguments must be Z3 expressions. This method assumes that
the sorts of the elements in `args` match the sorts of the
domain. Limited coersion is supported. For example, if
domain. Limited coercion is supported. For example, if
args[0] is a Python integer, and the function expects a Z3
integer, then the argument is automatically converted into a
Z3 integer.
@ -9243,7 +9243,7 @@ def fpMul(rm, a, b, ctx=None):
return _mk_fp_bin(Z3_mk_fpa_mul, rm, a, b, ctx)
def fpDiv(rm, a, b, ctx=None):
"""Create a Z3 floating-point divison expression.
"""Create a Z3 floating-point division expression.
>>> s = FPSort(8, 24)
>>> rm = RNE()
@ -9270,7 +9270,7 @@ def fpRem(a, b, ctx=None):
return _mk_fp_bin_norm(Z3_mk_fpa_rem, a, b, ctx)
def fpMin(a, b, ctx=None):
"""Create a Z3 floating-point minimium expression.
"""Create a Z3 floating-point minimum expression.
>>> s = FPSort(8, 24)
>>> rm = RNE()

50
src/api/z3_api.h
View file

@ -270,7 +270,7 @@ typedef enum
- Z3_OP_ARRAY_MAP Array map operator.
It satisfies map[f](a1,..,a_n)[i] = f(a1[i],...,a_n[i]) for every i.
- Z3_OP_SET_UNION Set union between two Booelan arrays (two arrays whose range type is Boolean). The function is binary.
- Z3_OP_SET_UNION Set union between two Boolean arrays (two arrays whose range type is Boolean). The function is binary.
- Z3_OP_SET_INTERSECT Set intersection between two Boolean arrays. The function is binary.
@ -406,7 +406,7 @@ typedef enum
- Z3_OP_BSMUL_NO_UDFL: check that bit-wise signed multiplication does not underflow.
Signed multiplication underflows if the operands have opposite signs and the result of multiplication
does not fit within the avaialble bits. Z3_mk_bvmul_no_underflow.
does not fit within the available bits. Z3_mk_bvmul_no_underflow.
- Z3_OP_BSDIV_I: Binary signed division.
It has the same semantics as Z3_OP_BSDIV, but created in a context where the second operand can be assumed to be non-zero.
@ -485,7 +485,7 @@ typedef enum
[monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n))
}
Remark: if t_i == s_i, then the antecedent Ti is suppressed.
That is, reflexivity proofs are supressed to save space.
That is, reflexivity proofs are suppressed to save space.
- Z3_OP_PR_QUANT_INTRO: Given a proof for (~ p q), produces a proof for (~ (forall (x) p) (forall (x) q)).
@ -832,7 +832,7 @@ typedef enum
- Z3_OP_RA_FILTER: Filter (restrict) a relation with respect to a predicate.
The first argument is a relation.
The second argument is a predicate with free de-Brujin indices
The second argument is a predicate with free de-Bruijn indices
corresponding to the columns of the relation.
So the first column in the relation has index 0.
@ -969,7 +969,7 @@ typedef enum
- Z3_OP_FPA_TO_FP: Floating-point conversion (various)
- Z3_OP_FPA_TO_FP_UNSIGNED: Floating-point conversion from unsigend bit-vector
- Z3_OP_FPA_TO_FP_UNSIGNED: Floating-point conversion from unsigned bit-vector
- Z3_OP_FPA_TO_UBV: Floating-point conversion to unsigned bit-vector
@ -984,7 +984,7 @@ typedef enum
of non-relevant terms in theory_fpa)
- Z3_OP_FPA_BV2RM: Conversion of a 3-bit bit-vector term to a
floating-point rouding-mode term
floating-point rounding-mode term
The conversion uses the following values:
0 = 000 = Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN,
@ -1922,7 +1922,7 @@ extern "C" {
\param c logical context
\param name name of the enumeration sort.
\param n number of elemenets in enumeration sort.
\param n number of elements in enumeration sort.
\param enum_names names of the enumerated elements.
\param enum_consts constants corresponding to the enumerated elements.
\param enum_testers predicates testing if terms of the enumeration sort correspond to an enumeration.
@ -3186,7 +3186,7 @@ extern "C" {
\param c logical context.
\param num numerator of rational.
\param den denomerator of rational.
\param den denominator of rational.
\pre den != 0
@ -3201,7 +3201,7 @@ extern "C" {
/**
\brief Create a numeral of an int, bit-vector, or finite-domain sort.
This function can be use to create numerals that fit in a machine integer.
This function can be used to create numerals that fit in a machine integer.
It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string.
\sa Z3_mk_numeral
@ -3213,7 +3213,7 @@ extern "C" {
/**
\brief Create a numeral of a int, bit-vector, or finite-domain sort.
This function can be use to create numerals that fit in a machine unsinged integer.
This function can be used to create numerals that fit in a machine unsigned integer.
It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string.
\sa Z3_mk_numeral
@ -3225,7 +3225,7 @@ extern "C" {
/**
\brief Create a numeral of a int, bit-vector, or finite-domain sort.
This function can be use to create numerals that fit in a machine __int64 integer.
This function can be used to create numerals that fit in a machine __int64 integer.
It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string.
\sa Z3_mk_numeral
@ -3237,7 +3237,7 @@ extern "C" {
/**
\brief Create a numeral of a int, bit-vector, or finite-domain sort.
This function can be use to create numerals that fit in a machine __uint64 integer.
This function can be used to create numerals that fit in a machine __uint64 integer.
It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string.
\sa Z3_mk_numeral
@ -3493,8 +3493,8 @@ extern "C" {
Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi);
/**
\brief Create a regular expression loop. The supplied regular expression \c r is repated
between \c lo and \c hi times. The \c lo should be below \c hi with one exection: when
\brief Create a regular expression loop. The supplied regular expression \c r is repeated
between \c lo and \c hi times. The \c lo should be below \c hi with one exception: when
supplying the value \c hi as 0, the meaning is to repeat the argument \c r at least
\c lo number of times, and with an unbounded upper bound.
@ -4248,7 +4248,7 @@ extern "C" {
Z3_sort Z3_API Z3_get_decl_sort_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
/**
\brief Return the expresson value associated with an expression parameter.
\brief Return the expression value associated with an expression parameter.
\pre Z3_get_decl_parameter_kind(c, d, idx) == Z3_PARAMETER_AST
@ -4257,7 +4257,7 @@ extern "C" {
Z3_ast Z3_API Z3_get_decl_ast_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
/**
\brief Return the expresson value associated with an expression parameter.
\brief Return the expression value associated with an expression parameter.
\pre Z3_get_decl_parameter_kind(c, d, idx) == Z3_PARAMETER_FUNC_DECL
@ -4327,7 +4327,7 @@ extern "C" {
/**
\brief Return a hash code for the given AST.
The hash code is structural. You can use Z3_get_ast_id interchangably with
The hash code is structural. You can use Z3_get_ast_id interchangeably with
this function.
def_API('Z3_get_ast_hash', UINT, (_in(CONTEXT), _in(AST)))
@ -4556,7 +4556,7 @@ extern "C" {
Z3_ast Z3_API Z3_get_pattern(Z3_context c, Z3_pattern p, unsigned idx);
/**
\brief Return index of de-Brujin bound variable.
\brief Return index of de-Bruijn bound variable.
\pre Z3_get_ast_kind(a) == Z3_VAR_AST
@ -4659,7 +4659,7 @@ extern "C" {
Provides an interface to the AST simplifier used by Z3.
It returns an AST object which is equal to the argument.
The returned AST is simplified using algebraic simplificaiton rules,
The returned AST is simplified using algebraic simplification rules,
such as constant propagation (propagating true/false over logical connectives).
def_API('Z3_simplify', AST, (_in(CONTEXT), _in(AST)))
@ -4861,9 +4861,9 @@ extern "C" {
Z3_func_decl Z3_API Z3_model_get_func_decl(Z3_context c, Z3_model m, unsigned i);
/**
\brief Return the number of uninterpreted sorts that \c m assigs an interpretation to.
\brief Return the number of uninterpreted sorts that \c m assigns an interpretation to.
Z3 also provides an intepretation for uninterpreted sorts used in a formua.
Z3 also provides an interpretation for uninterpreted sorts used in a formula.
The interpretation for a sort \c s is a finite set of distinct values. We say this finite set is
the "universe" of \c s.
@ -4971,7 +4971,7 @@ extern "C" {
unsigned Z3_API Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f);
/**
\brief Return a "point" of the given function intepretation. It represents the
\brief Return a "point" of the given function interpretation. It represents the
value of \c f in a particular point.
\pre i < Z3_func_interp_get_num_entries(c, f)
@ -5013,7 +5013,7 @@ extern "C" {
\brief add a function entry to a function interpretation.
\param c logical context
\param fi a function interpregation to be updated.
\param fi a function interpretation to be updated.
\param args list of arguments. They should be constant values (such as integers) and be of the same types as the domain of the function.
\param value value of the function when the parameters match args.
@ -5466,7 +5466,7 @@ extern "C" {
Z3_bool Z3_API Z3_goal_is_decided_unsat(Z3_context c, Z3_goal g);
/**
\brief Copy a goal \c g from the context \c source to a the context \c target.
\brief Copy a goal \c g from the context \c source to the context \c target.
def_API('Z3_goal_translate', GOAL, (_in(CONTEXT), _in(GOAL), _in(CONTEXT)))
*/
@ -5932,7 +5932,7 @@ extern "C" {
Z3_solver Z3_API Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t);
/**
\brief Copy a solver \c s from the context \c source to a the context \c target.
\brief Copy a solver \c s from the context \c source to the context \c target.
def_API('Z3_solver_translate', SOLVER, (_in(CONTEXT), _in(SOLVER), _in(CONTEXT)))
*/