From e21bd8dacc58b95c2d207092b1ec4a932b260086 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 15 Nov 2016 15:07:05 +0200
Subject: [PATCH] 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    | 2 ++
 src/muz/pdr/pdr_context.cpp | 1 +
 src/opt/maxsmt.cpp          | 8 ++++++++
 src/smt/theory_pb.h         | 1 +
 4 files changed, 12 insertions(+)

diff --git a/src/ast/pb_decl_plugin.h b/src/ast/pb_decl_plugin.h
index 2ed14a4ce..0750dcac7 100644
--- a/src/ast/pb_decl_plugin.h
+++ b/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; }
+
 };
 
 
diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index b6a889756..6d3a57581 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/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";);
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index fa4897046..7d3e8eda9 100644
--- a/src/opt/maxsmt.cpp
+++ b/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;
     }
 
diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h
index b9fddba38..1a08b7b61 100644
--- a/src/smt/theory_pb.h
+++ b/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);
     };