diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index b0a4def55..a95f1d8b1 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -623,6 +623,100 @@ extern "C" { to_fixedpoint_ref(d)->ctx().add_constraint(to_expr(e), lvl); } -#include "api_datalog_spacer.inc" + Z3_lbool Z3_API Z3_fixedpoint_query_from_lvl (Z3_context c, Z3_fixedpoint d, Z3_ast q, unsigned lvl) { + Z3_TRY; + LOG_Z3_fixedpoint_query_from_lvl (c, d, q, lvl); + RESET_ERROR_CODE(); + lbool r = l_undef; + unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout()); + unsigned rlimit = to_fixedpoint(d)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit()); + { + scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit); + cancel_eh eh(mk_c(c)->m().limit()); + api::context::set_interruptable si(*(mk_c(c)), eh); + scoped_timer timer(timeout, &eh); + try { + r = to_fixedpoint_ref(d)->ctx().query_from_lvl (to_expr(q), lvl); + } + catch (z3_exception& ex) { + mk_c(c)->handle_exception(ex); + r = l_undef; + } + to_fixedpoint_ref(d)->ctx().cleanup(); + } + return of_lbool(r); + Z3_CATCH_RETURN(Z3_L_UNDEF); + } + + Z3_ast Z3_API Z3_fixedpoint_get_ground_sat_answer(Z3_context c, Z3_fixedpoint d) { + Z3_TRY; + LOG_Z3_fixedpoint_get_ground_sat_answer(c, d); + RESET_ERROR_CODE(); + expr* e = to_fixedpoint_ref(d)->ctx().get_ground_sat_answer(); + mk_c(c)->save_ast_trail(e); + RETURN_Z3(of_expr(e)); + Z3_CATCH_RETURN(nullptr); + } + + Z3_ast_vector Z3_API Z3_fixedpoint_get_rules_along_trace( + Z3_context c, + Z3_fixedpoint d) + { + Z3_TRY; + LOG_Z3_fixedpoint_get_rules_along_trace(c, d); + ast_manager& m = mk_c(c)->m(); + Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, *mk_c(c), m); + mk_c(c)->save_object(v); + expr_ref_vector rules(m); + svector names; + + to_fixedpoint_ref(d)->ctx().get_rules_along_trace_as_formulas(rules, names); + for (unsigned i = 0; i < rules.size(); ++i) { + v->m_ast_vector.push_back(rules[i].get()); + } + RETURN_Z3(of_ast_vector(v)); + Z3_CATCH_RETURN(nullptr); + } + + Z3_symbol Z3_API Z3_fixedpoint_get_rule_names_along_trace( + Z3_context c, + Z3_fixedpoint d) + { + Z3_TRY; + LOG_Z3_fixedpoint_get_rule_names_along_trace(c, d); + ast_manager& m = mk_c(c)->m(); + Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, *mk_c(c), m); + mk_c(c)->save_object(v); + expr_ref_vector rules(m); + svector names; + std::stringstream ss; + + to_fixedpoint_ref(d)->ctx().get_rules_along_trace_as_formulas(rules, names); + for (unsigned i = 0; i < names.size(); ++i) { + ss << ";" << names[i].str(); + } + RETURN_Z3(of_symbol(symbol(ss.str().substr(1).c_str()))); + Z3_CATCH_RETURN(nullptr); + } + + void Z3_API Z3_fixedpoint_add_invariant(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred, Z3_ast property) { + Z3_TRY; + LOG_Z3_fixedpoint_add_invariant(c, d, pred, property); + RESET_ERROR_CODE(); + to_fixedpoint_ref(d)->ctx ().add_invariant(to_func_decl(pred), to_expr(property)); + Z3_CATCH; + } + + Z3_ast Z3_API Z3_fixedpoint_get_reachable(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred) { + Z3_TRY; + LOG_Z3_fixedpoint_get_reachable(c, d, pred); + RESET_ERROR_CODE(); + expr_ref r = to_fixedpoint_ref(d)->ctx().get_reachable(to_func_decl(pred)); + mk_c(c)->save_ast_trail(r); + RETURN_Z3(of_expr(r.get())); + Z3_CATCH_RETURN(nullptr); + } + + }; diff --git a/src/api/api_qe.cpp b/src/api/api_qe.cpp index 94e83144f..10ba9faa0 100644 --- a/src/api/api_qe.cpp +++ b/src/api/api_qe.cpp @@ -1,5 +1,5 @@ /*++ -Copyright (c) 2017 Arie Gurfinkel +Copyright (c) Microsoft Corporation, Arive Gurfinkel 2017 Module Name: @@ -70,39 +70,39 @@ extern "C" } Z3_ast Z3_API Z3_qe_model_project_skolem (Z3_context c, - Z3_model m, + Z3_model mdl, unsigned num_bounds, Z3_app const bound[], Z3_ast body, Z3_ast_map map) { Z3_TRY; - LOG_Z3_qe_model_project_skolem (c, m, num_bounds, bound, body, map); + LOG_Z3_qe_model_project_skolem (c, mdl, num_bounds, bound, body, map); RESET_ERROR_CODE(); - ast_manager& man = mk_c(c)->m (); - app_ref_vector vars(man); + ast_manager& m = mk_c(c)->m(); + app_ref_vector vars(m); if (!to_apps(num_bounds, bound, vars)) { RETURN_Z3(nullptr); } - expr_ref result (mk_c(c)->m ()); + expr_ref result (m); result = to_expr (body); - model_ref model (to_model_ref (m)); - expr_map emap (man); + model_ref model (to_model_ref (mdl)); + expr_map emap (m); - spacer::qe_project (mk_c(c)->m (), vars, result, model, emap); - mk_c(c)->save_ast_trail (result.get ()); + spacer::qe_project(m, vars, result, model, emap); + mk_c(c)->save_ast_trail(result); obj_map &map_z3 = to_ast_map_ref(map); - for (expr_map::iterator it = emap.begin(), end = emap.end(); it != end; ++it){ - man.inc_ref(&(it->get_key())); - man.inc_ref(it->get_value()); - map_z3.insert(&(it->get_key()), it->get_value()); + for (auto& kv : emap) { + m.inc_ref(kv.m_key); + m.inc_ref(kv.m_value); + map_z3.insert(kv.m_key, kv.m_value); } - return of_expr (result.get ()); + return of_expr (result); Z3_CATCH_RETURN(nullptr); } @@ -124,9 +124,9 @@ extern "C" expr_ref result (mk_c(c)->m ()); result = mk_and (lits); - mk_c(c)->save_ast_trail (result.get ()); + mk_c(c)->save_ast_trail (result); - return of_expr (result.get ()); + return of_expr (result); Z3_CATCH_RETURN(nullptr); } @@ -138,8 +138,8 @@ extern "C" ast_ref_vector &vVars = to_ast_vector_ref (vars); app_ref_vector vApps (mk_c(c)->m()); - for (unsigned i = 0; i < vVars.size (); ++i) { - app *a = to_app (vVars.get (i)); + for (ast* v : vVars) { + app * a = to_app(v); if (a->get_kind () != AST_APP) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); @@ -162,7 +162,7 @@ extern "C" } } - mk_c(c)->save_ast_trail (result.get ()); + mk_c(c)->save_ast_trail (result); return of_expr (result); Z3_CATCH_RETURN(nullptr); } diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index 2cce53e3a..5e2828adf 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -117,7 +117,7 @@ bool smt_renaming::all_is_legal(char const* s) { } smt_renaming::smt_renaming() { - for (unsigned i = 0; i < ARRAYSIZE(m_predef_names); ++i) { + for (unsigned i = 0; i < Z3_ARRAYSIZE(m_predef_names); ++i) { symbol s(m_predef_names[i]); m_translate.insert(s, sym_b(s, false)); m_rev_translate.insert(s, s); diff --git a/src/ast/format.cpp b/src/ast/format.cpp index 40df437ea..4aeaf183d 100644 --- a/src/ast/format.cpp +++ b/src/ast/format.cpp @@ -152,21 +152,13 @@ namespace format_ns { format * mk_int(ast_manager & m, int i) { char buffer[128]; -#ifdef _WINDOWS - sprintf_s(buffer, ARRAYSIZE(buffer), "%d", i); -#else - sprintf(buffer, "%d", i); -#endif + SPRINTF_D(buffer, i); return mk_string(m, buffer); } format * mk_unsigned(ast_manager & m, unsigned u) { char buffer[128]; -#ifdef _WINDOWS - sprintf_s(buffer, ARRAYSIZE(buffer), "%u", u); -#else - sprintf(buffer, "%u", u); -#endif + SPRINTF_U(buffer, u); return mk_string(m, buffer); } diff --git a/src/ast/proofs/proof_checker.cpp b/src/ast/proofs/proof_checker.cpp index baea760fa..08d69ff25 100644 --- a/src/ast/proofs/proof_checker.cpp +++ b/src/ast/proofs/proof_checker.cpp @@ -1248,7 +1248,7 @@ void proof_checker::dump_proof(proof const* pr) { void proof_checker::dump_proof(unsigned num_antecedents, expr * const * antecedents, expr * consequent) { char buffer[128]; #ifdef _WINDOWS - sprintf_s(buffer, ARRAYSIZE(buffer), "proof_lemma_%d.smt2", m_proof_lemma_id); + sprintf_s(buffer, Z3_ARRAYSIZE(buffer), "proof_lemma_%d.smt2", m_proof_lemma_id); #else sprintf(buffer, "proof_lemma_%d.smt2", m_proof_lemma_id); #endif diff --git a/src/smt/theory_arith_pp.h b/src/smt/theory_arith_pp.h index 59d386292..b6ddaecf8 100644 --- a/src/smt/theory_arith_pp.h +++ b/src/smt/theory_arith_pp.h @@ -544,7 +544,7 @@ namespace smt { char buffer[128]; static int id = 0; #ifdef _WINDOWS - sprintf_s(buffer, ARRAYSIZE(buffer), "arith_%d.smt", id); + sprintf_s(buffer, Z3_ARRAYSIZE(buffer), "arith_%d.smt", id); #else sprintf(buffer, "arith_%d.smt", id); #endif diff --git a/src/test/bit_blaster.cpp b/src/test/bit_blaster.cpp index c6853ae1e..b4c7a8e76 100644 --- a/src/test/bit_blaster.cpp +++ b/src/test/bit_blaster.cpp @@ -27,7 +27,7 @@ void mk_bits(ast_manager & m, char const * prefix, unsigned sz, expr_ref_vector for (unsigned i = 0; i < sz; ++i) { char buffer[128]; #ifdef _WINDOWS - sprintf_s(buffer, ARRAYSIZE(buffer), "%s%d.smt", prefix, i); + sprintf_s(buffer, Z3_ARRAYSIZE(buffer), "%s%d.smt", prefix, i); #else sprintf(buffer, "%s%d.smt", prefix, i); #endif diff --git a/src/test/for_each_file.cpp b/src/test/for_each_file.cpp index eeec69156..7b7a45042 100644 --- a/src/test/for_each_file.cpp +++ b/src/test/for_each_file.cpp @@ -21,6 +21,7 @@ Revision History: #include #include #include +#include "util/util.h" #include "test/for_each_file.h" bool for_each_file(for_each_file_proc& proc, const char* base, const char* suffix) @@ -36,7 +37,7 @@ bool for_each_file(for_each_file_proc& proc, const char* base, const char* suffi while (h != INVALID_HANDLE_VALUE) { - StringCchPrintfA(buffer, ARRAYSIZE(buffer), "%s\\%s", base, data.cFileName); + StringCchPrintfA(buffer, Z3_ARRAYSIZE(buffer), "%s\\%s", base, data.cFileName); if (!proc(buffer)) { return false; diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h index 83e03a2f7..c606824b4 100644 --- a/src/util/stopwatch.h +++ b/src/util/stopwatch.h @@ -23,8 +23,6 @@ Revision History: #if defined(_WINDOWS) || defined(_CYGWIN) // Does this redefinition work? -#define ARRAYSIZE_TEMP ARRAYSIZE -#undef ARRAYSIZE #include @@ -68,8 +66,6 @@ public: } }; -#undef ARRAYSIZE -#define ARRAYSIZE ARRAYSIZE_TEMP #undef max #undef min diff --git a/src/util/string_buffer.h b/src/util/string_buffer.h index 28ce84fc4..db49d4d82 100644 --- a/src/util/string_buffer.h +++ b/src/util/string_buffer.h @@ -43,6 +43,7 @@ class string_buffer { m_capacity = new_capacity; m_buffer = new_buffer; } + static const unsigned c_buffer_size = 24; public: string_buffer(): @@ -80,9 +81,9 @@ public: } void append(int n) { - char buffer[24]; + char buffer[c_buffer_size]; #ifdef _WINDOWS - sprintf_s(buffer, ARRAYSIZE(buffer), "%d", n); + sprintf_s(buffer, c_buffer_size, "%d", n); #else sprintf(buffer, "%d", n); #endif @@ -90,9 +91,9 @@ public: } void append(unsigned n) { - char buffer[24]; + char buffer[c_buffer_size]; #ifdef _WINDOWS - sprintf_s(buffer, ARRAYSIZE(buffer), "%d", n); + sprintf_s(buffer, c_buffer_size, "%d", n); #else sprintf(buffer, "%d", n); #endif @@ -100,9 +101,9 @@ public: } void append(long n) { - char buffer[24]; + char buffer[c_buffer_size]; #ifdef _WINDOWS - sprintf_s(buffer, ARRAYSIZE(buffer), "%ld", n); + sprintf_s(buffer, c_buffer_size, "%ld", n); #else sprintf(buffer, "%ld", n); #endif diff --git a/src/util/util.h b/src/util/util.h index 12fd2fe3b..4ccf76289 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -49,12 +49,18 @@ static_assert(sizeof(int64_t) == 8, "64 bits"); #ifdef _WINDOWS #define SSCANF sscanf_s #define SPRINTF sprintf_s +#define SPRINTF_D(_buffer_, _i_) sprintf_s(_buffer_, Z3_ARRAYSIZE(_buffer_), "%d", _i_) +#define SPRINTF_U(_buffer_, _u_) sprintf_s(_buffer_, Z3_ARRAYSIZE(_buffer_), "%u", _u_) #define _Exit exit #else #define SSCANF sscanf #define SPRINTF sprintf +#define SPRINTF_D(_buffer_, _i_) sprintf(_buffer_, "%d", _i_) +#define SPRINTF_U(_buffer_, _u_) sprintf(_buffer_, "%u", _u_) #endif + + #define VEC2PTR(_x_) ((_x_).size() ? &(_x_)[0] : 0) #ifdef _WINDOWS @@ -142,9 +148,7 @@ static inline uint64_t shift_left(uint64_t x, uint64_t y) { template char (*ArraySizer(T (&)[N]))[N]; // For determining the length of an array. See ARRAYSIZE() macro. This function is never actually called. -#ifndef ARRAYSIZE -#define ARRAYSIZE(a) sizeof(*ArraySizer(a)) -#endif +#define Z3_ARRAYSIZE(a) sizeof(*ArraySizer(a)) template void display(std::ostream & out, const IT & begin, const IT & end, const char * sep, bool & first) {