From 946b888b32d79e783e9793ff8bcbd4c491f2858e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 30 Oct 2013 13:24:21 -0700 Subject: [PATCH] adding timeout, parameters, statistics Signed-off-by: Nikolaj Bjorner --- src/opt/opt_cmds.cpp | 7 +------ src/opt/opt_solver.cpp | 20 ++++++++++++++++++++ 2 files changed, 21 insertions(+), 6 deletions(-) diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index 01d8b833e..5acbec9dd 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -15,13 +15,8 @@ Author: Notes: TODO: - - integrate with parameters. - Parameter infrastructure lets us control setttings, such as - timeouts and control which backend optimization approach to - use during experiments. - - Display statistics properly on exit when configured to do so. - Also add appropriate statistics tracking to opt::context + - Add appropriate statistics tracking to opt::context - Deal with push/pop (later) diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 5cde65cdb..64d8a32be 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -1,3 +1,23 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + opt_solver.cpp + +Abstract: + + Wraps smt::kernel as a solver for optimization + +Author: + + Anh-Dung Phan (t-anphan) 2013-10-16 + +Notes: + + Based directly on smt_solver. + +--*/ #include"reg_decl_plugins.h" #include"opt_solver.h" #include"smt_context.h"