mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 21:01:22 +00:00
Code Activity

Whitespace, typo

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-11-04 21:27:10 +00:00
parent e7f7090a01
commit ac7e1b145c
1 changed files with 6 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/api/z3_optimization.h
View file

@ -71,7 +71,6 @@ extern "C" {
*/ */
unsigned Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id); unsigned Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id);
/** /**
\brief Add a maximization constraint. \brief Add a maximization constraint.
\param c - context \param c - context
@ -91,7 +90,6 @@ extern "C" {
*/ */
unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t); unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t);
/** /**
\brief Create a backtracking point. \brief Create a backtracking point.
@ -198,7 +196,7 @@ extern "C" {
Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o); Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o);
/** /**
\brief Parse an SMT-LIB2 string with assertions, \brief Parse an SMT-LIB2 string with assertions,
soft constraints and optimization objectives. soft constraints and optimization objectives.
Add the parsed constraints and objectives to the optimization context. Add the parsed constraints and objectives to the optimization context.
@ -210,13 +208,11 @@ extern "C" {
*/ */
void Z3_API Z3_optimize_from_string(Z3_context c, Z3_optimize o, Z3_string s); void Z3_API Z3_optimize_from_string(Z3_context c, Z3_optimize o, Z3_string s);
/** /**
\brief Parse an SMT-LIB2 file with assertions, \brief Parse an SMT-LIB2 file with assertions,
soft constraints and optimization objectives. soft constraints and optimization objectives.
Add the parsed constraints and objectives to the optimization context. Add the parsed constraints and objectives to the optimization context.
\param c - context. \param c - context.
\param o - optimize context. \param o - optimize context.
\param s - string containing SMT2 specification. \param s - string containing SMT2 specification.
@ -225,7 +221,6 @@ extern "C" {
*/ */
void Z3_API Z3_optimize_from_file(Z3_context c, Z3_optimize o, Z3_string s); void Z3_API Z3_optimize_from_file(Z3_context c, Z3_optimize o, Z3_string s);
/** /**
\brief Return a string containing a description of parameters accepted by optimize. \brief Return a string containing a description of parameters accepted by optimize.
@ -240,7 +235,6 @@ extern "C" {
*/ */
Z3_stats Z3_API Z3_optimize_get_statistics(Z3_context c, Z3_optimize d); Z3_stats Z3_API Z3_optimize_get_statistics(Z3_context c, Z3_optimize d);
/** /**
\brief Return the set of asserted formulas on the optimization context. \brief Return the set of asserted formulas on the optimization context.
@ -251,15 +245,14 @@ extern "C" {
/** /**
\brief Return objectives on the optimization context. \brief Return objectives on the optimization context.
If the objective function is a max-sat objective it is returned If the objective function is a max-sat objective it is returned
as a Pseudo-Boolean (minimization) sum of the form (+ (if f1 w1 0) (if f2 w2 0) ...) as a Pseudo-Boolean (minimization) sum of the form (+ (if f1 w1 0) (if f2 w2 0) ...)
If the objective function is entered as a maximization objective, then return the corresponding minimizaiton If the objective function is entered as a maximization objective, then return
objective. In this way the resulting objective function is always returned as a minimization objective. the corresponding minimization objective. In this way the resulting objective
function is always returned as a minimization objective.
def_API('Z3_optimize_get_objectives', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE))) def_API('Z3_optimize_get_objectives', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE)))
*/ */
Z3_ast_vector Z3_API Z3_optimize_get_objectives(Z3_context c, Z3_optimize o); Z3_ast_vector Z3_API Z3_optimize_get_objectives(Z3_context c, Z3_optimize o);
/*@}*/ /*@}*/
/*@}*/ /*@}*/