mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

move from uint_set to hashtable over unsigned to save memory overhead in consequence generation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-09-08 13:34:59 -07:00
parent 94b67412ec
commit 76cf28d48b
3 changed files with 21 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/smt/smt_consequences.cpp
View file

@ -23,9 +23,9 @@ Revision History:
namespace smt {
expr_ref context::antecedent2fml(uint_set const& vars) {
expr_ref context::antecedent2fml(index_set const& vars) {
expr_ref_vector premises(m_manager);
uint_set::iterator it = vars.begin(), end = vars.end();
index_set::iterator it = vars.begin(), end = vars.end();
for (; it != end; ++it) {
expr* e = bool_var2expr(*it);
premises.push_back(get_assignment(*it) != l_false ? e : m_manager.mk_not(e));
@ -42,14 +42,14 @@ namespace smt {
// - e is an equality between a variable and value that is to be fixed.
// - e is a data-type recognizer of a variable that is to be fixed.
//
void context::extract_fixed_consequences(literal lit, obj_map<expr, expr*>& vars, uint_set const& assumptions, expr_ref_vector& conseq) {
void context::extract_fixed_consequences(literal lit, obj_map<expr, expr*>& vars, index_set const& assumptions, expr_ref_vector& conseq) {
ast_manager& m = m_manager;
datatype_util dt(m);
expr* e1, *e2;
expr_ref fml(m);
if (lit == true_literal) return;
expr* e = bool_var2expr(lit.var());
uint_set s;
index_set s;
if (assumptions.contains(lit.var())) {
s.insert(lit.var());
}
@ -86,7 +86,11 @@ namespace smt {
}
}
m_antecedents.insert(lit.var(), s);
TRACE("context", display_literal_verbose(tout, lit); tout << " " << s << "\n";);
TRACE("context", display_literal_verbose(tout, lit);
for (index_set::iterator it = s.begin(), end = s.end(); it != end; ++it) {
tout << " " << *it;
}
tout << "\n";);
bool found = false;
if (vars.contains(e)) {
found = true;
@ -116,7 +120,7 @@ namespace smt {
}
}
void context::extract_fixed_consequences(unsigned& start, obj_map<expr, expr*>& vars, uint_set const& assumptions, expr_ref_vector& conseq) {
void context::extract_fixed_consequences(unsigned& start, obj_map<expr, expr*>& vars, index_set const& assumptions, expr_ref_vector& conseq) {
pop_to_search_lvl();
SASSERT(!inconsistent());
literal_vector const& lits = assigned_literals();
@ -204,7 +208,7 @@ namespace smt {
if (!m.is_bool(k) && are_equal(k, v)) {
literal_vector literals;
m_conflict_resolution->eq2literals(get_enode(v), get_enode(k), literals);
uint_set s;
index_set s;
for (unsigned i = 0; i < literals.size(); ++i) {
SASSERT(get_assign_level(literals[i]) <= get_search_level());
s |= m_antecedents.find(literals[i].var());
@ -254,7 +258,7 @@ namespace smt {
return is_sat;
}
obj_map<expr, expr*> var2val;
uint_set _assumptions;
index_set _assumptions;
for (unsigned i = 0; i < assumptions.size(); ++i) {
_assumptions.insert(get_literal(assumptions[i]).var());
}
@ -440,7 +444,7 @@ namespace smt {
return is_sat;
}
obj_map<expr, expr*> var2val;
uint_set _assumptions;
index_set _assumptions;
for (unsigned i = 0; i < assumptions.size(); ++i) {
_assumptions.insert(get_literal(assumptions[i]).var());
}

12
src/smt/smt_context.h
View file

@ -1343,10 +1343,12 @@ namespace smt {
static literal translate_literal(
literal lit, context& src_ctx, context& dst_ctx,
vector<bool_var> b2v, ast_translation& tr);
u_map<uint_set> m_antecedents;
void extract_fixed_consequences(literal lit, obj_map<expr, expr*>& var2val, uint_set const& assumptions, expr_ref_vector& conseq);
void extract_fixed_consequences(unsigned& idx, obj_map<expr, expr*>& var2val, uint_set const& assumptions, expr_ref_vector& conseq);
typedef hashtable<unsigned, u_hash, u_eq> index_set;
//typedef uint_set index_set;
u_map<index_set> m_antecedents;
void extract_fixed_consequences(literal lit, obj_map<expr, expr*>& var2val, index_set const& assumptions, expr_ref_vector& conseq);
void extract_fixed_consequences(unsigned& idx, obj_map<expr, expr*>& var2val, index_set const& assumptions, expr_ref_vector& conseq);
void display_consequence_progress(std::ostream& out, unsigned it, unsigned nv, unsigned fixed, unsigned unfixed, unsigned eq);
@ -1354,7 +1356,7 @@ namespace smt {
unsigned extract_fixed_eqs(obj_map<expr, expr*>& var2val, expr_ref_vector& conseq);
expr_ref antecedent2fml(uint_set const& ante);
expr_ref antecedent2fml(index_set const& ante);
literal mk_diseq(expr* v, expr* val);

3
src/util/hashtable.h
View file

@ -558,14 +558,13 @@ public:
core_hashtable& operator|=(core_hashtable const& other) {
if (this == &other) return *this;
iterator i = begin(), e = end();
iterator i = other.begin(), e = other.end();
for (; i != e; ++i) {
insert(*i);
}
return *this;
}
core_hashtable& operator&=(core_hashtable const& other) {
if (this == &other) return *this;
core_hashtable copy(*this);