mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

fix #1575, fix #1585

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-04-23 07:11:15 +02:00
parent f22abaa713
commit 279f1986a6
4 changed files with 21 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/cmd_context/cmd_context.cpp
View file

@ -718,8 +718,8 @@ void cmd_context::init_manager_core(bool new_manager) {
} }
m_dt_eh = alloc(dt_eh, *this); m_dt_eh = alloc(dt_eh, *this);
m_pmanager->set_new_datatype_eh(m_dt_eh.get()); m_pmanager->set_new_datatype_eh(m_dt_eh.get());
if (!has_logic()) { if (!has_logic() && new_manager) {
TRACE("cmd_context", tout << "init manager\n";); TRACE("cmd_context", tout << "init manager " << m_logic << "\n";);
// add list type only if the logic is not specified. // add list type only if the logic is not specified.
// it prevents clashes with builtin types. // it prevents clashes with builtin types.
insert(pm().mk_plist_decl()); insert(pm().mk_plist_decl());
@ -757,6 +757,7 @@ void cmd_context::init_external_manager() {
} }
bool cmd_context::set_logic(symbol const & s) { bool cmd_context::set_logic(symbol const & s) {
TRACE("cmd_context", tout << s << "\n";);
if (has_logic()) if (has_logic())
throw cmd_exception("the logic has already been set"); throw cmd_exception("the logic has already been set");
if (has_manager() && m_main_ctx) if (has_manager() && m_main_ctx)

11
src/smt/theory_seq.cpp
View file

@ -1473,7 +1473,7 @@ bool theory_seq::add_solution(expr* l, expr* r, dependency* deps) {
if (l == r) { if (l == r) {
return false; return false;
} }
TRACE("seq", tout << mk_pp(l, m) << " ==> " << mk_pp(r, m) << "\n";); TRACE("seq", tout << mk_pp(l, m) << " ==> " << mk_pp(r, m) << "\n"; display_deps(tout, deps););
m_new_solution = true; m_new_solution = true;
m_rep.update(l, r, deps); m_rep.update(l, r, deps);
enode* n1 = ensure_enode(l); enode* n1 = ensure_enode(l);
@ -1513,7 +1513,9 @@ bool theory_seq::solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, de
change = canonize(r, rs, dep2) || change; change = canonize(r, rs, dep2) || change;
deps = m_dm.mk_join(dep2, deps); deps = m_dm.mk_join(dep2, deps);
TRACE("seq", tout << l << " = " << r << " ==> "; TRACE("seq", tout << l << " = " << r << " ==> ";
tout << ls << " = " << rs << "\n";); tout << ls << " = " << rs << "\n";
display_deps(tout, deps);
);
if (!ctx.inconsistent() && simplify_eq(ls, rs, deps)) { if (!ctx.inconsistent() && simplify_eq(ls, rs, deps)) {
return true; return true;
} }
@ -2674,7 +2676,12 @@ void theory_seq::init_model(expr_ref_vector const& es) {
} }
} }
void theory_seq::finalize_model(model_generator& mg) {
m_rep.pop_scope(1);
}
void theory_seq::init_model(model_generator & mg) { void theory_seq::init_model(model_generator & mg) {
m_rep.push_scope();
m_factory = alloc(seq_factory, get_manager(), get_family_id(), mg.get_model()); m_factory = alloc(seq_factory, get_manager(), get_family_id(), mg.get_model());
mg.register_factory(m_factory); mg.register_factory(m_factory);
for (ne const& n : m_nqs) { for (ne const& n : m_nqs) {

13
src/smt/theory_seq.h
View file

@ -64,14 +64,14 @@ namespace smt {
// + a cache for normalization. // + a cache for normalization.
class solution_map { class solution_map {
enum map_update { INS, DEL }; enum map_update { INS, DEL };
ast_manager& m; ast_manager& m;
dependency_manager& m_dm; dependency_manager& m_dm;
eqdep_map_t m_map; eqdep_map_t m_map;
eval_cache m_cache; eval_cache m_cache;
expr_ref_vector m_lhs, m_rhs; expr_ref_vector m_lhs, m_rhs;
ptr_vector<dependency> m_deps; ptr_vector<dependency> m_deps;
svector<map_update> m_updates; svector<map_update> m_updates;
unsigned_vector m_limit; unsigned_vector m_limit;
void add_trail(map_update op, expr* l, expr* r, dependency* d); void add_trail(map_update op, expr* l, expr* r, dependency* d);
public: public:
@ -362,6 +362,7 @@ namespace smt {
void collect_statistics(::statistics & st) const override; void collect_statistics(::statistics & st) const override;
model_value_proc * mk_value(enode * n, model_generator & mg) override; model_value_proc * mk_value(enode * n, model_generator & mg) override;
void init_model(model_generator & mg) override; void init_model(model_generator & mg) override;
void finalize_model(model_generator & mg) override;
void init_search_eh() override; void init_search_eh() override;
void init_model(expr_ref_vector const& es); void init_model(expr_ref_vector const& es);