mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
adding interval designator to output of non-optimal objectives, fix python doc test
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
8032217fd1
commit
a048d74bae
|
@ -6194,7 +6194,7 @@ class Solver(Z3PPObject):
|
|||
>>> s.consequences([a],[b,c,d])
|
||||
(sat, [Implies(a, b), Implies(a, c)])
|
||||
>>> s.consequences([Not(c),d],[a,b,c,d])
|
||||
(sat, [Implies(Not(c), Not(c)), Implies(d, d), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])
|
||||
(sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])
|
||||
"""
|
||||
if isinstance(assumptions, list):
|
||||
_asms = AstVector(None, self.ctx)
|
||||
|
|
|
@ -1235,7 +1235,7 @@ namespace opt {
|
|||
out << " (";
|
||||
display_objective(out, obj);
|
||||
if (get_lower_as_num(i) != get_upper_as_num(i)) {
|
||||
out << " (" << get_lower(i) << " " << get_upper(i) << ")";
|
||||
out << " (interval " << get_lower(i) << " " << get_upper(i) << ")";
|
||||
}
|
||||
else {
|
||||
out << " " << get_lower(i);
|
||||
|
|
Loading…
Reference in a new issue