mirror of
https://github.com/Z3Prover/z3
synced 2025-08-06 03:10:25 +00:00
check pb solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
e76cea4684
commit
a2dddbd7a5
3 changed files with 8 additions and 31 deletions
|
@ -52,15 +52,6 @@ namespace sat {
|
|||
BH_LRB
|
||||
};
|
||||
|
||||
enum pb_solver {
|
||||
PB_SOLVER,
|
||||
PB_CIRCUIT,
|
||||
PB_SORTING,
|
||||
PB_TOTALIZER,
|
||||
PB_SEGMENTED,
|
||||
PB_BINARY_MERGE
|
||||
};
|
||||
|
||||
enum pb_resolve {
|
||||
PB_CARDINALITY,
|
||||
PB_ROUNDING
|
||||
|
@ -183,9 +174,6 @@ namespace sat {
|
|||
void updt_params(params_ref const & p);
|
||||
static void collect_param_descrs(param_descrs & d);
|
||||
|
||||
private:
|
||||
pb_solver m_pb_solver;
|
||||
|
||||
};
|
||||
};
|
||||
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue