From a0b5f6937bcc8c2f38ac5dd524d9db28e4418478 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 8 Feb 2018 10:05:26 -0800 Subject: [PATCH] fix bugs, add soft timeout to opt frontend Signed-off-by: Nikolaj Bjorner --- src/sat/sat_big.cpp | 7 ++++--- src/shell/opt_frontend.cpp | 7 +++++++ 2 files changed, 11 insertions(+), 3 deletions(-) diff --git a/src/sat/sat_big.cpp b/src/sat/sat_big.cpp index 1845a9632..a59deeafd 100644 --- a/src/sat/sat_big.cpp +++ b/src/sat/sat_big.cpp @@ -52,11 +52,12 @@ namespace sat { for (unsigned i = 0; i < r.size(); ++i) { literal u = r[i]; for (unsigned j = i + 1; j < r.size(); ++j) { - // add r[i] -> ~r[j] - literal v = ~r[j]; + // add ~r[i] -> r[j] + literal v = r[j]; + literal u = ~r[j]; m_roots[v.index()] = false; m_dag[u.index()].push_back(v); - // add r[j] -> ~r[i] + // add ~r[j] -> r[i] v.neg(); u.neg(); m_roots[u.index()] = false; diff --git a/src/shell/opt_frontend.cpp b/src/shell/opt_frontend.cpp index 8ce573e9a..9509db760 100644 --- a/src/shell/opt_frontend.cpp +++ b/src/shell/opt_frontend.cpp @@ -9,6 +9,8 @@ Copyright (c) 2015 Microsoft Corporation #include #include "util/gparams.h" #include "util/timeout.h" +#include "util/cancel_eh.h" +#include "util/scoped_timer.h" #include "ast/ast_util.h" #include "ast/arith_decl_plugin.h" #include "ast/ast_pp.h" @@ -101,6 +103,11 @@ static unsigned parse_opt(std::istream& in, opt_format f) { break; } try { + cancel_eh eh(m.limit()); + unsigned timeout = std::stoi(gparams::get_value("timeout")); + unsigned rlimit = std::stoi(gparams::get_value("rlimit")); + scoped_timer timer(timeout, &eh); + scoped_rlimit _rlimit(m.limit(), rlimit); lbool r = opt.optimize(); switch (r) { case l_true: std::cout << "sat\n"; break;