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

C API cleanup. Mainly removal of ML-specific macros that are not used anymore and inline documentation fixes.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-12-03 17:33:25 +00:00
parent 2c6645ef2d
commit 00271e5531
18 changed files with 1282 additions and 1823 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
doc/mk_api_doc.py
View file

@ -84,10 +84,13 @@ try:
os.remove('website-adj.dox')
shutil.copyfile('../src/api/python/z3.py', 'tmp/z3py.py')
cleanup_API('../src/api/z3_api.h', 'tmp/z3_api.h')
cleanup_API('../src/api/z3_ast_containers.h', 'tmp/z3_ast_containers.h')
cleanup_API('../src/api/z3_algebraic.h', 'tmp/z3_algebraic.h')
cleanup_API('../src/api/z3_polynomial.h', 'tmp/z3_polynomial.h')
cleanup_API('../src/api/z3_rcf.h', 'tmp/z3_rcf.h')
cleanup_API('../src/api/z3_interp.h', 'tmp/z3_interp.h')
cleanup_API('../src/api/z3_fixedpoint.h', 'tmp/z3_fixedpoint.h')
cleanup_API('../src/api/z3_optimization.h', 'tmp/z3_optimization.h')
cleanup_API('../src/api/z3_interp.h', 'tmp/z3_interp.h')
cleanup_API('../src/api/z3_fpa.h', 'tmp/z3_fpa.h')
print("Removed annotations from z3_api.h.")
@ -100,15 +103,19 @@ try:
exit(1)
print("Generated C and .NET API documentation.")
os.remove('tmp/z3_api.h')
os.remove('tmp/z3_ast_containers.h')
os.remove('tmp/z3_algebraic.h')
os.remove('tmp/z3_polynomial.h')
os.remove('tmp/z3_rcf.h')
os.remove('tmp/z3_fixedpoint.h')
os.remove('tmp/z3_optimization.h')
os.remove('tmp/z3_interp.h')
os.remove('tmp/z3_fpa.h')
print("Removed temporary file z3_api.h.")
os.remove('tmp/website.dox')
print("Removed temporary file header files.")
os.remove('tmp/website.dox')
print("Removed temporary file website.dox")
os.remove('tmp/z3py.py')
os.remove('tmp/z3py.py')
print("Removed temporary file z3py.py")
os.removedirs('tmp')
print("Removed temporary directory tmp.")
@ -126,5 +133,6 @@ try:
print("Documentation was successfully generated at subdirectory './api/html'.")
except:
print("ERROR: failed to generate documentation")
exctype, value = sys.exc_info()[:2]
print("ERROR: failed to generate documentation: %s" % value)
exit(1)

5
doc/z3api.dox
View file

@ -214,11 +214,6 @@ ALIASES = "beginfaq=<ul>" \
"emph{1}=<em>\1</em>" \
"extdoc{2}=<a class=\"el\" href=\"\1\">\2</a>" \
"nicebox{1}=<div class=\"fragment\"><pre class=\"fragment\">\1</pre></div>" \
"mlonly=\if Ocaml" \
"endmlonly=\endif" \
"mlh=\if Ocaml" \
"endmlh=\endif" \
"conly=" \
"ccode{1}=<tt>\1</tt>" \
"zframe=<iframe allowtransparency=\"true\" frameborder=\"0\" style=\"width:600px;height:600px\" src=\"http://rise4fun.com/z3?frame=1&menu=0\"> </iframe>"

5
doc/z3code.dox
View file

@ -64,11 +64,6 @@ ALIASES = "beginfaq=<ul>" \
"emph{1}=<em>\1</em>" \
"extdoc{2}=<a class=\"el\" href=\"\1\">\2</a>" \
"nicebox{1}=<div class=\"fragment\"><pre class=\"fragment\">\1</pre></div>" \
"mlonly=\if Ocaml" \
"endmlonly=\endif" \
"mlh=\if Ocaml" \
"endmlh=\endif" \
"conly=" \
"ccode{1}=<tt>\1</tt>" \
"zframe=<iframe allowtransparency=\"true\" frameborder=\"0\" style=\"width:600px;height:600px\" src=\"http://rise4fun.com/z3?frame=1&menu=0\"> </iframe>"

2
scripts/mk_project.py
View file

