From f091b6ffddf3d5cd8c9dee5a4bfa53031b61765e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 16 Mar 2025 19:14:29 -0700 Subject: [PATCH] remove 'unsat' move, we already have 'conflict'. Add display for cancelled Signed-off-by: Nikolaj Bjorner --- src/math/lp/lia_move.h | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/src/math/lp/lia_move.h b/src/math/lp/lia_move.h index a0cc7f627..faac17dde 100644 --- a/src/math/lp/lia_move.h +++ b/src/math/lp/lia_move.h @@ -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)