ensure that FD logic understands pb from command context

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/pb_decl_plugin.cpp

@@ -91,7 +91,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) {
+    if (logic == symbol::null || logic == "QF_FD") {
         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));

src/cmd_context/check_logic.cpp

@@ -21,6 +21,7 @@ Revision History:
 #include"array_decl_plugin.h"
 #include"bv_decl_plugin.h"
 #include"seq_decl_plugin.h"
+#include"pb_decl_plugin.h"
 #include"datatype_decl_plugin.h"
 #include"ast_pp.h"
 #include"for_each_expr.h"
@@ -34,6 +35,7 @@ struct check_logic::imp {
     array_util    m_ar_util;
     seq_util      m_seq_util;
     datatype_util m_dt_util;
+    pb_util       m_pb_util;
     bool          m_uf;        // true if the logic supports uninterpreted functions
     bool          m_arrays;    // true if the logic supports arbitrary arrays
     bool          m_bv_arrays; // true if the logic supports only bv arrays
@@ -45,7 +47,7 @@ struct check_logic::imp {
     bool          m_quantifiers; // true if the logic supports quantifiers
     bool          m_unknown_logic;
 
-    imp(ast_manager & _m):m(_m), m_a_util(m), m_bv_util(m), m_ar_util(m), m_seq_util(m), m_dt_util(m) {
+    imp(ast_manager & _m):m(_m), m_a_util(m), m_bv_util(m), m_ar_util(m), m_seq_util(m), m_dt_util(m), m_pb_util(m) {
         reset();
     }
 
@@ -443,6 +445,9 @@ struct check_logic::imp {
         else if (fid == m_dt_util.get_family_id() && m_logic == "QF_FD") {
             // nothing to check
         }
+        else if (fid == m_pb_util.get_family_id() && m_logic == "QF_FD") {
+            // nothing to check
+        }
         else {
             std::stringstream strm;
             strm << "logic does not support theory " << m.get_family_name(fid);

src/cmd_context/cmd_context.cpp

@@ -519,6 +519,10 @@ bool cmd_context::logic_has_seq() const {
     return !has_logic() || smt_logics::logic_has_seq(m_logic);
 }
 
+bool cmd_context::logic_has_pb() const {
+    return !has_logic() || smt_logics::logic_has_pb(m_logic);
+}
+
 bool cmd_context::logic_has_fpa() const {
     return !has_logic() || smt_logics::logic_has_fpa(m_logic);
 }
@@ -547,7 +551,7 @@ void cmd_context::init_manager_core(bool new_manager) {
         register_plugin(symbol("array"),    alloc(array_decl_plugin), logic_has_array());
         register_plugin(symbol("datatype"), alloc(datatype_decl_plugin), logic_has_datatype());
         register_plugin(symbol("seq"),      alloc(seq_decl_plugin), logic_has_seq());
-        register_plugin(symbol("pb"),     alloc(pb_decl_plugin), !has_logic());
+        register_plugin(symbol("pb"),       alloc(pb_decl_plugin), logic_has_pb());
         register_plugin(symbol("fpa"),      alloc(fpa_decl_plugin), logic_has_fpa());
         register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin), !has_logic());
     }
@@ -563,6 +567,7 @@ void cmd_context::init_manager_core(bool new_manager) {
         load_plugin(symbol("datatype"), logic_has_datatype(), fids);
         load_plugin(symbol("seq"),      logic_has_seq(), fids);
         load_plugin(symbol("fpa"),      logic_has_fpa(), fids);
+        load_plugin(symbol("pb"),       logic_has_pb(), fids);
 
         svector<family_id>::iterator it  = fids.begin();
         svector<family_id>::iterator end = fids.end();

src/cmd_context/cmd_context.h

@@ -251,6 +251,7 @@ protected:
 
     bool logic_has_arith() const;
     bool logic_has_bv() const;
+    bool logic_has_pb() const;
     bool logic_has_seq() const;
     bool logic_has_array() const;
     bool logic_has_datatype() const;

src/solver/smt_logics.cpp

@@ -144,6 +144,10 @@ bool smt_logics::logic_has_horn(symbol const& s) {
     return s == "HORN";
 }
 
+bool smt_logics::logic_has_pb(symbol const& s) {
+    return s == "QF_FD" || s == "ALL";
+}
+
 bool smt_logics::logic_has_datatype(symbol const& s) {
     return s == "QF_FD";
 }

src/solver/smt_logics.h

@@ -32,6 +32,7 @@ public:
     static bool logic_has_seq(symbol const & s);
     static bool logic_has_fpa(symbol const & s);
     static bool logic_has_horn(symbol const& s);
+    static bool logic_has_pb(symbol const& s);
     static bool logic_has_fd(symbol const& s) { return s == "QF_FD"; }
     static bool logic_has_datatype(symbol const& s);
 };