@ -76,7 +76,7 @@ def init_project_def():
add_lib('portfolio', ['smtlogic_tactics', 'sat_solver', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
add_lib('smtparser', ['portfolio'], 'parsers/smt')
add_lib('opt', ['smt', 'smtlogic_tactics', 'sls_tactic', 'sat_solver'], 'opt')
API_files = ['z3_api.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h', 'z3_interp.h', 'z3_fpa.h']
API_files = ['z3_api.h', 'z3_ast_containers.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h', 'z3_fixedpoint.h', 'z3_optimization.h', 'z3_interp.h', 'z3_fpa.h']
add_lib('api', ['portfolio', 'smtparser', 'realclosure', 'interp', 'opt'],
includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files)
add_exe('shell', ['api', 'sat', 'extra_cmds','opt'], exe_name='z3')

3
src/api/api_bv.cpp
View file

@ -151,8 +151,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
}
/**
\brief \mlh mk_bvmsb c s \endmlh
Create a bit-vector of sort \s with 1 in the most significant bit position.
\brief Create a bit-vector of sort \s with 1 in the most significant bit position.
The sort \s must be a bit-vector sort.

5
src/api/java/Model.java
View file

@ -201,10 +201,11 @@ public class Model extends Z3Object
* Remarks: This function may fail if {@code t} contains
* quantifiers, is partial (MODEL_PARTIAL enabled), or if {@code t} is not well-sorted. In this case a
* {@code ModelEvaluationFailedException} is thrown.
* @param t An expression {@code completion} When this flag
* @param t the expression to evaluate
* @param completion An expression {@code completion} When this flag
* is enabled, a model value will be assigned to any constant or function
* that does not have an interpretation in the model.
*
* @return The evaluation of {@code t} in the model.
* @throws Z3Exception
**/

5
src/api/z3.h
View file

@ -15,7 +15,7 @@ Author:
Leonardo de Moura (leonardo) 2007-06-8
Notes:
--*/
#ifndef Z3_H_
@ -24,9 +24,12 @@ Notes:
#include<stdio.h>
#include"z3_macros.h"
#include"z3_api.h"
#include"z3_ast_containers.h"
#include"z3_algebraic.h"
#include"z3_polynomial.h"
#include"z3_rcf.h"
#include"z3_fixedpoint.h"
#include"z3_optimization.h"
#include"z3_interp.h"
#include"z3_fpa.h"

65
src/api/z3_algebraic.h
View file

@ -7,7 +7,7 @@ Module Name:
Abstract:
Additional APIs for handling Z3 algebraic numbers encoded as
Additional APIs for handling Z3 algebraic numbers encoded as
Z3_ASTs
Author:
@ -15,7 +15,7 @@ Author:
Leonardo de Moura (leonardo) 2012-12-07
Notes:
--*/
#ifndef Z3_ALGEBRAIC_H_
@ -23,20 +23,13 @@ Notes:
#ifdef __cplusplus
extern "C" {
#endif // __cplusplus
/**
\defgroup capi C API
*/
#endif // __cplusplus
/** \defgroup capi C API */
/*@{*/
/**
@name Algebraic Numbers API
*/
/** @name Algebraic Numbers */
/*@{*/
/**
\brief Return Z3_TRUE if \c can be used as value in the Z3 real algebraic
number package.
@ -82,7 +75,7 @@ extern "C" {
int Z3_API Z3_algebraic_sign(Z3_context c, Z3_ast a);
/**
\brief Return the value a + b.
\brief Return the value a + b.
\pre Z3_algebraic_is_value(c, a)
\pre Z3_algebraic_is_value(c, b)
@ -90,10 +83,10 @@ extern "C" {
def_API('Z3_algebraic_add', AST, (_in(CONTEXT), _in(AST), _in(AST)))
*/
Z3_ast Z3_API Z3_algebraic_add(Z3_context c, Z3_ast a, Z3_ast b);
Z3_ast Z3_API Z3_algebraic_add(Z3_context c, Z3_ast a, Z3_ast b);
/**
\brief Return the value a - b.
\brief Return the value a - b.
\pre Z3_algebraic_is_value(c, a)
\pre Z3_algebraic_is_value(c, b)
@ -101,10 +94,10 @@ extern "C" {
def_API('Z3_algebraic_sub', AST, (_in(CONTEXT), _in(AST), _in(AST)))
*/
Z3_ast Z3_API Z3_algebraic_sub(Z3_context c, Z3_ast a, Z3_ast b);
Z3_ast Z3_API Z3_algebraic_sub(Z3_context c, Z3_ast a, Z3_ast b);
/**
\brief Return the value a * b.
\brief Return the value a * b.
\pre Z3_algebraic_is_value(c, a)
\pre Z3_algebraic_is_value(c, b)
@ -112,10 +105,10 @@ extern "C" {
def_API('Z3_algebraic_mul', AST, (_in(CONTEXT), _in(AST), _in(AST)))
*/
Z3_ast Z3_API Z3_algebraic_mul(Z3_context c, Z3_ast a, Z3_ast b);
Z3_ast Z3_API Z3_algebraic_mul(Z3_context c, Z3_ast a, Z3_ast b);
/**
\brief Return the value a / b.
\brief Return the value a / b.
\pre Z3_algebraic_is_value(c, a)
\pre Z3_algebraic_is_value(c, b)
@ -124,8 +117,8 @@ extern "C" {
def_API('Z3_algebraic_div', AST, (_in(CONTEXT), _in(AST), _in(AST)))
*/
Z3_ast Z3_API Z3_algebraic_div(Z3_context c, Z3_ast a, Z3_ast b);
Z3_ast Z3_API Z3_algebraic_div(Z3_context c, Z3_ast a, Z3_ast b);
/**
\brief Return the a^(1/k)
@ -146,7 +139,7 @@ extern "C" {
def_API('Z3_algebraic_power', AST, (_in(CONTEXT), _in(AST), _in(UINT)))
*/
Z3_ast Z3_API Z3_algebraic_power(Z3_context c, Z3_ast a, unsigned k);
/**
\brief Return Z3_TRUE if a < b, and Z3_FALSE otherwise.
@ -155,8 +148,8 @@ extern "C" {
def_API('Z3_algebraic_lt', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
*/
Z3_bool Z3_API Z3_algebraic_lt(Z3_context c, Z3_ast a, Z3_ast b);
Z3_bool Z3_API Z3_algebraic_lt(Z3_context c, Z3_ast a, Z3_ast b);
/**
\brief Return Z3_TRUE if a > b, and Z3_FALSE otherwise.
@ -165,7 +158,7 @@ extern "C" {
def_API('Z3_algebraic_gt', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
*/
Z3_bool Z3_API Z3_algebraic_gt(Z3_context c, Z3_ast a, Z3_ast b);
Z3_bool Z3_API Z3_algebraic_gt(Z3_context c, Z3_ast a, Z3_ast b);
/**
\brief Return Z3_TRUE if a <= b, and Z3_FALSE otherwise.
@ -175,7 +168,7 @@ extern "C" {
def_API('Z3_algebraic_le', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
*/
Z3_bool Z3_API Z3_algebraic_le(Z3_context c, Z3_ast a, Z3_ast b);
Z3_bool Z3_API Z3_algebraic_le(Z3_context c, Z3_ast a, Z3_ast b);
/**
\brief Return Z3_TRUE if a >= b, and Z3_FALSE otherwise.
@ -185,7 +178,7 @@ extern "C" {
def_API('Z3_algebraic_ge', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
*/
Z3_bool Z3_API Z3_algebraic_ge(Z3_context c, Z3_ast a, Z3_ast b);
Z3_bool Z3_API Z3_algebraic_ge(Z3_context c, Z3_ast a, Z3_ast b);
/**
\brief Return Z3_TRUE if a == b, and Z3_FALSE otherwise.
@ -195,7 +188,7 @@ extern "C" {
def_API('Z3_algebraic_eq', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
*/
Z3_bool Z3_API Z3_algebraic_eq(Z3_context c, Z3_ast a, Z3_ast b);
Z3_bool Z3_API Z3_algebraic_eq(Z3_context c, Z3_ast a, Z3_ast b);
/**
\brief Return Z3_TRUE if a != b, and Z3_FALSE otherwise.
@ -205,30 +198,30 @@ extern "C" {
def_API('Z3_algebraic_neq', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
*/
Z3_bool Z3_API Z3_algebraic_neq(Z3_context c, Z3_ast a, Z3_ast b);
Z3_bool Z3_API Z3_algebraic_neq(Z3_context c, Z3_ast a, Z3_ast b);
/**
\brief Given a multivariate polynomial p(x_0, ..., x_{n-1}, x_n), returns the
\brief Given a multivariate polynomial p(x_0, ..., x_{n-1}, x_n), returns the
roots of the univariate polynomial p(a[0], ..., a[n-1], x_n).
\pre p is a Z3 expression that contains only arithmetic terms and free variables.
\pre forall i in [0, n) Z3_algebraic_is_value(c, a[i])
\post forall r in result Z3_algebraic_is_value(c, result)
def_API('Z3_algebraic_roots', AST_VECTOR, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST)))
*/
Z3_ast_vector Z3_API Z3_algebraic_roots(Z3_context c, Z3_ast p, unsigned n, Z3_ast a[]);
Z3_ast_vector Z3_API Z3_algebraic_roots(Z3_context c, Z3_ast p, unsigned n, Z3_ast a[]);
/**
\brief Given a multivariate polynomial p(x_0, ..., x_{n-1}), return the
\brief Given a multivariate polynomial p(x_0, ..., x_{n-1}), return the
sign of p(a[0], ..., a[n-1]).
\pre p is a Z3 expression that contains only arithmetic terms and free variables.
\pre forall i in [0, n) Z3_algebraic_is_value(c, a[i])
def_API('Z3_algebraic_eval', INT, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST)))
*/
int Z3_API Z3_algebraic_eval(Z3_context c, Z3_ast p, unsigned n, Z3_ast a[]);
int Z3_API Z3_algebraic_eval(Z3_context c, Z3_ast p, unsigned n, Z3_ast a[]);
/*@}*/
/*@}*/

1896
src/api/z3_api.h
View file

File diff suppressed because it is too large Load diff

200
src/api/z3_ast_containers.h Normal file
View file

@ -0,0 +1,200 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
z3_ast_containers.h
Abstract:
AST Containers
Author:
Christoph M. Wintersteiger (cwinter) 2015-12-03
Notes:
--*/
#ifndef Z3_AST_CONTAINERS_H_
#define Z3_AST_CONTAINERS_H_
#ifdef __cplusplus
extern "C" {
#endif // __cplusplus
/** \defgroup capi C API */
/*@{*/
/** @name AST vectors */
/*@{*/
/**
\brief Return an empty AST vector.
\remark Reference counting must be used to manage AST vectors, even when the Z3_context was
created using #Z3_mk_context instead of #Z3_mk_context_rc.
def_API('Z3_mk_ast_vector', AST_VECTOR, (_in(CONTEXT),))
*/
Z3_ast_vector Z3_API Z3_mk_ast_vector(Z3_context c);
/**
\brief Increment the reference counter of the given AST vector.
def_API('Z3_ast_vector_inc_ref', VOID, (_in(CONTEXT), _in(AST_VECTOR)))
*/
void Z3_API Z3_ast_vector_inc_ref(Z3_context c, Z3_ast_vector v);
/**
\brief Decrement the reference counter of the given AST vector.
def_API('Z3_ast_vector_dec_ref', VOID, (_in(CONTEXT), _in(AST_VECTOR)))
*/
void Z3_API Z3_ast_vector_dec_ref(Z3_context c, Z3_ast_vector v);
/**
\brief Return the size of the given AST vector.
def_API('Z3_ast_vector_size', UINT, (_in(CONTEXT), _in(AST_VECTOR)))
*/
unsigned Z3_API Z3_ast_vector_size(Z3_context c, Z3_ast_vector v);
/**
\brief Return the AST at position \c i in the AST vector \c v.
\pre i < Z3_ast_vector_size(c, v)
def_API('Z3_ast_vector_get', AST, (_in(CONTEXT), _in(AST_VECTOR), _in(UINT)))
*/
Z3_ast Z3_API Z3_ast_vector_get(Z3_context c, Z3_ast_vector v, unsigned i);
/**
\brief Update position \c i of the AST vector \c v with the AST \c a.
\pre i < Z3_ast_vector_size(c, v)
def_API('Z3_ast_vector_set', VOID, (_in(CONTEXT), _in(AST_VECTOR), _in(UINT), _in(AST)))
*/
void Z3_API Z3_ast_vector_set(Z3_context c, Z3_ast_vector v, unsigned i, Z3_ast a);
/**
\brief Resize the AST vector \c v.
def_API('Z3_ast_vector_resize', VOID, (_in(CONTEXT), _in(AST_VECTOR), _in(UINT)))
*/
void Z3_API Z3_ast_vector_resize(Z3_context c, Z3_ast_vector v, unsigned n);
/**
\brief Add the AST \c a in the end of the AST vector \c v. The size of \c v is increased by one.
def_API('Z3_ast_vector_push', VOID, (_in(CONTEXT), _in(AST_VECTOR), _in(AST)))
*/
void Z3_API Z3_ast_vector_push(Z3_context c, Z3_ast_vector v, Z3_ast a);
/**
\brief Translate the AST vector \c v from context \c s into an AST vector in context \c t.
def_API('Z3_ast_vector_translate', AST_VECTOR, (_in(CONTEXT), _in(AST_VECTOR), _in(CONTEXT)))
*/
Z3_ast_vector Z3_API Z3_ast_vector_translate(Z3_context s, Z3_ast_vector v, Z3_context t);
/**
\brief Convert AST vector into a string.
def_API('Z3_ast_vector_to_string', STRING, (_in(CONTEXT), _in(AST_VECTOR)))
*/
Z3_string Z3_API Z3_ast_vector_to_string(Z3_context c, Z3_ast_vector v);
/*@}*/
/** @name AST maps */
/*@{*/
/**
\brief Return an empty mapping from AST to AST
\remark Reference counting must be used to manage AST maps, even when the Z3_context was
created using #Z3_mk_context instead of #Z3_mk_context_rc.
def_API('Z3_mk_ast_map', AST_MAP, (_in(CONTEXT),) )
*/
Z3_ast_map Z3_API Z3_mk_ast_map(Z3_context c);
/**
\brief Increment the reference counter of the given AST map.
def_API('Z3_ast_map_inc_ref', VOID, (_in(CONTEXT), _in(AST_MAP)))
*/
void Z3_API Z3_ast_map_inc_ref(Z3_context c, Z3_ast_map m);
/**
\brief Decrement the reference counter of the given AST map.
def_API('Z3_ast_map_dec_ref', VOID, (_in(CONTEXT), _in(AST_MAP)))
*/
void Z3_API Z3_ast_map_dec_ref(Z3_context c, Z3_ast_map m);
/**
\brief Return true if the map \c m contains the AST key \c k.
def_API('Z3_ast_map_contains', BOOL, (_in(CONTEXT), _in(AST_MAP), _in(AST)))
*/
Z3_bool Z3_API Z3_ast_map_contains(Z3_context c, Z3_ast_map m, Z3_ast k);
/**
\brief Return the value associated with the key \c k.
The procedure invokes the error handler if \c k is not in the map.
def_API('Z3_ast_map_find', AST, (_in(CONTEXT), _in(AST_MAP), _in(AST)))
*/
Z3_ast Z3_API Z3_ast_map_find(Z3_context c, Z3_ast_map m, Z3_ast k);
/**
\brief Store/Replace a new key, value pair in the given map.
def_API('Z3_ast_map_insert', VOID, (_in(CONTEXT), _in(AST_MAP), _in(AST), _in(AST)))
*/
void Z3_API Z3_ast_map_insert(Z3_context c, Z3_ast_map m, Z3_ast k, Z3_ast v);
/**
\brief Erase a key from the map.
def_API('Z3_ast_map_erase', VOID, (_in(CONTEXT), _in(AST_MAP), _in(AST)))
*/
void Z3_API Z3_ast_map_erase(Z3_context c, Z3_ast_map m, Z3_ast k);
/**
\brief Remove all keys from the given map.
def_API('Z3_ast_map_reset', VOID, (_in(CONTEXT), _in(AST_MAP)))
*/
void Z3_API Z3_ast_map_reset(Z3_context c, Z3_ast_map m);
/**
\brief Return the size of the given map.
def_API('Z3_ast_map_size', UINT, (_in(CONTEXT), _in(AST_MAP)))
*/
unsigned Z3_API Z3_ast_map_size(Z3_context c, Z3_ast_map m);
/**
\brief Return the keys stored in the given map.
def_API('Z3_ast_map_keys', AST_VECTOR, (_in(CONTEXT), _in(AST_MAP)))
*/
Z3_ast_vector Z3_API Z3_ast_map_keys(Z3_context c, Z3_ast_map m);
/**
\brief Convert the given map into a string.
def_API('Z3_ast_map_to_string', STRING, (_in(CONTEXT), _in(AST_MAP)))
*/
Z3_string Z3_API Z3_ast_map_to_string(Z3_context c, Z3_ast_map m);
/*@}*/
/*@}*/
#ifdef __cplusplus
}
#endif // __cplusplus
#endif

377
src/api/z3_fixedpoint.h Normal file
View file

@ -0,0 +1,377 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
z3_fixedpoint.h
Abstract:
Fixedpoint API
Author:
Christoph M. Wintersteiger (cwinter) 2015-12-03
Notes:
--*/
#ifndef Z3_FIXEDPOINT_H_
#define Z3_FIXEDPOINT_H_
#ifdef __cplusplus
extern "C" {
#endif // __cplusplus
/** \defgroup capi C API */
/*@{*/
/** @name Fixedpoint facilities */
/*@{*/
/**
\brief Create a new fixedpoint context.
\remark User must use #Z3_fixedpoint_inc_ref and #Z3_fixedpoint_dec_ref to manage fixedpoint objects.
Even if the context was created using #Z3_mk_context instead of #Z3_mk_context_rc.
def_API('Z3_mk_fixedpoint', FIXEDPOINT, (_in(CONTEXT), ))
*/
Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c);
/**
\brief Increment the reference counter of the given fixedpoint context
def_API('Z3_fixedpoint_inc_ref', VOID, (_in(CONTEXT), _in(FIXEDPOINT)))
*/
void Z3_API Z3_fixedpoint_inc_ref(Z3_context c, Z3_fixedpoint d);
/**
\brief Decrement the reference counter of the given fixedpoint context.
def_API('Z3_fixedpoint_dec_ref', VOID, (_in(CONTEXT), _in(FIXEDPOINT)))
*/
void Z3_API Z3_fixedpoint_dec_ref(Z3_context c, Z3_fixedpoint d);
/**
\brief Add a universal Horn clause as a named rule.
The \c horn_rule should be of the form:
\code
horn_rule ::= (forall (bound-vars) horn_rule)
| (=> atoms horn_rule)
| atom
\endcode
def_API('Z3_fixedpoint_add_rule', VOID, (_in(CONTEXT), _in(FIXEDPOINT), _in(AST), _in(SYMBOL)))
*/
void Z3_API Z3_fixedpoint_add_rule(Z3_context c, Z3_fixedpoint d, Z3_ast rule, Z3_symbol name);
/**
\brief Add a Database fact.
\param c - context
\param d - fixed point context
\param r - relation signature for the row.
\param num_args - number of columns for the given row.
\param args - array of the row elements.
The number of arguments \c num_args should be equal to the number
of sorts in the domain of \c r. Each sort in the domain should be an integral
(bit-vector, Boolean or or finite domain sort).
The call has the same effect as adding a rule where \c r is applied to the arguments.
def_API('Z3_fixedpoint_add_fact', VOID, (_in(CONTEXT), _in(FIXEDPOINT), _in(FUNC_DECL), _in(UINT), _in_array(3, UINT)))
*/
void Z3_API Z3_fixedpoint_add_fact(Z3_context c, Z3_fixedpoint d,
Z3_func_decl r,
unsigned num_args, unsigned args[]);
/**
\brief Assert a constraint to the fixedpoint context.
The constraints are used as background axioms when the fixedpoint engine uses the PDR mode.
They are ignored for standard Datalog mode.
def_API('Z3_fixedpoint_assert', VOID, (_in(CONTEXT), _in(FIXEDPOINT), _in(AST)))
*/
void Z3_API Z3_fixedpoint_assert(Z3_context c, Z3_fixedpoint d, Z3_ast axiom);
/**
\brief Pose a query against the asserted rules.
\code
query ::= (exists (bound-vars) query)
| literals
\endcode
query returns
- Z3_L_FALSE if the query is unsatisfiable.
- Z3_L_TRUE if the query is satisfiable. Obtain the answer by calling #Z3_fixedpoint_get_answer.
- Z3_L_UNDEF if the query was interrupted, timed out or otherwise failed.
def_API('Z3_fixedpoint_query', INT, (_in(CONTEXT), _in(FIXEDPOINT), _in(AST)))
*/
Z3_lbool Z3_API Z3_fixedpoint_query(Z3_context c, Z3_fixedpoint d, Z3_ast query);
/**
\brief Pose multiple queries against the asserted rules.
The queries are encoded as relations (function declarations).
query returns
- Z3_L_FALSE if the query is unsatisfiable.
- Z3_L_TRUE if the query is satisfiable. Obtain the answer by calling #Z3_fixedpoint_get_answer.
- Z3_L_UNDEF if the query was interrupted, timed out or otherwise failed.
def_API('Z3_fixedpoint_query_relations', INT, (_in(CONTEXT), _in(FIXEDPOINT), _in(UINT), _in_array(2, FUNC_DECL)))
*/
Z3_lbool Z3_API Z3_fixedpoint_query_relations(
Z3_context c, Z3_fixedpoint d,
unsigned num_relations, Z3_func_decl const relations[]);
/**
\brief Retrieve a formula that encodes satisfying answers to the query.
When used in Datalog mode, the returned answer is a disjunction of conjuncts.
Each conjunct encodes values of the bound variables of the query that are satisfied.
In PDR mode, the returned answer is a single conjunction.
When used in Datalog mode the previous call to Z3_fixedpoint_query must have returned Z3_L_TRUE.
When used with the PDR engine, the previous call must have been either Z3_L_TRUE or Z3_L_FALSE.
def_API('Z3_fixedpoint_get_answer', AST, (_in(CONTEXT), _in(FIXEDPOINT)))
*/
Z3_ast Z3_API Z3_fixedpoint_get_answer(Z3_context c, Z3_fixedpoint d);
/**
\brief Retrieve a string that describes the last status returned by #Z3_fixedpoint_query.
Use this method when #Z3_fixedpoint_query returns Z3_L_UNDEF.
def_API('Z3_fixedpoint_get_reason_unknown', STRING, (_in(CONTEXT), _in(FIXEDPOINT) ))
*/
Z3_string Z3_API Z3_fixedpoint_get_reason_unknown(Z3_context c, Z3_fixedpoint d);
/**
\brief Update a named rule.
A rule with the same name must have been previously created.
def_API('Z3_fixedpoint_update_rule', VOID, (_in(CONTEXT), _in(FIXEDPOINT), _in(AST), _in(SYMBOL)))
*/
void Z3_API Z3_fixedpoint_update_rule(Z3_context c, Z3_fixedpoint d, Z3_ast a, Z3_symbol name);
/**
\brief Query the PDR engine for the maximal levels properties are known about predicate.
This call retrieves the maximal number of relevant unfoldings
of \c pred with respect to the current exploration state.
Note: this functionality is PDR specific.
def_API('Z3_fixedpoint_get_num_levels', UINT, (_in(CONTEXT), _in(FIXEDPOINT), _in(FUNC_DECL)))
*/
unsigned Z3_API Z3_fixedpoint_get_num_levels(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred);
/**
Retrieve the current cover of \c pred up to \c level unfoldings.
Return just the delta that is known at \c level. To
obtain the full set of properties of \c pred one should query
at \c level+1 , \c level+2 etc, and include \c level=-1.
Note: this functionality is PDR specific.
def_API('Z3_fixedpoint_get_cover_delta', AST, (_in(CONTEXT), _in(FIXEDPOINT), _in(INT), _in(FUNC_DECL)))
*/
Z3_ast Z3_API Z3_fixedpoint_get_cover_delta(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred);
/**
\brief Add property about the predicate \c pred.
Add a property of predicate \c pred at \c level.
It gets pushed forward when possible.
Note: level = -1 is treated as the fixedpoint. So passing -1 for the \c level
means that the property is true of the fixed-point unfolding with respect to \c pred.
Note: this functionality is PDR specific.
def_API('Z3_fixedpoint_add_cover', VOID, (_in(CONTEXT), _in(FIXEDPOINT), _in(INT), _in(FUNC_DECL), _in(AST)))
*/
void Z3_API Z3_fixedpoint_add_cover(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred, Z3_ast property);
/**
\brief Retrieve statistics information from the last call to #Z3_fixedpoint_query.
def_API('Z3_fixedpoint_get_statistics', STATS, (_in(CONTEXT), _in(FIXEDPOINT)))
*/
Z3_stats Z3_API Z3_fixedpoint_get_statistics(Z3_context c, Z3_fixedpoint d);
/**
\brief Register relation as Fixedpoint defined.
Fixedpoint defined relations have least-fixedpoint semantics.
For example, the relation is empty if it does not occur
in a head or a fact.
def_API('Z3_fixedpoint_register_relation', VOID, (_in(CONTEXT), _in(FIXEDPOINT), _in(FUNC_DECL)))
*/
void Z3_API Z3_fixedpoint_register_relation(Z3_context c, Z3_fixedpoint d, Z3_func_decl f);
/**
\brief Configure the predicate representation.
It sets the predicate to use a set of domains given by the list of symbols.
The domains given by the list of symbols must belong to a set
of built-in domains.
def_API('Z3_fixedpoint_set_predicate_representation', VOID, (_in(CONTEXT), _in(FIXEDPOINT), _in(FUNC_DECL), _in(UINT), _in_array(3, SYMBOL)))
*/
void Z3_API Z3_fixedpoint_set_predicate_representation(
Z3_context c,
Z3_fixedpoint d,
Z3_func_decl f,
unsigned num_relations,
Z3_symbol const relation_kinds[]);
/**
\brief Retrieve set of rules from fixedpoint context.
def_API('Z3_fixedpoint_get_rules', AST_VECTOR, (_in(CONTEXT),_in(FIXEDPOINT)))
*/
Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(
Z3_context c,
Z3_fixedpoint f);
/**
\brief Retrieve set of background assertions from fixedpoint context.
def_API('Z3_fixedpoint_get_assertions', AST_VECTOR, (_in(CONTEXT),_in(FIXEDPOINT)))
*/
Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions(
Z3_context c,
Z3_fixedpoint f);
/**
\brief Set parameters on fixedpoint context.
def_API('Z3_fixedpoint_set_params', VOID, (_in(CONTEXT), _in(FIXEDPOINT), _in(PARAMS)))
*/
void Z3_API Z3_fixedpoint_set_params(Z3_context c, Z3_fixedpoint f, Z3_params p);
/**
\brief Return a string describing all fixedpoint available parameters.
def_API('Z3_fixedpoint_get_help', STRING, (_in(CONTEXT), _in(FIXEDPOINT)))
*/
Z3_string Z3_API Z3_fixedpoint_get_help(Z3_context c, Z3_fixedpoint f);
/**
\brief Return the parameter description set for the given fixedpoint object.
def_API('Z3_fixedpoint_get_param_descrs', PARAM_DESCRS, (_in(CONTEXT), _in(FIXEDPOINT)))
*/
Z3_param_descrs Z3_API Z3_fixedpoint_get_param_descrs(Z3_context c, Z3_fixedpoint f);
/**
\brief Print the current rules and background axioms as a string.
\param c - context.
\param f - fixedpoint context.
\param num_queries - number of additional queries to print.
\param queries - additional queries.
def_API('Z3_fixedpoint_to_string', STRING, (_in(CONTEXT), _in(FIXEDPOINT), _in(UINT), _in_array(2, AST)))
*/
Z3_string Z3_API Z3_fixedpoint_to_string(
Z3_context c,
Z3_fixedpoint f,
unsigned num_queries,
Z3_ast queries[]);
/**
\brief Parse an SMT-LIB2 string with fixedpoint rules.
Add the rules to the current fixedpoint context.
Return the set of queries in the string.
\param c - context.
\param f - fixedpoint context.
\param s - string containing SMT2 specification.
def_API('Z3_fixedpoint_from_string', AST_VECTOR, (_in(CONTEXT), _in(FIXEDPOINT), _in(STRING)))
*/
Z3_ast_vector Z3_API Z3_fixedpoint_from_string(Z3_context c,
Z3_fixedpoint f,
Z3_string s);
/**
\brief Parse an SMT-LIB2 file with fixedpoint rules.
Add the rules to the current fixedpoint context.
Return the set of queries in the file.
\param c - context.
\param f - fixedpoint context.
\param s - string containing SMT2 specification.
def_API('Z3_fixedpoint_from_file', AST_VECTOR, (_in(CONTEXT), _in(FIXEDPOINT), _in(STRING)))
*/
Z3_ast_vector Z3_API Z3_fixedpoint_from_file(Z3_context c,
Z3_fixedpoint f,
Z3_string s);
/**
\brief Create a backtracking point.
The fixedpoint solver contains a set of rules, added facts and assertions.
The set of rules, facts and assertions are restored upon calling #Z3_fixedpoint_pop.
\sa Z3_fixedpoint_pop
def_API('Z3_fixedpoint_push', VOID, (_in(CONTEXT), _in(FIXEDPOINT)))
*/
void Z3_API Z3_fixedpoint_push(Z3_context c, Z3_fixedpoint d);
/**
\brief Backtrack one backtracking point.
\sa Z3_fixedpoint_push
\pre The number of calls to pop cannot exceed calls to push.
def_API('Z3_fixedpoint_pop', VOID, (_in(CONTEXT), _in(FIXEDPOINT)))
*/
void Z3_API Z3_fixedpoint_pop(Z3_context c, Z3_fixedpoint d);
/** \brief The following utilities allows adding user-defined domains. */
typedef void Z3_fixedpoint_reduce_assign_callback_fptr(
void*, Z3_func_decl,
unsigned, Z3_ast const [],
unsigned, Z3_ast const []);
typedef void Z3_fixedpoint_reduce_app_callback_fptr(
void*, Z3_func_decl,
unsigned, Z3_ast const [],
Z3_ast*);
/** \brief Initialize the context with a user-defined state. */
void Z3_API Z3_fixedpoint_init(Z3_context c, Z3_fixedpoint d, void* state);
/**
\brief Register a callback to destructive updates.
Registers are identified with terms encoded as fresh constants,
*/
void Z3_API Z3_fixedpoint_set_reduce_assign_callback(
Z3_context c ,Z3_fixedpoint d, Z3_fixedpoint_reduce_assign_callback_fptr cb);
/** \brief Register a callback for buildling terms based on the relational operators. */
void Z3_API Z3_fixedpoint_set_reduce_app_callback(
Z3_context c, Z3_fixedpoint d, Z3_fixedpoint_reduce_app_callback_fptr cb);
/*@}*/
/*@}*/
#ifdef __cplusplus
}
#endif // __cplusplus
#endif

209
src/api/z3_fpa.h
View file

@ -14,7 +14,7 @@ Author:
Christoph M. Wintersteiger (cwinter) 2013-06-05
Notes:
--*/
#ifndef Z3_FPA_H_
#define Z3_FPA_H_
@ -23,23 +23,16 @@ Notes:
extern "C" {
#endif // __cplusplus
/**
\defgroup capi C API
*/
/** \defgroup capi C API */
/*@{*/
/**
@name Floating-Point API
*/
/** @name Floating-Point Arithmetic */
/*@{*/
/**
\brief Create the RoundingMode sort.
\param c logical context
def_API('Z3_mk_fpa_rounding_mode_sort', SORT, (_in(CONTEXT),))
*/
Z3_sort Z3_API Z3_mk_fpa_rounding_mode_sort(Z3_context c);
@ -48,7 +41,7 @@ extern "C" {
\brief Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
\param c logical context
def_API('Z3_mk_fpa_round_nearest_ties_to_even', AST, (_in(CONTEXT),))
*/
Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_even(Z3_context c);
@ -66,7 +59,7 @@ extern "C" {
\brief Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
\param c logical context
def_API('Z3_mk_fpa_round_nearest_ties_to_away', AST, (_in(CONTEXT),))
*/
Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_away(Z3_context c);
@ -84,7 +77,7 @@ extern "C" {
\brief Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
\param c logical context
def_API('Z3_mk_fpa_round_toward_positive', AST, (_in(CONTEXT),))
*/
Z3_ast Z3_API Z3_mk_fpa_round_toward_positive(Z3_context c);
@ -100,7 +93,7 @@ extern "C" {
/**
\brief Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
\param c logical context
def_API('Z3_mk_fpa_round_toward_negative', AST, (_in(CONTEXT),))
@ -120,7 +113,7 @@ extern "C" {
\brief Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
\param c logical context
def_API('Z3_mk_fpa_round_toward_zero', AST, (_in(CONTEXT),))
*/
Z3_ast Z3_API Z3_mk_fpa_round_toward_zero(Z3_context c);
@ -142,8 +135,8 @@ extern "C" {
\param sbits number of significand bits
\remark ebits must be larger than 1 and sbits must be larger than 2.
def_API('Z3_mk_fpa_sort', SORT, (_in(CONTEXT), _in(UINT), _in(UINT)))
def_API('Z3_mk_fpa_sort', SORT, (_in(CONTEXT), _in(UINT), _in(UINT)))
*/
Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits);
@ -168,7 +161,7 @@ extern "C" {
/**
\brief Create the single-precision (32-bit) FloatingPoint sort.
\param c logical context.
\param c logical context.
def_API('Z3_mk_fpa_sort_single', SORT, (_in(CONTEXT),))
*/
@ -223,8 +216,8 @@ extern "C" {
\brief Create a floating-point NaN of sort s.
\param c logical context
\param s target sort
\param s target sort
def_API('Z3_mk_fpa_nan', AST, (_in(CONTEXT),_in(SORT)))
*/
Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s);
@ -233,9 +226,9 @@ extern "C" {
\brief Create a floating-point infinity of sort s.
\param c logical context
\param s target sort
\param s target sort
\param negative indicates whether the result should be negative
When \c negative is true, -oo will be generated instead of +oo.
def_API('Z3_mk_fpa_inf', AST, (_in(CONTEXT),_in(SORT),_in(BOOL)))
@ -258,14 +251,14 @@ extern "C" {
/**
\brief Create an expression of FloatingPoint sort from three bit-vector expressions.
This is the operator named `fp' in the SMT FP theory definition.
Note that \c sign is required to be a bit-vector of size 1. Significand and exponent
are required to be greater than 1 and 2 respectively. The FloatingPoint sort
This is the operator named `fp' in the SMT FP theory definition.
Note that \c sign is required to be a bit-vector of size 1. Significand and exponent
are required to be greater than 1 and 2 respectively. The FloatingPoint sort
of the resulting expression is automatically determined from the bit-vector sizes
of the arguments.
\param c logical context
\param sgn sign
\param sgn sign
\param exp exponent
\param sig significand
@ -292,8 +285,8 @@ extern "C" {
Z3_ast Z3_API Z3_mk_fpa_numeral_float(Z3_context c, float v, Z3_sort ty);
/**
\brief Create a numeral of FloatingPoint sort from a double.
\brief Create a numeral of FloatingPoint sort from a double.
This function is used to create numerals that fit in a double value.
It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string.
@ -363,21 +356,21 @@ extern "C" {
\param c logical context
\param t term of FloatingPoint sort
def_API('Z3_mk_fpa_abs', AST, (_in(CONTEXT),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t);
/**
\brief Floating-point negation
\param c logical context
\param t term of FloatingPoint sort
def_API('Z3_mk_fpa_neg', AST, (_in(CONTEXT),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t);
/**
\brief Floating-point addition
@ -387,11 +380,11 @@ extern "C" {
\param t2 term of FloatingPoint sort
rm must be of RoundingMode sort, t1 and t2 must have the same FloatingPoint sort.
def_API('Z3_mk_fpa_add', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2);
/**
\brief Floating-point subtraction
@ -401,11 +394,11 @@ extern "C" {
\param t2 term of FloatingPoint sort
rm must be of RoundingMode sort, t1 and t2 must have the same FloatingPoint sort.
def_API('Z3_mk_fpa_sub', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2);
Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2);
/**
\brief Floating-point multiplication
@ -415,11 +408,11 @@ extern "C" {
\param t2 term of FloatingPoint sort
rm must be of RoundingMode sort, t1 and t2 must have the same FloatingPoint sort.
def_API('Z3_mk_fpa_mul', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2);
Z3_ast Z3_API Z3_mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2);
/**
\brief Floating-point division
@ -429,11 +422,11 @@ extern "C" {
\param t2 term of FloatingPoint sort
The nodes rm must be of RoundingMode sort t1 and t2 must have the same FloatingPoint sort.
def_API('Z3_mk_fpa_div', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2);
Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2);
/**
\brief Floating-point fused multiply-add.
@ -446,11 +439,11 @@ extern "C" {
The result is round((t1 * t2) + t3)
rm must be of RoundingMode sort, t1, t2, and t3 must have the same FloatingPoint sort.
def_API('Z3_mk_fpa_fma', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_fma(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2, Z3_ast t3);
/**
\brief Floating-point square root
@ -459,11 +452,11 @@ extern "C" {
\param t term of FloatingPoint sort
rm must be of RoundingMode sort, t must have FloatingPoint sort.
def_API('Z3_mk_fpa_sqrt', AST, (_in(CONTEXT),_in(AST),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t);
/**
\brief Floating-point remainder
@ -472,13 +465,13 @@ extern "C" {
\param t2 term of FloatingPoint sort
t1 and t2 must have the same FloatingPoint sort.
def_API('Z3_mk_fpa_rem', AST, (_in(CONTEXT),_in(AST),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2);
/**
\brief Floating-point roundToIntegral. Rounds a floating-point number to
\brief Floating-point roundToIntegral. Rounds a floating-point number to
the closest integer, again represented as a floating-point number.
\param c logical context
@ -516,7 +509,7 @@ extern "C" {
def_API('Z3_mk_fpa_max', AST, (_in(CONTEXT),_in(AST),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2);
/**
\brief Floating-point less than or equal.
@ -525,9 +518,9 @@ extern "C" {
\param t2 term of FloatingPoint sort
t1 and t2 must have the same FloatingPoint sort.
def_API('Z3_mk_fpa_leq', AST, (_in(CONTEXT),_in(AST),_in(AST)))
*/
*/
Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2);
/**
@ -538,11 +531,11 @@ extern "C" {
\param t2 term of FloatingPoint sort
t1 and t2 must have the same FloatingPoint sort.
def_API('Z3_mk_fpa_lt', AST, (_in(CONTEXT),_in(AST),_in(AST)))
*/
*/
Z3_ast Z3_API Z3_mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2);
/**
\brief Floating-point greater than or equal.
@ -551,9 +544,9 @@ extern "C" {
\param t2 term of FloatingPoint sort
t1 and t2 must have the same FloatingPoint sort.
def_API('Z3_mk_fpa_geq', AST, (_in(CONTEXT),_in(AST),_in(AST)))
*/
*/
Z3_ast Z3_API Z3_mk_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2);
/**
@ -564,9 +557,9 @@ extern "C" {
\param t2 term of FloatingPoint sort
t1 and t2 must have the same FloatingPoint sort.
def_API('Z3_mk_fpa_gt', AST, (_in(CONTEXT),_in(AST),_in(AST)))
*/
*/
Z3_ast Z3_API Z3_mk_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2);
/**
@ -583,7 +576,7 @@ extern "C" {
def_API('Z3_mk_fpa_eq', AST, (_in(CONTEXT),_in(AST),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2);
/**
\brief Predicate indicating whether t is a normal floating-point number.
@ -591,9 +584,9 @@ extern "C" {
\param t term of FloatingPoint sort
t must have FloatingPoint sort.
def_API('Z3_mk_fpa_is_normal', AST, (_in(CONTEXT),_in(AST)))
*/
*/
Z3_ast Z3_API Z3_mk_fpa_is_normal(Z3_context c, Z3_ast t);
/**
@ -603,9 +596,9 @@ extern "C" {
\param t term of FloatingPoint sort
t must have FloatingPoint sort.
def_API('Z3_mk_fpa_is_subnormal', AST, (_in(CONTEXT),_in(AST)))
*/
*/
Z3_ast Z3_API Z3_mk_fpa_is_subnormal(Z3_context c, Z3_ast t);
/**
@ -615,9 +608,9 @@ extern "C" {
\param t term of FloatingPoint sort
t must have FloatingPoint sort.
def_API('Z3_mk_fpa_is_zero', AST, (_in(CONTEXT),_in(AST)))
*/
*/
Z3_ast Z3_API Z3_mk_fpa_is_zero(Z3_context c, Z3_ast t);
/**
@ -627,9 +620,9 @@ extern "C" {
\param t term of FloatingPoint sort
t must have FloatingPoint sort.
def_API('Z3_mk_fpa_is_infinite', AST, (_in(CONTEXT),_in(AST)))
*/
*/
Z3_ast Z3_API Z3_mk_fpa_is_infinite(Z3_context c, Z3_ast t);
/**
@ -639,9 +632,9 @@ extern "C" {
\param t term of FloatingPoint sort
t must have FloatingPoint sort.
def_API('Z3_mk_fpa_is_nan', AST, (_in(CONTEXT),_in(AST)))
*/
*/
Z3_ast Z3_API Z3_mk_fpa_is_nan(Z3_context c, Z3_ast t);
/**
@ -671,29 +664,29 @@ extern "C" {
/**
\brief Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
Produces a term that represents the conversion of a bit-vector term bv to a
Produces a term that represents the conversion of a bit-vector term bv to a
floating-point term of sort s.
\param c logical context
\param bv a bit-vector term
\param s floating-point sort
s must be a FloatingPoint sort, t must be of bit-vector sort, and the bit-vector
size of bv must be equal to ebits+sbits of s. The format of the bit-vector is
s must be a FloatingPoint sort, t must be of bit-vector sort, and the bit-vector
size of bv must be equal to ebits+sbits of s. The format of the bit-vector is
as defined by the IEEE 754-2008 interchange format.
def_API('Z3_mk_fpa_to_fp_bv', AST, (_in(CONTEXT),_in(AST),_in(SORT)))
*/
*/
Z3_ast Z3_API Z3_mk_fpa_to_fp_bv(Z3_context c, Z3_ast bv, Z3_sort s);
/**
\brief Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
Produces a term that represents the conversion of a floating-point term t to a
floating-point term of sort s. If necessary, the result will be rounded according
to rounding mode rm.
\param c logical context
\param c logical context
\param rm term of RoundingMode sort
\param t term of FloatingPoint sort
\param s floating-point sort
@ -711,7 +704,7 @@ extern "C" {
floating-point term of sort s. If necessary, the result will be rounded according
to rounding mode rm.
\param c logical context
\param c logical context
\param rm term of RoundingMode sort
\param t term of Real sort
\param s floating-point sort
@ -726,7 +719,7 @@ extern "C" {
\brief Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.
Produces a term that represents the conversion of the bit-vector term t into a
floating-point term of sort s. The bit-vector t is taken to be in signed
floating-point term of sort s. The bit-vector t is taken to be in signed
2's complement format. If necessary, the result will be rounded according
to rounding mode rm.
@ -764,8 +757,8 @@ extern "C" {
\brief Conversion of a floating-point term into an unsigned bit-vector.
Produces a term that represents the conversion of the floating-poiunt term t into a
bit-vector term of size sz in unsigned 2's complement format. If necessary, the result
will be rounded according to rounding mode rm.
bit-vector term of size sz in unsigned 2's complement format. If necessary, the result
will be rounded according to rounding mode rm.
\param c logical context
\param rm term of RoundingMode sort
@ -780,8 +773,8 @@ extern "C" {
\brief Conversion of a floating-point term into a signed bit-vector.
Produces a term that represents the conversion of the floating-poiunt term t into a
bit-vector term of size sz in signed 2's complement format. If necessary, the result
will be rounded according to rounding mode rm.
bit-vector term of size sz in signed 2's complement format. If necessary, the result
will be rounded according to rounding mode rm.
\param c logical context
\param rm term of RoundingMode sort
@ -796,10 +789,10 @@ extern "C" {
\brief Conversion of a floating-point term into a real-numbered term.
Produces a term that represents the conversion of the floating-poiunt term t into a
real number. Note that this type of conversion will often result in non-linear
real number. Note that this type of conversion will often result in non-linear
constraints over real terms.
\param c logical context
\param c logical context
\param t term of FloatingPoint sort
def_API('Z3_mk_fpa_to_real', AST, (_in(CONTEXT),_in(AST)))
@ -807,15 +800,12 @@ extern "C" {
Z3_ast Z3_API Z3_mk_fpa_to_real(Z3_context c, Z3_ast t);
/**
@name Z3-specific floating-point extensions
*/
/** @name Z3-specific floating-point extensions */
/*@{*/
/**
\brief Retrieves the number of bits reserved for the exponent in a FloatingPoint sort.
\param c logical context
\param c logical context
\param s FloatingPoint sort
def_API('Z3_fpa_get_ebits', UINT, (_in(CONTEXT),_in(SORT)))
@ -825,7 +815,7 @@ extern "C" {
/**
\brief Retrieves the number of bits reserved for the significand in a FloatingPoint sort.
\param c logical context
\param c logical context
\param s FloatingPoint sort
def_API('Z3_fpa_get_sbits', UINT, (_in(CONTEXT),_in(SORT)))
@ -835,9 +825,9 @@ extern "C" {
/**
\brief Retrieves the sign of a floating-point literal.
\param c logical context
\param c logical context
\param t a floating-point numeral
\param sgn sign
\param sgn sign
Remarks: sets \c sgn to 0 if the literal is NaN or positive and to 1 otherwise.
@ -848,7 +838,7 @@ extern "C" {
/**
\brief Return the significand value of a floating-point numeral as a string.
\param c logical context
\param c logical context
\param t a floating-point numeral
Remarks: The significand s is always 0 < s < 2.0; the resulting string is long
@ -863,9 +853,10 @@ extern "C" {
\param c logical context
\param t a floating-point numeral
\param n pointer to output uint64
Remarks: This function extracts the significand bits in `t`, without the
hidden bit or normalization. Sets the Z3_INVALID_ARG error code if the
Remarks: This function extracts the significand bits in `t`, without the
hidden bit or normalization. Sets the Z3_INVALID_ARG error code if the
significand does not fit into a uint64.
def_API('Z3_fpa_get_numeral_significand_uint64', BOOL, (_in(CONTEXT), _in(AST), _out(UINT64)))
@ -875,7 +866,7 @@ extern "C" {
/**
\brief Return the exponent value of a floating-point numeral as a string
\param c logical context
\param c logical context
\param t a floating-point numeral
def_API('Z3_fpa_get_numeral_exponent_string', STRING, (_in(CONTEXT), _in(AST)))
@ -887,7 +878,7 @@ extern "C" {
\param c logical context
\param t a floating-point numeral
\param n exponent
\param n exponent
def_API('Z3_fpa_get_numeral_exponent_int64', BOOL, (_in(CONTEXT), _in(AST), _out(INT64)))
*/
@ -899,12 +890,12 @@ extern "C" {
\param c logical context
\param t term of FloatingPoint sort
t must have FloatingPoint sort. The size of the resulting bit-vector is automatically
determined.
Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
knows only one NaN and it will always produce the same bit-vector represenatation of
that NaN.
t must have FloatingPoint sort. The size of the resulting bit-vector is automatically
determined.
Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
knows only one NaN and it will always produce the same bit-vector represenatation of
that NaN.
def_API('Z3_mk_fpa_to_ieee_bv', AST, (_in(CONTEXT),_in(AST)))
*/
@ -913,14 +904,14 @@ extern "C" {
/**
\brief Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort.
Produces a term that represents the conversion of sig * 2^exp into a
Produces a term that represents the conversion of sig * 2^exp into a
floating-point term of sort s. If necessary, the result will be rounded
according to rounding mode rm.
\param c logical context
\param c logical context
\param rm term of RoundingMode sort
\param exp exponent term of Int sort
\param sig significand term of Real sort
\param sig significand term of Real sort
\param s FloatingPoint sort
s must be a FloatingPoint sort, rm must be of RoundingMode sort, exp must be of int sort, sig must be of real sort.
@ -928,9 +919,7 @@ extern "C" {
def_API('Z3_mk_fpa_to_fp_int_real', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST),_in(SORT)))
*/
Z3_ast Z3_API Z3_mk_fpa_to_fp_int_real(Z3_context c, Z3_ast rm, Z3_ast exp, Z3_ast sig, Z3_sort s);
/*@}*/
/*@}*/
/*@}*/

25
src/api/z3_interp.h
View file

@ -23,21 +23,13 @@ Notes:
extern "C" {
#endif // __cplusplus
/**
\defgroup capi C API
*/
/** \defgroup capi C API */
/*@{*/
/**
@name Interpolation API
*/
/** @name Interpolation facilities */
/*@{*/
/**
\brief \mlh mk_interp c a \endmlh
Create an AST node marking a formula position for interpolation.
\brief Create an AST node marking a formula position for interpolation.
The node \c a must have Boolean sort.
@ -112,7 +104,7 @@ extern "C" {
Currently, the only SMT solver that is supported is the legacy
SMT solver. Such a solver is available as the default solver in
#Z3_context objects produced by #Z3_mk_interpolation_context.
\c Z3_context objects produced by #Z3_mk_interpolation_context.
Currently, the theories supported are equality with
uninterpreted functions, linear integer arithmetic, and the
theory of arrays (in SMT-LIB terms, this is AUFLIA).
@ -164,10 +156,10 @@ extern "C" {
def_API('Z3_compute_interpolant', INT, (_in(CONTEXT), _in(AST), _in(PARAMS), _out(AST_VECTOR), _out(MODEL)))
*/
Z3_lbool Z3_API Z3_compute_interpolant(Z3_context c,
Z3_ast pat,
Z3_params p,
Z3_ast_vector *interp,
Z3_lbool Z3_API Z3_compute_interpolant(Z3_context c,
Z3_ast pat,
Z3_params p,
Z3_ast_vector *interp,
Z3_model *model);
/** Return a string summarizing cumulative time used for
@ -282,7 +274,6 @@ extern "C" {
Z3_string filename,
unsigned num_theory,
Z3_ast theory[]);
/*@}*/
/*@}*/

9
src/api/z3_macros.h
View file

@ -14,7 +14,7 @@ Copyright (c) 2015 Microsoft Corporation
# else
# define Z3_API
# endif
#endif
#endif
#ifndef DEFINE_TYPE
#define DEFINE_TYPE(T) typedef struct _ ## T *T
@ -23,10 +23,3 @@ Copyright (c) 2015 Microsoft Corporation
#ifndef DEFINE_VOID
#define DEFINE_VOID(T) typedef void* T
#endif
#ifndef BEGIN_MLAPI_EXCLUDE
#define BEGIN_MLAPI_EXCLUDE
#endif
#ifndef END_MLAPI_EXCLUDE
#define END_MLAPI_EXCLUDE
#endif

223
src/api/z3_optimization.h Normal file
View file

@ -0,0 +1,223 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
z3_optimization.h
Abstract:
Optimization facilities
Author:
Christoph M. Wintersteiger (cwinter) 2015-12-03
Notes:
--*/
#ifndef Z3_OPTIMIZATION_H_
#define Z3_OPTIMIZATION_H_
#ifdef __cplusplus
extern "C" {
#endif // __cplusplus
/** \defgroup capi C API */
/*@{*/
/** @name Optimization facilities */
/*@{*/
/**
\brief Create a new optimize context.
\remark User must use #Z3_optimize_inc_ref and #Z3_optimize_dec_ref to manage optimize objects.
Even if the context was created using #Z3_mk_context instead of #Z3_mk_context_rc.
def_API('Z3_mk_optimize', OPTIMIZE, (_in(CONTEXT), ))
*/
Z3_optimize Z3_API Z3_mk_optimize(Z3_context c);
/**
\brief Increment the reference counter of the given optimize context
def_API('Z3_optimize_inc_ref', VOID, (_in(CONTEXT), _in(OPTIMIZE)))
*/
void Z3_API Z3_optimize_inc_ref(Z3_context c,Z3_optimize d);
/**
\brief Decrement the reference counter of the given optimize context.
def_API('Z3_optimize_dec_ref', VOID, (_in(CONTEXT), _in(OPTIMIZE)))
*/
void Z3_API Z3_optimize_dec_ref(Z3_context c,Z3_optimize d);
/**
\brief Assert hard constraint to the optimization context.
def_API('Z3_optimize_assert', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(AST)))
*/
void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a);
/**
\brief Assert soft constraint to the optimization context.
\param c - context
\param o - optimization context
\param a - formula
\param weight - a positive weight, penalty for violating soft constraint
\param id - optional identifier to group soft constraints
def_API('Z3_optimize_assert_soft', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST), _in(STRING), _in(SYMBOL)))
*/
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.
\param c - context
\param o - optimization context
\param a - arithmetical term
def_API('Z3_optimize_maximize', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST)))
*/
unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t);
/**
\brief Add a minimization constraint.
\param c - context
\param o - optimization context
\param a - arithmetical term
def_API('Z3_optimize_minimize', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST)))
*/
unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t);
/**
\brief Create a backtracking point.
The optimize solver contains a set of rules, added facts and assertions.
The set of rules, facts and assertions are restored upon calling #Z3_optimize_pop.
\sa Z3_optimize_pop
def_API('Z3_optimize_push', VOID, (_in(CONTEXT), _in(OPTIMIZE)))
*/
void Z3_API Z3_optimize_push(Z3_context c,Z3_optimize d);
/**
\brief Backtrack one level.
\sa Z3_optimize_push
\pre The number of calls to pop cannot exceed calls to push.
def_API('Z3_optimize_pop', VOID, (_in(CONTEXT), _in(OPTIMIZE)))
*/
void Z3_API Z3_optimize_pop(Z3_context c,Z3_optimize d);
/**
\brief Check consistency and produce optimal values.
\param c - context
\param o - optimization context
def_API('Z3_optimize_check', INT, (_in(CONTEXT), _in(OPTIMIZE)))
*/
Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o);
/**
\brief Retrieve a string that describes the last status returned by #Z3_optimize_check.
Use this method when #Z3_optimize_check returns Z3_L_UNDEF.
def_API('Z3_optimize_get_reason_unknown', STRING, (_in(CONTEXT), _in(OPTIMIZE) ))
*/
Z3_string Z3_API Z3_optimize_get_reason_unknown(Z3_context c,Z3_optimize d);
/**
\brief Retrieve the model for the last #Z3_optimize_check
The error handler is invoked if a model is not available because
the commands above were not invoked for the given optimization
solver, or if the result was \c Z3_L_FALSE.
def_API('Z3_optimize_get_model', MODEL, (_in(CONTEXT), _in(OPTIMIZE)))
*/
Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o);
/**
\brief Set parameters on optimization context.
\param c - context
\param o - optimization context
\param p - parameters
def_API('Z3_optimize_set_params', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(PARAMS)))
*/
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p);
/**
\brief Return the parameter description set for the given optimize object.
\param c - context
\param o - optimization context
def_API('Z3_optimize_get_param_descrs', PARAM_DESCRS, (_in(CONTEXT), _in(OPTIMIZE)))
*/
Z3_param_descrs Z3_API Z3_optimize_get_param_descrs(Z3_context c, Z3_optimize o);
/**
\brief Retrieve lower bound value or approximation for the i'th optimization objective.
\param c - context
\param o - optimization context
\param idx - index of optimization objective
def_API('Z3_optimize_get_lower', AST, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT)))
*/
Z3_ast Z3_API Z3_optimize_get_lower(Z3_context c, Z3_optimize o, unsigned idx);
/**
\brief Retrieve upper bound value or approximation for the i'th optimization objective.
\param c - context
\param o - optimization context
\param idx - index of optimization objective
def_API('Z3_optimize_get_upper', AST, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT)))
*/
Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx);
/**
\brief Print the current context as a string.
\param c - context.
\param o - optimization context.
def_API('Z3_optimize_to_string', STRING, (_in(CONTEXT), _in(OPTIMIZE)))
*/
Z3_string Z3_API Z3_optimize_to_string(
Z3_context c,
Z3_optimize o);
/**
\brief Return a string containing a description of parameters accepted by optimize.
def_API('Z3_optimize_get_help', STRING, (_in(CONTEXT), _in(OPTIMIZE)))
*/
Z3_string Z3_API Z3_optimize_get_help(Z3_context c, Z3_optimize t);
/**
\brief Retrieve statistics information from the last call to #Z3_optimize_check
def_API('Z3_optimize_get_statistics', STATS, (_in(CONTEXT), _in(OPTIMIZE)))
*/
Z3_stats Z3_API Z3_optimize_get_statistics(Z3_context c,Z3_optimize d);
/*@}*/
/*@}*/
#ifdef __cplusplus
}
#endif // __cplusplus
#endif

