minor refactoring..

ratioSolver · Jun 9, 2023 · ab0c716 · ab0c716
1 parent 298dfce
commit ab0c716
Show file tree

Hide file tree

Showing 6 changed files with 49 additions and 9 deletions.
diff --git a/.github/workflows/cmake.yml b/.github/workflows/cmake.yml
@@ -15,7 +15,7 @@ jobs:
         #heuristic_type: [h_max, h_add]
         #deferrable_flaws: [ON, OFF]
         #graph_pruning: [ON, OFF]
-        enum_pruning: [ON, OFF]
+        graph_refining: [ON, OFF]
         #check_inconsistencies: [ON, OFF]
         #build_listeners: [ON, OFF]
 
@@ -25,7 +25,7 @@ jobs:
       #HEURISTIC_TYPE: ${{ matrix.heuristic_type }}
       #DEFERRABLE_FLAWS: ${{ matrix.deferrable_flaws }}
       #GRAPH_PRUNING: ${{ matrix.graph_pruning }}
-      ENUM_PRUNING: ${{ matrix.enum_pruning }}
+      GRAPH_REFINING: ${{ matrix.graph_refining }}
       #CHECK_INCONSISTENCIES: ${{ matrix.check_inconsistencies }}
       #BUILD_LISTENERS: ${{ matrix.build_listeners }}
 
@@ -35,7 +35,7 @@ jobs:
           submodules: recursive
 
       - name: Configure CMake
-        run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -DENUM_PRUNING=${{env.ENUM_PRUNING}} #-DTEMPORAL_NETWORK_TYPE=${{env.TEMPORAL_NETWORK_TYPE}} -DHEURISTIC_TYPE=${{env.HEURISTIC_TYPE}} -DDEFERRABLE_FLAWS=${{env.DEFERRABLE_FLAWS}} -DGRAPH_PRUNING=${{env.GRAPH_PRUNING}} -DCHECK_INCONSISTENCIES=${{env.CHECK_INCONSISTENCIES}} -DBUILD_LISTENERS=${{env.BUILD_LISTENERS}}
+        run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -DGRAPH_REFINING=${{env.GRAPH_REFINING}} #-DTEMPORAL_NETWORK_TYPE=${{env.TEMPORAL_NETWORK_TYPE}} -DHEURISTIC_TYPE=${{env.HEURISTIC_TYPE}} -DDEFERRABLE_FLAWS=${{env.DEFERRABLE_FLAWS}} -DGRAPH_PRUNING=${{env.GRAPH_PRUNING}} -DCHECK_INCONSISTENCIES=${{env.CHECK_INCONSISTENCIES}} -DBUILD_LISTENERS=${{env.BUILD_LISTENERS}}
 
       - name: Build
         run: cmake --build ${{github.workspace}}/build --config ${{env.BUILD_TYPE}}

diff --git a/include/flaws/atom_flaw.h b/include/flaws/atom_flaw.h
@@ -59,6 +59,9 @@ namespace ratio
       semitone::lit unif_lit;
     };
 
+  public:
+    static bool is_unification(const resolver &r) noexcept { return dynamic_cast<const unify_atom *>(&r) != nullptr; }
+
   private:
     riddle::expr atm;
   };

diff --git a/include/graph.h b/include/graph.h
@@ -66,6 +66,13 @@ namespace ratio
     virtual void prune() {}
 #endif
 
+#ifdef GRAPH_REFINING
+    /**
+     * @brief Refines the causal graph.
+     */
+    virtual void refine() {}
+#endif
+
     virtual void push() {}
     virtual void pop() {}
 

diff --git a/include/heuristics/h_1.h b/include/heuristics/h_1.h
@@ -27,7 +27,8 @@ namespace ratio
 #endif
 
 #ifdef GRAPH_REFINING
-    void graph_refining();
+    void refine() override;
+    void prune_enums();
 #endif
 
     bool is_deferrable(flaw &f); // checks whether the given flaw is deferrable..

diff --git a/src/graph.cpp b/src/graph.cpp
@@ -35,6 +35,10 @@ namespace ratio
 #endif
             // we take `gamma` decision..
             s.take_decision(semitone::lit(gamma));
+#ifdef GRAPH_REFINING
+            // we refine the graph..
+            refine();
+#endif
         }
     }
 

diff --git a/src/heuristics/h_1.cpp b/src/heuristics/h_1.cpp
@@ -1,6 +1,7 @@
 #include "h_1.h"
 #include "solver.h"
 #include "enum_flaw.h"
+#include "atom_flaw.h"
 #include <cassert>
 
 namespace ratio
@@ -61,6 +62,14 @@ namespace ratio
                         expand_flaw(f);
                         if (auto e_f = dynamic_cast<enum_flaw *>(&f))
                             enum_flaws.insert(e_f);
+                        else if (auto a_f = dynamic_cast<atom_flaw *>(&f))
+                            for (const auto &r : a_f->get_resolvers())
+                                if (atom_flaw::is_unification(r.get()))
+                                {
+                                    auto &l = static_cast<atom_flaw &>(r.get().get_preconditions().front().get());
+                                    if (s.get_sat_core().value(l.get_phi()) == utils::Undefined)
+                                        landmarks.insert(&l);
+                                }
                     }
                 }
                 flaw_q.pop_front();
@@ -69,7 +78,7 @@ namespace ratio
             // we extract the inconsistencies (and translate them into flaws)..
             get_incs();
 #ifdef GRAPH_REFINING
-            graph_refining();
+            prune_enums();
 #endif
         } while (std::any_of(get_active_flaws().cbegin(), get_active_flaws().cend(), [](const auto &f)
                              { return is_positive_infinite(f->get_estimated_cost()); }));
@@ -106,14 +115,22 @@ namespace ratio
                     expand_flaw(f);
                     if (auto e_f = dynamic_cast<enum_flaw *>(&f))
                         enum_flaws.insert(e_f);
+                    else if (auto a_f = dynamic_cast<atom_flaw *>(&f))
+                        for (const auto &r : a_f->get_resolvers())
+                            if (atom_flaw::is_unification(r.get()))
+                            {
+                                auto &l = static_cast<atom_flaw &>(r.get().get_preconditions().front().get());
+                                if (s.get_sat_core().value(l.get_phi()) == utils::Undefined)
+                                    landmarks.insert(&l);
+                            }
                 }
                 flaw_q.pop_front();
             }
 
             // we extract the inconsistencies (and translate them into flaws)..
             get_incs();
 #ifdef GRAPH_REFINING
-            graph_refining();
+            prune_enums();
 #endif
         }
 
@@ -144,12 +161,20 @@ namespace ratio
 #endif
 
 #ifdef GRAPH_REFINING
-    void h_1::graph_refining()
+    void h_1::refine()
     {
-        LOG("refining the causal graph..");
+        LOG("checking landmarks..");
+        for (const auto l : landmarks)
+            if (s.get_sat_core().value(l->get_phi()) == utils::Undefined)
+                s.get_sat_core().check({!l->get_phi()});
+    }
+
+    void h_1::prune_enums()
+    {
+        LOG("checking enums..");
         for (const auto e_f : enum_flaws)
             for (const auto &r : e_f->get_resolvers())
-                if (s.get_sat_core().value(r.get().get_rho()) != utils::False)
+                if (s.get_sat_core().value(r.get().get_rho()) == utils::Undefined)
                     s.get_sat_core().check({r.get().get_rho()});
     }
 #endif