mirror of
https://github.com/Z3Prover/z3
synced 2025-11-03 04:57:52 +00:00
outline of parameter thread
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
85c9d9ed27
commit
cfb3ece846
2 changed files with 15 additions and 0 deletions
|
|
@ -25,6 +25,7 @@ Author:
|
||||||
#include "smt/smt_parallel.h"
|
#include "smt/smt_parallel.h"
|
||||||
#include "smt/smt_lookahead.h"
|
#include "smt/smt_lookahead.h"
|
||||||
#include "solver/solver_preprocess.h"
|
#include "solver/solver_preprocess.h"
|
||||||
|
// #include "params/smt_parallel_params.hpp"
|
||||||
|
|
||||||
#include <cmath>
|
#include <cmath>
|
||||||
#include <mutex>
|
#include <mutex>
|
||||||
|
|
|
||||||
|
|
@ -100,6 +100,20 @@ namespace smt {
|
||||||
lbool get_result() const;
|
lbool get_result() const;
|
||||||
};
|
};
|
||||||
|
|
||||||
|
// life cycle of
|
||||||
|
// 1. proof prefix with cubes
|
||||||
|
// 2. restart N separate contexts to check N new permutations of parameters.
|
||||||
|
// - one of the contexts uses the current configuration.
|
||||||
|
// 3. pick winner configuration if any are better than current.
|
||||||
|
// 4. update current configuration with the winner
|
||||||
|
|
||||||
|
class parameter_generator_thread {
|
||||||
|
unsigned N; // number of prefix permutation testers
|
||||||
|
scoped_ptr<context> prefix_solver;
|
||||||
|
scoped_ptr_vector<context> testers; // N testers
|
||||||
|
|
||||||
|
};
|
||||||
|
|
||||||
class worker {
|
class worker {
|
||||||
struct config {
|
struct config {
|
||||||
unsigned m_threads_max_conflicts = 1000;
|
unsigned m_threads_max_conflicts = 1000;
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue