From 81efbeaa45af96e83e5dbca8c22e6ec9ebe89878 Mon Sep 17 00:00:00 2001 From: Antonino Natale Date: Sun, 2 May 2021 19:02:27 +0200 Subject: [PATCH 1/3] Fixed #22 --- CMakeLists.txt | 2 +- cmake/build.cmake | 2 +- cmake/deps.cmake | 25 +++++++++++++++++++++++++ cmake/wasp.cmake | 10 ---------- src/qasp/QaspSolver.cpp | 37 +++++++++++++++++++------------------ src/qasp/QaspSolver.hpp | 3 ++- src/qasp/parser/Parser.cpp | 8 ++++---- test/Test01.asp | 12 ++---------- test/Test01.expected | 2 +- test/Test02.asp | 23 +++++++++++++++-------- test/Test02.expected | 2 +- test/Test03.asp | 12 ++++++++++++ test/Test03.expected | 1 + test/Test04.asp | 16 ++++++++++++++++ test/Test04.expected | 6 ++++++ test/Test05.asp | 16 ++++++++++++++++ test/Test05.expected | 1 + 17 files changed, 123 insertions(+), 55 deletions(-) create mode 100644 cmake/deps.cmake delete mode 100644 cmake/wasp.cmake create mode 100644 test/Test03.asp create mode 100644 test/Test03.expected create mode 100644 test/Test04.asp create mode 100644 test/Test04.expected create mode 100644 test/Test05.asp create mode 100644 test/Test05.expected diff --git a/CMakeLists.txt b/CMakeLists.txt index 58dd268..98e2a93 100644 --- a/CMakeLists.txt +++ b/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) diff --git a/cmake/build.cmake b/cmake/build.cmake index 7cd3155..656533f 100644 --- a/cmake/build.cmake +++ b/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() diff --git a/cmake/deps.cmake b/cmake/deps.cmake new file mode 100644 index 0000000..fe6f205 --- /dev/null +++ b/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() \ No newline at end of file diff --git a/cmake/wasp.cmake b/cmake/wasp.cmake deleted file mode 100644 index 867febb..0000000 --- a/cmake/wasp.cmake +++ /dev/null @@ -1,10 +0,0 @@ - -if(${HAVE_WASP}) - - find_package(Boost REQUIRED) - - if(Boost_FOUND) - add_subdirectory(lib/wasp) - endif() - -endif() diff --git a/src/qasp/QaspSolver.cpp b/src/qasp/QaspSolver.cpp index e84f601..197c917 100644 --- a/src/qasp/QaspSolver.cpp +++ b/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& solution, std::vector& coherencies) const { - - size_t incoherencies = 0; - size_t max = 0; +size_t QaspSolver::get_max_incoherencies(const Program& program, const std::vector& 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& solution, const size_t& max, std::vector& coherencies) const { + + size_t incoherencies = 0; + for(const auto& s : solution) { if(check(s)) @@ -144,10 +146,10 @@ bool QaspSolver::execute(std::vector::iterator chain, Assumptions assum return false; - // TODO: DUBBIO: COERENZA ALLA FINE O NEL MENTRE? std::vector 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::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; } diff --git a/src/qasp/QaspSolver.hpp b/src/qasp/QaspSolver.hpp index e53ac70..3e93499 100644 --- a/src/qasp/QaspSolver.hpp +++ b/src/qasp/QaspSolver.hpp @@ -62,7 +62,8 @@ namespace qasp { bool check(const AnswerSet& answer) const; bool execute(std::vector::iterator chain, Assumptions assumptions = {}, AnswerSet answer = {}); - bool get_coherent_answer(const Program& program, const std::vector& solution, std::vector& coherencies) const; + size_t get_max_incoherencies(const Program& program, const std::vector& solution) const; + bool get_coherent_answer(const Program& program, const std::vector& solution, const size_t& max, std::vector& coherencies) const; inline void model(const ProgramModel value) { this->__model = value; diff --git a/src/qasp/parser/Parser.cpp b/src/qasp/parser/Parser.cpp index a0e15fd..26e07e7 100644 --- a/src/qasp/parser/Parser.cpp +++ b/src/qasp/parser/Parser.cpp @@ -191,7 +191,7 @@ static std::vector parseSources(const std::vector& sources #ifdef DEBUG - LOG(__FILE__, TRACE) << " Found annotation with identifier: (" << programs.size() << ") @" << identifier.str() + LOG(__FILE__, TRACE) << " 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; @@ -199,11 +199,11 @@ static std::vector parseSources(const std::vector& sources 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 diff --git a/test/Test01.asp b/test/Test01.asp index 599f812..50a9267 100644 --- a/test/Test01.asp +++ b/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. \ No newline at end of file +% Result: { b, d } is COHERENT. \ No newline at end of file diff --git a/test/Test01.expected b/test/Test01.expected index 29520fb..6d9290e 100644 --- a/test/Test01.expected +++ b/test/Test01.expected @@ -1 +1 @@ -{b,d,g} \ No newline at end of file +{b,d} \ No newline at end of file diff --git a/test/Test02.asp b/test/Test02.asp index 5a86caa..599f812 100644 --- a/test/Test02.asp +++ b/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. \ No newline at end of file +:- c, not d. % C +:- e. + +% Result: { b, d, g } is COHERENT. \ No newline at end of file diff --git a/test/Test02.expected b/test/Test02.expected index 7dc6920..29520fb 100644 --- a/test/Test02.expected +++ b/test/Test02.expected @@ -1 +1 @@ -INCOHERENT \ No newline at end of file +{b,d,g} \ No newline at end of file diff --git a/test/Test03.asp b/test/Test03.asp new file mode 100644 index 0000000..5a86caa --- /dev/null +++ b/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. \ No newline at end of file diff --git a/test/Test03.expected b/test/Test03.expected new file mode 100644 index 0000000..7dc6920 --- /dev/null +++ b/test/Test03.expected @@ -0,0 +1 @@ +INCOHERENT \ No newline at end of file diff --git a/test/Test04.asp b/test/Test04.asp new file mode 100644 index 0000000..afa5f82 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/test/Test04.expected b/test/Test04.expected new file mode 100644 index 0000000..28ff909 --- /dev/null +++ b/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} \ No newline at end of file diff --git a/test/Test05.asp b/test/Test05.asp new file mode 100644 index 0000000..9039d3a --- /dev/null +++ b/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 \ No newline at end of file diff --git a/test/Test05.expected b/test/Test05.expected new file mode 100644 index 0000000..7dc6920 --- /dev/null +++ b/test/Test05.expected @@ -0,0 +1 @@ +INCOHERENT \ No newline at end of file From 080d597dae0f6e63c7f54b2c5d5bf630325b4954 Mon Sep 17 00:00:00 2001 From: Antonino Natale Date: Sun, 2 May 2021 19:05:59 +0200 Subject: [PATCH 2/3] Update cmake-build.yml --- .github/workflows/cmake-build.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/cmake-build.yml b/.github/workflows/cmake-build.yml index 591df55..5453268 100644 --- a/.github/workflows/cmake-build.yml +++ b/.github/workflows/cmake-build.yml @@ -10,11 +10,12 @@ jobs: steps: - uses: actions/checkout@v2 + - uses: s-weigand/setup-conda@v1.0.5 - 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 From e85340e757821938005bde0bea98681268c743a5 Mon Sep 17 00:00:00 2001 From: Antonino Natale Date: Sun, 2 May 2021 19:06:44 +0200 Subject: [PATCH 3/3] Update cmake-deploy.yml --- .github/workflows/cmake-deploy.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/cmake-deploy.yml b/.github/workflows/cmake-deploy.yml index 9a5cc5c..69b249c 100644 --- a/.github/workflows/cmake-deploy.yml +++ b/.github/workflows/cmake-deploy.yml @@ -11,11 +11,12 @@ jobs: steps: - uses: actions/checkout@v2 + - uses: s-weigand/setup-conda@v1.0.5 - 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