merge SAT verifier

.gitignore

@@ -0,0 +1,3 @@
+build/
+.vscode/
+cmdline.*

src/.gitignore

@@ -0,0 +1,6 @@
+.vscode/
+build/
+cmake-build-debug
+cmake-build-*
+.idea/
+src/.idea

src/CMakeLists.txt

@@ -115,3 +115,6 @@ endif (SAT)
 
 ## must be added *after* SAT due to the use of the printMemory function, which is currently defined in the SAT module ... this is probably not a good idea.
 target_link_libraries(pandaPIengine PUBLIC intDataStructures)
+
+# add plan verifiers
+add_subdirectory(verifier)

src/sat/CMakeLists.txt

@@ -1,7 +1,16 @@
 file(GLOB sat_SRC "*.h" "*.cpp")
 
-add_library(sat ${sat_SRC})
+add_library(sat
+        ${sat_SRC}
+        ${pandaPIengine_SOURCE_DIR}/Util.cpp
+        ${pandaPIengine_SOURCE_DIR}/Debug.cpp
+        ${pandaPIengine_SOURCE_DIR}/Invariants.cpp)
+
 target_compile_options(sat PUBLIC ${compiler_flags})
 target_link_options(sat PUBLIC ${linker_flags})
+target_include_directories(sat
+        PUBLIC
+            ${pandaPIengine_SOURCE_DIR}/)
 
+find_package(cryptominisat5)
 target_link_libraries(sat ipasircryptominisat5)

src/sat/pdt.cpp

@@ -4,7 +4,7 @@
 #include <bitset>
 #include "pdt.h"
 #include "ipasir.h"
-#include "../Util.h"
+#include "Util.h"
 
 void printMemory();
 
@@ -675,12 +675,12 @@ void PDT::printDecomposition(Model * htn){
 	if (outputTask < htn->numActions) return;
 
 	cout << outputID << " " << htn->taskNames[outputTask] << " -> " << 
-		htn->methodNames[outputMethod];
+		htn->methodNames[outputMethod] << endl;
 
 	// output children
 	for (PDT* & child : children){
 		int sub = child->getNextOutputTask();
-		if (sub != -1) cout << " " << sub;
+		if (sub != -1) cout << "- " << sub << " " << htn->taskNames[child->outputTask] << endl;
 	}
 	cout << endl;
 

src/sat/state_formula.cpp

@@ -1,6 +1,6 @@
 #include "state_formula.h"
 #include "ipasir.h"
-#include "../Invariants.h"
+#include "Invariants.h"
 #include <cassert>
 #include <iomanip>
 

src/verifier/CMakeLists.txt

@@ -0,0 +1,98 @@
+project(verifier)
+
+
+# commands for the util library
+file(GLOB UTIL_SOURCE_FILES "util/src/*.cpp")
+
+add_library(util
+    ${UTIL_SOURCE_FILES}
+        util/src/distribution.cpp)
+
+target_include_directories(util
+    PUBLIC
+        ${pandaPIengine_SOURCE_DIR}
+        util/include
+)
+
+target_link_libraries(util
+    PUBLIC
+        intDataStructures
+)
+
+add_library(sat_verifier
+    	sat_verifier/src/sat_verifier.cpp
+		sat_verifier/src/variables.cpp
+		sat_verifier/src/constraints.cpp
+		${pandaPIengine_SOURCE_DIR}/Model.cpp
+		${pandaPIengine_SOURCE_DIR}/Util.cpp
+		${pandaPIengine_SOURCE_DIR}/Debug.cpp
+		${pandaPIengine_SOURCE_DIR}/ProgressionNetwork.cpp
+		${pandaPIengine_SOURCE_DIR}/Invariants.cpp sat_verifier/src/depth.cpp sat_verifier/src/marker.cpp)
+
+target_include_directories(sat_verifier
+    PUBLIC
+        ${PROJECT_SOURCE_DIR}/include
+        ${PROJECT_SOURCE_DIR}/sat_verifier/include
+        ${pandaPIengine_SOURCE_DIR}/
+)
+
+target_link_libraries(sat_verifier
+    PUBLIC
+        util
+        intDataStructures
+        sat
+)
+
+# commands for command-line arguments
+find_program(GENGETOPT gengetopt)
+
+add_custom_command(
+	OUTPUT ${PROJECT_SOURCE_DIR}/cmdline.h ${PROJECT_SOURCE_DIR}/cmdline.c
+	COMMAND gengetopt --include-getopt --default-optional --unamed-opts -i options.ggo
+	DEPENDS options.ggo
+	WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
+	COMMENT "Generating getopt parser code (cmdline.{h,c}) ..."
+	VERBATIM
+)
+
+add_custom_target(cmd
+    DEPENDS cmdline.h cmdline.c
+)
+
+file(GLOB VERIFIER_SOUCE_FILES "src/*.cpp")
+
+add_executable(run_verifier ${VERIFIER_SOUCE_FILES} cmdline.c cmdline.h)
+
+target_link_libraries(run_verifier
+	PUBLIC
+        sat_verifier
+)
+
+target_include_directories(run_verifier
+	PUBLIC
+		${PROJECT_SOURCE_DIR}
+		${PROJECT_SOURCE_DIR}/include
+)
+
+add_subdirectory(test)
+enable_testing()
+add_executable(test_util
+		${CMAKE_CURRENT_SOURCE_DIR}/test/test_util.cpp)
+target_link_libraries(test_util
+		PUBLIC
+			test_main
+			catch2
+			util)
+
+add_executable(test_depth
+		${CMAKE_CURRENT_SOURCE_DIR}/test/test_depth.cpp
+		${pandaPIengine_SOURCE_DIR}/ProgressionNetwork.cpp)
+
+target_link_libraries(test_depth
+		PUBLIC
+			test_main
+			catch2
+			sat_verifier)
+target_include_directories(test_depth
+		PUBLIC
+		${pandaPIengine_SOURCE_DIR}/)