From 8eeaa27cf34eeba7e8c832e83362e11f439ff282 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 25 May 2018 07:33:43 -0700
Subject: [PATCH] remove interp from documentation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 doc/mk_api_doc.py       | 1 -
 src/opt/opt_context.cpp | 9 ++++++---
 src/opt/opt_pareto.cpp  | 7 ++++---
 src/smt/theory_pb.cpp   | 2 +-
 4 files changed, 11 insertions(+), 8 deletions(-)

diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py
index a1a9e64bd..bfe865e06 100644
--- a/doc/mk_api_doc.py
+++ b/doc/mk_api_doc.py
@@ -272,7 +272,6 @@ try:
     cleanup_API(doc_path('../src/api/z3_rcf.h'), temp_path('z3_rcf.h'))
     cleanup_API(doc_path('../src/api/z3_fixedpoint.h'), temp_path('z3_fixedpoint.h'))
     cleanup_API(doc_path('../src/api/z3_optimization.h'), temp_path('z3_optimization.h'))
-    cleanup_API(doc_path('../src/api/z3_interp.h'), temp_path('z3_interp.h'))
     cleanup_API(doc_path('../src/api/z3_fpa.h'), temp_path('z3_fpa.h'))
 
     print("Removed annotations from z3_api.h.")
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index e5f4bc133..004a83a14 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -497,7 +497,7 @@ namespace opt {
         case O_MINIMIZE:
             is_ge = !is_ge;
         case O_MAXIMIZE:
-            if (mdl->eval(obj.m_term, val) && is_numeral(val, k)) {
+            if (mdl->eval(obj.m_term, val, true) && is_numeral(val, k)) {
                 if (is_ge) {
                     result = mk_ge(obj.m_term, val);
                 }
@@ -517,9 +517,12 @@ namespace opt {
             for (unsigned i = 0; i < sz; ++i) {
                 terms.push_back(obj.m_terms[i]);
                 coeffs.push_back(obj.m_weights[i]);
-                if (mdl->eval(obj.m_terms[i], val) && m.is_true(val)) {
+                if (mdl->eval(obj.m_terms[i], val, true) && m.is_true(val)) {
                     k += obj.m_weights[i];
                 }
+                else {
+                    TRACE("opt", tout << val << "\n";);
+                }
             }
             if (is_ge) {
                 result = pb.mk_ge(sz, coeffs.c_ptr(), terms.c_ptr(), k);
@@ -1044,7 +1047,7 @@ namespace opt {
         model_ref mdl = md->copy();
         fix_model(mdl);
 
-        if (!mdl->eval(term, val)) {
+        if (!mdl->eval(term, val, true)) {
             TRACE("opt", tout << "Term does not evaluate " << term << "\n";);
             return false;
         }
diff --git a/src/opt/opt_pareto.cpp b/src/opt/opt_pareto.cpp
index c316e697e..56eed72ac 100644
--- a/src/opt/opt_pareto.cpp
+++ b/src/opt/opt_pareto.cpp
@@ -20,6 +20,7 @@ Notes:
 
 #include "opt/opt_pareto.h"
 #include "ast/ast_pp.h"
+#include "ast/ast_util.h"
 #include "model/model_smt2_pp.h"
 
 namespace opt {
@@ -66,8 +67,8 @@ namespace opt {
             fmls.push_back(cb.mk_ge(i, m_model));
             gt.push_back(cb.mk_gt(i, m_model));
         }
-        fmls.push_back(m.mk_or(gt.size(), gt.c_ptr()));
-        fml = m.mk_and(fmls.size(), fmls.c_ptr());
+        fmls.push_back(mk_or(gt));
+        fml = mk_and(fmls);
         IF_VERBOSE(10, verbose_stream() << "dominates: " << fml << "\n";);
         TRACE("opt", tout << fml << "\n"; model_smt2_pp(tout, m, *m_model, 0););
         m_solver->assert_expr(fml);        
@@ -80,7 +81,7 @@ namespace opt {
         for (unsigned i = 0; i < sz; ++i) {
             le.push_back(cb.mk_le(i, m_model));
         }
-        fml = m.mk_not(m.mk_and(le.size(), le.c_ptr()));
+        fml = m.mk_not(mk_and(le));
         IF_VERBOSE(10, verbose_stream() << "not dominated by: " << fml << "\n";);
         TRACE("opt", tout << fml << "\n";);
         m_solver->assert_expr(fml);        
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 9fc33a6a9..d45590bff 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -2007,7 +2007,7 @@ namespace smt {
         if (m_bound > static_cast<int>(m_active_vars.size())) {
             return;
         }           
-        if (m_bound == m_active_vars.size()) {
+        if (m_bound == static_cast<int>(m_active_vars.size())) {
             return;
         }