fix lexicographic combinations for wmax: pb constrsaints were not interpreted in Boolean benchmarks. #782

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

src/ast/pb_decl_plugin.h

@@ -73,6 +73,8 @@ public:
                                      unsigned arity, sort * const * domain, sort * range);
     virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
 
+    virtual bool is_considered_uninterpreted(func_decl * f) { return false; }
+
 };
 
 

src/muz/pdr/pdr_context.cpp

@@ -1760,6 +1760,7 @@ namespace pdr {
                 smt::kernel solver(m, get_fparams());
                 solver.assert_expr(tmp);
                 lbool res = solver.check();
+                TRACE("pdr", tout << tmp << " " << res << "\n";);
                 if (res != l_false) {
                     msg << "rule validation failed when checking: " << mk_pp(tmp, m);
                     IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";);

src/opt/maxsmt.cpp

@@ -25,6 +25,7 @@ Notes:
 #include "uint_set.h"
 #include "opt_context.h"
 #include "theory_wmaxsat.h"
+#include "theory_pb.h"
 #include "ast_util.h"
 #include "pb_decl_plugin.h"
 
@@ -124,6 +125,13 @@ namespace opt {
             wth = alloc(smt::theory_wmaxsat, m, m_c.fm());
             m_c.smt_context().register_plugin(wth);
         }
+        smt::theory_id th_pb = m.get_family_id("pb");
+        smt::theory_pb* pb = dynamic_cast<smt::theory_pb*>(m_c.smt_context().get_theory(th_pb));
+        if (!pb) {
+            theory_pb_params params;
+            pb = alloc(smt::theory_pb, m, params);
+            m_c.smt_context().register_plugin(pb);
+        }
         return wth;
     }
 

src/smt/theory_pb.h

@@ -316,6 +316,7 @@ namespace smt {
         virtual void collect_statistics(::statistics & st) const;
         virtual model_value_proc * mk_value(enode * n, model_generator & mg);
         virtual void init_model(model_generator & m);        
+        virtual bool include_func_interp(func_decl* f) { return false; }
 
         static literal assert_ge(context& ctx, unsigned k, unsigned n, literal const* xs);
     };