Merge pull request #25 from kwrx/dev

Iterazioni

Author: kwrx

CMakeLists.txt

@@ -13,11 +13,13 @@ set(HAVE_IDLV       0)
 set(HAVE_WASP       1)
 set(HAVE_CLASP      0)
 
-## Multithreading
-set(HAVE_THREADS    1)
+## QASP
+set(HAVE_THREADS            1)
+set(HAVE_ITERATIONS         1)
 
 ## Wasp
 set(HAVE_WASP_ASSUMPTIONS   1)
+set(HAVE_WASP_RESET         1)
 
 ## Logger
 set(HAVE_PRETTY_LOGGER      1)

config.h.in

@@ -27,7 +27,9 @@
 #cmakedefine HAVE_GRINGO            @HAVE_GRINGO@
 #cmakedefine HAVE_CLASP             @HAVE_CLASP@
 #cmakedefine HAVE_THREADS           @HAVE_THREADS@
+#cmakedefine HAVE_ITERATIONS        @HAVE_ITERATIONS@
 #cmakedefine HAVE_WASP_ASSUMPTIONS  @HAVE_WASP_ASSUMPTIONS@
+#cmakedefine HAVE_WASP_RESET        @HAVE_WASP_RESET@
 #cmakedefine HAVE_PRETTY_LOGGER     @HAVE_PRETTY_LOGGER@
 
 

include/qasp/qasp.h

@@ -23,14 +23,19 @@
 
 #include <stdint.h>
 
-#define QASP_OPTIONS_DEFAULT_CPUS       8
 #define QASP_OPTIONS_DEFAULT_QUIET      0
+#define QASP_OPTIONS_DEFAULT_CPUS       8
+#define QASP_OPTIONS_DEFAULT_ITERATIONS 1
 
 #define QASP_RESULT_COHERENT            1
 #define QASP_RESULT_INCOHERENT          2
 #define QASP_RESULT_UNKNOWN             0
 
 
+typedef uint64_t qasp_iteration_t;
+
+
+
 #if defined(__cplusplus)
 
 #include <vector>
