mirror of
https://github.com/Z3Prover/z3
synced 2025-07-19 10:52:02 +00:00
remove passing suffixes into pdr_sym_mux, trying to isolate cause of issue #420
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
660eff0b9e
commit
94be6fc776
4 changed files with 10 additions and 10 deletions
|
@ -164,12 +164,11 @@ namespace pdr {
|
||||||
m(manager),
|
m(manager),
|
||||||
m_fparams(fparams),
|
m_fparams(fparams),
|
||||||
m_brwr(m),
|
m_brwr(m),
|
||||||
m_mux(m, m_state_suffixes),
|
m_mux(m),
|
||||||
m_background(m.mk_true(), m),
|
m_background(m.mk_true(), m),
|
||||||
m_contexts(fparams, max_num_contexts, m),
|
m_contexts(fparams, max_num_contexts, m),
|
||||||
m_next_unique_num(0)
|
m_next_unique_num(0)
|
||||||
{
|
{
|
||||||
m_state_suffixes.push_back("_n");
|
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -81,7 +81,6 @@ namespace pdr {
|
||||||
|
|
||||||
mutable bool_rewriter m_brwr;
|
mutable bool_rewriter m_brwr;
|
||||||
|
|
||||||
vector<std::string> m_state_suffixes;
|
|
||||||
sym_mux m_mux;
|
sym_mux m_mux;
|
||||||
expr_ref m_background;
|
expr_ref m_background;
|
||||||
decl_vector m_o0_preds;
|
decl_vector m_o0_preds;
|
||||||
|
|
|
@ -28,9 +28,10 @@ Revision History:
|
||||||
|
|
||||||
using namespace pdr;
|
using namespace pdr;
|
||||||
|
|
||||||
sym_mux::sym_mux(ast_manager & m, vector<std::string> & suffixes)
|
sym_mux::sym_mux(ast_manager & m)
|
||||||
: m(m), m_ref_holder(m), m_next_sym_suffix_idx(0), m_suffixes(suffixes)
|
: m(m), m_ref_holder(m),
|
||||||
{
|
m_next_sym_suffix_idx(0) {
|
||||||
|
m_suffixes.push_back("_n");
|
||||||
unsigned suf_sz = m_suffixes.size();
|
unsigned suf_sz = m_suffixes.size();
|
||||||
for(unsigned i = 0; i < suf_sz; ++i) {
|
for(unsigned i = 0; i < suf_sz; ++i) {
|
||||||
symbol suff_sym = symbol(m_suffixes[i].c_str());
|
symbol suff_sym = symbol(m_suffixes[i].c_str());
|
||||||
|
@ -53,7 +54,8 @@ std::string sym_mux::get_suffix(unsigned i) {
|
||||||
m_used_suffixes.insert(new_syffix_sym);
|
m_used_suffixes.insert(new_syffix_sym);
|
||||||
m_suffixes.push_back(new_suffix);
|
m_suffixes.push_back(new_suffix);
|
||||||
}
|
}
|
||||||
return m_suffixes[i];
|
std::string result = m_suffixes[i];
|
||||||
|
return result;
|
||||||
}
|
}
|
||||||
|
|
||||||
void sym_mux::create_tuple(func_decl* prefix, unsigned arity, sort * const * domain, sort * range,
|
void sym_mux::create_tuple(func_decl* prefix, unsigned arity, sort * const * domain, sort * range,
|
||||||
|
|
|
@ -94,7 +94,7 @@ private:
|
||||||
|
|
||||||
expr_ref isolate_o_idx(expr* e, unsigned idx) const;
|
expr_ref isolate_o_idx(expr* e, unsigned idx) const;
|
||||||
public:
|
public:
|
||||||
sym_mux(ast_manager & m, vector<std::string> & suffixes);
|
sym_mux(ast_manager & m);
|
||||||
|
|
||||||
ast_manager & get_manager() const { return m; }
|
ast_manager & get_manager() const { return m; }
|
||||||
|
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue