diff --git a/CMakeLists.txt b/CMakeLists.txt
index 4c32148..fa2de36 100644
@@ -1,4 +1,4 @@
-cmake_minimum_required(VERSION 2.6)
+cmake_minimum_required(VERSION 3.10)
project(glucose)
@@ -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")
diff --git a/simp/StdSimpSolver.cc b/simp/StdSimpSolver.cc
new file mode 100644
index 0000000..1ef856a
@@ -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<Lit> 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<int> &assumps, bool do_simp, bool turn_off_simp)
+ {
+ SimpSolver *solver = (SimpSolver *)this->solver;
+ vec<Lit> 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<int> &assumps, bool do_simp, bool turn_off_simp)
+ {
+ SimpSolver *solver = (SimpSolver *)this->solver;
+ vec<Lit> 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
@@ -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 <cstdint>
+#include <cstdio>
+#include <vector>
+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<int> &assumps, bool do_simp = true, bool turn_off_simp = false);
+ int solveLimited(const std::vector<int> &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