3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00

add documentation comment for evaluation, Issue #536

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-04-04 12:59:18 +02:00
parent 9667185af0
commit ec5a4ba63d
2 changed files with 6 additions and 1 deletions

View file

@ -4538,6 +4538,9 @@ extern "C" {
If \c model_completion is Z3_TRUE, then Z3 will assign an interpretation for any constant or function that does
not have an interpretation in \c m. These constants and functions were essentially don't cares.
If \c model_completion is Z3_FALSE, then Z3 will not assign interpretations to constants for functions that do
not have interpretations in \c m. Evaluation behaves as the identify function in this case.
The evaluation may fail for the following reasons:
- \c t contains a quantifier.
@ -4547,6 +4550,8 @@ extern "C" {
- \c t is type incorrect.
- \c Z3_interrupt was invoked during evaluation.
def_API('Z3_model_eval', BOOL, (_in(CONTEXT), _in(MODEL), _in(AST), _in(BOOL), _out(AST)))
*/
Z3_bool_opt Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, Z3_bool model_completion, Z3_ast * v);

View file

@ -118,7 +118,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
expr * val = m_model.get_const_interp(f);
if (val != 0) {
result = val;
return BR_DONE;
return m().is_value(val)?BR_DONE:BR_REWRITE_FULL;
}
if (m_model_completion) {