diff --git a/.github/workflows/build_cmake.yml b/.github/workflows/build_cmake.yml index 05b3fe5c..2129f470 100644 --- a/.github/workflows/build_cmake.yml +++ b/.github/workflows/build_cmake.yml @@ -28,17 +28,6 @@ jobs: sudo apt-get install -f flex bison sudo apt-get install -f libgraphviz-dev sudo python -m pip install gcovr - - name: Install Cryptominisat - run: | - wget https://github.com/msoos/cryptominisat/archive/5.7.1.tar.gz - tar -xzvf 5.7.1.tar.gz - cd cryptominisat-5.7.1 - mkdir build - cd build - cmake .. - make - sudo make install - sudo ldconfig - name: Install CUDD run: | sudo apt-get install -f automake libtool diff --git a/.gitmodules b/.gitmodules index b4f12742..50a7488d 100644 --- a/.gitmodules +++ b/.gitmodules @@ -19,3 +19,6 @@ [submodule "third_party/cppitertools"] path = third_party/cppitertools url = https://github.com/ryanhaining/cppitertools.git +[submodule "third_party/minisat"] + path = third_party/minisat + url = https://github.com/whitemech/minisat.git diff --git a/CMakeLists.txt b/CMakeLists.txt index 097fb802..f536cae5 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -74,7 +74,6 @@ set( CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib ) set (THREADS_PREFER_PTHREAD_FLAG ON) find_package (Threads REQUIRED) find_package(cudd REQUIRED) -find_package(cryptominisat5 REQUIRED) find_package(Graphviz REQUIRED) find_package(BISON 3.0 REQUIRED) find_package(FLEX 2.6 REQUIRED) diff --git a/CMakeModules/Findortools.cmake b/CMakeModules/Findortools.cmake new file mode 100644 index 00000000..04ae3e52 --- /dev/null +++ b/CMakeModules/Findortools.cmake @@ -0,0 +1,97 @@ +if(WIN32) + if(NOT TARGET ortools::ortools) + find_library(ORTOOLS_LIBRARIES NAME ortools PATH_SUFFIXES lib ) + find_path(ORTOOLS_INCLUDE_DIRS NAME zlib.h PATH_SUFFIXES include) + set(ORTOOLS_DEFINITIONS /DNOMINMAX -DUSE_CBC -DUSE_CLP -DUSE_BOP -DUSE_GLOP) + + add_library(ortools::ortools STATIC IMPORTED GLOBAL) + set_target_properties(ortools::ortools PROPERTIES IMPORTED_LOCATION ${ORTOOLS_LIBRARIES} ) + target_include_directories(ortools::ortools INTERFACE ${ORTOOLS_INCLUDE_DIRS}) + target_link_libraries(ortools::ortools INTERFACE ${ORTOOLS_LIBRARIES}) + target_compile_options(ortools::ortools INTERFACE ${ORTOOLS_DEFINITIONS}) + + include(FindPackageHandleStandardArgs) + # handle the QUIETLY and REQUIRED arguments and set ortools to TRUE + # if all listed variables are TRUE + find_package_handle_standard_args(ortools_FOUND REQUIRED_VARS + ORTOOLS_LIBRARIES ORTOOLS_INCLUDE_DIRS) + + endif() +elseif(UNIX) + if(NOT TARGET ortools::ortools) + # Include directories + find_path(ORTOOLS_INCLUDE_DIRS NAME ortools PATH_SUFFIXES include/) + message(STATUS "ortools found here : ${ORTOOLS_INCLUDE_DIRS}") + + ## Libraries + set(LIB_TO_FIND + CbcSolver #CBC_LNK + Cbc + OsiCbc + Cgl + ClpSolver + Clp + OsiClp + Osi + CoinUtils + absl_bad_any_cast_impl #ABSL_LNK + absl_bad_optional_access + absl_bad_variant_access + absl_base + absl_city + absl_civil_time + absl_debugging_internal + absl_demangle_internal + absl_dynamic_annotations + absl_examine_stack + absl_failure_signal_handler + absl_graphcycles_internal + absl_hash + absl_hashtablez_sampler + absl_int128 + absl_leak_check + absl_malloc_internal +# absl_optional + absl_raw_hash_set + absl_spinlock_wait + absl_stacktrace + absl_str_format_internal + absl_strings + absl_strings_internal + absl_symbolize + absl_synchronization + absl_throw_delegate + absl_time + absl_time_zone + protobuf #protobuf + glog #glog + gflags #gflags + ortools #ortools + ) + + foreach(X ${LIB_TO_FIND}) + find_library(LIB_${X} NAME ${X} PATH_SUFFIXES lib/) + message(STATUS "${X} lib found here : ${LIB_${X}}") + set(ORTOOLS_LIBRARIES ${ORTOOLS_LIBRARIES} ${LIB_${X}}) + endforeach() + + + # Definitions + set(ORTOOLS_DEFINITIONS -DUSE_CBC -DUSE_CLP -DUSE_BOP -DUSE_GLOP) + + + add_library(ortools INTERFACE) + add_library(ortools::ortools ALIAS ortools) + target_include_directories(ortools INTERFACE ${ORTOOLS_INCLUDE_DIRS}) + target_link_libraries(ortools INTERFACE ${ORTOOLS_LIBRARIES}) + target_compile_options(ortools INTERFACE ${ORTOOLS_DEFINITIONS}) + + include(FindPackageHandleStandardArgs) + # handle the QUIETLY and REQUIRED arguments and set ortools to TRUE + # if all listed variables are TRUE + find_package_handle_standard_args(ortools_FOUND + REQUIRED_VARS ORTOOLS_LIBRARIES ORTOOLS_INCLUDE_DIRS) + endif() +else() + message(FATAL_ERROR "No other platform supported yet") +endif() \ No newline at end of file diff --git a/README.md b/README.md index f162bcdd..ad3d0a09 100644 --- a/README.md +++ b/README.md @@ -58,17 +58,16 @@ sudo make install 3. Using a version of aclocal other than 1.14: modify the version 1.14 in configure accordingly. -# CryptoMiniSat +## ZLib -We use Cryptominisat as SAT solver library. +The software depends on MiniSAT Solver, which in turn depends +on [ZLib](https://www.zlib.net/). -For Ubuntu systems: -``` -sudo apt-get install libcryptominisat5-dev -``` +To install it, e.g. on Ubuntu: -For other systems, please look at -the [documentation](https://github.com/msoos/cryptominisat#compiling-in-linux). +```bash +sudo apt-get install zlib1g-dev +``` ## Graphviz diff --git a/lib/CMakeLists.txt b/lib/CMakeLists.txt index a517832a..df098ae8 100644 --- a/lib/CMakeLists.txt +++ b/lib/CMakeLists.txt @@ -46,7 +46,10 @@ add_library (${LIB_NAME} ${BISON_lydia_parser_OUTPUTS} ${FLEX_lydia_lexer_OUTPUTS}) -target_link_libraries(${LIB_NAME} ${CUDD_LIBRARIES} ${GRAPHVIZ_LIBRARIES} ${CRYPTOMINISAT5_LIBRARIES}) +target_link_libraries(${LIB_NAME} + ${CUDD_LIBRARIES} + ${GRAPHVIZ_LIBRARIES} + ${MINISAT_LIBRARIES}) #export vars set (LIBRARY_INCLUDE_PATH ${LIBRARY_INCLUDE_PATH} PARENT_SCOPE) diff --git a/lib/benchmark/src/pl.cpp b/lib/benchmark/src/pl.cpp index f926cd21..3b32e81f 100644 --- a/lib/benchmark/src/pl.cpp +++ b/lib/benchmark/src/pl.cpp @@ -17,43 +17,93 @@ #include #include -#include +#include +#include #include +#include #include namespace whitemech::lydia::Benchmark { -static void BM_pl_models_cryptominisat_true(benchmark::State &state) { - auto solver = CMSat::SATSolver(); - solver.set_num_threads(4); +static void BM_pl_models_minisat_1(benchmark::State &state) { for (auto _ : state) { - auto result = solver.solve(); - escape(&result); - (void)result; + Minisat::SimpSolver solver; + solver.verbosity = -1; + + // Create variables + auto A = solver.newVar(); + auto B = solver.newVar(); + auto C = solver.newVar(); + + // Create the clauses + solver.addClause(Minisat::mkLit(A), Minisat::mkLit(B), Minisat::mkLit(C)); + solver.addClause(~Minisat::mkLit(A), Minisat::mkLit(B), Minisat::mkLit(C)); + solver.addClause(Minisat::mkLit(A), ~Minisat::mkLit(B), Minisat::mkLit(C)); + solver.addClause(Minisat::mkLit(A), Minisat::mkLit(B), ~Minisat::mkLit(C)); + + // Check for solution and retrieve model if found + auto sat = solver.solve(); + + escape((void *)&sat); + (void)sat; } } -BENCHMARK(BM_pl_models_cryptominisat_true); +BENCHMARK(BM_pl_models_minisat_1); -static void BM_pl_models_cryptominisat_false(benchmark::State &state) { - auto solver = CMSat::SATSolver(); - solver.set_num_threads(4); - solver.add_clause(std::vector()); +static void BM_pl_models_naive_all_models_tautology(benchmark::State &state) { + auto t = boolean_prop(true); for (auto _ : state) { - auto result = solver.solve(); - escape(&result); - (void)result; + auto m = all_models(*t); + escape(&m); + (void)m; + } +} +BENCHMARK(BM_pl_models_naive_all_models_tautology); + +static void BM_pl_models_sat_all_models_tautology(benchmark::State &state) { + auto t = boolean_prop(true); + for (auto _ : state) { + auto m = all_models(*t); + escape(&m); + (void)m; + } +} +BENCHMARK(BM_pl_models_sat_all_models_tautology); + +static void BM_pl_models_naive_all_models_or(benchmark::State &state) { + auto t = boolean_prop(true); + for (auto _ : state) { + auto N = state.range(0); + auto operands = std::vector(); + operands.reserve(N); + for (int i = 0; i < N; i++) { + operands.push_back(prop_atom(UniquePropositionalSymbol())); + } + auto f = logical_or(set_prop_formulas(operands.begin(), operands.end())); + auto m = all_models(*f); + assert(m.size() == 2 << N); + escape(&m); + (void)m; } } -BENCHMARK(BM_pl_models_cryptominisat_false); +BENCHMARK(BM_pl_models_naive_all_models_or)->Arg(5)->Arg(10)->Arg(15); -static void BM_pl_models_sat_all_models_t(benchmark::State &state) { +static void BM_pl_models_sat_all_models_or(benchmark::State &state) { auto t = boolean_prop(true); for (auto _ : state) { - auto m = all_models_sat(*t); + auto N = state.range(0); + auto operands = std::vector(); + operands.reserve(N); + for (int i = 0; i < N; i++) { + operands.push_back(prop_atom(UniquePropositionalSymbol())); + } + auto f = logical_or(set_prop_formulas(operands.begin(), operands.end())); + auto m = all_models(*t); + assert(m.size() == 2 << N); escape(&m); (void)m; } } -BENCHMARK(BM_pl_models_sat_all_models_t); +BENCHMARK(BM_pl_models_sat_all_models_or)->Arg(5)->Arg(10)->Arg(20)->Arg(50); } // namespace whitemech::lydia::Benchmark diff --git a/lib/benchmark/src/to_dfa.cpp b/lib/benchmark/src/to_dfa.cpp index 03f235ae..8c20feef 100644 --- a/lib/benchmark/src/to_dfa.cpp +++ b/lib/benchmark/src/to_dfa.cpp @@ -105,9 +105,9 @@ static void BM_translate_sequence_of_stars_of_atoms(benchmark::State &state) { // clang-format off BENCHMARK(BM_translate_sequence_of_stars_of_atoms) ->Arg(5)->Arg(10)->Arg(15) -// ->Arg(20)->Arg(25)->Arg(30) -// ->Arg(40)->Arg(80)->Arg(100) -// ->Arg(200)->Arg(500)->Arg(1000) + ->Arg(20)->Arg(25)->Arg(30) + ->Arg(40)->Arg(80)->Arg(100) + ->Arg(200)->Arg(500)->Arg(1000) ->Unit(benchmark::kMillisecond) ->Repetitions(5) ->DisplayAggregatesOnly(true); @@ -134,9 +134,9 @@ static void BM_translate_union(benchmark::State &state) { // clang-format off BENCHMARK(BM_translate_union) ->Arg(5)->Arg(10)->Arg(15) -//->Arg(20)->Arg(25)->Arg(30) -//->Arg(40)->Arg(80)->Arg(100) -//->Arg(200)->Arg(500)->Arg(1000) +->Arg(20)->Arg(25)->Arg(30) +->Arg(40)->Arg(80)->Arg(100) +->Arg(200)->Arg(500)->Arg(1000) ->Unit(benchmark::kMillisecond) ->Repetitions(5) ->DisplayAggregatesOnly(true); diff --git a/lib/include/lydia/basic.hpp b/lib/include/lydia/basic.hpp index 056d9e4e..d6685d3d 100644 --- a/lib/include/lydia/basic.hpp +++ b/lib/include/lydia/basic.hpp @@ -122,10 +122,6 @@ class Basic : public std::enable_shared_from_this { int compare_(const Basic &o) const; virtual void accept(Visitor &v) const = 0; std::string str() const; - - template std::shared_ptr shared_from_base() { - return std::static_pointer_cast(shared_from_this()); - } }; // TODO decide what to do with this: diff --git a/lib/include/lydia/pl/cnf.hpp b/lib/include/lydia/pl/cnf.hpp index 96ff69b6..f9c93d22 100644 --- a/lib/include/lydia/pl/cnf.hpp +++ b/lib/include/lydia/pl/cnf.hpp @@ -28,22 +28,6 @@ class CNFTransformer : public Visitor { std::shared_ptr result; public: - // callbacks for LDLf - void visit(const Symbol &) override{}; - void visit(const LDLfBooleanAtom &) override{}; - void visit(const LDLfAnd &) override{}; - void visit(const LDLfOr &) override{}; - void visit(const LDLfNot &) override{}; - void visit(const LDLfDiamond &x) override{}; - void visit(const LDLfBox &x) override{}; - - // callbacks for regular expressions - void visit(const PropositionalRegExp &) override{}; - void visit(const TestRegExp &) override{}; - void visit(const UnionRegExp &) override{}; - void visit(const SequenceRegExp &) override{}; - void visit(const StarRegExp &) override{}; - // callbacks for propositional logic void visit(const PropositionalTrue &) override; void visit(const PropositionalFalse &) override; @@ -62,5 +46,8 @@ class CNFTransformer : public Visitor { set_prop_formulas to_container(prop_ptr p); prop_ptr to_cnf(const PropositionalFormula &); +std::vector> +to_clauses(const PropositionalFormula &cnf_f); + } // namespace lydia } // namespace whitemech \ No newline at end of file diff --git a/lib/include/lydia/pl/models.hpp b/lib/include/lydia/pl/models/base.hpp similarity index 62% rename from lib/include/lydia/pl/models.hpp rename to lib/include/lydia/pl/models/base.hpp index cdd2e32f..2ac0475b 100644 --- a/lib/include/lydia/pl/models.hpp +++ b/lib/include/lydia/pl/models/base.hpp @@ -16,29 +16,38 @@ * along with Lydia. If not, see . */ -#include #include +#include #include #include +#include +#include namespace whitemech { namespace lydia { -/*! - * Compute all the models of a propositional formula. - * - * @param f the propositional formula - * @return the set of the models of a formula +/* + * Functor to enumerate the models of a + * propositional formula. */ -std::vector all_models(const PropositionalFormula &f); +class ModelEnumerationStrategy { -/*! - * Compute the minimal models of a propositional formula. - * - * @param f the propositional formula - * @return the set of minimal models. - */ -std::vector minimal_models(const PropositionalFormula &f); +public: + /*! + * Compute all the models of a propositional formula. + * + * @param f the propositional formula + * @return the set of the models of a formula + */ + virtual std::vector + all_models(const PropositionalFormula &f) = 0; +}; + +template +std::vector all_models(const PropositionalFormula &f) { + T s = T(); + return s.all_models(f); +} } // namespace lydia } // namespace whitemech \ No newline at end of file diff --git a/lib/src/pl/models.cpp b/lib/include/lydia/pl/models/naive.hpp similarity index 50% rename from lib/src/pl/models.cpp rename to lib/include/lydia/pl/models/naive.hpp index 06d3da59..24c977b4 100644 --- a/lib/src/pl/models.cpp +++ b/lib/include/lydia/pl/models/naive.hpp @@ -1,3 +1,4 @@ +#pragma once /* * This file is part of Lydia. * @@ -15,30 +16,33 @@ * along with Lydia. If not, see . */ +#include #include -#include +#include +#include +#include +#include +#include namespace whitemech { namespace lydia { -std::vector all_models(const PropositionalFormula &f) { - std::vector models; - auto all_atoms = find_atoms(f); - std::vector all_interpretations = - powerset(all_atoms); - for (set_atoms_ptr &interpretation : all_interpretations) { - if (eval(f, interpretation)) { - models.emplace_back(interpretation); +class NaiveModelEnumerationStategy : public ModelEnumerationStrategy { + +public: + std::vector all_models(const PropositionalFormula &f) { + std::vector models; + auto all_atoms = find_atoms(f); + std::vector all_interpretations = + powerset(all_atoms); + for (set_atoms_ptr &interpretation : all_interpretations) { + if (eval(f, interpretation)) { + models.push_back(interpretation); + } } + return models; } - return models; -} - -std::vector minimal_models(const PropositionalFormula &f) { - // TODO - auto models = all_models(f); - return models; -} +}; } // namespace lydia } // namespace whitemech \ No newline at end of file diff --git a/lib/include/lydia/pl/models/sat.hpp b/lib/include/lydia/pl/models/sat.hpp new file mode 100644 index 00000000..37fa2b11 --- /dev/null +++ b/lib/include/lydia/pl/models/sat.hpp @@ -0,0 +1,104 @@ +#pragma once +/* + * This file is part of Lydia. + * + * Lydia is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * Lydia is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with Lydia. If not, see . + */ + +#include +#include +#include +#include +#include +#include +#include +#include + +namespace whitemech { +namespace lydia { + +class PopulateSolverVisitor : Visitor { + +private: + Minisat::Solver &s; + bool in_or = false; + bool in_not = false; + Minisat::vec current_clause; + +public: + std::map atom2idx; + std::vector idx2atom; + std::vector idx2var; + + /* + * in_clause: switch behavior in case you are in a clause or not. + */ + PopulateSolverVisitor(Minisat::Solver &s) : s{s} {} + + // callbacks for propositional logic + void visit(const PropositionalTrue &) override; + void visit(const PropositionalFalse &) override; + void visit(const PropositionalAtom &) override; + void visit(const PropositionalAnd &) override; + void visit(const PropositionalOr &) override; + void visit(const PropositionalNot &) override; + + void apply(const PropositionalFormula &b); +}; + +class SATModelEnumerationStategy : public ModelEnumerationStrategy { +private: + Minisat::Solver solver_; + +public: + explicit SATModelEnumerationStategy() : solver_{} {} + + set_atoms_ptr extract_model(Minisat::Solver &solver, + const std::vector &idx2atom) { + set_atoms_ptr result; + // TODO could simplify the raw loop + for (int i = 0; i < solver.model.size(); i++) { + if (solver.model[i] == Minisat::l_True) + result.insert(idx2atom[i]); + } + return result; + } + + void ban_solution(Minisat::Solver &solver) { + Minisat::vec clause; + for (int i = 0; i < solver.model.size(); i++) { + auto literal = Minisat::mkLit(i); + if (solver.model[i] == Minisat::l_True) + literal = ~literal; + clause.push(literal); + } + solver.addClause(clause); + } + + std::vector all_models(const PropositionalFormula &f) { + std::vector result; + auto cnf_f = to_cnf(f); + auto visitor = PopulateSolverVisitor(solver_); + visitor.apply(*cnf_f); + while (solver_.solve()) { + auto model = extract_model(solver_, visitor.idx2atom); + result.push_back(model); + ban_solution(solver_); + } + return result; + } +}; + +} // namespace lydia +} // namespace whitemech \ No newline at end of file diff --git a/lib/include/lydia/pl/models_sat.hpp b/lib/include/lydia/pl/models_sat.hpp deleted file mode 100644 index a8712708..00000000 --- a/lib/include/lydia/pl/models_sat.hpp +++ /dev/null @@ -1,72 +0,0 @@ -#pragma once -/* - * This file is part of Lydia. - * - * Lydia is free software: you can redistribute it and/or modify - * it under the terms of the GNU General Public License as published by - * the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * Lydia is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with Lydia. If not, see . - */ - -#include -#include -#include -#include - -namespace whitemech { -namespace lydia { - -/* - * Check whether the formula is satisfiable. - */ -bool is_sat(const PropositionalFormula &f); - -class SATSolverWrapper : public Visitor { -private: - std::vector clause; - void apply(const PropositionalFormula &); - -public: - std::vector> clauses; - std::map atom2id; - std::map id2atom; - std::vector varset; - - set_atoms_ptr get_model(const std::vector &model); - set_atoms_ptr get_model(const std::vector &model); - CMSat::SATSolver get_solver(); - bool is_sat(); - - std::optional> find_minimal_model(); - std::vector quickxplain(std::vector &, - std::vector &, bool has_set); - bool predicate(const std::vector &v); - - void visit(const PropositionalTrue &) override; - void visit(const PropositionalFalse &) override; - void visit(const PropositionalAtom &) override; - void visit(const PropositionalAnd &) override; - void visit(const PropositionalOr &) override; - void visit(const PropositionalNot &) override; - - void visit_atom(const atom_ptr &, bool is_inverted); - static SATSolverWrapper create(const PropositionalFormula &f); -}; - -std::vector all_models_sat(const PropositionalFormula &f); - -std::vector -all_minimal_models_sat(const PropositionalFormula &f); - -set_atoms_ptr minimal_model_sat(const PropositionalFormula &f); - -} // namespace lydia -} // namespace whitemech \ No newline at end of file diff --git a/lib/include/lydia/to_dfa/strategies/sat.hpp b/lib/include/lydia/to_dfa/strategies/sat.hpp index 8fc18734..5a28d77c 100644 --- a/lib/include/lydia/to_dfa/strategies/sat.hpp +++ b/lib/include/lydia/to_dfa/strategies/sat.hpp @@ -33,12 +33,13 @@ class SATStrategy : public Strategy { private: const CUDD::Cudd &mgr; const size_t max_nb_bits; + dfa_ptr automaton; public: explicit SATStrategy(const CUDD::Cudd &mgr, uint32_t max_nb_bits = 10) : mgr{mgr}, max_nb_bits{max_nb_bits} {}; - std::shared_ptr to_dfa(const LDLfFormula &formula); + dfa_ptr to_dfa(const LDLfFormula &formula); std::vector> next_transitions(const DFAState &state); diff --git a/lib/src/pl/cnf.cpp b/lib/src/pl/cnf.cpp index a925f8ef..97973893 100644 --- a/lib/src/pl/cnf.cpp +++ b/lib/src/pl/cnf.cpp @@ -29,7 +29,8 @@ void CNFTransformer::visit(const PropositionalFalse &) { } void CNFTransformer::visit(const PropositionalAtom &f) { - result = std::make_shared(f.symbol); + result = + std::static_pointer_cast(f.shared_from_this()); } void CNFTransformer::visit(const PropositionalAnd &f) { @@ -45,7 +46,7 @@ void CNFTransformer::visit(const PropositionalAnd &f) { args.insert(subformula_cnf); } } - result = std::make_shared(args); + result = logical_and(args); } void CNFTransformer::visit(const PropositionalOr &f) { diff --git a/lib/src/pl/eval.cpp b/lib/src/pl/eval.cpp index 027a5358..04c8d3ea 100644 --- a/lib/src/pl/eval.cpp +++ b/lib/src/pl/eval.cpp @@ -14,11 +14,10 @@ * You should have received a copy of the GNU General Public License * along with Lydia. If not, see . */ -#include #include #include #include -#include +#include #include namespace whitemech { diff --git a/lib/src/pl/logic.cpp b/lib/src/pl/logic.cpp index 2daeb63c..12283140 100644 --- a/lib/src/pl/logic.cpp +++ b/lib/src/pl/logic.cpp @@ -15,7 +15,6 @@ * along with Lydia. If not, see . */ #include -#include #include #include #include diff --git a/lib/src/pl/models/sat.cpp b/lib/src/pl/models/sat.cpp new file mode 100644 index 00000000..80872fdf --- /dev/null +++ b/lib/src/pl/models/sat.cpp @@ -0,0 +1,80 @@ +/* + * This file is part of Lydia. + * + * Lydia is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * Lydia is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with Lydia. If not, see . + */ + +#include +#include +#include + +namespace whitemech { +namespace lydia { + +void PopulateSolverVisitor::visit(const PropositionalTrue &) { + if (in_or) { + // TODO the true helps only if in the or. We should simplify the clause in + // this case. + } +} +void PopulateSolverVisitor::visit(const PropositionalFalse &) { + if (not in_or) { + // we must be in the and... add empty clause + s.addEmptyClause(); + } +} +void PopulateSolverVisitor::visit(const PropositionalAtom &f) { + atom_ptr f_ptr = + std::static_pointer_cast(f.shared_from_this()); + auto var_index = atom2idx.find(f_ptr); + int index = 0; + if (var_index == atom2idx.end()) { + auto new_var = s.newVar(); + index = idx2var.size(); + idx2var.push_back(new_var); + idx2atom.push_back(f_ptr); + } else { + index = var_index->second; + } + Minisat::Lit literal = Minisat::mkLit(idx2var[index]); + if (in_not) + literal = ~literal; + if (in_or) + current_clause.push(literal); + else + s.addClause(literal); +} +void PopulateSolverVisitor::visit(const PropositionalAnd &f) { + for (const auto &subf : f.get_container()) + subf->accept(*this); +} +void PopulateSolverVisitor::visit(const PropositionalOr &f) { + in_or = true; + for (const auto &subf : f.get_container()) + subf->accept(*this); + s.addClause(current_clause); + in_or = false; +} +void PopulateSolverVisitor::visit(const PropositionalNot &f) { + in_not = true; + f.get_arg()->accept(*this); + in_not = false; +} + +void PopulateSolverVisitor::apply(const PropositionalFormula &b) { + b.accept(*this); +} + +} // namespace lydia +} // namespace whitemech \ No newline at end of file diff --git a/lib/src/pl/models_sat.cpp b/lib/src/pl/models_sat.cpp deleted file mode 100644 index 6ebe5e63..00000000 --- a/lib/src/pl/models_sat.cpp +++ /dev/null @@ -1,225 +0,0 @@ -/* - * This file is part of Lydia. - * - * Lydia is free software: you can redistribute it and/or modify - * it under the terms of the GNU General Public License as published by - * the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * Lydia is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with Lydia. If not, see . - */ - -#include -#include -#include - -namespace whitemech { -namespace lydia { - -bool SATSolverWrapper::is_sat() { - return this->get_solver().solve() == CMSat::l_True; -} - -std::vector all_models_sat(const PropositionalFormula &f) { - std::vector models; - auto sat_converter = SATSolverWrapper::create(f); - auto solver = sat_converter.get_solver(); - - while (true) { - CMSat::lbool ret = solver.solve(); - if (ret != CMSat::l_True) { - assert(ret == CMSat::l_False); - // All solutions found. - return models; - } - models.push_back(sat_converter.get_model(solver.get_model())); - - // Banning found solution - std::vector ban_solution; - for (uint32_t var = 0; var < solver.nVars(); var++) { - if (solver.get_model()[var] != CMSat::l_Undef) { - ban_solution.emplace_back(var, - solver.get_model()[var] == CMSat::l_True); - } - } - solver.add_clause(ban_solution); - } -} - -set_atoms_ptr minimal_model_sat(const PropositionalFormula &f) { - set_atoms_ptr result; - auto converter = SATSolverWrapper::create(f); - return result; -} - -std::vector -all_minimal_models_sat(const PropositionalFormula &f) { - std::vector models; - auto sat_converter = SATSolverWrapper::create(f); - - while (true) { - auto model = sat_converter.find_minimal_model(); - if (!model.has_value()) { - return models; - } - models.push_back(sat_converter.get_model(model.value())); - - // Banning found solution - std::vector ban_solution; - for (const auto &i : model.value()) { - ban_solution.emplace_back(i, true); - } - sat_converter.clauses.emplace_back(ban_solution); - } -} - -bool is_sat(const PropositionalFormula &f) { - auto sat_converter = SATSolverWrapper::create(f); - return sat_converter.get_solver().solve() == CMSat::l_True; -} - -std::optional> SATSolverWrapper::find_minimal_model() { - if (this->get_solver().solve() != CMSat::l_True) { - return std::nullopt; - } - auto b = std::vector(); - auto target = std::vector(this->id2atom.size()); - std::iota(target.begin(), target.end(), 0); - auto model = quickxplain(b, target, true); - return model; -} - -void SATSolverWrapper::visit(const PropositionalTrue &) {} - -void SATSolverWrapper::visit(const PropositionalFalse &) {} - -void SATSolverWrapper::visit(const PropositionalAtom &f) { - auto x = - std::static_pointer_cast(f.shared_from_this()); - visit_atom(x, false); -} - -void SATSolverWrapper::visit(const PropositionalAnd &f) { - for (const auto &subformula : f.get_container()) { - clause.clear(); - apply(*subformula); - clauses.emplace_back(clause); - } -} - -void SATSolverWrapper::visit(const PropositionalOr &f) { - for (const auto &subformula : f.get_container()) { - apply(*subformula); - } -} - -void SATSolverWrapper::visit(const PropositionalNot &f) { - auto x = std::static_pointer_cast(f.get_arg()); - visit_atom(x, true); -} - -void SATSolverWrapper::apply(const PropositionalFormula &f) { f.accept(*this); } - -set_atoms_ptr -SATSolverWrapper::get_model(const std::vector &model) { - set_atoms_ptr result; - for (uint32_t i = 0; i < id2atom.size(); i++) { - if (model[i] == CMSat::l_True) - result.insert(this->id2atom[i]); - } - return result; -} -set_atoms_ptr SATSolverWrapper::get_model(const std::vector &model) { - set_atoms_ptr result; - for (const auto &i : model) { - result.insert(this->id2atom[i]); - } - return result; -} - -SATSolverWrapper SATSolverWrapper::create(const PropositionalFormula &f) { - auto converter = SATSolverWrapper(); - converter.apply(f); - if (is_a(f)) { - converter.clause.clear(); - converter.clauses.emplace_back(converter.clause); - } else if (!is_a(f) and !is_a(f)) { - // add clause - converter.clauses.emplace_back(converter.clause); - } - converter.varset = std::vector(converter.id2atom.size()); - std::iota(converter.varset.begin(), converter.varset.end(), 0); - return converter; -} - -void SATSolverWrapper::visit_atom(const atom_ptr &f, bool is_inverted) { - auto it = atom2id.find(f); - uint32_t id; - if (it == atom2id.end()) { - id = atom2id.size(); - atom2id[f] = id; - id2atom[id] = f; - } else { - id = it->second; - } - clause.emplace_back(id, is_inverted); -} - -CMSat::SATSolver SATSolverWrapper::get_solver() { - auto solver = CMSat::SATSolver(); - solver.set_num_threads(4); - solver.new_vars(this->id2atom.size()); - for (const auto &clause_ : this->clauses) { - solver.add_clause(clause_); - } - return solver; -} - -bool SATSolverWrapper::predicate(const std::vector &v) { - auto solver = this->get_solver(); - std::vector negated_atoms; - std::set_difference(varset.begin(), varset.end(), v.begin(), v.end(), - std::inserter(negated_atoms, negated_atoms.begin())); - for (const auto &x : negated_atoms) { - solver.add_clause(std::vector{CMSat::Lit(x, true)}); - } - return solver.solve() == CMSat::l_True; -} - -std::vector SATSolverWrapper::quickxplain(std::vector &b, - std::vector &t, - bool has_set) { - if (has_set and this->predicate(b)) { - return std::vector(); - } - if (t.size() == 1) { - return t; - } - size_t m = t.size() / 2; - std::vector t1, t2; - t1 = std::vector(t.begin(), t.begin() + m); - t2 = std::vector(t.begin() + m, t.end()); - assert(t1.size() + t2.size() == t.size()); - - // no need to sort - // std::sort(t1.begin(), t1.end()); - // std::sort(t2.begin(), t2.end()); - - auto b_union_t1 = set_union(b, t1); - auto m2 = quickxplain(b_union_t1, t2, not t1.empty()); - - auto b_union_m2 = set_union(b, m2); - auto m1 = quickxplain(b_union_m2, t1, not m2.empty()); - - auto m1_union_m2 = set_union(m1, m2); - return m1_union_m2; -} - -} // namespace lydia -} // namespace whitemech \ No newline at end of file diff --git a/lib/src/to_dfa/nfa_state.cpp b/lib/src/to_dfa/nfa_state.cpp index 0fe5a334..00483ab7 100644 --- a/lib/src/to_dfa/nfa_state.cpp +++ b/lib/src/to_dfa/nfa_state.cpp @@ -16,7 +16,7 @@ */ #include -#include +#include #include #include diff --git a/lib/src/to_dfa/strategies/naive.cpp b/lib/src/to_dfa/strategies/naive.cpp index 41d32b43..a7beeed9 100644 --- a/lib/src/to_dfa/strategies/naive.cpp +++ b/lib/src/to_dfa/strategies/naive.cpp @@ -15,7 +15,8 @@ * along with Lydia. If not, see . */ -#include +#include +#include #include namespace whitemech { @@ -110,7 +111,7 @@ set_nfa_states NaiveStrategy::next_states(const NFAState &state, PropositionalAnd(set_prop_formulas(args.begin(), args.end())); set_nfa_states result; - auto models = minimal_models(conjunction); + auto models = all_models(conjunction); for (const auto &model : models) { set_formulas tmp; for (const auto &atom : model) { diff --git a/lib/src/to_dfa/strategies/sat.cpp b/lib/src/to_dfa/strategies/sat.cpp index ad95272b..a3762890 100644 --- a/lib/src/to_dfa/strategies/sat.cpp +++ b/lib/src/to_dfa/strategies/sat.cpp @@ -15,7 +15,7 @@ * along with Lydia. If not, see . */ #include -#include +#include #include #include @@ -29,7 +29,7 @@ struct cmp_set_of_ptr { } }; -std::shared_ptr SATStrategy::to_dfa(const LDLfFormula &formula) { +dfa_ptr SATStrategy::to_dfa(const LDLfFormula &formula) { // build initial state of the DFA. auto formula_nnf = to_nnf(formula); set_formulas initial_state_formulas{formula_nnf}; @@ -43,8 +43,7 @@ std::shared_ptr SATStrategy::to_dfa(const LDLfFormula &formula) { for (const auto &atom : atoms) atom2index[atom] = index++; - std::shared_ptr automaton = - std::make_shared(mgr, max_nb_bits, atoms.size()); + automaton = std::make_shared(mgr, max_nb_bits, atoms.size()); automaton->add_state(); automaton->set_initial_state(1); @@ -125,6 +124,75 @@ SATStrategy::next_transitions(const DFAState &state) { return result; } +//// only works if formula is in CNF +// void update_model(operations_research::sat::CpModelBuilder& cp_model, +// const PropositionalFormula& f, +// const std::map& atom2var){ +// if (is_a(f)){ +// cp_model.AddBoolOr({cp_model.TrueVar()}); +// } +// else if (is_a(f)){ +// cp_model.AddBoolAnd({cp_model.FalseVar()}); +// } +// else if (is_a(f)){ +// auto casted_p = std::static_pointer_cast(f.shared_from_this()); auto var = +// atom2var.at(casted_p); cp_model.AddBoolAnd({var}); +// } +// else if (is_a(f)){ +// const auto& casted_p = dynamic_cast(f); +// auto var = atom2var.at(casted_p.get_arg()); +// cp_model.AddBoolAnd({Not(var)}); +// } +// else if (is_a(f)){ +// const auto& or_ = dynamic_cast(f); +// std::vector or_of_vars; +// or_of_vars.reserve(or_.get_container().size()); +// for (const auto& p :or_.get_container()){ +// if (is_a(*p)) +// or_of_vars.push_back({cp_model.TrueVar()}); +// else if(is_a(*p)) +// or_of_vars.push_back({cp_model.FalseVar()}); +// else if(is_a(*p)){ +// const auto& casted_p = dynamic_cast(*p); +// auto var = atom2var.at(casted_p.get_arg()); +// or_of_vars.push_back({Not(var)}); +// } +// else{ +// auto casted_p = std::static_pointer_cast(p); +// or_of_vars.push_back(atom2var.at(casted_p)); +// } +// } +// cp_model.AddBoolOr(or_of_vars); +// } +// else if (is_a(f)){ +// const auto& and_ = dynamic_cast(f); +// std::vector and_of_vars; +// for (const auto& subf: and_.get_container()){ +// if (is_a(*subf)){ +// update_model(cp_model, *subf, atom2var); +// } +// else if (is_a(*subf)) +// and_of_vars.push_back({cp_model.TrueVar()}); +// else if(is_a(*subf)) +// and_of_vars.push_back({cp_model.FalseVar()}); +// else if(is_a(*subf)){ +// const auto& casted_p = dynamic_cast(*subf); +// auto var = atom2var.at(casted_p.get_arg()); +// and_of_vars.push_back({Not(var)}); +// } +// else{ +// auto casted_p = std::static_pointer_cast(subf); +// and_of_vars.push_back(atom2var.at(casted_p)); +// } +// } +// cp_model.AddBoolAnd(and_of_vars); +// } +// +//} + std::vector> SATStrategy::next_transitions(const NFAState &state) { set_prop_formulas setPropFormulas; @@ -132,7 +200,6 @@ SATStrategy::next_transitions(const NFAState &state) { const auto &delta_formula = delta_symbolic(*f, false); setPropFormulas.insert(delta_formula); } - // Don't do CNF, o/w the replacement does not work auto and_ = logical_and(setPropFormulas); return this->next_transitions_from_delta_formula(*and_); } @@ -142,46 +209,105 @@ SATStrategy::next_transitions_from_delta_formula( const PropositionalFormula &f) { std::vector> result; std::map symbol2nfastates; - set_formulas quoted_formulas; + set_atoms_ptr quoted_formulas; set_atoms_ptr propositionals; auto atoms = find_atoms(f); - for (const atom_ptr &ptr : atoms) { - if (is_a(*ptr->symbol)) - quoted_formulas.insert( - dynamic_cast(*ptr->symbol).formula); - else - propositionals.insert(ptr); - } - - auto symbols = powerset(propositionals); - for (const auto &symbol : symbols) { - std::map replacements; - for (const auto &x : propositionals) { - replacements[x] = boolean_prop(!(symbol.end() == symbol.find(x))); - } - set_nfa_states nfa_states; - symbol2nfastates[symbol] = set_nfa_states(); - - auto replaced_delta = replace(replacements, f); - const auto &all_minimal_models = all_models(*replaced_delta); - for (const auto &model : all_minimal_models) { - set_formulas current_formulas; - for (const auto ¤t_quoted_formula : model) { - current_formulas.insert( - dynamic_cast(*current_quoted_formula->symbol) - .formula); - } - symbol2nfastates[symbol].insert( - std::make_shared(current_formulas)); - } - } - - result.reserve(symbol2nfastates.size()); - for (const auto &pair : symbol2nfastates) { - result.emplace_back(pair); - } return result; } +// std::vector> +// SATStrategy::next_transitions_from_delta_formula( +// const PropositionalFormula &f) { +// std::vector> result; +// std::map symbol2nfastates; +// +// set_atoms_ptr quoted_formulas; +// set_atoms_ptr propositionals; +// auto atoms = find_atoms(f); +// std::map +// atom2var; std::vector all_vars; +// std::vector idx2atom; +// idx2atom.reserve(atoms.size()); +// all_vars.reserve(atoms.size()); +// +// //build SAT problem +// operations_research::sat::CpModelBuilder cp_model; +// for (const atom_ptr &ptr : atoms) { +// std::string name; +// if (is_a(*ptr->symbol)) { +// quoted_formulas.insert(ptr); +// name = "q_" + std::to_string(quoted_formulas.size()); +// } +// else { +// propositionals.insert(ptr); +// name = "p_" + std::to_string(propositionals.size()); +// } +// auto var = cp_model.NewBoolVar().WithName(name); +// atom2var[ptr] = var; +// idx2atom.push_back(ptr); +// all_vars.push_back(var); +// } +// update_model(cp_model, f, atom2var); +// operations_research::sat::Model model; +// int num_solutions = 0; +// model.Add(operations_research::sat::NewFeasibleSolutionObserver +// ([&](const operations_research::sat::CpSolverResponse& +// response) { +// LOG(INFO) << "Solution " << num_solutions; +// num_solutions++; +// })); +// operations_research::sat::SatParameters parameters; +// parameters.set_enumerate_all_solutions(true); +// model.Add(NewSatParameters(parameters)); +// operations_research::sat::TableConstraint t = +// cp_model.AddForbiddenAssignments(all_vars); +// +// std::vector> solutions; +// operations_research::sat::CpSolverResponse response = +// Solve(cp_model.Build()); while (response.status() == +// operations_research::sat::CpSolverStatus::FEASIBLE){ +// std::vector solution; +// solution.reserve(atom2var.size()); +// for (const auto& atom_var_pair : atom2var){ +// solution.push_back(SolutionIntegerValue(response, +// atom_var_pair.second)); +// } +// solutions.push_back(solution); +// } +// const operations_research::sat::CpSolverResponse response = +// SolveCpModel(cp_model.Build(), &model); LOG(INFO) << "Number of solutions +// found: " << num_solutions; std::cout<< "hello"< replacements; +// for (const auto &x : propositionals) { +// replacements[x] = boolean_prop(!(symbol.end() == symbol.find(x))); +// } +// set_nfa_states nfa_states; +// symbol2nfastates[symbol] = set_nfa_states(); +// +// auto replaced_delta = replace(replacements, f); +// const auto &all_minimal_models = all_models(*replaced_delta); +// for (const auto &model : all_minimal_models) { +// set_formulas current_formulas; +// for (const auto ¤t_quoted_formula : model) { +// current_formulas.insert( +// dynamic_cast(*current_quoted_formula->symbol) +// .formula); +// } +// symbol2nfastates[symbol].insert( +// std::make_shared(current_formulas)); +// } +// } +// +// result.reserve(symbol2nfastates.size()); +// for (const auto &pair : symbol2nfastates) { +// result.emplace_back(pair); +// } +// return result; +// } + } // namespace lydia } // namespace whitemech \ No newline at end of file diff --git a/lib/test/CMakeLists.txt b/lib/test/CMakeLists.txt index ef3bdced..60f65b23 100644 --- a/lib/test/CMakeLists.txt +++ b/lib/test/CMakeLists.txt @@ -37,7 +37,11 @@ file (GLOB_RECURSE TEST_HEADER_FILES "${TEST_SRC_PATH}/*.hpp") add_executable (${TEST_APP_NAME} ${TEST_SOURCE_FILES} ${TEST_HEADER_FILES}) #add the library -target_link_libraries (${TEST_APP_NAME} ${LIB_NAME} Threads::Threads ${CUDD_LIBRARIES}) +target_link_libraries (${TEST_APP_NAME} + ${LIB_NAME} + Threads::Threads + ${CUDD_LIBRARIES} + ${MINISAT_LIBRARIES}) # Turn on CMake testing capabilities enable_testing() diff --git a/lib/test/src/test_misc.cpp b/lib/test/src/test_misc.cpp index b824327c..fc92cd0b 100644 --- a/lib/test/src/test_misc.cpp +++ b/lib/test/src/test_misc.cpp @@ -91,4 +91,36 @@ TEST_CASE("Test bdd2dot", "[dfa]") { dfa_to_bdds(my_dfa, output_dir_path); } +// TEST_CASE("glucose", "[glucose]") { +// Glucose::SimpSolver solver; +// solver.verbosity = -1; +// solver.verbEveryConflicts = -1; +// +// // Create variables +// auto A = solver.newVar(); +// auto B = solver.newVar(); +// auto C = solver.newVar(); +// +// // Create the clauses +// solver.addClause( Glucose::mkLit(A), Glucose::mkLit(B), +// Glucose::mkLit(C)); solver.addClause(~Glucose::mkLit(A), +// Glucose::mkLit(B), Glucose::mkLit(C)); solver.addClause( +// Glucose::mkLit(A), ~Glucose::mkLit(B), Glucose::mkLit(C)); +// solver.addClause( Glucose::mkLit(A), Glucose::mkLit(B), +// ~Glucose::mkLit(C)); +// +// // Check for solution and retrieve model if found +// auto sat = solver.solve(); +// if (sat) { +// std::clog << "SAT\n" +// << "Model found:\n"; +// std::clog << "A := " << (solver.modelValue(A) == l_True) << '\n'; +// std::clog << "B := " << (solver.modelValue(B) == l_True) << '\n'; +// std::clog << "C := " << (solver.modelValue(C) == l_True) << '\n'; +// } else { +// std::clog << "UNSAT\n"; +// } +// +//} + } // namespace whitemech::lydia::Test \ No newline at end of file diff --git a/lib/test/src/test_propositional_logic.cpp b/lib/test/src/test_propositional_logic.cpp index 91e745ce..5b32e327 100644 --- a/lib/test/src/test_propositional_logic.cpp +++ b/lib/test/src/test_propositional_logic.cpp @@ -15,11 +15,12 @@ * along with Lydia. If not, see . */ #include -#include #include #include #include -#include +#include +#include +#include namespace whitemech::lydia::Test { TEST_CASE("Propositional Logic", "[pl/logic]") { @@ -267,78 +268,29 @@ TEST_CASE("to cnf", "[pl/cnf]") { } } -TEST_CASE("Test Cryptominisat", "[cryptominisat]") { - CMSat::SATSolver solver; - std::vector clause; - - // Let's use 4 threads - solver.set_num_threads(4); - - // without literals - auto result = solver.solve(); - REQUIRE(result == CMSat::l_True); - - // We need 3 variables. They will be: 0,1,2 - // Variable numbers are always trivially increasing - solver.new_vars(3); - - // add "1 0" - clause.emplace_back(0, false); - solver.add_clause(clause); - - // add "-2 0" - clause.clear(); - clause.emplace_back(1, true); - solver.add_clause(clause); - - // add "-1 2 3 0" - clause.clear(); - clause.emplace_back(0, true); - clause.emplace_back(1, false); - clause.emplace_back(2, false); - solver.add_clause(clause); - - CMSat::lbool ret = solver.solve(); - REQUIRE(ret == CMSat::l_True); - std::cout << "Solution is: " << solver.get_model()[0] << ", " - << solver.get_model()[1] << ", " << solver.get_model()[2] - << std::endl; - - // assumes 3 = FALSE, no solutions left - std::vector assumptions; - assumptions.emplace_back(2, true); - ret = solver.solve(&assumptions); - REQUIRE(ret == CMSat::l_False); - - // without assumptions we still have a solution - ret = solver.solve(); - REQUIRE(ret == CMSat::l_True); - - // add "-3 0" - // No solutions left, UNSATISFIABLE returned - clause.clear(); - clause.emplace_back(2, true); - solver.add_clause(clause); - ret = solver.solve(); - REQUIRE(ret == CMSat::l_False); -} - -TEST_CASE("is_sat", "[pl/models]") { - auto t = boolean_prop(true); - auto f = boolean_prop(false); - auto p = prop_atom("p"); - auto q = prop_atom("q"); - REQUIRE(is_sat(*t)); - REQUIRE(!is_sat(*f)); - REQUIRE(is_sat(*p)); - REQUIRE(is_sat(*q)); - REQUIRE(is_sat(*logical_or({p, q}))); - REQUIRE(is_sat(*logical_and({p, q}))); - - auto non_sat = - logical_and({logical_or({p, q}), p->logical_not(), q->logical_not()}); - REQUIRE(!is_sat(*non_sat)); -} +// TEST_CASE("is_sat", "[pl/models]") { +// auto t = boolean_prop(true); +// auto f = boolean_prop(false); +// auto p = prop_atom("p"); +// auto q = prop_atom("q"); +// REQUIRE(is_sat(*t)); +// REQUIRE(!is_sat(*f)); +// REQUIRE(is_sat(*p)); +// REQUIRE(is_sat(*q)); +// REQUIRE(is_sat(*logical_or({p, q}))); +// REQUIRE(is_sat(*logical_and({p, q}))); +// +// auto non_sat = +// logical_and({logical_or({p, q}), p->logical_not(), q->logical_not()}); +// REQUIRE(!is_sat(*non_sat)); +//} + +struct SetComparator { + template + bool operator()(const std::set &lhs, const std::set &rhs) const { + return unified_compare(lhs, rhs) == -1; + } +}; TEST_CASE("All models", "[pl/models]") { auto p = prop_atom("p"); @@ -347,111 +299,68 @@ TEST_CASE("All models", "[pl/models]") { auto true_ = boolean_prop(true); auto false_ = boolean_prop(false); + auto model_enumeration_function = + GENERATE(all_models, + all_models); + SECTION("models of true") { - auto models = all_models_sat(*true_); + auto models = model_enumeration_function(*true_); REQUIRE(models.size() == 1); REQUIRE(models[0].empty()); } SECTION("models of false") { - auto models = all_models_sat(*false_); + auto models = model_enumeration_function(*false_); REQUIRE(models.empty()); } SECTION("models of p") { - auto models = all_models_sat(*p); + auto models = model_enumeration_function(*p); REQUIRE(models.size() == 1); - REQUIRE(models[0] == set_atoms_ptr{p}); + auto expected_model = set_atoms_ptr({p}); + auto actual_model = models[0]; + REQUIRE(unified_eq(actual_model, expected_model)); } SECTION("models of ~q") { - auto models = all_models_sat(*p->logical_not()); + auto models = model_enumeration_function(*q->logical_not()); REQUIRE(models.size() == 1); REQUIRE(models[0].empty()); } SECTION("models of p | q") { - auto models = all_models_sat(*logical_or({p, q})); + auto models = model_enumeration_function(*logical_or({p, q})); REQUIRE(models.size() == 3); - auto expected_models = std::set({ + auto expected_models = std::set({ set_atoms_ptr({p, q}), set_atoms_ptr({p}), set_atoms_ptr({q}), }); - auto actual_models = std::set(models.begin(), models.end()); - REQUIRE(expected_models == actual_models); + auto actual_models = + std::set(models.begin(), models.end()); + REQUIRE(unified_eq(expected_models, actual_models)); } SECTION("models of p & q") { - auto models = all_models_sat(*logical_and({p, q})); + auto models = model_enumeration_function(*logical_and({p, q})); REQUIRE(models.size() == 1); - REQUIRE(models[0] == set_atoms_ptr({p, q})); + REQUIRE(unified_eq(models[0], set_atoms_ptr({p, q}))); } SECTION("models of !(p | q)") { - auto models = all_models_sat(*logical_or({p, q})->logical_not()); + auto models = + model_enumeration_function(*logical_or({p, q})->logical_not()); REQUIRE(models.size() == 1); - REQUIRE(models[0] == set_atoms_ptr({})); + REQUIRE(unified_eq(models[0], set_atoms_ptr({}))); } SECTION("models of r & (p | q)") { auto f = logical_and({r, logical_or({p, q})}); - auto models = all_models_sat(*f); + auto models = model_enumeration_function(*f); REQUIRE(models.size() == 3); - auto expected_models = std::set({ + auto expected_models = std::set({ set_atoms_ptr({r, p}), set_atoms_ptr({r, q}), set_atoms_ptr({r, p, q}), }); - auto actual_models = std::set(models.begin(), models.end()); - REQUIRE(actual_models == expected_models); - } -} - -TEST_CASE("Minmal models", "[pl/models]") { - auto p = prop_atom("p"); - auto q = prop_atom("q"); - auto r = prop_atom("r"); - auto true_ = boolean_prop(true); - auto false_ = boolean_prop(false); - - SECTION("models of true") { - auto models = all_minimal_models_sat(*true_); - REQUIRE(models.size() == 1); - REQUIRE(models[0].empty()); - } - SECTION("models of false") { - auto models = all_minimal_models_sat(*false_); - REQUIRE(models.empty()); - } - - SECTION("models of p") { - auto models = all_minimal_models_sat(*p); - REQUIRE(models.size() == 1); - REQUIRE(models[0] == set_atoms_ptr{p}); - } - SECTION("models of ~q") { - auto models = all_minimal_models_sat(*p->logical_not()); - REQUIRE(models.size() == 1); - REQUIRE(models[0].empty()); - } - - SECTION("models of p | q") { - auto models = all_minimal_models_sat(*logical_or({p, q})); - REQUIRE(models.size() == 2); - auto expected_models = std::set({ - set_atoms_ptr({p}), - set_atoms_ptr({q}), - }); - auto actual_models = std::set(models.begin(), models.end()); - REQUIRE(expected_models == actual_models); - } - - SECTION("models of r & (p | q)") { - auto f = logical_and({r, logical_or({p, q})}); - auto models = all_minimal_models_sat(*f); - REQUIRE(models.size() == 2); - auto expected_models = std::set({ - set_atoms_ptr({r, p}), - set_atoms_ptr({r, q}), - }); - auto actual_models = std::set(models.begin(), models.end()); - REQUIRE(expected_models == actual_models); + auto actual_models = + std::set(models.begin(), models.end()); + REQUIRE(unified_eq(actual_models, expected_models)); } } diff --git a/third_party/CMakeLists.txt b/third_party/CMakeLists.txt index e8fed0b3..f2b04c04 100644 --- a/third_party/CMakeLists.txt +++ b/third_party/CMakeLists.txt @@ -39,8 +39,6 @@ set (GOOGLE_BENCHMARK_INCLUDE_PATH "${GOOGLE_BENCHMARK_MODULE_PATH}/include") set(BENCHMARK_ENABLE_GTEST_TESTS OFF) add_subdirectory(${GOOGLE_BENCHMARK_MODULE_PATH}) -#include custom cmake function -include ( "${CATCH_MODULE_PATH}/contrib/ParseAndAddCatchTests.cmake") # ------------------------------------------------------------------------- # spdlog @@ -86,11 +84,31 @@ set (CUDD_INCLUDE_PATH ${CUDD_INCLUDE_DIRS}) # ------------------------------------------------------------------------- +# ------------------------------------------------------------------------- +# MiniSAT + +#configure directories +set (MINISAT_MODULE_PATH "${THIRD_PARTY_MODULE_PATH}/minisat") +set (MINISAT_INCLUDE_PATH "${MINISAT_MODULE_PATH}") +add_subdirectory(${MINISAT_MODULE_PATH}) +set(MINISAT_LIBRARIES minisat-lib-static PARENT_SCOPE) + +# ------------------------------------------------------------------------- + #set variables -set (THIRD_PARTY_INCLUDE_PATH ${FMT_INCLUDE_PATH} ${SPDLOG_INCLUDE_PATH} ${CLI11_INCLUDE_PATH} ${CUDD_INCLUDE_PATH} ${GOOGLE_BENCHMARK_INCLUDE_PATH}) +set (THIRD_PARTY_INCLUDE_PATH + ${FMT_INCLUDE_PATH} + ${SPDLOG_INCLUDE_PATH} + ${CLI11_INCLUDE_PATH} + ${CUDD_INCLUDE_PATH} + ${GOOGLE_BENCHMARK_INCLUDE_PATH} + ${MINISAT_INCLUDE_PATH}) #set variables for tests -set (TEST_THIRD_PARTY_INCLUDE_PATH ${CATCH_INCLUDE_PATH} ${CPPITERTOOLS_INCLUDE_PATH}) +set (TEST_THIRD_PARTY_INCLUDE_PATH + ${CATCH_INCLUDE_PATH} + ${CPPITERTOOLS_INCLUDE_PATH} + ${MINISAT_INCLUDE_PATH}) #export vars set (THIRD_PARTY_INCLUDE_PATH ${THIRD_PARTY_INCLUDE_PATH} PARENT_SCOPE) diff --git a/third_party/minisat b/third_party/minisat new file mode 160000 index 00000000..78505a63 --- /dev/null +++ b/third_party/minisat @@ -0,0 +1 @@ +Subproject commit 78505a630fc6c6f6c78495c980c702d095d01d7e