mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
pareto take 3
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
a307bd67e0
commit
8d0d123a4c
|
@ -306,12 +306,15 @@ private:
|
|||
}
|
||||
|
||||
void decompose(goal_ref const& g) {
|
||||
#if 0
|
||||
// TBD
|
||||
for (unsigned i = 0; !g->inconsistent() && i < g->size(); ++i) {
|
||||
expr* e = g->form(i);
|
||||
if (pb.is_ge(e) && to_app(e)->get_num_args() > 20) {
|
||||
// TBD: decompose inequality int smaller ones.
|
||||
}
|
||||
}
|
||||
#endif
|
||||
}
|
||||
|
||||
void process_vars(unsigned i, goal_ref const& g) {
|
||||
|
|
Loading…
Reference in a new issue