Merge branch 'prepost-WIP' into prepost

Author: MortenSchou

src/CMakeLists.txt

@@ -17,7 +17,7 @@ include_directories(${Boost_INCLUDE_DIR})
 add_executable(aalwines ${HEADER_FILES} main.cpp model/builders/JuniperBuilder.cpp model/builders/PRexBuilder.cpp
     model/Router.cpp model/RoutingTable.cpp model/Query.cpp model/Network.cpp model/filter.cpp model/NetworkPDAFactory.cpp
     ${BISON_bparser_OUTPUTS} ${FLEX_flexer_OUTPUTS} query/QueryBuilder.cpp 
-    pdaaal/model/PDA.cpp pdaaal/engine/Moped.cpp pdaaal/engine/UntypedPAutomaton.cpp
+    pdaaal/model/PDA.cpp pdaaal/engine/Moped.cpp pdaaal/engine/PAutomaton.cpp
     utils/parsing.cpp utils/system.cpp)
 add_dependencies(aalwines ptrie-ext rapidxml-ext)
 target_link_libraries(aalwines PRIVATE ${Boost_LIBRARIES})

src/main.cpp

@@ -34,8 +34,7 @@
 #include "query/parsererrors.h"
 #include "pdaaal/model/PDAFactory.h"
 #include "pdaaal/engine/Moped.h"
-#include "pdaaal/engine/PostStar.h"
-#include "pdaaal/engine/PreStar.h"
+#include "pdaaal/engine/Solver.h"
 
 #include "utils/stopwatch.h"
 #include "utils/outcome.h"
@@ -246,8 +245,7 @@ int main(int argc, const char** argv)
             std::cout << "\t\"answers\":{\n";
         }
         Moped moped;
-        PostStar post_star;
-        PreStar pre_star;
+        Solver solver;
 
         for(auto& q : builder._result)
         {
@@ -286,6 +284,7 @@ int main(int argc, const char** argv)
                     verification_time.start();
                     bool engine_outcome;
                     bool need_trace = was_dual || get_trace;
+                    Solver::res_type solver_result;
                     switch(engine)
                     {
                     case 1:
@@ -299,21 +298,23 @@ int main(int argc, const char** argv)
                         }
                         break;
                     case 2:
-                        engine_outcome = post_star.verify(pda, need_trace);
+                        solver_result = solver.post_star(pda, need_trace);
+                        engine_outcome = solver_result.first;
                         verification_time.stop();
                         if(need_trace && engine_outcome)
                         {
-                            trace = post_star.get_trace(pda);
+                            trace = solver.get_trace(pda, std::move(solver_result.second));
                             if(factory->write_json_trace(proof, trace))
                                 result = utils::YES;
                         }
                         break;
                     case 3:
-                        engine_outcome = pre_star.verify(pda, need_trace);
+                        solver_result = solver.pre_star(pda, need_trace);
+                        engine_outcome = solver_result.first;
                         verification_time.stop();
                         if(need_trace && engine_outcome)
                         {
-                            trace = pre_star.get_trace(pda);
+                            trace = solver.get_trace(pda, std::move(solver_result.second));
                             if(factory->write_json_trace(proof, trace))
                                 result = utils::YES;
                         }

src/model/Network.cpp

@@ -358,6 +358,7 @@ namespace aalwines
         for(auto& r : _routers)
         {
             if(r->is_null()) continue;
+            if(r->interfaces().empty()) continue;
             s << "    <router name=\"" << r->name() << "\">\n";
             s << "      <interfaces>\n";
             for(auto& inf : r->interfaces())

src/model/Query.h

@@ -52,7 +52,7 @@ namespace aalwines {
             uint8_t _mask = 0;
             uint64_t _value = 0;               
         public:
-            friend class ptrie::byte_iterator<label_t>;
+            friend struct ptrie::byte_iterator<label_t>;
             label_t()
             {
                 _type = NONE;