mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3
This commit is contained in:
commit
46df31babf
|
@ -1168,7 +1168,8 @@ class ExeComponent(Component):
|
|||
c_dep = get_component(dep)
|
||||
out.write(' ' + c_dep.get_link_name())
|
||||
out.write('\n')
|
||||
out.write('\t$(LINK) $(LINK_OUT_FLAG)%s $(LINK_FLAGS)' % exefile)
|
||||
extra_opt = '-static' if not IS_WINDOWS and STATIC_BIN else ''
|
||||
out.write('\t$(LINK) %s $(LINK_OUT_FLAG)%s $(LINK_FLAGS)' % (extra_opt, exefile))
|
||||
for obj in objs:
|
||||
out.write(' ')
|
||||
out.write(obj)
|
||||
|
@ -1972,7 +1973,7 @@ class MLComponent(Component):
|
|||
z3mls = os.path.join(self.sub_dir, 'z3ml')
|
||||
out.write('%s.cma: %s %s %s\n' % (z3mls, cmos, stubso, z3dllso))
|
||||
out.write('\t%s -o %s -I %s %s %s %s\n' % (OCAMLMKLIB, z3mls, self.sub_dir, stubso, cmos, LIBZ3))
|
||||
out.write('%s.cmxa: %s %s %s\n' % (z3mls, cmxs, stubso, z3dllso))
|
||||
out.write('%s.cmxa: %s %s %s %s.cma\n' % (z3mls, cmxs, stubso, z3dllso, z3mls))
|
||||
out.write('\t%s -o %s -I %s %s %s %s\n' % (OCAMLMKLIB, z3mls, self.sub_dir, stubso, cmxs, LIBZ3))
|
||||
out.write('%s.cmxs: %s.cmxa\n' % (z3mls, z3mls))
|
||||
out.write('\t%s -shared -o %s.cmxs -I %s %s.cmxa\n' % (OCAMLOPTF, z3mls, self.sub_dir, z3mls))
|
||||
|
@ -2506,10 +2507,7 @@ def mk_config():
|
|||
config.write('AR_OUTFLAG=\n')
|
||||
config.write('EXE_EXT=\n')
|
||||
config.write('LINK=%s\n' % CXX)
|
||||
if STATIC_BIN:
|
||||
config.write('LINK_FLAGS=-static\n')
|
||||
else:
|
||||
config.write('LINK_FLAGS=\n')
|
||||
config.write('LINK_FLAGS=\n')
|
||||
config.write('LINK_OUT_FLAG=-o \n')
|
||||
config.write('LINK_EXTRA_FLAGS=-lpthread %s\n' % LDFLAGS)
|
||||
config.write('SO_EXT=%s\n' % SO_EXT)
|
||||
|
|
|
@ -1611,7 +1611,7 @@ _lib = None
|
|||
def lib():
|
||||
global _lib
|
||||
if _lib is None:
|
||||
_dirs = ['.', pkg_resources.resource_filename('z3', 'lib'), os.path.join(sys.prefix, 'lib'), None]
|
||||
_dirs = ['.', os.path.dirname(os.path.abspath(__file__)), pkg_resources.resource_filename('z3', 'lib'), os.path.join(sys.prefix, 'lib'), None]
|
||||
for _dir in _dirs:
|
||||
try:
|
||||
init(_dir)
|
||||
|
|
|
@ -312,11 +312,11 @@ void bv2fpa_converter::convert_consts(model_core * mc, model_core * target_model
|
|||
unsigned sbits = m_fpa_util.get_sbits(var->get_range());
|
||||
|
||||
app * a0 = to_app(val->get_arg(0));
|
||||
app * a1 = to_app(val->get_arg(1));
|
||||
app * a2 = to_app(val->get_arg(2));
|
||||
|
||||
expr_ref v0(m), v1(m), v2(m);
|
||||
#ifdef Z3DEBUG
|
||||
app * a1 = to_app(val->get_arg(1));
|
||||
app * a2 = to_app(val->get_arg(2));
|
||||
v0 = mc->get_const_interp(a0->get_decl());
|
||||
v1 = mc->get_const_interp(a1->get_decl());
|
||||
v2 = mc->get_const_interp(a2->get_decl());
|
||||
|
@ -555,4 +555,4 @@ void bv2fpa_converter::convert(model_core * mc, model_core * float_mdl) {
|
|||
tout << "else " << mk_ismt2_pp(fi->get_else(), m) << std::endl;
|
||||
});
|
||||
|
||||
}
|
||||
}
|
||||
|
|
|
@ -474,13 +474,15 @@ void pattern_inference::reset_pre_patterns() {
|
|||
m_pre_patterns.reset();
|
||||
}
|
||||
|
||||
|
||||
#ifdef _TRACE
|
||||
static void dump_app_vector(std::ostream & out, ptr_vector<app> const & v, ast_manager & m) {
|
||||
ptr_vector<app>::const_iterator it = v.begin();
|
||||
ptr_vector<app>::const_iterator end = v.end();
|
||||
for (; it != end; ++it)
|
||||
out << mk_pp(*it, m) << "\n";
|
||||
}
|
||||
#endif
|
||||
|
||||
bool pattern_inference::is_forbidden(app * n) const {
|
||||
func_decl const * decl = n->get_decl();
|
||||
if (is_ground(n))
|
||||
|
|
|
@ -24,9 +24,8 @@ bv_bounds::~bv_bounds() {
|
|||
bv_bounds::conv_res bv_bounds::record(app * v, numeral lo, numeral hi, bool negated, vector<ninterval>& nis) {
|
||||
TRACE("bv_bounds", tout << "record0 " << mk_ismt2_pp(v, m_m) << ":" << (negated ? "~[" : "[") << lo << ";" << hi << "]" << std::endl;);
|
||||
const unsigned bv_sz = m_bv_util.get_bv_size(v);
|
||||
const numeral& zero = numeral::zero();
|
||||
const numeral& one = numeral::one();
|
||||
SASSERT(zero <= lo);
|
||||
SASSERT(numeral::zero() <= lo);
|
||||
SASSERT(lo <= hi);
|
||||
SASSERT(hi < numeral::power_of_two(bv_sz));
|
||||
numeral vmax, vmin;
|
||||
|
@ -49,7 +48,7 @@ bv_bounds::conv_res bv_bounds::record(app * v, numeral lo, numeral hi, bool nega
|
|||
hi_max = hi >= vmax;
|
||||
lo_min = true;
|
||||
}
|
||||
SASSERT(zero <= lo);
|
||||
SASSERT(lo.is_nonneg());
|
||||
SASSERT(lo <= hi);
|
||||
SASSERT(hi < numeral::power_of_two(bv_sz));
|
||||
}
|
||||
|
|
|
@ -650,10 +650,12 @@ void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) {
|
|||
#define Grey 1
|
||||
#define Black 2
|
||||
|
||||
#ifdef Z3DEBUG
|
||||
static int get_color(obj_map<expr, int> & colors, expr * n) {
|
||||
obj_map<expr, int>::obj_map_entry * entry = colors.insert_if_not_there2(n, White);
|
||||
return entry->get_data().m_value;
|
||||
}
|
||||
#endif
|
||||
|
||||
static bool visit_ac_children(func_decl * f, expr * n, obj_map<expr, int> & colors, ptr_buffer<expr> & todo, ptr_buffer<expr> & result) {
|
||||
if (is_app_of(n, f)) {
|
||||
|
|
|
@ -366,6 +366,7 @@ public:
|
|||
app * a = to_app(s);
|
||||
func_decl * sym = a->get_decl();
|
||||
if(!m_parent.has_index(sym, m_from_idx)) {
|
||||
(void) m_homogenous;
|
||||
SASSERT(!m_homogenous || !m_parent.is_muxed(sym));
|
||||
return false;
|
||||
}
|
||||
|
|
|
@ -88,7 +88,7 @@ namespace datalog {
|
|||
svector<bool> m_can_remove, m_can_expand;
|
||||
obj_map<expr, unsigned_vector> m_positions;
|
||||
public:
|
||||
visitor(context& c, substitution & s): st_visitor(s), m_context(c) {}
|
||||
visitor(context& c, substitution & s): st_visitor(s), m_context(c) { (void) m_context; }
|
||||
virtual bool operator()(expr* e);
|
||||
void reset() { m_unifiers.reset(); }
|
||||
void reset(unsigned sz);
|
||||
|
|
|
@ -2183,7 +2183,7 @@ namespace smt2 {
|
|||
SASSERT(curr_id() == m_check_sat_assuming);
|
||||
next();
|
||||
unsigned spos = expr_stack().size();
|
||||
check_rparen_next("invalid check-sat-assuming command, '(', expected");
|
||||
check_lparen_next("invalid check-sat-assuming command, '(', expected");
|
||||
parse_assumptions();
|
||||
check_rparen_next("invalid check-sat-assuming command, ')', expected");
|
||||
m_ctx.check_sat(expr_stack().size() - spos, expr_stack().c_ptr() + spos);
|
||||
|
|
|
@ -96,8 +96,8 @@ namespace sat {
|
|||
}
|
||||
|
||||
// the first two literals must be watched.
|
||||
SASSERT(contains_watched(s.get_wlist(~c[0]), c, s.get_offset(c)));
|
||||
SASSERT(contains_watched(s.get_wlist(~c[1]), c, s.get_offset(c)));
|
||||
VERIFY(contains_watched(s.get_wlist(~c[0]), c, s.get_offset(c)));
|
||||
VERIFY(contains_watched(s.get_wlist(~c[1]), c, s.get_offset(c)));
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
|
|
@ -113,6 +113,8 @@ unsigned arith_eq_solver::find_abs_min(vector<numeral>& values) {
|
|||
return index;
|
||||
}
|
||||
|
||||
#ifdef _TRACE
|
||||
|
||||
static void print_row(std::ostream& out, vector<rational> const& row) {
|
||||
for(unsigned i = 0; i < row.size(); ++i) {
|
||||
out << row[i] << " ";
|
||||
|
@ -125,6 +127,7 @@ static void print_rows(std::ostream& out, vector<vector<rational> > const& rows)
|
|||
print_row(out, rows[i]);
|
||||
}
|
||||
}
|
||||
#endif
|
||||
|
||||
//
|
||||
// The gcd of the coefficients to variables have to divide the
|
||||
|
|
|
@ -490,6 +490,7 @@ namespace smt {
|
|||
#ifdef _PROFILE_MAM
|
||||
m_counter = 0;
|
||||
#endif
|
||||
(void)m_lbl_hasher;
|
||||
}
|
||||
|
||||
#ifdef _PROFILE_MAM
|
||||
|
@ -2881,6 +2882,7 @@ namespace smt {
|
|||
- first_idx: index to be used as head of the multi-pattern mp
|
||||
*/
|
||||
void add_pattern(quantifier * qa, app * mp, unsigned first_idx) {
|
||||
(void)m_ast_manager;
|
||||
SASSERT(m_ast_manager.is_pattern(mp));
|
||||
SASSERT(first_idx < mp->get_num_args());
|
||||
app * p = to_app(mp->get_arg(first_idx));
|
||||
|
|
|
@ -566,8 +566,7 @@ namespace smt {
|
|||
TRACE("context", tout << "checking: " << mk_pp(conseq[i], m) << "\n";);
|
||||
tmp = m.mk_not(conseq[i]);
|
||||
assert_expr(tmp);
|
||||
lbool is_sat = check();
|
||||
SASSERT(is_sat != l_true);
|
||||
VERIFY(check() != l_true);
|
||||
pop(1);
|
||||
}
|
||||
model_ref mdl;
|
||||
|
|
|
@ -335,23 +335,6 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
static bool find_arg(app * n, expr * t, expr * & other) {
|
||||
SASSERT(n->get_num_args() == 2);
|
||||
if (n->get_arg(0) == t) {
|
||||
other = n->get_arg(1);
|
||||
return true;
|
||||
}
|
||||
else if (n->get_arg(1) == t) {
|
||||
other = n->get_arg(0);
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
static bool check_args(app * n, expr * t1, expr * t2) {
|
||||
SASSERT(n->get_num_args() == 2);
|
||||
return (n->get_arg(0) == t1 && n->get_arg(1) == t2) || (n->get_arg(1) == t1 && n->get_arg(0) == t2);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Internalize the given formula into the logical context.
|
||||
|
|
|
@ -120,7 +120,7 @@ namespace smt {
|
|||
|
||||
public:
|
||||
fpa_rm_value_proc(theory_fpa * th) :
|
||||
m_th(*th), m(th->get_manager()), m_fu(th->m_fpa_util), m_bu(th->m_bv_util) {}
|
||||
m_th(*th), m(th->get_manager()), m_fu(th->m_fpa_util), m_bu(th->m_bv_util) { (void) m_th; }
|
||||
|
||||
void add_dependency(enode * e) { m_deps.push_back(model_value_dependency(e)); }
|
||||
|
||||
|
|
|
@ -527,7 +527,8 @@ namespace smt {
|
|||
c->m_compilation_threshold = UINT_MAX;
|
||||
}
|
||||
init_watch_var(*c);
|
||||
m_ineqs.insert(abv, c);
|
||||
init_watch(abv);
|
||||
m_var_infos[abv].m_ineq = c;
|
||||
m_ineqs_trail.push_back(abv);
|
||||
|
||||
if (m_enable_simplex) {
|
||||
|
@ -687,35 +688,43 @@ namespace smt {
|
|||
watch_literal(lit, &c);
|
||||
}
|
||||
|
||||
void theory_pb::init_watch(bool_var v) {
|
||||
if (m_var_infos.size() <= static_cast<unsigned>(v)) {
|
||||
m_var_infos.resize(static_cast<unsigned>(v)+100);
|
||||
}
|
||||
}
|
||||
|
||||
void theory_pb::watch_literal(literal lit, ineq* c) {
|
||||
ptr_vector<ineq>* ineqs;
|
||||
if (!m_lwatch.find(lit.index(), ineqs)) {
|
||||
init_watch(lit.var());
|
||||
ptr_vector<ineq>* ineqs = m_var_infos[lit.var()].m_lit_watch[lit.sign()];
|
||||
if (ineqs == 0) {
|
||||
ineqs = alloc(ptr_vector<ineq>);
|
||||
m_lwatch.insert(lit.index(), ineqs);
|
||||
m_var_infos[lit.var()].m_lit_watch[lit.sign()] = ineqs;
|
||||
}
|
||||
ineqs->push_back(c);
|
||||
}
|
||||
|
||||
void theory_pb::watch_var(bool_var v, ineq* c) {
|
||||
ptr_vector<ineq>* ineqs;
|
||||
if (!m_vwatch.find(v, ineqs)) {
|
||||
init_watch(v);
|
||||
ptr_vector<ineq>* ineqs = m_var_infos[v].m_var_watch;
|
||||
if (ineqs == 0) {
|
||||
ineqs = alloc(ptr_vector<ineq>);
|
||||
m_vwatch.insert(v, ineqs);
|
||||
m_var_infos[v].m_var_watch = ineqs;
|
||||
}
|
||||
ineqs->push_back(c);
|
||||
}
|
||||
|
||||
void theory_pb::unwatch_var(bool_var v, ineq* c) {
|
||||
ptr_vector<ineq>* ineqs = 0;
|
||||
if (m_vwatch.find(v, ineqs)) {
|
||||
ptr_vector<ineq>* ineqs = m_var_infos[v].m_var_watch;
|
||||
if (ineqs) {
|
||||
remove(*ineqs, c);
|
||||
}
|
||||
}
|
||||
|
||||
void theory_pb::unwatch_literal(literal w, ineq* c) {
|
||||
ptr_vector<ineq>* ineqs = 0;
|
||||
if (m_lwatch.find(w.index(), ineqs)) {
|
||||
remove(*ineqs, c);
|
||||
void theory_pb::unwatch_literal(literal lit, ineq* c) {
|
||||
ptr_vector<ineq>* ineqs = m_var_infos[lit.var()].m_lit_watch[lit.sign()];
|
||||
if (ineqs) {
|
||||
remove(*ineqs, c);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -741,22 +750,9 @@ namespace smt {
|
|||
|
||||
void theory_pb::reset_eh() {
|
||||
|
||||
// m_watch;
|
||||
u_map<ptr_vector<ineq>*>::iterator it = m_lwatch.begin(), end = m_lwatch.end();
|
||||
for (; it != end; ++it) {
|
||||
dealloc(it->m_value);
|
||||
for (unsigned i = 0; i < m_var_infos.size(); ++i) {
|
||||
m_var_infos[i].reset();
|
||||
}
|
||||
it = m_vwatch.begin(), end = m_vwatch.end();
|
||||
for (; it != end; ++it) {
|
||||
dealloc(it->m_value);
|
||||
}
|
||||
u_map<ineq*>::iterator itc = m_ineqs.begin(), endc = m_ineqs.end();
|
||||
for (; itc != endc; ++itc) {
|
||||
dealloc(itc->m_value);
|
||||
}
|
||||
m_lwatch.reset();
|
||||
m_vwatch.reset();
|
||||
m_ineqs.reset();
|
||||
m_ineqs_trail.reset();
|
||||
m_ineqs_lim.reset();
|
||||
m_stats.reset();
|
||||
|
@ -777,7 +773,8 @@ namespace smt {
|
|||
ptr_vector<ineq>* ineqs = 0;
|
||||
literal nlit(v, is_true);
|
||||
TRACE("pb", tout << "assign: " << ~nlit << "\n";);
|
||||
if (m_lwatch.find(nlit.index(), ineqs)) {
|
||||
ineqs = m_var_infos[v].m_lit_watch[nlit.sign()];
|
||||
if (ineqs != 0) {
|
||||
if (m_enable_simplex) {
|
||||
mpq_inf num(mpq(is_true?1:0),mpq(0));
|
||||
if (!update_bound(v, ~nlit, is_true, num)) {
|
||||
|
@ -797,14 +794,15 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
}
|
||||
if (m_vwatch.find(v, ineqs)) {
|
||||
ineqs = m_var_infos[v].m_var_watch;
|
||||
if (ineqs != 0) {
|
||||
for (unsigned i = 0; i < ineqs->size(); ++i) {
|
||||
ineq* c = (*ineqs)[i];
|
||||
assign_watch(v, is_true, *c);
|
||||
}
|
||||
}
|
||||
ineq* c = 0;
|
||||
if (m_ineqs.find(v, c)) {
|
||||
ineq* c = m_var_infos[v].m_ineq;
|
||||
if (c != 0) {
|
||||
if (m_enable_simplex) {
|
||||
row_info const& info = m_ineq_row_info.find(v);
|
||||
scoped_eps_numeral coeff(m_mpq_inf_mgr);
|
||||
|
@ -1317,10 +1315,9 @@ namespace smt {
|
|||
unsigned sz = m_ineqs_lim[new_lim];
|
||||
while (m_ineqs_trail.size() > sz) {
|
||||
bool_var v = m_ineqs_trail.back();
|
||||
ineq* c = 0;
|
||||
VERIFY(m_ineqs.find(v, c));
|
||||
ineq* c = m_var_infos[v].m_ineq;
|
||||
clear_watch(*c);
|
||||
m_ineqs.remove(v);
|
||||
m_var_infos[v].m_ineq = 0;
|
||||
m_ineqs_trail.pop_back();
|
||||
if (m_enable_simplex) {
|
||||
row_info r_info;
|
||||
|
@ -1866,9 +1863,11 @@ namespace smt {
|
|||
}
|
||||
|
||||
void theory_pb::validate_final_check() {
|
||||
u_map<ineq*>::iterator itc = m_ineqs.begin(), endc = m_ineqs.end();
|
||||
for (; itc != endc; ++itc) {
|
||||
validate_final_check(*itc->m_value);
|
||||
for (unsigned i = 0; i < m_var_infos.size(); ++i) {
|
||||
ineq* c = m_var_infos[i].m_ineq;
|
||||
if (c) {
|
||||
validate_final_check(*c);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -2076,29 +2075,37 @@ namespace smt {
|
|||
return p;
|
||||
}
|
||||
|
||||
void theory_pb::display_watch(std::ostream& out, bool_var v, bool sign) const {
|
||||
watch_list const* w = m_var_infos[v].m_lit_watch[sign];
|
||||
if (!w) return;
|
||||
watch_list const& wl = *w;
|
||||
out << "watch: " << literal(v, sign) << " |-> ";
|
||||
for (unsigned i = 0; i < wl.size(); ++i) {
|
||||
out << wl[i]->lit() << " ";
|
||||
}
|
||||
out << "\n";
|
||||
}
|
||||
|
||||
void theory_pb::display(std::ostream& out) const {
|
||||
u_map<ptr_vector<ineq>*>::iterator it = m_lwatch.begin(), end = m_lwatch.end();
|
||||
for (; it != end; ++it) {
|
||||
out << "watch: " << to_literal(it->m_key) << " |-> ";
|
||||
watch_list const& wl = *it->m_value;
|
||||
for (unsigned vi = 0; vi < m_var_infos.size(); ++vi) {
|
||||
display_watch(out, vi, false);
|
||||
display_watch(out, vi, true);
|
||||
}
|
||||
for (unsigned vi = 0; vi < m_var_infos.size(); ++vi) {
|
||||
watch_list const* w = m_var_infos[vi].m_var_watch;
|
||||
if (!w) continue;
|
||||
out << "watch (v): " << literal(vi) << " |-> ";
|
||||
watch_list const& wl = *w;
|
||||
for (unsigned i = 0; i < wl.size(); ++i) {
|
||||
out << wl[i]->lit() << " ";
|
||||
}
|
||||
out << "\n";
|
||||
}
|
||||
it = m_vwatch.begin(), end = m_vwatch.end();
|
||||
for (; it != end; ++it) {
|
||||
out << "watch (v): " << literal(it->m_key) << " |-> ";
|
||||
watch_list const& wl = *it->m_value;
|
||||
for (unsigned i = 0; i < wl.size(); ++i) {
|
||||
out << wl[i]->lit() << " ";
|
||||
for (unsigned vi = 0; vi < m_var_infos.size(); ++vi) {
|
||||
ineq* c = m_var_infos[vi].m_ineq;
|
||||
if (c) {
|
||||
display(out, *c, true);
|
||||
}
|
||||
out << "\n";
|
||||
}
|
||||
u_map<ineq*>::iterator itc = m_ineqs.begin(), endc = m_ineqs.end();
|
||||
for (; itc != endc; ++itc) {
|
||||
ineq& c = *itc->m_value;
|
||||
display(out, c, true);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -193,10 +193,32 @@ namespace smt {
|
|||
typedef ptr_vector<ineq> watch_list;
|
||||
typedef map<arg_t, bool_var, arg_t::hash, arg_t::eq> arg_map;
|
||||
|
||||
struct var_info {
|
||||
watch_list* m_lit_watch[2];
|
||||
watch_list* m_var_watch;
|
||||
ineq* m_ineq;
|
||||
|
||||
var_info(): m_var_watch(0), m_ineq(0)
|
||||
{
|
||||
m_lit_watch[0] = 0;
|
||||
m_lit_watch[1] = 0;
|
||||
}
|
||||
|
||||
void reset() {
|
||||
dealloc(m_lit_watch[0]);
|
||||
dealloc(m_lit_watch[1]);
|
||||
dealloc(m_var_watch);
|
||||
dealloc(m_ineq);
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
theory_pb_params m_params;
|
||||
u_map<watch_list*> m_lwatch; // per literal.
|
||||
u_map<watch_list*> m_vwatch; // per variable.
|
||||
u_map<ineq*> m_ineqs; // per inequality.
|
||||
|
||||
svector<var_info> m_var_infos;
|
||||
// u_map<watch_list*> m_lwatch; // per literal.
|
||||
// u_map<watch_list*> m_vwatch; // per variable.
|
||||
// u_map<ineq*> m_ineqs; // per inequality.
|
||||
arg_map m_ineq_rep; // Simplex: representative inequality
|
||||
u_map<row_info> m_ineq_row_info; // Simplex: row information per variable
|
||||
uint_set m_vars; // Simplex: 0-1 variables.
|
||||
|
@ -221,6 +243,7 @@ namespace smt {
|
|||
literal compile_arg(expr* arg);
|
||||
void add_watch(ineq& c, unsigned index);
|
||||
void del_watch(watch_list& watch, unsigned index, ineq& c, unsigned ineq_index);
|
||||
void init_watch(bool_var v);
|
||||
void init_watch_literal(ineq& c);
|
||||
void init_watch_var(ineq& c);
|
||||
void clear_watch(ineq& c);
|
||||
|
@ -242,6 +265,7 @@ namespace smt {
|
|||
std::ostream& display(std::ostream& out, ineq const& c, bool values = false) const;
|
||||
std::ostream& display(std::ostream& out, arg_t const& c, bool values = false) const;
|
||||
virtual void display(std::ostream& out) const;
|
||||
void display_watch(std::ostream& out, bool_var v, bool sign) const;
|
||||
void display_resolved_lemma(std::ostream& out) const;
|
||||
|
||||
void add_clause(ineq& c, literal_vector const& lits);
|
||||
|
|
|
@ -102,6 +102,7 @@ namespace smt {
|
|||
m_enabled.push_back(true);
|
||||
m_normalize = true;
|
||||
bool_var bv = register_var(var, true);
|
||||
(void)bv;
|
||||
TRACE("opt", tout << "enable: v" << m_bool2var[bv] << " b" << bv << " " << mk_pp(var, get_manager()) << "\n";
|
||||
tout << wfml << "\n";);
|
||||
return var;
|
||||
|
|
|
@ -53,24 +53,21 @@ struct aig {
|
|||
aig() {}
|
||||
};
|
||||
|
||||
static bool is_true(aig_lit const & r) { return !r.is_inverted() && r.ptr_non_inverted()->m_id == 0; }
|
||||
static bool is_false(aig_lit const & r) { return r.is_inverted() && r.ptr()->m_id == 0; }
|
||||
static bool is_var(aig * n) { return n->m_children[0].is_null(); }
|
||||
static bool is_var(aig_lit const & n) { return is_var(n.ptr()); }
|
||||
static unsigned id(aig_lit const & n) { return n.ptr()->m_id; }
|
||||
static unsigned ref_count(aig_lit const & n) { return n.ptr()->m_ref_count; }
|
||||
static aig_lit left(aig * n) { return n->m_children[0]; }
|
||||
static aig_lit right(aig * n) { return n->m_children[1]; }
|
||||
static aig_lit left(aig_lit const & n) { return left(n.ptr()); }
|
||||
static aig_lit right(aig_lit const & n) { return right(n.ptr()); }
|
||||
#if Z3DEBUG
|
||||
inline bool is_true(aig_lit const & r) { return !r.is_inverted() && r.ptr_non_inverted()->m_id == 0; }
|
||||
#endif
|
||||
// inline bool is_false(aig_lit const & r) { return r.is_inverted() && r.ptr()->m_id == 0; }
|
||||
inline bool is_var(aig * n) { return n->m_children[0].is_null(); }
|
||||
inline bool is_var(aig_lit const & n) { return is_var(n.ptr()); }
|
||||
inline unsigned id(aig_lit const & n) { return n.ptr()->m_id; }
|
||||
inline unsigned ref_count(aig_lit const & n) { return n.ptr()->m_ref_count; }
|
||||
inline aig_lit left(aig * n) { return n->m_children[0]; }
|
||||
inline aig_lit right(aig * n) { return n->m_children[1]; }
|
||||
inline aig_lit left(aig_lit const & n) { return left(n.ptr()); }
|
||||
inline aig_lit right(aig_lit const & n) { return right(n.ptr()); }
|
||||
|
||||
inline unsigned to_idx(aig * p) { SASSERT(!is_var(p)); return p->m_id - FIRST_NODE_ID; }
|
||||
|
||||
static void unmark(unsigned sz, aig_lit const * ns) {
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
ns[i].ptr()->m_mark = false;
|
||||
}
|
||||
}
|
||||
|
||||
static void unmark(unsigned sz, aig * const * ns) {
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
|
|
|
@ -148,10 +148,12 @@ struct interval {
|
|||
}
|
||||
};
|
||||
|
||||
#ifdef _TRACE
|
||||
std::ostream& operator<<(std::ostream& o, const interval& I) {
|
||||
o << "[" << I.l << ", " << I.h << "]";
|
||||
return o;
|
||||
}
|
||||
#endif
|
||||
|
||||
|
||||
struct undo_bound {
|
||||
|
|
|
@ -25,7 +25,7 @@ Notes:
|
|||
extension_model_converter::~extension_model_converter() {
|
||||
}
|
||||
|
||||
|
||||
#ifdef _TRACE
|
||||
static void display_decls_info(std::ostream & out, model_ref & md) {
|
||||
ast_manager & m = md->get_manager();
|
||||
unsigned sz = md->get_num_decls();
|
||||
|
@ -42,6 +42,7 @@ static void display_decls_info(std::ostream & out, model_ref & md) {
|
|||
out << " :id " << d->get_id() << "\n";
|
||||
}
|
||||
}
|
||||
#endif
|
||||
|
||||
void extension_model_converter::operator()(model_ref & md, unsigned goal_idx) {
|
||||
SASSERT(goal_idx == 0);
|
||||
|
|
|
@ -126,7 +126,7 @@ tactic * mk_report_verbose_tactic(char const * msg, unsigned lvl) {
|
|||
class trace_tactic : public skip_tactic {
|
||||
char const * m_tag;
|
||||
public:
|
||||
trace_tactic(char const * tag):m_tag(tag) {}
|
||||
trace_tactic(char const * tag): m_tag(tag) {}
|
||||
|
||||
virtual void operator()(goal_ref const & in,
|
||||
goal_ref_buffer & result,
|
||||
|
@ -134,6 +134,7 @@ public:
|
|||
proof_converter_ref & pc,
|
||||
expr_dependency_ref & core) {
|
||||
TRACE(m_tag, in->display(tout););
|
||||
(void)m_tag;
|
||||
skip_tactic::operator()(in, result, mc, pc, core);
|
||||
}
|
||||
};
|
||||
|
|
|
@ -13,9 +13,6 @@ Copyright (c) 2015 Microsoft Corporation
|
|||
|
||||
expr_rand::expr_rand(ast_manager& m):
|
||||
m_manager(m),
|
||||
m_num_vars(0),
|
||||
m_num_apps(0),
|
||||
m_num_nodes(0),
|
||||
m_max_steps(10),
|
||||
m_funcs(m)
|
||||
{}
|
||||
|
|
|
@ -24,9 +24,6 @@ Revision History:
|
|||
|
||||
class expr_rand {
|
||||
ast_manager& m_manager;
|
||||
unsigned m_num_vars;
|
||||
unsigned m_num_apps;
|
||||
unsigned m_num_nodes;
|
||||
unsigned m_max_steps;
|
||||
random_gen m_random;
|
||||
|
||||
|
|
|
@ -73,6 +73,7 @@ struct scoped_timer::imp {
|
|||
pthread_cond_t m_cond;
|
||||
unsigned m_ms;
|
||||
bool m_initialized;
|
||||
bool m_signal_sent;
|
||||
#else
|
||||
// Other
|
||||
#endif
|
||||
|
@ -119,10 +120,18 @@ struct scoped_timer::imp {
|
|||
|
||||
pthread_mutex_lock(&st->m_mutex);
|
||||
st->m_initialized = true;
|
||||
int e = pthread_cond_timedwait(&st->m_cond, &st->m_mutex, &end_time);
|
||||
ENSURE(e == 0 || e == ETIMEDOUT);
|
||||
|
||||
int e = 0;
|
||||
// `pthread_cond_timedwait()` may spuriously wake even if the signal
|
||||
// was not sent so we loop until a timeout occurs or the signal was
|
||||
// **really** sent.
|
||||
while (!(e == 0 && st->m_signal_sent)) {
|
||||
e = pthread_cond_timedwait(&st->m_cond, &st->m_mutex, &end_time);
|
||||
ENSURE(e == 0 || e == ETIMEDOUT);
|
||||
if (e == ETIMEDOUT)
|
||||
break;
|
||||
}
|
||||
pthread_mutex_unlock(&st->m_mutex);
|
||||
|
||||
if (e == ETIMEDOUT)
|
||||
st->m_eh->operator()();
|
||||
return 0;
|
||||
|
@ -170,6 +179,7 @@ struct scoped_timer::imp {
|
|||
// Linux & FreeBSD
|
||||
m_ms = ms;
|
||||
m_initialized = false;
|
||||
m_signal_sent = false;
|
||||
ENSURE(pthread_mutex_init(&m_mutex, NULL) == 0);
|
||||
ENSURE(pthread_cond_init(&m_cond, NULL) == 0);
|
||||
ENSURE(pthread_create(&m_thread_id, NULL, &thread_func, this) == 0);
|
||||
|
@ -218,6 +228,10 @@ struct scoped_timer::imp {
|
|||
if (!init)
|
||||
sched_yield();
|
||||
}
|
||||
pthread_mutex_lock(&m_mutex);
|
||||
m_signal_sent = true;
|
||||
pthread_mutex_unlock(&m_mutex);
|
||||
// Perform signal outside of lock to avoid waking timing thread twice.
|
||||
pthread_cond_signal(&m_cond);
|
||||
|
||||
pthread_join(m_thread_id, NULL);
|
||||
|
|
Loading…
Reference in a new issue