diff --git a/README-CMake.md b/README-CMake.md index 0d323e08f..1b1f72729 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -5,7 +5,7 @@ of the project written in the ``CMakeLists.txt`` files and emits a build system for that project of your choice using one of CMake's "generators". This allows CMake to support many different platforms and build tools. You can run ``cmake --help`` to see the list of supported "generators" -on your platform. Example generators include "UNIX Makfiles" and "Visual Studio +on your platform. Example generators include "UNIX Makefiles" and "Visual Studio 12 2013". ## Getting started @@ -44,7 +44,7 @@ cmake -G "Unix Makefiles" ../ make -j4 # Replace 4 with an appropriate number ``` -Note that on some platforms "Unix Makesfiles" is the default generator so on those +Note that on some platforms "Unix Makefiles" is the default generator so on those platforms you don't need to pass ``-G "Unix Makefiles"`` command line option to ``cmake``. diff --git a/RELEASE_NOTES b/RELEASE_NOTES index 4f10cad26..5ce4d2682 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -712,7 +712,7 @@ The following bugs are fixed in this release: bvshl when using a shift amount that evaluates to the length of the bit-vector. Thanks to Trevor Hansen and Robert Brummayer. -- Incorrect NNF conversion in linear quantifier elimniation routines. +- Incorrect NNF conversion in linear quantifier elimination routines. Thanks to Josh Berdine. - Missing constant folding of extraction for large bit-vectors. diff --git a/cmake/Z3Config.cmake.in b/cmake/Z3Config.cmake.in index e7f604591..dbd63b103 100644 --- a/cmake/Z3Config.cmake.in +++ b/cmake/Z3Config.cmake.in @@ -2,7 +2,7 @@ # @AUTO_GEN_MSG@ # # This file is intended to be consumed by clients who wish to use Z3 from CMake. -# It can be use by doing `find_package(Z3 config)` from within a +# It can be used by doing `find_package(Z3 config)` from within a # `CMakeLists.txt` file. If CMake doesn't find this package automatically you # can give it a hint by passing `-DZ3_DIR=` to the CMake invocation where # `` is the path to the directory containing this file. diff --git a/contrib/suppressions/sanitizers/README.md b/contrib/suppressions/sanitizers/README.md index f76f920b2..1d7cd0ac8 100644 --- a/contrib/suppressions/sanitizers/README.md +++ b/contrib/suppressions/sanitizers/README.md @@ -1,4 +1,4 @@ -# Sanitizer supression files +# Sanitizer suppression files This directory contains files used to suppress ASan/LSan/UBSan warnings/errors. diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c index d71771f98..b947928a7 100644 --- a/examples/c/test_capi.c +++ b/examples/c/test_capi.c @@ -1546,7 +1546,7 @@ void two_contexts_example1() } /** - \brief Demonstrates how error codes can be read insted of registering an error handler. + \brief Demonstrates how error codes can be read instead of registering an error handler. */ void error_code_example1() { @@ -2533,7 +2533,7 @@ void reference_counter_example() { cfg = Z3_mk_config(); Z3_set_param_value(cfg, "model", "true"); - // Create a Z3 context where the user is reponsible for managing + // Create a Z3 context where the user is responsible for managing // Z3_ast reference counters. ctx = Z3_mk_context_rc(cfg); Z3_del_config(cfg); diff --git a/examples/dotnet/Program.cs b/examples/dotnet/Program.cs index 71364013b..aec3bdcc5 100644 --- a/examples/dotnet/Program.cs +++ b/examples/dotnet/Program.cs @@ -622,7 +622,7 @@ namespace test_mapi Console.WriteLine("{0}", q1); } - // Quantifier with de-Brujin indices. + // Quantifier with de-Bruijn indices. { Expr x = ctx.MkBound(1, ctx.IntSort); Expr y = ctx.MkBound(0, ctx.IntSort); diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index 40fb25a92..7b8902768 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -660,7 +660,7 @@ class JavaExample System.out.println(q1); } - // Quantifier with de-Brujin indices. + // Quantifier with de-Bruijn indices. { Expr x = ctx.mkBound(1, ctx.getIntSort()); Expr y = ctx.mkBound(0, ctx.getIntSort()); diff --git a/examples/maxsat/README b/examples/maxsat/README index e5e4ba610..6c24da66b 100644 --- a/examples/maxsat/README +++ b/examples/maxsat/README @@ -9,4 +9,4 @@ On OSX and Linux, you must install z3 first using sudo make install OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (OSX) with the build directory. You need that to be able to find the Z3 shared library. -This directory contains a test file (ex.smt) that can be use as input for the maxsat test application. +This directory contains a test file (ex.smt) that can be used as input for the maxsat test application. diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index ac23d1dbc..cbd6a1bac 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -2262,7 +2262,7 @@ namespace Microsoft.Z3 /// 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]. /// @@ -2862,7 +2862,7 @@ namespace Microsoft.Z3 } /// - /// 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 MakeNumeral since it is not necessary to parse a string. /// /// Value of the numeral @@ -2878,7 +2878,7 @@ namespace Microsoft.Z3 } /// - /// 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 MakeNumeral since it is not necessary to parse a string. /// /// Value of the numeral @@ -2894,7 +2894,7 @@ namespace Microsoft.Z3 } /// - /// 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 MakeNumeral since it is not necessary to parse a string. /// /// Value of the numeral @@ -2910,7 +2910,7 @@ namespace Microsoft.Z3 } /// - /// 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 MakeNumeral since it is not necessary to parse a string. /// /// Value of the numeral @@ -3211,7 +3211,7 @@ namespace Microsoft.Z3 /// Create an existential Quantifier. /// /// - /// Creates an existential quantifier using de-Brujin indexed variables. + /// Creates an existential quantifier using de-Bruijn indexed variables. /// (). /// public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index 4fd306052..0726f9d53 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -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. /// 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; } } /// - /// 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). @@ -1112,7 +1112,7 @@ namespace Microsoft.Z3 public bool IsProofQuantInst { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INST; } } /// - /// 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. public bool IsProofHypothesis { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_HYPOTHESIS; } } @@ -1433,7 +1433,7 @@ namespace Microsoft.Z3 /// /// 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. /// @@ -1649,7 +1649,7 @@ namespace Microsoft.Z3 public bool IsFPMul { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MUL; } } /// - /// Indicates whether the term is a floating-point divison term + /// Indicates whether the term is a floating-point division term /// 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; } } /// - /// 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 /// 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 /// - /// 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 diff --git a/src/api/dotnet/Model.cs b/src/api/dotnet/Model.cs index 12992fa8a..d11a57052 100644 --- a/src/api/dotnet/Model.cs +++ b/src/api/dotnet/Model.cs @@ -253,7 +253,7 @@ namespace Microsoft.Z3 /// 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. /// diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 3458f4d97..7e73fc15e 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -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, diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index d3793a24b..7b20b7993 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -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 diff --git a/src/api/java/Model.java b/src/api/java/Model.java index 9c7013aca..d809b6790 100644 --- a/src/api/java/Model.java +++ b/src/api/java/Model.java @@ -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. * diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 80923a0c7..20a1e9c10 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -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 diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 465e9aab8..4896a475d 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -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() diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 0ba49a5e5..5e5b84450 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -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))) */ diff --git a/src/ast/ast.h b/src/ast/ast.h index 2d06d03de..24e2b93b6 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -330,7 +330,7 @@ std::ostream& operator<<(std::ostream& out, sort_size const & ss); // ----------------------------------- /** - \brief Extra information that may be attached to intepreted sorts. + \brief Extra information that may be attached to interpreted sorts. */ class sort_info : public decl_info { sort_size m_num_elements; @@ -932,7 +932,7 @@ struct builtin_name { }; /** - \brief Each family of intepreted function declarations and sorts must provide a plugin + \brief Each family of interpreted function declarations and sorts must provide a plugin to build sorts and decls of the family. */ class decl_plugin { @@ -1059,7 +1059,7 @@ protected: ptr_vector m_eq_decls; // cached eqs ptr_vector m_ite_decls; // cached ites - ptr_vector m_oeq_decls; // cached obsevational eqs + ptr_vector m_oeq_decls; // cached observational eqs sort * m_proof_sort; func_decl * m_undef_decl; func_decl * m_true_pr_decl; @@ -1161,7 +1161,7 @@ public: virtual expr * get_some_value(sort * s); }; -typedef app proof; /* a proof is just an applicaton */ +typedef app proof; /* a proof is just an application */ // ----------------------------------- // @@ -1220,7 +1220,7 @@ enum pattern_op_kind { /** \brief Patterns are used to group expressions. These expressions are using during E-matching for - heurisitic quantifier instantiation. + heuristic quantifier instantiation. */ class pattern_decl_plugin : public decl_plugin { public: @@ -1245,13 +1245,13 @@ enum model_value_op_kind { /** \brief Values are used during model construction. All values are assumed to be different. Users should not use them, since they may - introduce unsoundess if the sort of a value is finite. + introduce unsoundness if the sort of a value is finite. Moreover, values should never be internalized in a logical context. However, values can be used during evaluation (i.e., simplification). - \remark Model values can be viewed as the partion ids in Z3 1.x. + \remark Model values can be viewed as the partition ids in Z3 1.x. */ class model_value_decl_plugin : public decl_plugin { public: diff --git a/src/ast/proofs/proof_checker.cpp b/src/ast/proofs/proof_checker.cpp index 6fd876efc..5126198c6 100644 --- a/src/ast/proofs/proof_checker.cpp +++ b/src/ast/proofs/proof_checker.cpp @@ -502,7 +502,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) { return false; } case PR_HYPOTHESIS: { - // TBD all branches with hyptheses must be closed by a later lemma. + // TBD all branches with hypotheses must be closed by a later lemma. if (match_proof(p) && match_fact(p, fml)) { return true; diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index fc9d0fac6..32cb9cccb 100755 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -55,7 +55,7 @@ class iz3proof_itp_impl : public iz3proof_itp { /* The summation rule. The term sum(p,c,i) takes a proof p of an inequality i', an integer coefficient c and an inequality i, and - yieds a proof of i' + ci. */ + yields a proof of i' + ci. */ symb sum; /* Proof rotation. The proof term rotate(q,p) takes a @@ -75,7 +75,7 @@ class iz3proof_itp_impl : public iz3proof_itp { symb leq2eq; /* Equality to inequality. eq2leq(p, q) takes a proof p of x=y, and - a proof q ~(x <= y) and and yields a proof of false. */ + a proof q ~(x <= y) and yields a proof of false. */ symb eq2leq; /* Proof term cong(p,q) takes a proof p of x=y and a proof @@ -97,7 +97,7 @@ class iz3proof_itp_impl : public iz3proof_itp { /* This oprerator represents a concatenation of rewrites. The term a=b;c=d represents an A rewrite from a to b, followed by a B - rewrite fron b to c, followed by an A rewrite from c to d. + rewrite from b to c, followed by an A rewrite from c to d. */ symb concat; @@ -1542,7 +1542,7 @@ class iz3proof_itp_impl : public iz3proof_itp { return my_implies(arg(rew,1),arg(rew,2)); } - // make rewrite rew conditon on rewrite cond + // make rewrite rew condition on rewrite cond ast rewrite_conditional(const ast &cond, const ast &rew){ ast cf = rewrite_to_formula(cond); return make(sym(rew),arg(rew,0),my_and(arg(rew,1),cf),arg(rew,2)); diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp index b88e488b4..e71475e45 100755 --- a/src/interp/iz3translate_direct.cpp +++ b/src/interp/iz3translate_direct.cpp @@ -9,7 +9,7 @@ Translate a Z3 proof into the interpolating proof calculus. Translation is direct, without transformations on the target proof - representaiton. + representation. Author: diff --git a/src/math/simplex/simplex_def.h b/src/math/simplex/simplex_def.h index 762e8ceb2..ceec60622 100644 --- a/src/math/simplex/simplex_def.h +++ b/src/math/simplex/simplex_def.h @@ -634,7 +634,7 @@ namespace simplex { // // max { c*x | A*x = 0 and l <= x <= u } // - // start with feasible assigment + // start with feasible assignment // A*x0 = 0 and l <= x0 <= u // // Identify pivot: i, j: such that x_i is base, diff --git a/src/muz/rel/dl_compiler.h b/src/muz/rel/dl_compiler.h index 9aedf141a..6ac33ae91 100644 --- a/src/muz/rel/dl_compiler.h +++ b/src/muz/rel/dl_compiler.h @@ -60,7 +60,7 @@ namespace datalog { ACK_UNBOUND_VAR(var_index) - encodes that the column contains a variable that is unbound (by the corresponding rule body), - var_index is the de-Brujin index (var->get_idx()) + var_index is the de-Bruijn index (var->get_idx()) of the variable associated with the column. ACK_CONSTANT(constant) - encodes that the column contains the constant. diff --git a/src/muz/rel/dl_relation_manager.h b/src/muz/rel/dl_relation_manager.h index c77127eb7..610c523e1 100644 --- a/src/muz/rel/dl_relation_manager.h +++ b/src/muz/rel/dl_relation_manager.h @@ -609,7 +609,7 @@ namespace datalog { std::string to_nice_string(const relation_element & el) const; /** This one may give a nicer representation of \c el than the - \c to_nice_string(const relation_element & el) function, by unsing the information about the sort + \c to_nice_string(const relation_element & el) function, by using the information about the sort of the element. */ std::string to_nice_string(const relation_sort & s, const relation_element & el) const; diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 448aa624d..12b063759 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -89,7 +89,7 @@ namespace nlsat { unsigned m_num_bool_vars; atom_vector m_atoms; // bool_var -> atom - svector m_bvalues; // boolean assigment + svector m_bvalues; // boolean assignment unsigned_vector m_levels; // bool_var -> level svector m_justifications; vector m_bwatches; // bool_var (that are not attached to atoms) -> clauses where it is maximal @@ -1051,7 +1051,7 @@ namespace nlsat { } /** - \brief Process a clause that contains nonlinar arithmetic literals + \brief Process a clause that contains nonlinear arithmetic literals If satisfy_learned is true, then learned clauses are satisfied even if m_lazy > 0 */ @@ -1569,7 +1569,7 @@ namespace nlsat { max = lvl; } else { - // l must be a literal from a previous stage that is false in the current intepretation + // l must be a literal from a previous stage that is false in the current interpretation SASSERT(assigned_value(l) == l_undef); SASSERT(max_var(b) != null_var); SASSERT(m_xk != null_var); @@ -1890,7 +1890,7 @@ namespace nlsat { // ----------------------- // - // Variable reodering + // Variable reordering // // ----------------------- diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 01806bc24..3975945cb 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -974,7 +974,7 @@ namespace ar { // ------------------------------------------------------------ -// fm_tactic adapted to eliminate designated de-Brujin indices. +// fm_tactic adapted to eliminate designated de-Bruijn indices. namespace fm { typedef ptr_vector clauses; diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index 96334e3ce..c979e476e 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -188,7 +188,7 @@ namespace smt { 1) Variables: (f ... X ...) 2) Ground terms: (f ... t ...) 3) depth 2 joint: (f ... (g ... X ...) ...) - Joint2 stores the declartion g, and the position of variable X, and its idx. + Joint2 stores the declaration g, and the position of variable X, and its idx. \remark Z3 has no support for depth 3 joints (f ... (g ... (h ... X ...) ...) ....) */ @@ -211,7 +211,7 @@ namespace smt { approx_set m_lbl_set; // singleton set containing m_label /* The following field is an array of tagged pointers. - Each positon contains: + Each position contains: 1- null (no joint), NULL_TAG 2- a boxed integer (i.e., register that contains the variable bind) VAR_TAG 3- an enode pointer (ground term) GROUND_TERM_TAG diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index ffaee434f..c38ef4e4a 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -369,7 +369,7 @@ namespace smt { else { TRACE("internalize_bug", tout << "creating enode for #" << n->get_id() << "\n";); mk_enode(to_app(n), - true, /* supress arguments, we not not use CC for this kind of enode */ + true, /* suppress arguments, we not not use CC for this kind of enode */ true, /* bool enode must be merged with true/false, since it is not in the context of a gate */ false /* CC is not enabled */ ); set_enode_flag(v, false); @@ -453,7 +453,7 @@ namespace smt { // must be associated with an enode. if (!e_internalized(n)) { mk_enode(to_app(n), - true, /* supress arguments, we not not use CC for this kind of enode */ + true, /* suppress arguments, we not not use CC for this kind of enode */ true /* bool enode must be merged with true/false, since it is not in the context of a gate */, false /* CC is not enabled */); } @@ -739,7 +739,7 @@ namespace smt { app_ref eq1(mk_eq_atom(n, t), m_manager); app_ref eq2(mk_eq_atom(n, e), m_manager); mk_enode(n, - true /* supress arguments, I don't want to apply CC on ite terms */, + true /* suppress arguments, I don't want to apply CC on ite terms */, false /* it is a term, so it should not be merged with true/false */, false /* CC is not enabled */); internalize(c, true); @@ -797,7 +797,7 @@ namespace smt { } enode * e = mk_enode(n, - false, /* do not supress args */ + false, /* do not suppress args */ false, /* it is a term, so it should not be merged with true/false */ true); apply_sort_cnstr(n, e); @@ -1506,7 +1506,7 @@ namespace smt { relevancy_eh * eh = m_relevancy_propagator->mk_and_relevancy_eh(n); unsigned num = n->get_num_args(); for (unsigned i = 0; i < num; i++) { - // if one child is assigned to false, the the and-parent must be notified + // if one child is assigned to false, the and-parent must be notified literal l = get_literal(n->get_arg(i)); add_rel_watch(~l, eh); } @@ -1518,7 +1518,7 @@ namespace smt { relevancy_eh * eh = m_relevancy_propagator->mk_or_relevancy_eh(n); unsigned num = n->get_num_args(); for (unsigned i = 0; i < num; i++) { - // if one child is assigned to true, the the or-parent must be notified + // if one child is assigned to true, the or-parent must be notified literal l = get_literal(n->get_arg(i)); add_rel_watch(l, eh); } diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 28a65f898..f443d671b 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -537,7 +537,7 @@ namespace smt { } } - // For each instantiation_set, reemove entries that do not evaluate to values. + // For each instantiation_set, remove entries that do not evaluate to values. void cleanup_instantiation_sets() { ptr_vector to_delete; for (node * curr : m_nodes) { @@ -735,7 +735,7 @@ namespace smt { } } // TBD: add support for the else of bitvectors. - // Idea: get the term t with the minimal interpreation and use t - 1. + // Idea: get the term t with the minimal interpretation and use t - 1. } n->set_else((*(elems.begin())).m_key); } @@ -955,7 +955,7 @@ namespace smt { if (elems.empty()) { // The method get_some_value cannot be used if n->get_sort() is an uninterpreted sort or is a sort built using uninterpreted sorts // (e.g., (Array S S) where S is uninterpreted). The problem is that these sorts do not have a fixed interpretation. - // Moreover, a model assigns an arbitrary intepretation to these sorts using "model_values" a model value. + // Moreover, a model assigns an arbitrary interpretation to these sorts using "model_values" a model value. // If these module values "leak" inside the logical context, they may affect satisfiability. // sort * ns = n->get_sort(); @@ -1007,7 +1007,7 @@ namespace smt { This may happen because the evaluator uses model_completion. In the beginning of fix_model() we collected all f with partial interpretations. During the process of computing the - projections we used the evalutator with model_completion, + projections we used the evaluator with model_completion, and it may have fixed the "else" case of some partial interpretations. This is ok, because in the "limit" the "else" of the interpretation is irrelevant after the projections are applied. @@ -1570,7 +1570,7 @@ namespace smt { ast_manager & m = ctx->get_manager(); sort * s = q->get_decl_sort(num_vars - m_var_i - 1); if (m.is_uninterp(s)) { - // For uninterpreted sorst, we add all terms in the context. + // For uninterpreted sorts, we add all terms in the context. // See Section 4.1 in the paper "Complete Quantifier Instantiation" node * S_q_i = slv.get_uvar(q, m_var_i); ptr_vector::const_iterator it = ctx->begin_enodes(); @@ -1741,7 +1741,7 @@ namespace smt { if (has_quantifiers(q->get_expr())) { static bool displayed_flat_msg = false; if (!displayed_flat_msg) { - // [Leo]: This warning message is not usefult. + // [Leo]: This warning message is not useful. // warning_msg("For problems containing quantifiers, the model finding capabilities of Z3 work better when the formula does not contain nested quantifiers. You can use PULL_NESTED_QUANTIFIERS=true to eliminate nested quantifiers."); displayed_flat_msg = true; } @@ -2104,7 +2104,7 @@ namespace smt { } /** - \brief Process unintrepreted applications. + \brief Process uninterpreted applications. */ void process_u_app(app * t) { unsigned num_args = t->get_num_args(); @@ -2130,7 +2130,7 @@ namespace smt { /** \brief A term \c t is said to be a auf_select if - it is of ther form + it is of the form (select a i) Where: @@ -2151,7 +2151,7 @@ namespace smt { } /** - \brief Process intrepreted applications. + \brief Process interpreted applications. */ void process_i_app(app * t) { if (is_auf_select(t)) { @@ -2512,7 +2512,7 @@ namespace smt { SASSERT(f_else != 0); // Remark: I can ignore the conditions of m because // I know the (partial) interpretation of f satisfied the ground part. - // MBQI will force extra instantiations if the the (partial) interpretation of f + // MBQI will force extra instantiations if the (partial) interpretation of f // does not satisfy the quantifier. // In all other cases the "else" of f will satisfy the quantifier. set_else_interp(f, f_else); @@ -2937,7 +2937,7 @@ namespace smt { } /** - \brief Use m_fs to set the interpreation of the function symbols that were used to satisfy the + \brief Use m_fs to set the interpretation of the function symbols that were used to satisfy the quantifiers in m_satisfied. */ void set_interp() { diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h index d89f3f6a4..ad5f58e49 100644 --- a/src/smt/smt_quantifier.h +++ b/src/smt/smt_quantifier.h @@ -152,7 +152,7 @@ namespace smt { virtual bool mbqi_enabled(quantifier *q) const {return true;} /** - \brief Give a change to the plugin to adjust the interpretation of unintepreted functions. + \brief Give a change to the plugin to adjust the interpretation of uninterpreted functions. It can basically change the "else" of each uninterpreted function. */ virtual void adjust_model(proto_model * m) = 0; diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 806b2a05b..6794ca3ac 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -660,7 +660,7 @@ namespace smt { satisfy their respective constraints. However, when they do that the may create inconsistencies in the other modules. I use m_liberal_final_check to avoid infinite - loops where the modules keep changing the assigment and no + loops where the modules keep changing the assignment and no progress is made. If m_liberal_final_check is set to false, these modules will avoid mutating the assignment to satisfy constraints. diff --git a/src/tactic/arith/purify_arith_tactic.h b/src/tactic/arith/purify_arith_tactic.h index bbb62710c..44b4f9b58 100644 --- a/src/tactic/arith/purify_arith_tactic.h +++ b/src/tactic/arith/purify_arith_tactic.h @@ -16,7 +16,7 @@ Abstract: Remarks: - The semantics of division by zero is not specified. Thus, uninterpreted functions are used. An ExRCF procedure may - treat the unintepreted function applications as fresh + treat the uninterpreted function applications as fresh constants. Then, in any model produced by this procedure, the interpretation for division by zero must be checked. diff --git a/src/tactic/ufbv/ufbv_rewriter.h b/src/tactic/ufbv/ufbv_rewriter.h index 1e13f4fa4..af9888751 100644 --- a/src/tactic/ufbv/ufbv_rewriter.h +++ b/src/tactic/ufbv/ufbv_rewriter.h @@ -74,7 +74,7 @@ each offset is a different "variable bank". A pair (expr, offset) is essentially where every variable in expr is assumed to be from the "bank" offset. The class substitution (in substitution.h) manages offsets for us. -The class matcher (in matcher.h) can be use to test whether an expression is an instance of another one. +The class matcher (in matcher.h) can be used to test whether an expression is an instance of another one. Finally, there is the problem when we have N demodulators (where N is big), and a big formula, and we want to traverse the formula only once looking for opportunities for applying these N demodulators.