From f1ebf2002ade0bb141bddf01d5c918ec986a4b44 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 5 May 2014 16:40:54 -0700 Subject: [PATCH] tuning sls Signed-off-by: Nikolaj Bjorner --- src/duality/duality.h | 2 +- src/duality/duality_solver.cpp | 2 +- src/opt/pb_sls.cpp | 3 +++ 3 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index fc70ffa70..4005adc1a 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -29,7 +29,7 @@ using namespace stl_ext; namespace Duality { - class implicant_solver; + struct implicant_solver; /* Generic operations on Z3 formulas */ diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index ff3bc190b..c10d83603 100644 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -2201,7 +2201,7 @@ namespace Duality { #endif int expand_max = 1; if(0&&duality->BatchExpand){ - int thing = stack.size() * 0.1; + int thing = static_cast(stack.size() * 0.1); expand_max = std::max(1,thing); if(expand_max > 1) std::cout << "foo!\n"; diff --git a/src/opt/pb_sls.cpp b/src/opt/pb_sls.cpp index f04301c06..29d814a43 100644 --- a/src/opt/pb_sls.cpp +++ b/src/opt/pb_sls.cpp @@ -623,6 +623,9 @@ namespace smt { m_orig_clauses.push_back(f); return result; } + if (pb.is_ge(f)) { + + } IF_VERBOSE(0, verbose_stream() << "not handled: " << mk_pp(f, m) << "\n";); return mk_aux_literal(f); }