Merge branch 'main' of github.com:kwrx/qasp

.github/workflows/cmake-build.yml

@@ -10,11 +10,12 @@ jobs:
 
     steps:
     - uses: actions/checkout@v2
+    - uses: s-weigand/[email protected]
 
     - name: Install Dependencies
       shell: bash
       working-directory: ${{github.workspace}}
-      run: sudo apt update && sudo apt install libboost-dev ninja-build
+      run: sudo apt update && sudo apt install libboost-dev ninja-build && conda install -c potassco clingo
 
     - name: Create Build Environment (Debug)
       run: cmake -E make_directory ${{github.workspace}}/debug

.github/workflows/cmake-deploy.yml

@@ -11,11 +11,12 @@ jobs:
 
     steps:
     - uses: actions/checkout@v2
+    - uses: s-weigand/[email protected]
 
     - name: Install Dependencies
       working-directory: ${{github.workspace}}
       shell: bash
-      run: sudo apt update && sudo apt install dpkg rpm libboost-dev ninja-build
+      run: sudo apt update && sudo apt install dpkg rpm libboost-dev ninja-build && conda install -c potassco clingo
 
     - name: Create Build Environment
       run: cmake -E make_directory ${{github.workspace}}/build

CMakeLists.txt

@@ -28,8 +28,8 @@ set(HAVE_PRETTY_LOGGER      1)
 
 include(cmake/version.cmake)
 include(cmake/package.cmake)
+include(cmake/deps.cmake)
 include(cmake/build.cmake)
-include(cmake/wasp.cmake)
 include(CPack)
 include(GNUInstallDirs)
 

cmake/build.cmake

@@ -12,7 +12,7 @@ if(CMAKE_CXX_COMPILER_ID MATCHES GNU OR CMAKE_CXX_COMPILER_ID MATCHES Clang)
     endif()
 
     if(HAVE_THREADS)
-        set(CMAKE_EXE_LINKER_FLAGS          "${CMAKE_EXE_LINKER_FLAGS} -lpthread")
+        set(CMAKE_EXE_LINKER_FLAGS          "${CMAKE_EXE_LINKER_FLAGS} ${CMAKE_THREAD_LIBS_INIT}")
     endif()
 endif()
 

cmake/deps.cmake

@@ -0,0 +1,25 @@
+if(${HAVE_THREADS})
+    find_package(Threads REQUIRED)
+endif()
+
+if(${HAVE_WASP})
+
+    find_package(Boost REQUIRED)
+
+    if(Boost_FOUND)
+        add_subdirectory(lib/wasp)
+    endif()
+
+endif()
+
+if(${HAVE_CLASP})
+    message(FATAL_ERROR "clasp not yet supported")
+endif()
+
+if(${HAVE_GRINGO})
+    find_program(GRINGO gringo REQUIRED)
+endif()
+
+if(${HAVE_IDLV})
+    find_program(IDLV idlv REQUIRED)
+endif()

src/qasp/QaspSolver.cpp

