mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 20:33:38 +00:00
Code Activity

porting to windows

Browse source
This commit is contained in:
U-REDMOND\kenmcmil 2013-03-28 11:18:20 -07:00
parent 28266786f3
commit 7a0d49cb32
4 changed files with 8 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/api/z3_api.h
View file

@ -7788,7 +7788,7 @@ END_MLAPI_EXCLUDE
def_API('Z3_interpolation_profile', STRING, (_in(CONTEXT),)) def_API('Z3_interpolation_profile', STRING, (_in(CONTEXT),))
*/ */
Z3_string Z3_API Z3_interpolation_profile(Z3_context ctx); Z3_string Z3_API Z3_interpolation_profile(__in Z3_context ctx);
/** /**
\brief Read an interpolation problem from file. \brief Read an interpolation problem from file.
@ -7824,8 +7824,7 @@ END_MLAPI_EXCLUDE
*/ */
int Z3_API int Z3_API Z3_read_interpolation_problem(__in Z3_context ctx,
Z3_read_interpolation_problem(__in Z3_context ctx,
__out int *num, __out int *num,
__out_ecount(*num) Z3_ast **cnsts, __out_ecount(*num) Z3_ast **cnsts,
__out_ecount(*num) int **parents, __out_ecount(*num) int **parents,
@ -7853,8 +7852,7 @@ END_MLAPI_EXCLUDE
*/ */
int Z3_API int Z3_API Z3_check_interpolant(Z3_context ctx, int num, Z3_ast *cnsts, int *parents, Z3_ast *interps, const char **error,
Z3_check_interpolant(Z3_context ctx, int num, Z3_ast *cnsts, int *parents, Z3_ast *interps, const char **error,
int num_theory, Z3_ast *theory); int num_theory, Z3_ast *theory);
/** Write an interpolation problem to file suitable for reading with /** Write an interpolation problem to file suitable for reading with
@ -7870,8 +7868,7 @@ END_MLAPI_EXCLUDE
*/ */
void Z3_API void Z3_API Z3_write_interpolation_problem(Z3_context ctx,
Z3_write_interpolation_problem(Z3_context ctx,
int num, int num,
Z3_ast *cnsts, Z3_ast *cnsts,
int *parents, int *parents,

2
src/interp/iz3base.cpp
View file

@ -247,7 +247,7 @@ bool iz3base::is_sat(ast f){
} }
void iz3base::find_children(const hash_set<ast> &cnsts_set, void iz3base::find_children(const stl_ext::hash_set<ast> &cnsts_set,
const ast &tree, const ast &tree,
std::vector<ast> &cnsts, std::vector<ast> &cnsts,
std::vector<int> &parents, std::vector<int> &parents,

2
src/interp/iz3base.h
View file

@ -145,7 +145,7 @@ class iz3base : public iz3mgr, public scopes {
ast simplify_and(std::vector<ast> &conjuncts); ast simplify_and(std::vector<ast> &conjuncts);
ast simplify_with_lit_rec(ast n, ast lit, stl_ext::hash_map<ast,ast> &memo, int depth); ast simplify_with_lit_rec(ast n, ast lit, stl_ext::hash_map<ast,ast> &memo, int depth);
ast simplify_with_lit(ast n, ast lit); ast simplify_with_lit(ast n, ast lit);
void find_children(const hash_set<ast> &cnsts_set, void find_children(const stl_ext::hash_set<ast> &cnsts_set,
const ast &tree, const ast &tree,
std::vector<ast> &cnsts, std::vector<ast> &cnsts,
std::vector<int> &parents, std::vector<int> &parents,

3
src/interp/iz3foci.cpp
View file

@ -307,7 +307,8 @@ public:
int interpolate(const std::vector<ast> &cnsts, std::vector<ast> &itps){ int interpolate(const std::vector<ast> &cnsts, std::vector<ast> &itps){
assert((int)cnsts.size() == frames); assert((int)cnsts.size() == frames);
foci = foci2::create("lia"); std::string lia("lia");
foci = foci2::create(lia);
if(!foci){ if(!foci){
std::cerr << "iZ3: cannot find foci lia solver.\n"; std::cerr << "iZ3: cannot find foci lia solver.\n";
assert(0); assert(0);