From bea8744f7d133f1341e6c2babfa762a72de9a690 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 31 Jul 2015 11:20:01 +0100 Subject: [PATCH 1/3] Disabled superfluous wellformedness check and fixed type checking in basic_decl_plugin::join --- src/ast/ast.cpp | 8 ++++++-- src/cmd_context/context_params.cpp | 2 +- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 2881f1b62..6e2fac4bd 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1018,15 +1018,19 @@ func_decl * basic_decl_plugin::mk_ite_decl(sort * s) { sort* basic_decl_plugin::join(sort* s1, sort* s2) { if (s1 == s2) return s1; - if (s1->get_family_id() == m_manager->m_arith_family_id && + if (s1->get_family_id() == m_manager->m_arith_family_id && s2->get_family_id() == m_manager->m_arith_family_id) { if (s1->get_decl_kind() == REAL_SORT) { return s1; } + return s2; } - return s2; + std::ostringstream buffer; + buffer << "Sorts " << mk_pp(s1, *m_manager) << " and " << mk_pp(s2, *m_manager) << " are incompatible"; + throw ast_exception(buffer.str().c_str()); } + func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { switch (static_cast(k)) { diff --git a/src/cmd_context/context_params.cpp b/src/cmd_context/context_params.cpp index 8760ade15..70f110c92 100644 --- a/src/cmd_context/context_params.cpp +++ b/src/cmd_context/context_params.cpp @@ -33,7 +33,7 @@ context_params::context_params() { m_trace = false; m_debug_ref_count = false; m_smtlib2_compliant = false; - m_well_sorted_check = true; + m_well_sorted_check = false; m_timeout = UINT_MAX; updt_params(); } From ca4a7ca74e4f1c736d9d950ef2cd2e6c42af3d03 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 1 Aug 2015 14:29:45 +0100 Subject: [PATCH 2/3] style --- src/solver/solver.h | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/solver/solver.h b/src/solver/solver.h index c4e1be13e..63592ea3b 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -139,6 +139,7 @@ public: \brief Display the content of this solver. */ virtual void display(std::ostream & out) const; + class scoped_push { solver& s; bool m_nopop; @@ -147,9 +148,9 @@ public: ~scoped_push() { if (!m_nopop) s.pop(1); } void disable_pop() { m_nopop = true; } }; + protected: virtual void set_cancel(bool f) = 0; - }; #endif From 5e0aaee2c7523bf8f322739278f28c87927764be Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 4 Aug 2015 15:26:03 +0100 Subject: [PATCH 3/3] Made num_clauses in sat_solver public --- src/sat/sat_solver.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index d4c9ecf79..f8948e3b6 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -210,6 +210,7 @@ namespace sat { public: bool inconsistent() const { return m_inconsistent; } unsigned num_vars() const { return m_level.size(); } + unsigned num_clauses() const; bool is_external(bool_var v) const { return m_external[v] != 0; } bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; } unsigned scope_lvl() const { return m_scope_lvl; } @@ -446,8 +447,7 @@ namespace sat { protected: void display_binary(std::ostream & out) const; - void display_units(std::ostream & out) const; - unsigned num_clauses() const; + void display_units(std::ostream & out) const; bool is_unit(clause const & c) const; bool is_empty(clause const & c) const; bool check_missed_propagation(clause_vector const & cs) const;