From 3f407982f376ea6b50c863039d76c34503949f17 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 14 Nov 2024 21:55:44 -0800 Subject: [PATCH] build fixes Signed-off-by: Nikolaj Bjorner --- src/ast/converters/expr_inverter.cpp | 7 +++---- src/ast/sls/sls_smt_plugin.h | 2 +- src/sat/smt/sls_solver.h | 4 ++-- src/smt/theory_sls.h | 5 +++-- 4 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/ast/converters/expr_inverter.cpp b/src/ast/converters/expr_inverter.cpp index e2d6f025510..8bb316dfc8c 100644 --- a/src/ast/converters/expr_inverter.cpp +++ b/src/ast/converters/expr_inverter.cpp @@ -790,17 +790,16 @@ class seq_expr_inverter : public iexpr_inverter { 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; } diff --git a/src/ast/sls/sls_smt_plugin.h b/src/ast/sls/sls_smt_plugin.h index 073e5bc96fe..d5d597647dd 100644 --- a/src/ast/sls/sls_smt_plugin.h +++ b/src/ast/sls/sls_smt_plugin.h @@ -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; diff --git a/src/sat/smt/sls_solver.h b/src/sat/smt/sls_solver.h index 0378f584538..a9fedf4d190 100644 --- a/src/sat/smt/sls_solver.h +++ b/src/sat/smt/sls_solver.h @@ -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 \ No newline at end of file +#endif diff --git a/src/smt/theory_sls.h b/src/smt/theory_sls.h index d57b35945fc..db1aa204d16 100644 --- a/src/smt/theory_sls.h +++ b/src/smt/theory_sls.h @@ -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; + }; }