From 5e3303ae857262749a3aff7c3f3714d54743623a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 2 Jul 2018 11:46:03 -0700 Subject: [PATCH] let HORN solver know about cardinality constraints Signed-off-by: Nikolaj Bjorner --- src/ast/pb_decl_plugin.cpp | 2 +- src/cmd_context/check_logic.cpp | 3 ++- src/solver/smt_logics.cpp | 2 +- 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/ast/pb_decl_plugin.cpp b/src/ast/pb_decl_plugin.cpp index c8e707cee..dfdcc6206 100644 --- a/src/ast/pb_decl_plugin.cpp +++ b/src/ast/pb_decl_plugin.cpp @@ -92,7 +92,7 @@ func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p } void pb_decl_plugin::get_op_names(svector & op_names, symbol const & logic) { - if (logic == symbol::null || logic == "QF_FD" || logic == "ALL") { + if (logic == symbol::null || logic == "QF_FD" || logic == "ALL" || logic == "HORN") { op_names.push_back(builtin_name(m_at_most_sym.bare_str(), OP_AT_MOST_K)); op_names.push_back(builtin_name(m_at_least_sym.bare_str(), OP_AT_LEAST_K)); op_names.push_back(builtin_name(m_pble_sym.bare_str(), OP_PB_LE)); diff --git a/src/cmd_context/check_logic.cpp b/src/cmd_context/check_logic.cpp index 55be27c6d..57e15c6a3 100644 --- a/src/cmd_context/check_logic.cpp +++ b/src/cmd_context/check_logic.cpp @@ -17,6 +17,7 @@ Revision History: --*/ #include "cmd_context/check_logic.h" +#include "solver/smt_logics.h" #include "ast/arith_decl_plugin.h" #include "ast/array_decl_plugin.h" #include "ast/bv_decl_plugin.h" @@ -453,7 +454,7 @@ struct check_logic::imp { else if (fid == m_dt_util.get_family_id() && m_dt) { // nothing to check } - else if (fid == m_pb_util.get_family_id() && m_logic == "QF_FD") { + else if (fid == m_pb_util.get_family_id() && smt_logics::logic_has_pb(m_logic)) { // nothing to check } else { diff --git a/src/solver/smt_logics.cpp b/src/solver/smt_logics.cpp index 5d845b78b..59a9a1562 100644 --- a/src/solver/smt_logics.cpp +++ b/src/solver/smt_logics.cpp @@ -150,7 +150,7 @@ bool smt_logics::logic_has_horn(symbol const& s) { } bool smt_logics::logic_has_pb(symbol const& s) { - return s == "QF_FD" || s == "ALL" || s == "HORN"; + return s == "QF_FD" || s == "ALL" || logic_has_horn(s); } bool smt_logics::logic_has_datatype(symbol const& s) {