@@ -37,8 +37,8 @@ void QaspSolver::init() {
     if(unlikely(program().subprograms().empty()))
         throw std::invalid_argument("empty fragments collection");
 
-    if(unlikely(program().subprograms()[0].type() != TYPE_EXISTS))
-        throw std::invalid_argument("fragment #0 must be @exists");
+    // if(unlikely(program().subprograms()[0].type() != TYPE_EXISTS))
+    //     throw std::invalid_argument("fragment #0 must be @exists");
 
 
     const auto& found = std::find_if(program().subprograms().begin(), program().subprograms().end(), [] (const auto& i) {
@@ -82,26 +82,28 @@ bool QaspSolver::check(const AnswerSet& answer) const {
 
 
 
-bool QaspSolver::get_coherent_answer(const Program& program, const std::vector<AnswerSet>& solution, std::vector<AnswerSet>& coherencies) const {
-
-    size_t incoherencies = 0;
-    size_t max = 0;
+size_t QaspSolver::get_max_incoherencies(const Program& program, const std::vector<AnswerSet>& solution) const {
 
     switch(program.type()) {
 
         case TYPE_EXISTS:
-            max = solution.size();
-            break;
+            return solution.size();
 
         case TYPE_FORALL:
-            max = 1;
-            break;
+            return 1;
 
         default:
-            assert(0 && "BUG! Invalid Program Type");
-            return false;
+            throw std::runtime_error("invalid Program Type");
+
     }
 
+}
+
+
+bool QaspSolver::get_coherent_answer(const Program& program, const std::vector<AnswerSet>& solution, const size_t& max, std::vector<AnswerSet>& coherencies) const {
+
+    size_t incoherencies = 0;
+
     for(const auto& s : solution) {
 
         if(check(s))
@@ -144,10 +146,10 @@ bool QaspSolver::execute(std::vector<Program>::iterator chain, Assumptions assum
         return false;
 
 
-    // TODO: DUBBIO: COERENZA ALLA FINE O NEL MENTRE?
     std::vector<AnswerSet> coherencies;
+    std::size_t max = get_max_incoherencies(program, solution);
 
-    if(!get_coherent_answer(program, solution, coherencies)) {
+    if(!get_coherent_answer(program, solution, max, coherencies)) {
 
         LOG(__FILE__, ERROR) << "No sufficient coherent solution found for program #" 
                              << program.id() << std::endl;
@@ -157,16 +159,15 @@ bool QaspSolver::execute(std::vector<Program>::iterator chain, Assumptions assum
 
 
 
-    size_t success = 0;
+    std::size_t fail = 0;
 
     for(const auto& i : coherencies)
         assumptions.insert(assumptions.end(), i.begin(), i.end());
 
     for(const auto& i : coherencies)
-        success += execute(chain + 1, assumptions, i) ? 1 : 0;
-
+        fail += execute(chain + 1, assumptions, i) ? 0 : 1;
 
-    return success > 0;
+    return fail < max;
 
 }
 

src/qasp/QaspSolver.hpp

@@ -62,7 +62,8 @@ namespace qasp {
             bool check(const AnswerSet& answer) const;
             bool execute(std::vector<Program>::iterator chain, Assumptions assumptions = {}, AnswerSet answer = {});
 
-            bool get_coherent_answer(const Program& program, const std::vector<AnswerSet>& solution, std::vector<AnswerSet>& coherencies) const;
+            size_t get_max_incoherencies(const Program& program, const std::vector<AnswerSet>& solution) const;
+            bool get_coherent_answer(const Program& program, const std::vector<AnswerSet>& solution, const size_t& max, std::vector<AnswerSet>& coherencies) const;
 
             inline void model(const ProgramModel value) {
                 this->__model = value;

src/qasp/parser/Parser.cpp

@@ -191,19 +191,19 @@ static std::vector<Program> parseSources(const std::vector<std::string>& sources
 
 
 #ifdef DEBUG
-                LOG(__FILE__, TRACE) << "<PARSER> Found annotation with identifier: (" << programs.size() << ") @" << identifier.str()
+                LOG(__FILE__, TRACE) << "<PARSER> Found annotation with identifier: #" << programs.size() + 1 << " @" << identifier.str()
                                      //<< " and source: \n" << source.str() << "\n"
                                      << " in " << (*begin).tk_source
                                      << " at " << (*begin).tk_line << ":" << (*begin).tk_column << std::endl;
 #endif
 
 
                 if(identifier.str() == ANNOTATION_EXISTS)
-                    programs.emplace_back(programs.size(), ProgramType::TYPE_EXISTS, source.str());
+                    programs.emplace_back(programs.size() + 1, ProgramType::TYPE_EXISTS, source.str());
                 else if(identifier.str() == ANNOTATION_FORALL)
-                    programs.emplace_back(programs.size(), ProgramType::TYPE_FORALL, source.str());
+                    programs.emplace_back(programs.size() + 1, ProgramType::TYPE_FORALL, source.str());
                 else if(identifier.str() == ANNOTATION_CONSTRAINTS)
-                    programs.emplace_back(programs.size(), ProgramType::TYPE_CONSTRAINTS, source.str());
+                    programs.emplace_back(programs.size() + 1, ProgramType::TYPE_CONSTRAINTS, source.str());
                 else {
 
 #ifdef DEBUG

test/Test01.asp

@@ -4,16 +4,8 @@ a | b.                      % P1 = {a} {b}
 c | d :- a.                 % P2 U {a} = {a,c} {a,d}        -> {a,c} U C -> INCOHERENT      |   Non tutti gli AS(P2) U {a} sono coerenti con un AS(P1)
 d :- b.                     %                               -> {a,d} U C -> COHERENT        |   
                             % P2 U {b} = {b,d}              -> {b,d} U C -> COHERENT        |   Un AS(P1) = {b} è coerente con tutti gli AS(P2) U {b}
-%@exists
-e | f | g :- b, d.          % P3 U {b,d} = {b,d,f} {b,d,f}  -> {b,d,e} U C -> INCOHERENT    | 
-                            %                               -> {b,d,f} U C -> COHERENT      |   Tutti gli AS(P2) sono coerenti con almeno un AS(P3) U {b,d}
-                            %                               -> {b,d,g} U C -> COHERENT      |   Tutti gli AS(P2) sono coerenti con almeno un AS(P3) U {b,d}
-%@forall
-:- f.                       % P4 U {b,d,f} = INCOHERENT     -> {b,d,f} U C -> INCOHERENT    | 
-                            % P4 U {b,d,g} = {b,d,g}        -> {b,d,g} U C -> COHERENT      |   Almeno un AS(P3) è coerente con tutti gli AS(P4) U {b,d,g}
 %@constraints
-{c;d;e}.
+{c;d}.
 :- c, not d.                % C
-:- e.
 
-% Result: { b, d, g } is COHERENT.
+% Result: { b, d } is COHERENT.

test/Test01.expected

@@ -1 +1 @@
-{b,d,g}
+{b,d}

test/Test02.asp

@@ -1,12 +1,19 @@
 %@exists
-a | na.
-b | nb.
+a | b.                      % P1 = {a} {b}
 %@forall
-c | nc.
-d | nd.
-e | ne.
+c | d :- a.                 % P2 U {a} = {a,c} {a,d}        -> {a,c} U C -> INCOHERENT      |   Non tutti gli AS(P2) U {a} sono coerenti con un AS(P1)
+d :- b.                     %                               -> {a,d} U C -> COHERENT        |   
+                            % P2 U {b} = {b,d}              -> {b,d} U C -> COHERENT        |   Un AS(P1) = {b} è coerente con tutti gli AS(P2) U {b}
+%@exists
+e | f | g :- b, d.          % P3 U {b,d} = {b,d,f} {b,d,f}  -> {b,d,e} U C -> INCOHERENT    | 
+                            %                               -> {b,d,f} U C -> COHERENT      |   Tutti gli AS(P2) sono coerenti con almeno un AS(P3) U {b,d}
+                            %                               -> {b,d,g} U C -> COHERENT      |   Tutti gli AS(P2) sono coerenti con almeno un AS(P3) U {b,d}
+%@forall
+:- f.                       % P4 U {b,d,f} = INCOHERENT     -> {b,d,f} U C -> INCOHERENT    | 
+                            % P4 U {b,d,g} = {b,d,g}        -> {b,d,g} U C -> COHERENT      |   Almeno un AS(P3) è coerente con tutti gli AS(P4) U {b,d,g}
 %@constraints
 {c;d;e}.
-:- c, not e.
-:- d, not e.
-:- not c, not d, e.
+:- c, not d.                % C
+:- e.
+
+% Result: { b, d, g } is COHERENT.

test/Test02.expected

@@ -1 +1 @@
-INCOHERENT
+{b,d,g}

test/Test03.asp

@@ -0,0 +1,12 @@
+%@exists
+a | na.
+b | nb.
+%@forall
+c | nc.
+d | nd.
+e | ne.
+%@constraints
+{c;d;e}.
+:- c, not e.
+:- d, not e.
+:- not c, not d, e.

test/Test03.expected

@@ -0,0 +1 @@
+INCOHERENT

test/Test04.asp

@@ -0,0 +1,16 @@
+% https://en.wikipedia.org/wiki/Boolean_satisfiability_problem
+% ∀x ∀y ∃z (x ∨ y ∨ z) ∧ (¬x ∨ ¬y ∨ ¬z)
+
+%@forall
+x | nx.
+%@forall
+y | ny.
+%@exists
+z | nz.
+%@constraints
+{x;y;z;nx;ny;nz}.
+:- nx, ny, nz.
+:- x, y, z.
+
+
+%% Result: COHERENT

test/Test04.expected

@@ -0,0 +1,6 @@
+{x,y,nz}
+{x,ny,z}
+{x,ny,nz}
+{nx,y,z}
+{nx,y,nz}
+{nx,ny,z}

test/Test05.asp

@@ -0,0 +1,16 @@
+% https://en.wikipedia.org/wiki/Boolean_satisfiability_problem
+% ∀x ∀y ∀z (x ∨ y ∨ z) ∧ (¬x ∨ ¬y ∨ ¬z)
+
+%@forall
+x | nx.
+%@forall
+y | ny.
+%@forall
+z | nz.
+%@constraints
+{x;y;z;nx;ny;nz}.
+:- nx, ny, nz.
+:- x, y, z.
+
+
+%% Result: INCOHERENT

test/Test05.expected

@@ -0,0 +1 @@
+INCOHERENT