mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fixed some address dependencies
This commit is contained in:
parent
bb61f17989
commit
3764064e98
|
@ -3161,3 +3161,6 @@ void prexpr(expr_ref &e){
|
|||
std::cout << mk_pp(e.get(), e.get_manager()) << std::endl;
|
||||
}
|
||||
|
||||
void ast_manager::show_id_gen(){
|
||||
std::cout << "id_gen: " << m_expr_id_gen.show_hash() << " " << m_decl_id_gen.show_hash() << "\n";
|
||||
}
|
||||
|
|
|
@ -1418,6 +1418,8 @@ protected:
|
|||
public:
|
||||
typedef expr_dependency_array_manager::ref expr_dependency_array;
|
||||
|
||||
void show_id_gen();
|
||||
|
||||
protected:
|
||||
small_object_allocator m_alloc;
|
||||
family_manager m_family_manager;
|
||||
|
|
|
@ -513,7 +513,6 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
|
|||
opts.set("weak","1");
|
||||
|
||||
::ast *proof = m_solver->get_proof();
|
||||
show_assertion_ids();
|
||||
iz3interpolate(m(),proof,_assumptions,_parents,_interpolants,_theory,&opts);
|
||||
|
||||
std::vector<expr> linearized_interpolants(_interpolants.size());
|
||||
|
@ -604,6 +603,14 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
|
|||
std::cout << std::endl;
|
||||
}
|
||||
|
||||
void model::show_hash() const {
|
||||
std::ostringstream ss;
|
||||
model_smt2_pp(ss, m(), *m_model, 0);
|
||||
std::hash<std::string> hasher;
|
||||
unsigned h = hasher(ss.str());
|
||||
std::cout << "model hash: " << h << "\n";
|
||||
}
|
||||
|
||||
void solver::show() {
|
||||
unsigned n = m_solver->get_num_assertions();
|
||||
if(!n)
|
||||
|
@ -615,11 +622,20 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
|
|||
}
|
||||
|
||||
void solver::show_assertion_ids() {
|
||||
#if 0
|
||||
unsigned n = m_solver->get_num_assertions();
|
||||
std::cerr << "assertion ids: ";
|
||||
for (unsigned i = 0; i < n-1; ++i)
|
||||
std::cerr << " " << m_solver->get_assertion(i)->get_id();
|
||||
std::cerr << "\n";
|
||||
#else
|
||||
unsigned n = m_solver->get_num_assertions();
|
||||
std::cerr << "assertion ids hash: ";
|
||||
unsigned h = 0;
|
||||
for (unsigned i = 0; i < n-1; ++i)
|
||||
h += m_solver->get_assertion(i)->get_id();
|
||||
std::cerr << h << "\n";
|
||||
#endif
|
||||
}
|
||||
|
||||
void include_ast_show(ast &a){
|
||||
|
|
|
@ -727,6 +727,7 @@ namespace Duality {
|
|||
}
|
||||
|
||||
void show() const;
|
||||
void show_hash() const;
|
||||
|
||||
unsigned num_consts() const {return m_model.get()->get_num_constants();}
|
||||
unsigned num_funcs() const {return m_model.get()->get_num_functions();}
|
||||
|
@ -1386,7 +1387,8 @@ namespace std {
|
|||
class less<Duality::ast> {
|
||||
public:
|
||||
bool operator()(const Duality::ast &s, const Duality::ast &t) const {
|
||||
return s.raw() < t.raw(); // s.raw()->get_id() < t.raw()->get_id();
|
||||
// return s.raw() < t.raw();
|
||||
return s.raw()->get_id() < t.raw()->get_id();
|
||||
}
|
||||
};
|
||||
}
|
||||
|
|
|
@ -213,6 +213,7 @@ public:
|
|||
test_secondary(cnsts,parents,interps);
|
||||
return;
|
||||
#endif
|
||||
|
||||
profiling::timer_start("Interpolation prep");
|
||||
|
||||
// get rid of frames not used in proof
|
||||
|
|
|
@ -140,7 +140,8 @@ namespace std {
|
|||
class less<ast_r> {
|
||||
public:
|
||||
bool operator()(const ast_r &s, const ast_r &t) const {
|
||||
return s.raw() < t.raw(); // s.raw()->get_id() < t.raw()->get_id();
|
||||
// return s.raw() < t.raw();
|
||||
return s.raw()->get_id() < t.raw()->get_id();
|
||||
}
|
||||
};
|
||||
}
|
||||
|
|
|
@ -57,6 +57,11 @@ public:
|
|||
m_free_ids.finalize();
|
||||
}
|
||||
|
||||
unsigned show_hash(){
|
||||
unsigned h = string_hash((char *)&m_free_ids[0],m_free_ids.size()*sizeof(unsigned),17);
|
||||
return hash_u_u(h,m_next_id);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Return N if the range of ids generated by this module is in the set [0..N)
|
||||
*/
|
||||
|
|
Loading…
Reference in a new issue