20
src/api/z3_polynomial.h
View file

@ -14,7 +14,7 @@ Author:
Leonardo de Moura (leonardo) 2012-12-09
Notes:
--*/
#ifndef Z3_POLYNOMIAL_H_
@ -24,27 +24,21 @@ Notes:
extern "C" {
#endif // __cplusplus
/**
\defgroup capi C API
*/
/** \defgroup capi C API */
/*@{*/
/**
@name Polynomials API
*/
/** @name Polynomials */
/*@{*/
/**
\brief Return the nonzero subresultants of \c p and \c q with respect to the "variable" \c x.
\pre \c p, \c q and \c x are Z3 expressions where \c p and \c q are arithmetic terms.
Note that, any subterm that cannot be viewed as a polynomial is assumed to be a variable.
Example: f(a) is a considered to be a variable in the polynomial
f(a)*f(a) + 2*f(a) + 1
Example: f(a) is a considered to be a variable in the polynomial
f(a)*f(a) + 2*f(a) + 1
def_API('Z3_polynomial_subresultants', AST_VECTOR, (_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
*/

11
src/api/z3_private.h
View file

@ -15,7 +15,7 @@ Author:
Leonardo de Moura (leonardo) 2007-06-8
Notes:
--*/
#include<iostream>
@ -25,24 +25,15 @@ Notes:
#ifndef Z3_PRIVATE_H_
#define Z3_PRIVATE_H_
#ifndef CAMLIDL
#ifdef __cplusplus
extern "C" {
#endif // __cplusplus
#else
[pointer_default(ref)] interface Z3 {
#endif // CAMLIDL
Z3_bool Z3_API Z3_get_numeral_rational(Z3_context c, Z3_ast a, rational& r);
#ifndef CAMLIDL
#ifdef __cplusplus
};
#endif // __cplusplus
#else
}
#endif // CAMLIDL
#endif

27
src/api/z3_rcf.h
View file

@ -17,7 +17,7 @@ Author:
Leonardo de Moura (leonardo) 2012-01-05
Notes:
--*/
#ifndef Z3_RCF_H_
#define Z3_RCF_H_
@ -25,19 +25,12 @@ Notes:
#ifdef __cplusplus
extern "C" {
#endif // __cplusplus
/**
\defgroup capi C API
*/
/** \defgroup capi C API */
/*@{*/
/**
@name Real Closed Fields API
*/
/** @name Real Closed Fields */
/*@{*/
/**
\brief Delete a RCF numeral created using the RCF API.
@ -82,43 +75,43 @@ extern "C" {
/**
\brief Store in roots the roots of the polynomial <tt>a[n-1]*x^{n-1} + ... + a[0]</tt>.
The output vector \c roots must have size \c n.
The output vector \c roots must have size \c n.
It returns the number of roots of the polynomial.
\pre The input polynomial is not the zero polynomial.
\pre The input polynomial is not the zero polynomial.
def_API('Z3_rcf_mk_roots', UINT, (_in(CONTEXT), _in(UINT), _in_array(1, RCF_NUM), _out_array(1, RCF_NUM)))
*/
unsigned Z3_API Z3_rcf_mk_roots(Z3_context c, unsigned n, Z3_rcf_num const a[], Z3_rcf_num roots[]);
/**
\brief Return the value a + b.
\brief Return the value a + b.
def_API('Z3_rcf_add', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
Z3_rcf_num Z3_API Z3_rcf_add(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return the value a - b.
\brief Return the value a - b.
def_API('Z3_rcf_sub', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
Z3_rcf_num Z3_API Z3_rcf_sub(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return the value a * b.
\brief Return the value a * b.
def_API('Z3_rcf_mul', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
Z3_rcf_num Z3_API Z3_rcf_mul(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return the value a / b.
\brief Return the value a / b.
def_API('Z3_rcf_div', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
Z3_rcf_num Z3_API Z3_rcf_div(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return the value -a