From 87228b6a9df329ad194c942d8567767e11bcbc10 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 Jan 2016 14:47:15 -0800 Subject: [PATCH] add a little more verbiage to description of simplify. Issue #424 Signed-off-by: Nikolaj Bjorner --- src/api/z3_api.h | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 528399394..78506e414 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -4419,6 +4419,9 @@ extern "C" { \brief Interface to simplifier. 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, + such as constant propagation (propagating true/false over logical connectives). def_API('Z3_simplify', AST, (_in(CONTEXT), _in(AST))) */