mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

remove 'unsat' move, we already have 'conflict'. Add display for cancelled

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-03-16 19:14:29 -07:00 • committed by Lev Nachmanson
parent 1af2474f7b
commit f091b6ffdd
1 changed files with 2 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/math/lp/lia_move.h
View file

@ -28,7 +28,6 @@ namespace lp {
conflict,
continue_with_check,
undef,
unsat,
cancelled
};
inline std::string lia_move_to_string(lia_move m) {
@ -45,8 +44,8 @@ namespace lp {
return "continue_with_check";
case lia_move::undef:
return "undef";
case lia_move::unsat:
return "unsat";
case lia_move::cancelled:
return "cancelled";
default:
UNREACHABLE();
};
@ -62,8 +61,6 @@ namespace lp {
return r1;
if (r1 == lia_move::conflict || r2 == lia_move::conflict)
return lia_move::conflict;
if (r1 == lia_move::unsat || r2 == lia_move::unsat)
return lia_move::unsat;
if (r1 == lia_move::cancelled || r2 == lia_move::cancelled)
return lia_move::cancelled;
if (r1 == lia_move::sat || r2 == lia_move::sat)