Merge pull request DEIS-Tools#23 from MortenSchou/prepost

Implementation of Pre* and Post*
petergjoel · Feb 14, 2020 · 69eff67 · 69eff67
2 parents f6cd25d + c8c1e28
commit 69eff67
Show file tree

Hide file tree

Showing 13 changed files with 1,191 additions and 290 deletions.
diff --git a/src/CMakeLists.txt b/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/PostStar.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})

diff --git a/src/main.cpp b/src/main.cpp
@@ -34,7 +34,7 @@
 #include "query/parsererrors.h"
 #include "pdaaal/model/PDAFactory.h"
 #include "pdaaal/engine/Moped.h"
-#include "pdaaal/engine/PostStar.h"
+#include "pdaaal/engine/Solver.h"
 
 #include "utils/stopwatch.h"
 #include "utils/outcome.h"
@@ -137,7 +137,7 @@ int main(int argc, const char** argv)
         exit(-1);
     }
 
-    if(engine > 2)
+    if(engine > 3)
     {
         std::cerr << "Unknown value for --engine : " << engine << std::endl;
         exit(-1);        
@@ -245,7 +245,7 @@ int main(int argc, const char** argv)
             std::cout << "\t\"answers\":{\n";
         }
         Moped moped;
-        PostStar post_star;
+        Solver solver;
 
         for(auto& q : builder._result)
         {
@@ -284,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:
@@ -297,17 +298,27 @@ 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:
-                        // break;
+                        solver_result = solver.pre_star(pda, need_trace);
+                        engine_outcome = solver_result.first;
+                        verification_time.stop();
+                        if(need_trace && engine_outcome)
+                        {
+                            trace = solver.get_trace(pda, std::move(solver_result.second));
+                            if(factory->write_json_trace(proof, trace))
+                                result = utils::YES;
+                        }
+                        break;
                     default:
                         throw base_error("Unsupported --engine value given");
                     }