@@ -40,16 +45,19 @@ namespace qasp {
 
     struct Options {
 
-        uint16_t cpus;
         uint16_t quiet;
+        uint16_t cpus;
+        qasp_iteration_t iterations;
 
-        Options(uint16_t cpus, uint16_t quiet)
-            : cpus(cpus)
-            , quiet(quiet) {}
+        Options(uint16_t quiet, uint16_t cpus, qasp_iteration_t iterations)
+            : quiet(quiet)
+            , cpus(cpus)
+            , iterations(iterations) {}
 
         Options()
-            : cpus(QASP_OPTIONS_DEFAULT_CPUS)
-            , quiet(QASP_OPTIONS_DEFAULT_QUIET) {}
+            : quiet(QASP_OPTIONS_DEFAULT_QUIET)
+            , cpus(QASP_OPTIONS_DEFAULT_CPUS)
+            , iterations(QASP_OPTIONS_DEFAULT_ITERATIONS) {}
 
     };
 
@@ -74,11 +82,11 @@ namespace qasp {
                 __options = std::move(options);
             }
 
-            inline const auto& options() {
+            inline const auto& options() const {
                 return __options;
             }
 
-            inline const auto& sources() {
+            inline const auto& sources() const {
                 return __sources;
             }
 

lib/wasp/CMakeLists.txt

@@ -7,4 +7,5 @@ add_library(wasp ${SOURCES} ${HEADERS})
 target_link_libraries(wasp PUBLIC ${Boost_LIBRARIES})
 target_include_directories(wasp PUBLIC ${Boost_INCLUDE_DIRS})
 
-target_compile_options(wasp PRIVATE -Wno-error -w)
+target_compile_options(wasp PRIVATE -Wno-error -w)
+target_compile_definitions(wasp PRIVATE __qasp__)

lib/wasp/util/VariableNames.cpp

@@ -20,9 +20,19 @@
 #include "WaspAssert.h"
 #include <sstream>
 using namespace std;
+
+
+#if defined(__qasp__)
+thread_local
+#endif
 vector< string > VariableNames::variables;
+
+#if defined(__qasp__)
+thread_local
+#endif
 bool VariableNames::toBePrinted = false;
 
+
 bool
 VariableNames::isHidden(
     Var v )

lib/wasp/util/VariableNames.h

@@ -19,6 +19,10 @@
 #ifndef WASP_VARIABLENAMES_H
 #define WASP_VARIABLENAMES_H
 
+#if defined(__qasp__)
+#include <thread>
+#endif
+
 #include <cassert>
 #include <iostream>
 #include <vector>
@@ -36,9 +40,23 @@ class VariableNames
         static bool hasToBePrinted( Var v );
         static void addVariable();
         static const vector< string >& getVariables();
+
+        #if defined(__qasp__)
+        static inline void reset() {
+            variables.clear();
+        }
+        #endif
 
     private:
+
+        #if defined(__qasp__)
+        thread_local
+        #endif
         static vector< string > variables;
+
+        #if defined(__qasp__)
+        thread_local
+        #endif
         static bool toBePrinted;
 };
 

src/main.cc

@@ -35,11 +35,13 @@ static void show_usage(int argc, char** argv) {
     std::cout 
         << "Use: " << QASP_PROGRAM_NAME << " [OPTIONS] SOURCES...\n"
         << "Process qasp SOURCES and blabla...\n\n"
-        << "    -q, --quiet                 hide log information\n"
-        << "        --help                  show this help\n"
-        << "        --version               print version info and exit\n";
+        << "    -j N, --parallel=N          allow N jobs at once.\n"
+        << "    -n N, --iterations=N        iterate solving N times (infinite: N <- 0).\n"
+        << "    -q, --quiet                 hide log information.\n"
+        << "        --help                  print this message and exit.\n"
+        << "        --version               print version info and exit.\n";
 
-    exit(1);
+    exit(EXIT_FAILURE);
 
 }
 
@@ -63,7 +65,7 @@ static void show_version(int argc, char** argv) {
         << __TIMESTAMP__            << ")\n";
 
 
-    exit(1);
+    exit(EXIT_FAILURE);
 
 }
 
@@ -83,7 +85,7 @@ int main(int argc, char** argv) {
     qasp::Options options;
 
     int c, idx;
-    while((c = getopt_long(argc, argv, "qj:hv", long_options, &idx)) != -1) {
+    while((c = getopt_long(argc, argv, "qj:n:hv", long_options, &idx)) != -1) {
 
         switch(c) {
             case 'q':
@@ -92,6 +94,9 @@ int main(int argc, char** argv) {
             case 'j':
                 options.cpus = atoi(optarg);
                 break;
+            case 'n':
+                options.iterations = atoll(optarg);
+                break;
             case 'v':
                 show_version(argc, argv);
                 break;
@@ -111,6 +116,11 @@ int main(int argc, char** argv) {
         abort();
     }
 
+    if(unlikely(options.iterations <= 0)) {
+        options.iterations = std::numeric_limits<decltype(options.iterations)>().max();
+    }
+
+
 
     std::vector<std::string> sources;
 
@@ -153,6 +163,6 @@ int main(int argc, char** argv) {
 
     }
 
-    return 0;
+    return EXIT_SUCCESS;
 
 }

src/qasp/AnswerSet.hpp

@@ -34,6 +34,22 @@ namespace qasp {
     class AnswerSet : public std::vector<Atom> {
         public:
 
+            inline friend bool operator==(const AnswerSet& a, const AnswerSet& b) {
+
+                if(a.size() != b.size())
+                    return false;
+
+
+                std::vector<Atom> v1 = a;
+                std::vector<Atom> v2 = b;
+
+                std::sort(v1.begin(), v1.end(), [] (const auto& i, const auto& j) { return i.predicate() < j.predicate(); });
+                std::sort(v2.begin(), v2.end(), [] (const auto& i, const auto& j) { return i.predicate() < j.predicate(); });
+
+                return std::equal(v1.begin(), v1.end(), v2.begin());
+
+            }
+
             inline friend std::ostream& operator <<(std::ostream& os, const AnswerSet& a) {
 
                 os << "{";
@@ -51,6 +67,11 @@ namespace qasp {
 
             }
 
+
+            inline const bool contains(const Atom& atom) const {
+                return std::find(this->begin(), this->end(), atom) != this->end();
+            }
+
     };
 
 }

src/qasp/Assumptions.hpp

@@ -60,6 +60,12 @@ namespace qasp {
 
             }
 
+
+            inline const bool contains(const Atom& atom) const {
+                return this->std::unordered_set<std::string>::find(atom.predicate()) != this->std::unordered_set<std::string>::end();
+            }
+            
+
             template <typename ...T>
             inline void emplace_back(T&&... args) {
 

src/qasp/Program.cpp

@@ -128,9 +128,7 @@ std::tuple<ProgramModel, std::vector<AnswerSet>> Program::solve(const AnswerSet&
 
     for(const auto& i : answer) {
 
-        auto found = std::find(assumptions().begin(), assumptions().end(), i); // FIXME: Da rivedere...
-
-        if(unlikely(found != assumptions().end()))
+        if(unlikely(assumptions().contains(i)))
             continue;
 
 
@@ -150,9 +148,7 @@ std::tuple<ProgramModel, std::vector<AnswerSet>> Program::solve(const AnswerSet&
 
     for(const auto& i : assumptions()) {
 
-        auto found = std::find(answer.begin(), answer.end(), i);
-
-        if(found != answer.end())
+        if(answer.contains(i))
             positive.emplace_back(map_index(i), i.predicate());
         else
             negative.emplace_back(map_index(i), i.predicate());