Enhance solver logic by adding new clause creation for false values a…

…nd update GOAC test cases in CMakeLists.txt
ratioSolver · Nov 13, 2024 · 7a150e6 · 7a150e6
1 parent 3220eab
commit 7a150e6
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 4 deletions.
diff --git a/src/types/reusable_resource.cpp b/src/types/reusable_resource.cpp
@@ -213,6 +213,11 @@ namespace ratio
                 leqs[atm.get()][&c_atm.get()] = before;
             if (get_solver().get_sat().value(after) == utils::Undefined)
                 leqs[&c_atm.get()][atm.get()] = after;
+            if (get_solver().get_sat().value(before) == utils::False || get_solver().get_sat().value(after) == utils::False)
+            {
+                [[maybe_unused]] auto nc = get_solver().get_sat().new_clause({!atm->get_sigma(), !c_atm.get().get_sigma(), before, after});
+                assert(nc);
+            }
         }
 
         const auto tau = atm->get(riddle::TAU_NAME);

diff --git a/src/types/state_variable.cpp b/src/types/state_variable.cpp
@@ -149,6 +149,11 @@ namespace ratio
                 leqs[atm.get()][&c_atm.get()] = before;
             if (get_solver().get_sat().value(after) == utils::Undefined)
                 leqs[&c_atm.get()][atm.get()] = after;
+            if (get_solver().get_sat().value(before) == utils::False || get_solver().get_sat().value(after) == utils::False)
+            {
+                [[maybe_unused]] auto nc = get_solver().get_sat().new_clause({!atm->get_sigma(), !c_atm.get().get_sigma(), before, after});
+                assert(nc);
+            }
         }
 
         const auto tau = atm->get(riddle::TAU_NAME);

diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt
@@ -59,10 +59,10 @@ if(TEMPORAL_NETWORK_TYPE STREQUAL LRA)
     add_test(NAME GOAC_4Pic_4Wind COMMAND solver_tests "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/goac_domain.rddl" "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/map.rddl" "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/goac_4pic_4wind.rddl" "solution.json")
     add_test(NAME GOAC_4Pic_5Wind COMMAND solver_tests "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/goac_domain.rddl" "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/map.rddl" "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/goac_4pic_5wind.rddl" "solution.json")
     add_test(NAME GOAC_5Pic_1Wind COMMAND solver_tests "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/goac_domain.rddl" "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/map.rddl" "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/goac_5pic_1wind.rddl" "solution.json")
-    #add_test(NAME GOAC_5Pic_2Wind COMMAND solver_tests "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/goac_domain.rddl" "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/map.rddl" "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/goac_5pic_2wind.rddl" "solution.json")
-    #add_test(NAME GOAC_5Pic_3Wind COMMAND solver_tests "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/goac_domain.rddl" "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/map.rddl" "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/goac_5pic_3wind.rddl" "solution.json")
-    #add_test(NAME GOAC_5Pic_4Wind COMMAND solver_tests "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/goac_domain.rddl" "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/map.rddl" "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/goac_5pic_4wind.rddl" "solution.json")
-    #add_test(NAME GOAC_5Pic_5Wind COMMAND solver_tests "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/goac_domain.rddl" "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/map.rddl" "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/goac_5pic_5wind.rddl" "solution.json")
+    add_test(NAME GOAC_5Pic_2Wind COMMAND solver_tests "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/goac_domain.rddl" "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/map.rddl" "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/goac_5pic_2wind.rddl" "solution.json")
+    add_test(NAME GOAC_5Pic_3Wind COMMAND solver_tests "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/goac_domain.rddl" "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/map.rddl" "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/goac_5pic_3wind.rddl" "solution.json")
+    add_test(NAME GOAC_5Pic_4Wind COMMAND solver_tests "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/goac_domain.rddl" "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/map.rddl" "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/goac_5pic_4wind.rddl" "solution.json")
+    add_test(NAME GOAC_5Pic_5Wind COMMAND solver_tests "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/goac_domain.rddl" "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/map.rddl" "${PROJECT_SOURCE_DIR}/extern/riddle/examples/goac/goac_5pic_5wind.rddl" "solution.json")
 
     #add_test(NAME Logistics_0 COMMAND solver_tests "${PROJECT_SOURCE_DIR}/extern/riddle/examples/logistics/logistics_domain.rddl" "${PROJECT_SOURCE_DIR}/extern/riddle/examples/logistics/logistics_problem_0.rddl" "solution.json")
     #add_test(NAME Logistics_1 COMMAND solver_tests "${PROJECT_SOURCE_DIR}/extern/riddle/examples/logistics/logistics_domain.rddl" "${PROJECT_SOURCE_DIR}/extern/riddle/examples/logistics/logistics_problem_1.rddl" "solution.json")