mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-04 06:15:46 +00:00
Code Activity

add eval feature #1553

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-03-23 16:26:20 -07:00
parent 705439cb85
commit 966a8f73d3
3 changed files with 41 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/api/z3_api.h
View file

@ -5209,6 +5209,17 @@ extern "C" {
Z3_func_decl const decls[]);
/**
\brief Parse and evaluate and SMT-LIB2 command sequence. The state from a previous call is saved so the next
evaluation builds on top of the previous call.
\returns output generated from processing commands.
def_API('Z3_eval_smtlib2_string', STRING, (_in(CONTEXT), _in(STRING),))
*/
Z3_string Z3_API Z3_eval_smtlib2_string(Z3_context, Z3_string str);
/**
\brief Retrieve that last error message information generated from parsing.