mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

let HORN solver know about cardinality constraints

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-07-02 11:46:03 -07:00
parent fcd9936e88
commit 5e3303ae85
3 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/pb_decl_plugin.cpp
View file

@ -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<builtin_name> & 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));

3
src/cmd_context/check_logic.cpp
View file

@ -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 {

2
src/solver/smt_logics.cpp
View file

@ -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) {