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

throttle big-reductions #2101 #2098

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-01-24 14:00:56 -08:00
parent 498864c582
commit 8da1d6070b
3 changed files with 21 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/api/c++/z3++.h
View file

@ -518,6 +518,12 @@ namespace z3 {
sort(context & c, Z3_ast a):ast(c, a) {} sort(context & c, Z3_ast a):ast(c, a) {}
sort(sort const & s):ast(s) {} sort(sort const & s):ast(s) {}
operator Z3_sort() const { return reinterpret_cast<Z3_sort>(m_ast); } operator Z3_sort() const { return reinterpret_cast<Z3_sort>(m_ast); }
/**
\brief retrieve unique identifier for func_decl.
*/
unsigned id() const { unsigned r = Z3_get_sort_id(ctx(), *this); check_error(); return r; }
/** /**
\brief Return true if this sort and \c s are equal. \brief Return true if this sort and \c s are equal.
*/ */
@ -615,6 +621,11 @@ namespace z3 {
operator Z3_func_decl() const { return reinterpret_cast<Z3_func_decl>(m_ast); } operator Z3_func_decl() const { return reinterpret_cast<Z3_func_decl>(m_ast); }
func_decl & operator=(func_decl const & s) { return static_cast<func_decl&>(ast::operator=(s)); } func_decl & operator=(func_decl const & s) { return static_cast<func_decl&>(ast::operator=(s)); }
/**
\brief retrieve unique identifier for func_decl.
*/
unsigned id() const { unsigned r = Z3_get_func_decl_id(ctx(), *this); check_error(); return r; }
unsigned arity() const { return Z3_get_arity(ctx(), *this); } unsigned arity() const { return Z3_get_arity(ctx(), *this); }
sort domain(unsigned i) const { assert(i < arity()); Z3_sort r = Z3_get_domain(ctx(), *this, i); check_error(); return sort(ctx(), r); } sort domain(unsigned i) const { assert(i < arity()); Z3_sort r = Z3_get_domain(ctx(), *this, i); check_error(); return sort(ctx(), r); }
sort range() const { Z3_sort r = Z3_get_range(ctx(), *this); check_error(); return sort(ctx(), r); } sort range() const { Z3_sort r = Z3_get_range(ctx(), *this); check_error(); return sort(ctx(), r); }
@ -771,6 +782,11 @@ namespace z3 {
return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision)); return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision));
} }
/**
\brief retrieve unique identifier for expression.
*/
unsigned id() const { unsigned r = Z3_get_ast_id(ctx(), m_ast); check_error(); return r; }
/** /**
\brief Return int value of numeral, throw if result cannot fit in \brief Return int value of numeral, throw if result cannot fit in
machine int machine int

2
src/sat/sat_big.cpp
View file

@ -172,6 +172,7 @@ namespace sat {
void big::add_del(literal u, literal v) { void big::add_del(literal u, literal v) {
if (u.index() > v.index()) std::swap(u, v); if (u.index() > v.index()) std::swap(u, v);
m_del_bin[u.index()].push_back(v); m_del_bin[u.index()].push_back(v);
} }
@ -210,7 +211,6 @@ namespace sat {
} }
wlist.set_end(itprev); wlist.set_end(itprev);
} }
s.propagate(false); s.propagate(false);
return elim; return elim;
} }

8
src/sat/sat_scc.cpp
View file

@ -244,10 +244,10 @@ namespace sat {
} }
void scc::reduce_tr() { void scc::reduce_tr() {
unsigned quota = 0, num_reduced = 0; unsigned quota = 0, num_reduced = 0, count = 0;
while ((num_reduced = reduce_tr(false)) > quota) { quota = std::max(100u, num_reduced / 2); } while ((num_reduced = reduce_tr(false)) > quota && count++ < 10) { quota = std::max(100u, num_reduced / 2); }
quota = 0; quota = 0; count = 0;
while ((num_reduced = reduce_tr(true)) > quota) { quota = std::max(100u, num_reduced / 2); } while ((num_reduced = reduce_tr(true)) > quota && count++ < 10) { quota = std::max(100u, num_reduced / 2); }
} }
void scc::collect_statistics(statistics & st) const { void scc::collect_statistics(statistics & st) const {