mirror of
https://github.com/Z3Prover/z3
synced 2025-06-19 20:33:38 +00:00
adding timeout, parameters, statistics
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
9fc84f1389
commit
946b888b32
2 changed files with 21 additions and 6 deletions
|
@ -15,13 +15,8 @@ Author:
|
||||||
Notes:
|
Notes:
|
||||||
|
|
||||||
TODO:
|
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.
|
- Add appropriate statistics tracking to opt::context
|
||||||
Also add appropriate statistics tracking to opt::context
|
|
||||||
|
|
||||||
- Deal with push/pop (later)
|
- Deal with push/pop (later)
|
||||||
|
|
||||||
|
|
|
@ -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"reg_decl_plugins.h"
|
||||||
#include"opt_solver.h"
|
#include"opt_solver.h"
|
||||||
#include"smt_context.h"
|
#include"smt_context.h"
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue