diff --git a/CMakeLists.txt b/CMakeLists.txt index 4c32148..163c971 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -47,4 +47,13 @@ target_link_libraries(glucose-simp glucose) # PARALLEL STUFF: add_library(glucosep ${lib_type} ${lib_srcs} ${lib_parallel_srcs}) add_executable(glucose-syrup ${main_parallel}) -target_link_libraries(glucose-syrup glucosep ${CMAKE_THREAD_LIBS_INIT}) \ No newline at end of file +target_link_libraries(glucose-syrup glucosep ${CMAKE_THREAD_LIBS_INIT}) + +install(TARGETS glucose + RUNTIME DESTINATION bin + LIBRARY DESTINATION lib + ARCHIVE DESTINATION lib) + +install(DIRECTORY simp + DESTINATION include/glucose + FILES_MATCHING PATTERN "*.hpp") \ No newline at end of file diff --git a/simp/StdSimpSolver.cc b/simp/StdSimpSolver.cc new file mode 100644 index 0000000..1ef856a --- /dev/null +++ b/simp/StdSimpSolver.cc @@ -0,0 +1,136 @@ + +#include "StdSimpSolver.hpp" +#include "SimpSolver.h" +namespace Glucose +{ + Lit makeLit(SimpSolver *solver,int val) + { + int value = abs(val) - 1; + while (value>= solver->nVars()) + { + solver->newVar(); + } + return mkLit(value, val < 0); + } + StdSimpSolver::StdSimpSolver() + { + this->solver = new SimpSolver(); + } + StdSimpSolver::~StdSimpSolver() + { + SimpSolver *solver = (SimpSolver *)this->solver; + delete solver; + this->solver = nullptr; + } + int StdSimpSolver::newVar() + { + SimpSolver *solver = (SimpSolver *)this->solver; + return solver->newVar(); + } + + bool StdSimpSolver::addClause(const int ps[],size_t length) + { + SimpSolver *solver = (SimpSolver *)this->solver; + vec lits; + for (size_t i = 0; i < length; i++) + { + lits.push(makeLit(solver,ps[i])); + } + return solver->addClause(lits); + } + bool StdSimpSolver::addEmptyClause() + { + SimpSolver *solver = (SimpSolver *)this->solver; + } + bool StdSimpSolver::addClause(int p) + { + SimpSolver *solver = (SimpSolver *)this->solver; + return solver->addClause(makeLit(solver,p)); + } + bool StdSimpSolver::addClause(int p, int q) + { + SimpSolver *solver = (SimpSolver *)this->solver; + return solver->addClause(makeLit(solver,p), makeLit(solver,q)); + } + bool StdSimpSolver::addClause(int p, int q, int r) + { + SimpSolver *solver = (SimpSolver *)this->solver; + return solver->addClause(makeLit(solver,p), makeLit(solver,q), makeLit(solver,r)); + } + bool StdSimpSolver::solve(const std::vector &assumps, bool do_simp, bool turn_off_simp) + { + SimpSolver *solver = (SimpSolver *)this->solver; + vec lits; + for (auto &&i : assumps) + { + lits.push(makeLit(solver,i)); + } + return solver->solve(lits, do_simp, turn_off_simp); + } + int StdSimpSolver::solveLimited(const std::vector &assumps, bool do_simp, bool turn_off_simp) + { + SimpSolver *solver = (SimpSolver *)this->solver; + vec lits; + for (auto &&i : assumps) + { + lits.push(makeLit(solver,i)); + } + return toInt(solver->solveLimited(lits, do_simp, turn_off_simp)); + } + bool StdSimpSolver::solve(bool do_simp, bool turn_off_simp) + { + SimpSolver *solver = (SimpSolver *)this->solver; + return solver->solve(do_simp, turn_off_simp); + } + bool StdSimpSolver::solve(int p, bool do_simp, bool turn_off_simp) + { + SimpSolver *solver = (SimpSolver *)this->solver; + return solver->solve(makeLit(solver,p), do_simp, turn_off_simp); + } + bool StdSimpSolver::solve(int p, int q, bool do_simp, bool turn_off_simp) + { + SimpSolver *solver = (SimpSolver *)this->solver; + return solver->solve(makeLit(solver,p), makeLit(solver,q), do_simp, turn_off_simp); + } + bool StdSimpSolver::solve(int p, int q, int r, bool do_simp, bool turn_off_simp) + { + SimpSolver *solver = (SimpSolver *)this->solver; + return solver->solve(makeLit(solver,p), makeLit(solver,q), makeLit(solver,r), do_simp, turn_off_simp); + } + bool StdSimpSolver::eliminate(bool turn_off_elim) + { + SimpSolver *solver = (SimpSolver *)this->solver; + return solver->eliminate(turn_off_elim); + } + int StdSimpSolver::nAssigns() const + { + SimpSolver *solver = (SimpSolver *)this->solver; + return solver->nAssigns(); + } + int StdSimpSolver::nClauses() const + { + SimpSolver *solver = (SimpSolver *)this->solver; + return solver->nClauses(); + } + int StdSimpSolver::nLearnts() const + { + SimpSolver *solver = (SimpSolver *)this->solver; + return solver->nLearnts(); + } + int StdSimpSolver::nVars() const + { + SimpSolver *solver = (SimpSolver *)this->solver; + return solver->nVars(); + } + int StdSimpSolver::nFreeVars() const + { + SimpSolver *solver = (SimpSolver *)this->solver; + return solver->nFreeVars(); + } + bool StdSimpSolver::value(int val) const + { + SimpSolver *solver = (SimpSolver *)this->solver; + lbool b =solver->model[val]; + return(b==l_True); + } +} \ No newline at end of file diff --git a/simp/StdSimpSolver.hpp b/simp/StdSimpSolver.hpp new file mode 100644 index 0000000..4597554 --- /dev/null +++ b/simp/StdSimpSolver.hpp @@ -0,0 +1,69 @@ +/************************************************************************************[SimpSolver.h] +Copyright (c) 2006, Niklas Een, Niklas Sorensson +Copyright (c) 2007-2010, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#ifndef Glucose_StdSimpSolver_h +#define Glucose_StdSimpSolver_h + +#include +#include +#include +namespace Glucose +{ + + //================================================================================================= + + class StdSimpSolver + { + public: + // Constructor/Destructor: + // + StdSimpSolver(); + ~StdSimpSolver(); + + // Problem specification: + // + int newVar(); + bool addClause(const int ps[],size_t length); + bool addEmptyClause(); // Add the empty clause to the solver. + bool addClause(int p); // Add a unit clause to the solver. + bool addClause(int p, int q); // Add a binary clause to the solver. + bool addClause(int p, int q, int r); // Add a ternary clause to the solver. + bool value (int x) const; + + // Solving: + // + bool solve(const std::vector &assumps, bool do_simp = true, bool turn_off_simp = false); + int solveLimited(const std::vector &assumps, bool do_simp = true, bool turn_off_simp = false); + bool solve(bool do_simp = true, bool turn_off_simp = false); + bool solve(int p, bool do_simp = true, bool turn_off_simp = false); + bool solve(int p, int q, bool do_simp = true, bool turn_off_simp = false); + bool solve(int p, int q, int r, bool do_simp = true, bool turn_off_simp = false); + bool eliminate(bool turn_off_elim = false); // Perform variable elimination based simplification. + int nAssigns() const; // The current number of assigned literals. + int nClauses() const; // The current number of original clauses. + int nLearnts() const; // The current number of learnt clauses. + int nVars() const; // The current number of variables. + int nFreeVars() const; + private: + void *solver; + }; + +}; +#endif