mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
build fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
ca6ec0d9e4
commit
3f407982f3
|
@ -790,17 +790,16 @@ public:
|
|||
r = m.mk_or(r, emp);
|
||||
return true;
|
||||
}
|
||||
if (uncnstr(args[1])) {
|
||||
if (uncnstr(args[1]) && seq.is_string(args[0]->get_sort())) {
|
||||
// x contains y -> r
|
||||
// y -> if r then x else x + x
|
||||
// y -> if r then x else x + x + a
|
||||
mk_fresh_uncnstr_var_for(f, r);
|
||||
if (m_mc)
|
||||
add_def(args[1], m.mk_ite(r, args[0], seq.str.mk_concat(args[0], args[0])));
|
||||
add_def(args[1], m.mk_ite(r, args[0], seq.str.mk_concat(args[0], args[0], seq.str.mk_string(zstring("a")))));
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
default:
|
||||
verbose_stream() << f->get_name() << "\n";
|
||||
return false;
|
||||
|
||||
}
|
||||
|
|
|
@ -33,7 +33,7 @@ namespace sls {
|
|||
virtual void set_value(expr* t, expr* v) = 0;
|
||||
virtual void force_phase(sat::literal lit) = 0;
|
||||
virtual void set_has_new_best_phase(bool b) = 0;
|
||||
virtual bool get_value(expr* v, expr_ref& val) = 0;
|
||||
virtual bool get_smt_value(expr* v, expr_ref& val) = 0;
|
||||
virtual bool get_best_phase(sat::bool_var v) = 0;
|
||||
virtual expr* bool_var2expr(sat::bool_var v) = 0;
|
||||
virtual void inc_activity(sat::bool_var v, double inc) = 0;
|
||||
|
|
|
@ -101,10 +101,10 @@ namespace sls {
|
|||
void inc_activity(sat::bool_var v, double inc) override {}
|
||||
unsigned get_num_bool_vars() const override;
|
||||
bool parallel_mode() const override { return false; }
|
||||
bool get_value(expr* v, expr_ref& value) override { return false; }
|
||||
bool get_smt_value(expr* v, expr_ref& value) override { return false; }
|
||||
|
||||
};
|
||||
|
||||
}
|
||||
|
||||
#endif
|
||||
#endif
|
||||
|
|
|
@ -110,8 +110,9 @@ namespace smt {
|
|||
void set_finished() override;
|
||||
unsigned get_num_bool_vars() const override;
|
||||
void inc_activity(sat::bool_var v, double inc) override;
|
||||
bool parallel_mode() const { return m_parallel_mode; }
|
||||
bool get_value(expr* v, expr_ref& value) override;
|
||||
bool parallel_mode() const override { return m_parallel_mode; }
|
||||
bool get_smt_value(expr* v, expr_ref& value) override;
|
||||
|
||||
};
|
||||
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue