3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00

Fixes for the build on OS X 10.9

This commit is contained in:
Christoph M. Wintersteiger 2014-01-28 14:00:42 +00:00
parent 0e74362ecb
commit f111dd4e61
5 changed files with 10 additions and 8 deletions

View file

@ -17,6 +17,7 @@ Revision History:
--*/ --*/
#include<iostream> #include<iostream>
#include<sstream> #include<sstream>
#include<vector>
#include"z3.h" #include"z3.h"
#include"api_log_macros.h" #include"api_log_macros.h"
#include"api_context.h" #include"api_context.h"

View file

@ -66,7 +66,7 @@ Revision History:
namespace stl_ext { namespace stl_ext {
template <> template <>
class hash<std::string> { class hash<std::string> {
stl_ext::hash<char *> H; stl_ext::hash<const char *> H;
public: public:
size_t operator()(const std::string &s) const { size_t operator()(const std::string &s) const {
return H(s.c_str()); return H(s.c_str());

View file

@ -172,7 +172,7 @@ iz3mgr::ast iz3mgr::make_quant(opr op, const std::vector<ast> &bvs, ast &body){
std::vector<symbol> names; std::vector<symbol> names;
std::vector<sort *> types; std::vector<class sort *> types;
std::vector<expr *> bound_asts; std::vector<expr *> bound_asts;
unsigned num_bound = bvs.size(); unsigned num_bound = bvs.size();
@ -485,7 +485,7 @@ void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector<ast>& coeffs){
get_farkas_coeffs(proof,rats); get_farkas_coeffs(proof,rats);
coeffs.resize(rats.size()); coeffs.resize(rats.size());
for(unsigned i = 0; i < rats.size(); i++){ for(unsigned i = 0; i < rats.size(); i++){
sort *is = m().mk_sort(m_arith_fid, INT_SORT); class sort *is = m().mk_sort(m_arith_fid, INT_SORT);
ast coeff = cook(m_arith_util.mk_numeral(rats[i],is)); ast coeff = cook(m_arith_util.mk_numeral(rats[i],is));
coeffs[i] = coeff; coeffs[i] = coeff;
} }

View file

@ -22,6 +22,7 @@ Revision History:
#include <assert.h> #include <assert.h>
#include <vector>
#include "iz3hash.h" #include "iz3hash.h"
#include"well_sorted.h" #include"well_sorted.h"

View file

@ -58,20 +58,20 @@ namespace stl_ext {
class free_func_visitor { class free_func_visitor {
ast_manager& m; ast_manager& m;
func_decl_set m_funcs; func_decl_set m_funcs;
obj_hashtable<sort> m_sorts; obj_hashtable<class sort> m_sorts;
public: public:
free_func_visitor(ast_manager& m): m(m) {} free_func_visitor(ast_manager& m): m(m) {}
void operator()(var * n) { } void operator()(var * n) { }
void operator()(app * n) { void operator()(app * n) {
m_funcs.insert(n->get_decl()); m_funcs.insert(n->get_decl());
sort* s = m.get_sort(n); class sort* s = m.get_sort(n);
if (s->get_family_id() == null_family_id) { if (s->get_family_id() == null_family_id) {
m_sorts.insert(s); m_sorts.insert(s);
} }
} }
void operator()(quantifier * n) { } void operator()(quantifier * n) { }
func_decl_set& funcs() { return m_funcs; } func_decl_set& funcs() { return m_funcs; }
obj_hashtable<sort>& sorts() { return m_sorts; } obj_hashtable<class sort>& sorts() { return m_sorts; }
}; };
class iz3pp_helper : public iz3mgr { class iz3pp_helper : public iz3mgr {
@ -146,8 +146,8 @@ void iz3pp(ast_manager &m,
func_decl_set &funcs = visitor.funcs(); func_decl_set &funcs = visitor.funcs();
func_decl_set::iterator it = funcs.begin(), end = funcs.end(); func_decl_set::iterator it = funcs.begin(), end = funcs.end();
obj_hashtable<sort>& sorts = visitor.sorts(); obj_hashtable<class sort>& sorts = visitor.sorts();
obj_hashtable<sort>::iterator sit = sorts.begin(), send = sorts.end(); obj_hashtable<class sort>::iterator sit = sorts.begin(), send = sorts.end();