From 4dc71acde0493aa4462b96ca5be0a650e6ba35aa Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 9 May 2014 11:31:54 -0700
Subject: [PATCH] add logging
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/opt/maxsmt.cpp | 1 +
src/opt/opt_context.cpp | 1 +
src/opt/optsmt.cpp | 1 +
3 files changed, 3 insertions(+)
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index 1f43bbe36..dd0171c6a 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -32,6 +32,7 @@ namespace opt {
m_msolver = 0;
m_s = s;
IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";);
+ TRACE("opt", tout << "maxsmt\n";);
if (m_soft_constraints.empty()) {
TRACE("opt", tout << "no constraints\n";);
m_msolver = 0;
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 7b9ca0a8d..ceab047b7 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -145,6 +145,7 @@ namespace opt {
IF_VERBOSE(1, verbose_stream() << "(optimize:check-sat)\n";);
lbool is_sat = s.check_sat_core(0,0);
+ TRACE("opt", tout << "initial search result: " << is_sat << "\n";);
if (is_sat != l_true) {
m_model = 0;
return is_sat;
diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp
index e5370e82d..980ad7037 100644
--- a/src/opt/optsmt.cpp
+++ b/src/opt/optsmt.cpp
@@ -235,6 +235,7 @@ namespace opt {
lbool optsmt::lex(unsigned obj_index) {
IF_VERBOSE(1, verbose_stream() << "(optsmt:lex)\n";);
+ TRACE("opt", tout << "optsmt:lex\n";);
solver::scoped_push _push(*m_s);
SASSERT(obj_index < m_vars.size());
return basic_lex(obj_index);