From fc55262575766ed73b1ff9d1e6fb5c4d617d5977 Mon Sep 17 00:00:00 2001 From: Vyom Patel Date: Thu, 27 Mar 2025 23:29:35 -0400 Subject: [PATCH] fix Glucose namespace issue --- include/easy/esop/synthesis.hpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/include/easy/esop/synthesis.hpp b/include/easy/esop/synthesis.hpp index f4f7691..5b03751 100644 --- a/include/easy/esop/synthesis.hpp +++ b/include/easy/esop/synthesis.hpp @@ -48,8 +48,8 @@ inline esop_t esop_from_model( const sat::sat_solver::model_t& model, unsigned n bool cancel_cube = false; for ( auto l = 0u; l < num_vars; ++l ) { - const auto p_value = model[j * num_vars + l] == l_True; - const auto q_value = model[num_vars * num_terms + j * num_vars + l] == l_True; + const auto p_value = model[j * num_vars + l] == Glucose::l_True; + const auto q_value = model[num_vars * num_terms + j * num_vars + l] == Glucose::l_True; if ( p_value && q_value ) { @@ -787,8 +787,8 @@ class minimum_all_synthesizer { for ( auto l = 0u; l < num_vars; ++l ) { - const auto p_value = result.model[j * num_vars + l] == l_True; - const auto q_value = result.model[num_vars * k + j * num_vars + l] == l_True; + const auto p_value = result.model[j * num_vars + l] == Glucose::l_True; + const auto q_value = result.model[num_vars * k + j * num_vars + l] == Glucose::l_True; /* do not consider all possibilities for canceled cubes */ if ( p_value && q_value )