From fa0c75e76ef03db5309bbdd0a884f49171dba174 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 7 Feb 2018 15:13:13 -0800 Subject: [PATCH] rename to core2 to avoid overloaded virtual Signed-off-by: Nikolaj Bjorner --- src/muz/spacer/spacer_itp_solver.h | 2 +- src/muz/spacer/spacer_virtual_solver.cpp | 2 +- src/sat/sat_lookahead.h | 2 +- src/sat/sat_solver/inc_sat_solver.cpp | 4 ++-- src/smt/smt_solver.cpp | 4 ++-- src/solver/combined_solver.cpp | 2 +- src/solver/solver.cpp | 2 +- src/solver/solver.h | 2 +- src/solver/solver_na2as.cpp | 6 +++--- src/solver/solver_na2as.h | 2 +- src/solver/solver_pool.cpp | 2 +- 11 files changed, 15 insertions(+), 15 deletions(-) diff --git a/src/muz/spacer/spacer_itp_solver.h b/src/muz/spacer/spacer_itp_solver.h index 55c1711c3..41e67afd1 100644 --- a/src/muz/spacer/spacer_itp_solver.h +++ b/src/muz/spacer/spacer_itp_solver.h @@ -115,7 +115,7 @@ public: virtual void assert_expr_core(expr *t) {m_solver.assert_expr(t);} - virtual void assert_expr_core(expr *t, expr *a) + virtual void assert_expr_core2(expr *t, expr *a) {NOT_IMPLEMENTED_YET();} virtual void assert_lemma(expr* e) { NOT_IMPLEMENTED_YET(); } virtual expr_ref lookahead(const expr_ref_vector &,const expr_ref_vector &) { return expr_ref(m.mk_true(), m); } diff --git a/src/muz/spacer/spacer_virtual_solver.cpp b/src/muz/spacer/spacer_virtual_solver.cpp index 0c3adbbbd..ecb3c15a1 100644 --- a/src/muz/spacer/spacer_virtual_solver.cpp +++ b/src/muz/spacer/spacer_virtual_solver.cpp @@ -50,7 +50,7 @@ virtual_solver::virtual_solver(virtual_solver_factory &factory, // -- change m_context, but will add m_pred to // -- the private field solver_na2as::m_assumptions if (m_virtual) - { solver_na2as::assert_expr_core(m.mk_true(), m_pred); } + { solver_na2as::assert_expr_core2(m.mk_true(), m_pred); } } virtual_solver::~virtual_solver() diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index a37f32a1b..f81417d41 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -186,7 +186,7 @@ namespace sat { m_is_decision.reset(); m_cube.reset(); m_freevars_threshold = 0; - m_psat_threshold = DBL_MAX; + m_psat_threshold = 100000000.0; reset_stats(); } void reset_stats() { m_conflicts = 0; m_cutoffs = 0; } diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 03f6e6d0b..0ba8926cd 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -243,10 +243,10 @@ public: --n; } } - virtual unsigned get_scope_level() const { + unsigned get_scope_level() const override { return m_num_scopes; } - virtual void assert_expr_core(expr * t, expr * a) { + void assert_expr_core2(expr * t, expr * a) override { if (a) { m_asmsf.push_back(a); assert_expr_core(m.mk_implies(a, t)); diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 3449ad480..780495e9c 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -105,11 +105,11 @@ namespace smt { m_context.assert_expr(t); } - virtual void assert_expr_core(expr * t, expr * a) { + virtual void assert_expr_core2(expr * t, expr * a) { if (m_name2assertion.contains(a)) { throw default_exception("named assertion defined twice"); } - solver_na2as::assert_expr_core(t, a); + solver_na2as::assert_expr_core2(t, a); get_manager().inc_ref(t); m_name2assertion.insert(a, t); } diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index 713009cd6..521cf8dec 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -172,7 +172,7 @@ public: m_solver2->assert_expr(t); } - virtual void assert_expr_core(expr * t, expr * a) { + virtual void assert_expr_core2(expr * t, expr * a) { if (m_check_sat_executed) switch_inc_mode(); m_solver1->assert_expr(t, a); diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index 356eaf2ed..3a772e7f2 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -199,7 +199,7 @@ void solver::assert_expr(expr* f, expr* t) { // (*mc)(a); } } - assert_expr_core(fml, a); + assert_expr_core2(fml, a); } void solver::collect_param_descrs(param_descrs & r) { diff --git a/src/solver/solver.h b/src/solver/solver.h index bc6ffb0e0..5bd25d8a6 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -102,7 +102,7 @@ public: void assert_expr(expr * t, expr* a); - virtual void assert_expr_core(expr * t, expr * a) = 0; + virtual void assert_expr_core2(expr * t, expr * a) = 0; /** \brief Create a backtracking point. diff --git a/src/solver/solver_na2as.cpp b/src/solver/solver_na2as.cpp index 3cffd40cf..f98e08cdb 100644 --- a/src/solver/solver_na2as.cpp +++ b/src/solver/solver_na2as.cpp @@ -30,9 +30,9 @@ solver_na2as::solver_na2as(ast_manager & m): solver_na2as::~solver_na2as() {} -void solver_na2as::assert_expr_core(expr * t, expr * a) { +void solver_na2as::assert_expr_core2(expr * t, expr * a) { if (a == 0) { - solver::assert_expr_core(t); + assert_expr_core(t); } else { SASSERT(is_uninterp_const(a)); @@ -41,7 +41,7 @@ void solver_na2as::assert_expr_core(expr * t, expr * a) { m_assumptions.push_back(a); expr_ref new_t(m); new_t = m.mk_implies(a, t); - solver::assert_expr_core(new_t); + assert_expr_core(new_t); } } diff --git a/src/solver/solver_na2as.h b/src/solver/solver_na2as.h index 2cbaaba5a..93526e844 100644 --- a/src/solver/solver_na2as.h +++ b/src/solver/solver_na2as.h @@ -34,7 +34,7 @@ public: solver_na2as(ast_manager & m); virtual ~solver_na2as(); - void assert_expr_core(expr * t, expr * a) override; + void assert_expr_core2(expr * t, expr * a) override; // virtual void assert_expr_core(expr * t) = 0; // Subclasses of solver_na2as should redefine the following *_core methods instead of these ones. diff --git a/src/solver/solver_pool.cpp b/src/solver/solver_pool.cpp index 2f6a22580..772650e64 100644 --- a/src/solver/solver_pool.cpp +++ b/src/solver/solver_pool.cpp @@ -49,7 +49,7 @@ public: m_in_delayed_scope(false), m_dump_counter(0) { if (is_virtual()) { - solver_na2as::assert_expr_core(m.mk_true(), pred); + solver_na2as::assert_expr_core2(m.mk_true(), pred); } }