From 372cab2c5bc2705eb7c2dee9ed35c01e09691405 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Wed, 17 Oct 2018 22:49:39 +0700 Subject: [PATCH] Fix some typos. --- examples/maxsat/maxsat.c | 4 ++-- src/api/c++/z3++.h | 2 +- src/api/python/z3/z3.py | 6 +++--- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/examples/maxsat/maxsat.c b/examples/maxsat/maxsat.c index 5696f5b89..50550106e 100644 --- a/examples/maxsat/maxsat.c +++ b/examples/maxsat/maxsat.c @@ -138,7 +138,7 @@ void assert_hard_constraints(Z3_context ctx, Z3_solver s, unsigned num_cnstrs, Z /** \brief Assert soft constraints stored in the given array. - This funtion will assert each soft-constraint C_i as (C_i or k_i) where k_i is a fresh boolean variable. + This function will assert each soft-constraint C_i as (C_i or k_i) where k_i is a fresh boolean variable. It will also return an array containing these fresh variables. */ Z3_ast * assert_soft_constraints(Z3_context ctx, Z3_solver s, unsigned num_cnstrs, Z3_ast * cnstrs) @@ -565,7 +565,7 @@ int fu_malik_maxsat(Z3_context ctx, Z3_solver s, unsigned num_hard_cnstrs, Z3_as /** \brief Finds the maximal number of assumptions that can be satisfied. - An assumption is any formula preceeded with the :assumption keyword. + An assumption is any formula preceded with the :assumption keyword. "Hard" constraints can be supported by using the :formula keyword. Input: file in SMT-LIB format, and MaxSAT algorithm to be used: 0 - Naive, 1 - Fu&Malik's algo. diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 1b1820909..a355e0233 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -291,7 +291,7 @@ namespace z3 { \brief Return a tuple constructor. \c name is the name of the returned constructor, \c n are the number of arguments, \c names and \c sorts are their projected sorts. - \c projs is an output paramter. It contains the set of projection functions. + \c projs is an output parameter. It contains the set of projection functions. */ func_decl tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs); diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 703105356..d466d2e77 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -8327,7 +8327,7 @@ def prove(claim, **keywords): print(s.model()) def _solve_html(*args, **keywords): - """Version of funcion `solve` used in RiSE4Fun.""" + """Version of function `solve` used in RiSE4Fun.""" s = Solver() s.set(**keywords) s.add(*args) @@ -8349,7 +8349,7 @@ def _solve_html(*args, **keywords): print(s.model()) def _solve_using_html(s, *args, **keywords): - """Version of funcion `solve_using` used in RiSE4Fun.""" + """Version of function `solve_using` used in RiSE4Fun.""" if __debug__: _z3_assert(isinstance(s, Solver), "Solver object expected") s.set(**keywords) @@ -8372,7 +8372,7 @@ def _solve_using_html(s, *args, **keywords): print(s.model()) def _prove_html(claim, **keywords): - """Version of funcion `prove` used in RiSE4Fun.""" + """Version of function `prove` used in RiSE4Fun.""" if __debug__: _z3_assert(is_bool(claim), "Z3 Boolean expression expected") s = Solver()