mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

Fix some typos.

Browse source
This commit is contained in:
Bruce Mitchener 2018-10-17 22:49:39 +07:00
parent 8431a54190
commit 372cab2c5b
3 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
examples/maxsat/maxsat.c
View file

@ -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. \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. 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) 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. \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. "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. Input: file in SMT-LIB format, and MaxSAT algorithm to be used: 0 - Naive, 1 - Fu&Malik's algo.

2
src/api/c++/z3++.h
View file

@ -291,7 +291,7 @@ namespace z3 {
\brief Return a tuple constructor. \brief Return a tuple constructor.
\c name is the name of the returned 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 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); func_decl tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs);

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

@ -8327,7 +8327,7 @@ def prove(claim, **keywords):
print(s.model()) print(s.model())
def _solve_html(*args, **keywords): def _solve_html(*args, **keywords):
"""Version of funcion `solve` used in RiSE4Fun.""" """Version of function `solve` used in RiSE4Fun."""
s = Solver() s = Solver()
s.set(**keywords) s.set(**keywords)
s.add(*args) s.add(*args)
@ -8349,7 +8349,7 @@ def _solve_html(*args, **keywords):
print(s.model()) print(s.model())
def _solve_using_html(s, *args, **keywords): 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__: if __debug__:
_z3_assert(isinstance(s, Solver), "Solver object expected") _z3_assert(isinstance(s, Solver), "Solver object expected")
s.set(**keywords) s.set(**keywords)
@ -8372,7 +8372,7 @@ def _solve_using_html(s, *args, **keywords):
print(s.model()) print(s.model())
def _prove_html(claim, **keywords): def _prove_html(claim, **keywords):
"""Version of funcion `prove` used in RiSE4Fun.""" """Version of function `prove` used in RiSE4Fun."""
if __debug__: if __debug__:
_z3_assert(is_bool(claim), "Z3 Boolean expression expected") _z3_assert(is_bool(claim), "Z3 Boolean expression expected")
s = Solver() s = Solver()