mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-02-12 18:32:46 +00:00
commit 6319861e26
14 changed files with 232 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

17
examples/c++/example.cpp
View file

@ -1095,6 +1095,22 @@ void sudoku_example() {
}
}
void param_descrs_example() {
std::cout << "parameter description example\n";
context c;
param_descrs p = param_descrs::simplify_param_descrs(c);
std::cout << p << "\n";
unsigned sz = p.size();
for (unsigned i = 0; i < sz; ++i) {
symbol nm = p.name(i);
char const* kind = "other";
Z3_param_kind k = p.kind(nm);
if (k == Z3_PK_UINT) kind = "uint";
if (k == Z3_PK_BOOL) kind = "bool";
std::cout << nm << ": " << p.documentation(nm) << " kind: " << kind << "\n";
}
}
int main() {
try {
@ -1136,6 +1152,7 @@ int main() {
substitute_example(); std::cout << "\n";
opt_example(); std::cout << "\n";
extract_example(); std::cout << "\n";
param_descrs_example(); std::cout << "\n";
sudoku_example(); std::cout << "\n";
std::cout << "done\n";
}

41
examples/c/test_capi.c
View file

@ -2341,6 +2341,46 @@ void unsat_core_and_proof_example() {
Z3_del_context(ctx);
}
void interpolation_example() {
Z3_context ctx = mk_context();
Z3_ast pa = mk_bool_var(ctx, "PredA");
Z3_ast pb = mk_bool_var(ctx, "PredB");
Z3_ast pc = mk_bool_var(ctx, "PredC");
Z3_ast args1[2] = {pa,pb}, args2[2] = {Z3_mk_not(ctx,pb),pc};
Z3_ast args3[2] = {Z3_mk_interpolant(ctx,Z3_mk_and(ctx,2,args1)),Z3_mk_and(ctx,2,args2)};
Z3_ast f = Z3_mk_and(ctx,2,args3);
Z3_ast_vector interpolant = 0;
Z3_model m = 0;
printf("\ninterpolation_example\n");
LOG_MSG("interpolation_example");
Z3_lbool result = Z3_compute_interpolant(ctx,f,0,&interpolant,&m);
switch (result) {
case Z3_L_FALSE:
printf("unsat\n");
printf("interpolant: %s\n", Z3_ast_to_string(ctx, Z3_ast_vector_get(ctx, interpolant, 0)));
printf("\n");
break;
case Z3_L_UNDEF:
printf("unknown\n");
printf("potential model:\n");
if (m) Z3_model_inc_ref(ctx, m);
display_model(ctx, stdout, m);
break;
case Z3_L_TRUE:
printf("sat\n");
if (m) Z3_model_inc_ref(ctx, m);
display_model(ctx, stdout, m);
break;
}
/* delete logical context */
if (m) Z3_model_dec_ref(ctx, m);
Z3_del_context(ctx);
}
#define MAX_RETRACTABLE_ASSERTIONS 1024
/**
@ -2825,6 +2865,7 @@ int main() {
binary_tree_example();
enum_example();
unsat_core_and_proof_example();
interpolation_example();
incremental_example1();
reference_counter_example();
smt2parser_example();

4
src/api/api_interp.cpp
View file

@ -289,7 +289,7 @@ extern "C" {
}
catch (z3_exception & ex) {
mk_c(c)->handle_exception(ex);
return Z3_L_UNDEF;
RETURN_Z3_compute_interpolant Z3_L_UNDEF;
}
}
@ -323,7 +323,7 @@ extern "C" {
*out_interp = of_ast_vector(v);
return status;
RETURN_Z3_compute_interpolant status;
Z3_CATCH_RETURN(Z3_L_UNDEF);
}

13
src/api/api_params.cpp
View file

@ -179,6 +179,19 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
Z3_string Z3_API Z3_param_descrs_get_documentation(Z3_context c, Z3_param_descrs p, Z3_symbol s) {
Z3_TRY;
LOG_Z3_param_descrs_get_documentation(c, p, s);
RESET_ERROR_CODE();
char const* result = to_param_descrs_ptr(p)->get_descr(to_symbol(s));
if (result == 0) {
SET_ERROR_CODE(Z3_IOB);
RETURN_Z3(0);
}
return mk_c(c)->mk_external_string(result);
Z3_CATCH_RETURN(0);
}
Z3_string Z3_API Z3_param_descrs_to_string(Z3_context c, Z3_param_descrs p) {
Z3_TRY;
LOG_Z3_param_descrs_to_string(c, p);

31
src/api/c++/z3++.h
View file

@ -49,6 +49,7 @@ namespace z3 {
class context;
class symbol;
class params;
class param_descrs;
class ast;
class sort;
class func_decl;
@ -286,6 +287,9 @@ namespace z3 {
};
template<typename T>
class array {
T * m_array;
@ -338,6 +342,30 @@ namespace z3 {
}
class param_descrs : public object {
Z3_param_descrs m_descrs;
public:
param_descrs(context& c, Z3_param_descrs d): object(c), m_descrs(d) { Z3_param_descrs_inc_ref(c, d); }
param_descrs(param_descrs const& o): object(o.ctx()), m_descrs(o.m_descrs) { Z3_param_descrs_inc_ref(ctx(), m_descrs); }
param_descrs& operator=(param_descrs const& o) {
Z3_param_descrs_inc_ref(o.ctx(), o.m_descrs);
Z3_param_descrs_dec_ref(ctx(), m_descrs);
m_descrs = o.m_descrs;
m_ctx = o.m_ctx;
return *this;
}
~param_descrs() { Z3_param_descrs_dec_ref(ctx(), m_descrs); }
static param_descrs simplify_param_descrs(context& c) { return param_descrs(c, Z3_simplify_get_param_descrs(c)); }
unsigned size() { return Z3_param_descrs_size(ctx(), m_descrs); }
symbol name(unsigned i) { return symbol(ctx(), Z3_param_descrs_get_name(ctx(), m_descrs, i)); }
Z3_param_kind kind(symbol const& s) { return Z3_param_descrs_get_kind(ctx(), m_descrs, s); }
std::string documentation(symbol const& s) { char const* r = Z3_param_descrs_get_documentation(ctx(), m_descrs, s); check_error(); return r; }
std::string to_string() const { return Z3_param_descrs_to_string(ctx(), m_descrs); }
};
inline std::ostream& operator<<(std::ostream & out, param_descrs const & d) { return out << d.to_string(); }
class params : public object {
Z3_params m_params;
public:
@ -1572,6 +1600,8 @@ namespace z3 {
fmls,
fml));
}
param_descrs get_param_descrs() { return param_descrs(ctx(), Z3_solver_get_param_descrs(ctx(), m_solver)); }
};
inline std::ostream & operator<<(std::ostream & out, solver const & s) { out << Z3_solver_to_string(s.ctx(), s); return out; }
@ -1686,6 +1716,7 @@ namespace z3 {
friend tactic repeat(tactic const & t, unsigned max);
friend tactic with(tactic const & t, params const & p);
friend tactic try_for(tactic const & t, unsigned ms);
param_descrs get_param_descrs() { return param_descrs(ctx(), Z3_tactic_get_param_descrs(ctx(), m_tactic)); }
};
inline tactic operator&(tactic const & t1, tactic const & t2) {

9
src/api/dotnet/ParamDescrs.cs
View file

@ -46,6 +46,15 @@ namespace Microsoft.Z3
return (Z3_param_kind)Native.Z3_param_descrs_get_kind(Context.nCtx, NativeObject, name.NativeObject);
}
/// <summary>
/// Retrieve documentation of parameter.
/// </summary>
public string GetDocumentation(Symbol name)
{
Contract.Requires(name != null);
return Native.Z3_param_descrs_get_documentation(Context.nCtx, NativeObject, name.NativeObject);
}
/// <summary>
/// Retrieve all names of parameters.
/// </summary>

9
src/api/java/ParamDescrs.java
View file

@ -44,6 +44,15 @@ public class ParamDescrs extends Z3Object
getContext().nCtx(), getNativeObject(), name.getNativeObject()));
}
/**
* Retrieve documentation of parameter.
**/
public String getDocumentation(Symbol name)
{
return Native.paramDescrsGetDocumentation(getContext().nCtx(), getNativeObject(), name.getNativeObject());
}
/**
* Retrieve all names of parameters.
*

5
src/api/python/z3.py
View file

@ -4649,6 +4649,11 @@ class ParamDescrsRef:
"""
return Z3_param_descrs_get_kind(self.ctx.ref(), self.descr, to_symbol(n, self.ctx))
def get_documentation(self, n):
"""Return the documentation string of the parameter named `n`.
"""
return Z3_param_descrs_get_documentation(self.ctx.ref(), self.descr, to_symbol(n, self.ctx))
def __getitem__(self, arg):
if _is_int(arg):
return self.get_name(arg)

7
src/api/z3_api.h
View file

@ -1666,6 +1666,13 @@ extern "C" {
*/
Z3_symbol Z3_API Z3_param_descrs_get_name(Z3_context c, Z3_param_descrs p, unsigned i);
/**
\brief Retrieve documentation string corresponding to parameter name \c s.
def_API('Z3_param_descrs_get_documentation', STRING, (_in(CONTEXT), _in(PARAM_DESCRS), _in(SYMBOL)))
*/
Z3_string Z3_API Z3_param_descrs_get_documentation(Z3_context c, Z3_param_descrs p, Z3_symbol s);
/**
\brief Convert a parameter description set into a string. This function is mainly used for printing the
contents of a parameter description set.

63
src/ast/rewriter/seq_rewriter.cpp
View file

@ -83,7 +83,7 @@ eautomaton* re2automaton::operator()(expr* e) {
eautomaton* re2automaton::re2aut(expr* e) {
SASSERT(u.is_re(e));
expr* e1, *e2;
expr *e0, *e1, *e2;
scoped_ptr<eautomaton> a, b;
unsigned lo, hi;
zstring s1, s2;
@ -98,8 +98,7 @@ eautomaton* re2automaton::re2aut(expr* e) {
}
else if (u.re.is_star(e, e1) && (a = re2aut(e1))) {
a->add_final_to_init_moves();
a->add_init_to_final_states();
a->add_init_to_final_states();
return a.detach();
}
else if (u.re.is_plus(e, e1) && (a = re2aut(e1))) {
@ -116,8 +115,6 @@ eautomaton* re2automaton::re2aut(expr* e) {
unsigned start = s1[0];
unsigned stop = s2[0];
unsigned nb = s1.num_bits();
sort_ref s(bv.mk_sort(nb), m);
expr_ref v(m.mk_var(0, s), m);
expr_ref _start(bv.mk_numeral(start, nb), m);
expr_ref _stop(bv.mk_numeral(stop, nb), m);
a = alloc(eautomaton, sm, sym_expr::mk_range(_start, _stop));
@ -127,6 +124,39 @@ eautomaton* re2automaton::re2aut(expr* e) {
TRACE("seq", tout << "Range expression is not handled: " << mk_pp(e, m) << "\n";);
}
}
else if (u.re.is_complement(e, e0)) {
if (u.re.is_range(e0, e1, e2) && u.str.is_string(e1, s1) && u.str.is_string(e2, s2) &&
s1.length() == 1 && s2.length() == 1) {
unsigned start = s1[0];
unsigned stop = s2[0];
unsigned nb = s1.num_bits();
sort_ref s(bv.mk_sort(nb), m);
expr_ref v(m.mk_var(0, s), m);
expr_ref _start(bv.mk_numeral(start, nb), m);
expr_ref _stop(bv.mk_numeral(stop, nb), m);
expr_ref _pred(m.mk_not(m.mk_and(bv.mk_ule(_start, v), bv.mk_ule(v, _stop))), m);
a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred));
return a.detach();
}
else if (u.re.is_to_re(e0, e1) && u.str.is_string(e1, s1) && s1.length() == 1) {
unsigned nb = s1.num_bits();
sort_ref s(bv.mk_sort(nb), m);
expr_ref v(m.mk_var(0, s), m);
expr_ref _ch(bv.mk_numeral(s1[0], nb), m);
expr_ref _pred(m.mk_not(m.mk_eq(v, _ch)), m);
a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred));
return a.detach();
}
else if (u.re.is_to_re(e0, e1) && u.str.is_unit(e1, e2)) {
expr_ref v(m.mk_var(0, m.get_sort(e2)), m);
expr_ref _pred(m.mk_not(m.mk_eq(v, e2)), m);
a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred));
return a.detach();
}
else {
TRACE("seq", tout << "Complement expression is not handled: " << mk_pp(e, m) << "\n";);
}
}
else if (u.re.is_loop(e, e1, lo, hi) && (a = re2aut(e1))) {
scoped_ptr<eautomaton> eps = eautomaton::mk_epsilon(sm);
b = eautomaton::mk_epsilon(sm);
@ -225,6 +255,9 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
case OP_RE_INTERSECT:
SASSERT(num_args == 2);
return mk_re_inter(args[0], args[1], result);
case OP_RE_COMPLEMENT:
SASSERT(num_args == 1);
return mk_re_complement(args[0], result);
case OP_RE_LOOP:
return mk_re_loop(num_args, args, result);
case OP_RE_EMPTY_SET:
@ -967,6 +1000,26 @@ br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) {
return BR_FAILED;
}
br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) {
expr* e1, *e2;
if (m_util.re.is_intersection(a, e1, e2)) {
result = m_util.re.mk_union(m_util.re.mk_complement(e1), m_util.re.mk_complement(e2));
return BR_REWRITE2;
}
if (m_util.re.is_union(a, e1, e2)) {
result = m_util.re.mk_inter(m_util.re.mk_complement(e1), m_util.re.mk_complement(e2));
return BR_REWRITE2;
}
if (m_util.re.is_empty(a)) {
result = m_util.re.mk_full(m().get_sort(a));
return BR_DONE;
}
if (m_util.re.is_full(a)) {
result = m_util.re.mk_empty(m().get_sort(a));
return BR_DONE;
}
return BR_FAILED;
}
/**
(emp n r) = emp

1
src/ast/rewriter/seq_rewriter.h
View file

@ -96,6 +96,7 @@ class seq_rewriter {
br_status mk_re_concat(expr* a, expr* b, expr_ref& result);
br_status mk_re_union(expr* a, expr* b, expr_ref& result);
br_status mk_re_inter(expr* a, expr* b, expr_ref& result);
br_status mk_re_complement(expr* a, expr_ref& result);
br_status mk_re_star(expr* a, expr_ref& result);
br_status mk_re_plus(expr* a, expr_ref& result);
br_status mk_re_opt(expr* a, expr_ref& result);

29
src/ast/seq_decl_plugin.cpp
View file

@ -456,6 +456,7 @@ void seq_decl_plugin::init() {
m_sigs[OP_RE_UNION] = alloc(psig, m, "re.union", 1, 2, reAreA, reA);
m_sigs[OP_RE_INTERSECT] = alloc(psig, m, "re.inter", 1, 2, reAreA, reA);
m_sigs[OP_RE_LOOP] = alloc(psig, m, "re.loop", 1, 1, &reA, reA);
m_sigs[OP_RE_COMPLEMENT] = alloc(psig, m, "re.complement", 1, 1, &reA, reA);
m_sigs[OP_RE_EMPTY_SET] = alloc(psig, m, "re.empty", 1, 0, 0, reA);
m_sigs[OP_RE_FULL_SET] = alloc(psig, m, "re.all", 1, 0, 0, reA);
m_sigs[OP_RE_OF_PRED] = alloc(psig, m, "re.of.pred", 1, 1, &predA, reA);
@ -574,7 +575,6 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
case OP_RE_STAR:
case OP_RE_OPTION:
case OP_RE_RANGE:
case OP_RE_EMPTY_SET:
case OP_RE_OF_PRED:
case OP_STRING_ITOS:
case OP_STRING_STOI:
@ -587,6 +587,15 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
}
match(*m_sigs[k], arity, domain, range, rng);
return m.mk_func_decl(symbol("re.allchar"), arity, domain, rng, func_decl_info(m_family_id, OP_RE_FULL_SET));
case OP_RE_FULL_SET:
if (!range) range = m_re;
if (range == m_re) {
match(*m_sigs[k], arity, domain, range, rng);
return m.mk_func_decl(symbol("re.allchar"), arity, domain, rng, func_decl_info(m_family_id, k));
}
return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
case _OP_REGEXP_EMPTY:
if (!range) {
range = m_re;
@ -594,6 +603,14 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
match(*m_sigs[k], arity, domain, range, rng);
return m.mk_func_decl(symbol("re.nostr"), arity, domain, rng, func_decl_info(m_family_id, OP_RE_EMPTY_SET));
case OP_RE_EMPTY_SET:
if (!range) range = m_re;
if (range == m_re) {
match(*m_sigs[k], arity, domain, range, rng);
return m.mk_func_decl(symbol("re.nostr"), arity, domain, rng, func_decl_info(m_family_id, k));
}
return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
case OP_RE_LOOP:
switch (arity) {
case 1:
@ -624,6 +641,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
return m.mk_const_decl(m_stringc_sym, m_string,
func_decl_info(m_family_id, OP_STRING_CONST, num_parameters, parameters));
case OP_RE_COMPLEMENT:
case OP_RE_UNION:
case OP_RE_CONCAT:
case OP_RE_INTERSECT:
@ -825,6 +843,15 @@ app* seq_util::re::mk_loop(expr* r, unsigned lo, unsigned hi) {
return m.mk_app(m_fid, OP_RE_LOOP, 2, params, 1, &r);
}
app* seq_util::re::mk_full(sort* s) {
return m.mk_app(m_fid, OP_RE_FULL_SET, 0, 0, 0, 0, s);
}
app* seq_util::re::mk_empty(sort* s) {
return m.mk_app(m_fid, OP_RE_EMPTY_SET, 0, 0, 0, 0, s);
}
bool seq_util::re::is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi) {
if (is_loop(n)) {
app const* a = to_app(n);

6
src/ast/seq_decl_plugin.h
View file

@ -54,6 +54,7 @@ enum seq_op_kind {
OP_RE_UNION,
OP_RE_INTERSECT,
OP_RE_LOOP,
OP_RE_COMPLEMENT,
OP_RE_EMPTY_SET,
OP_RE_FULL_SET,
OP_RE_OF_PRED,
@ -299,16 +300,20 @@ public:
app* mk_concat(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_CONCAT, r1, r2); }
app* mk_union(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_UNION, r1, r2); }
app* mk_inter(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_INTERSECT, r1, r2); }
app* mk_complement(expr* r) { return m.mk_app(m_fid, OP_RE_COMPLEMENT, r); }
app* mk_star(expr* r) { return m.mk_app(m_fid, OP_RE_STAR, r); }
app* mk_plus(expr* r) { return m.mk_app(m_fid, OP_RE_PLUS, r); }
app* mk_opt(expr* r) { return m.mk_app(m_fid, OP_RE_OPTION, r); }
app* mk_loop(expr* r, unsigned lo);
app* mk_loop(expr* r, unsigned lo, unsigned hi);
app* mk_full(sort* s);
app* mk_empty(sort* s);
bool is_to_re(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_TO_RE); }
bool is_concat(expr const* n) const { return is_app_of(n, m_fid, OP_RE_CONCAT); }
bool is_union(expr const* n) const { return is_app_of(n, m_fid, OP_RE_UNION); }
bool is_intersection(expr const* n) const { return is_app_of(n, m_fid, OP_RE_INTERSECT); }
bool is_complement(expr const* n) const { return is_app_of(n, m_fid, OP_RE_COMPLEMENT); }
bool is_star(expr const* n) const { return is_app_of(n, m_fid, OP_RE_STAR); }
bool is_plus(expr const* n) const { return is_app_of(n, m_fid, OP_RE_PLUS); }
bool is_opt(expr const* n) const { return is_app_of(n, m_fid, OP_RE_OPTION); }
@ -321,6 +326,7 @@ public:
MATCH_BINARY(is_union);
MATCH_BINARY(is_intersection);
MATCH_BINARY(is_range);
MATCH_UNARY(is_complement);
MATCH_UNARY(is_star);
MATCH_UNARY(is_plus);
MATCH_UNARY(is_opt);

7
src/util/hwf.cpp
View file

@ -29,7 +29,8 @@ Revision History:
#include<fenv.h>
#endif
#ifndef _M_IA64
#if defined(__x86_64__) || defined(_M_X64) || \
defined(__i386) || defined(_M_IX86)
#define USE_INTRINSICS
#endif
@ -47,7 +48,9 @@ Revision History:
// Luckily, these are kind of standardized, at least for Windows/Linux/OSX.
#ifdef __clang__
#undef USE_INTRINSICS
#else
#endif
#ifdef USE_INTRINSICS
#include <emmintrin.h>
#endif