Merge pull request #3 from sbeyer/update-to-2024

Update to 2024

.github/workflows/tests.yml

@@ -0,0 +1,12 @@
+name: Compilation and Tests
+
+on: [push, pull_request]
+
+jobs:
+  linux-build:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Clone and checkout commit
+        uses: actions/checkout@v4
+      - name: Quickstart
+        run: util/quickstart.sh

.gitignore

@@ -1,9 +1,3 @@
-/Makefile
-/CMakeCache.txt
-/CMakeDoxyfile.in
-/CMakeDoxygenDefaults.cmake
-CMakeFiles
-cmake_install.cmake
-CTestTestfile.cmake
-/Testing
+/build
+/compile_commands.json
 /doc

.gitmodules

@@ -1,3 +1,3 @@
 [submodule "test/bandit"]
 	path = test/bandit
-	url = https://github.com/joakimkarlsson/bandit.git
+	url = https://github.com/banditcpp/bandit.git

CMakeLists.txt

@@ -1,4 +1,4 @@
-cmake_minimum_required(VERSION 3.0)
+cmake_minimum_required(VERSION 3.25)
 
 project(CommonSAT)
 
@@ -56,4 +56,6 @@ endif(USE_PICOSAT)
 add_subdirectory(test)
 
 find_package(Doxygen)
-add_custom_target(doc ${DOXYGEN_EXECUTABLE} Doxyfile)
+add_custom_target(doc
+	COMMAND ${DOXYGEN_EXECUTABLE} Doxyfile
+	WORKING_DIRECTORY ${CMAKE_SOURCE_DIR})

LICENSE

@@ -1,6 +1,6 @@
 The MIT License (MIT)
 
-Copyright (c) 2015, Stephan Beyer
+Copyright (c) 2015–2024, Stephan Beyer
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal

README.md

@@ -1,9 +1,9 @@
 # CommonSAT
 
-CommonSAT is intended as a common C++11 SAT solver interface for different SAT solvers.
+CommonSAT is intended as a common SAT solver interface for different SAT solvers.
+
+The minimum required C++ version is C++11.
 
-[![Build Status](https://travis-ci.org/sbeyer/commonsat.svg)](https://travis-ci.org/sbeyer/commonsat)
-[![Codacy Badge](https://api.codacy.com/project/badge/Grade/d2e9f78b43924f418914201125716925)](https://www.codacy.com/app/sbeyer/commonsat?utm_source=github.com&utm_medium=referral&utm_content=sbeyer/commonsat&utm_campaign=Badge_Grade)
 [![CodeDocs](https://codedocs.xyz/sbeyer/commonsat.svg)](https://codedocs.xyz/sbeyer/commonsat/)
 
 ## So... what is CommonSAT?
@@ -35,15 +35,42 @@ for SAT solver libraries like
 Note that the things mentioned above are TODO list items that are probably not
 implemented.
 
+## Code example
+
+```c++
+/* commonsat::SolverInterface solver */
+solver.add_clause({1, 2});
+solver.add_clause({1, -2, 3});
+solver.add_clause({-1, 2});
+solver.add_clause({-1, -2});
+bool isSatisfiable = solver.solve();
+if (isSatisfiable) {
+  for (int i : std::views::iota(1, 4)) {
+    std::println("Variable {} is assigned {}", i, solver.is_true(2));
+  }
+} else {
+  std::println("Not satisfiable");
+}
+```
+
 ## How do I get something to run ...quickly?
 
 The quickest way to get started is along the following lines:
 ```sh
-sudo apt install git cmake doxygen graphviz
+# install dependencies, e.g.,
+sudo apt install git cmake doxygen graphviz zlib1g-dev libgmp-dev
+# or
+sudo dnf install git cmake doxygen graphviz zlib-devel gmp-devel
+
+# clone the repo
 git clone https://github.com/sbeyer/commonsat.git
+
+# run the quickstart script
 cd commonsat
 util/quickstart.sh
-doxygen .
+
+# make the documentation
+util/check-doxygen-errors.sh
 ```
 
 The quickstart script will do a lot of magic, like updating submodules (for

commonsat/commonsat.h

@@ -1,6 +1,6 @@
 /*! \file
  * \brief Definition of the main interface for CommonSAT.
- * \copyright Copyright 2015–2016 Stephan Beyer.
+ * \copyright Copyright 2015–2024 Stephan Beyer.
  * \par
  * This file is part of CommonSAT.
  * \par
@@ -26,7 +26,6 @@
 #ifndef COMMONSAT_H
 #define COMMONSAT_H
 
-#include <stdexcept>
 #include <vector>
 #include <cstdint>
 
@@ -45,9 +44,8 @@ enum class Assignment : std::uint8_t {
 //! The general solver interface class
 class SolverInterface {
 public:
-	SolverInterface()
-	{
-	}
+	SolverInterface() = default;
+	virtual ~SolverInterface() = default;
 
 	//! Add a clause to the CNF
 	//!

commonsat/cryptominisat.h

@@ -1,6 +1,6 @@
 /*! \file
  * \brief Definition of the CryptoMiniSat interface for CommonSAT.
- * \copyright Copyright 2015 Stephan Beyer.
+ * \copyright Copyright 2015–2024 Stephan Beyer.
  * \par
  * This file is part of CommonSAT.
  * \par

commonsat/lingeling.h

@@ -1,6 +1,6 @@
 /*! \file
  * \brief Definition of the Lingeling interface for CommonSAT.
- * \copyright Copyright 2015–2016 Stephan Beyer.
+ * \copyright Copyright 2015–2024 Stephan Beyer.
  * \par
  * This file is part of CommonSAT.
  * \par

commonsat/minisat.h

@@ -1,6 +1,6 @@
 /*! \file
  * \brief Definition of the MiniSat interface for CommonSAT.
- * \copyright Copyright 2015 Stephan Beyer.
+ * \copyright Copyright 2015–2024 Stephan Beyer.
  * \par
  * This file is part of CommonSAT.
  * \par

commonsat/picosat.h

@@ -1,6 +1,6 @@
 /*! \file
  * \brief Definition of the PicoSAT interface for CommonSAT.
- * \copyright Copyright 2016 Stephan Beyer.
+ * \copyright Copyright 2016–2024 Stephan Beyer.
  * \par
  * This file is part of CommonSAT.
  * \par

solvers/Makefile

@@ -1,46 +1,63 @@
 all: compile_all
 
-LINGELING_VERSION=bal-2293bef-151109
 PICOSAT_VERSION=965
 
 minisat:
-	git clone https://github.com/niklasso/minisat
+	# https://github.com/niklasso/minisat is unmaintained and does not compile, hence we use a fork
+	git clone -b fix-c++ https://github.com/spakin/minisat
 
 cryptominisat:
 	git clone https://github.com/msoos/cryptominisat.git
 
 lingeling:
-	curl -o ll.tar.gz http://fmv.jku.at/lingeling/lingeling-$(LINGELING_VERSION).tar.gz
-	tar xf ll.tar.gz
-	mv lingeling-$(LINGELING_VERSION) lingeling
-	$(RM) ll.tar.gz
+	git clone https://github.com/arminbiere/lingeling
 
 picosat:
-	curl -o ps.tar.gz http://fmv.jku.at/picosat/picosat-$(PICOSAT_VERSION).tar.gz
+	curl -o ps.tar.gz https://fmv.jku.at/picosat/picosat-$(PICOSAT_VERSION).tar.gz
 	tar xf ps.tar.gz
 	mv picosat-$(PICOSAT_VERSION) picosat
 	$(RM) ps.tar.gz
 
-.PHONY: compile_all
+.PHONY: compile_all clean
 
 compile_minisat: minisat
 	cd minisat && mkdir -p build && cd build && cmake ..
 	$(MAKE) -C minisat/build
-	echo "Removing this file will make Make compile Minisat again." > "$@"
+	echo "Removing this file will make Make compile Minisat again." >"$@"
 
-compile_cryptominisat: cryptominisat
-	cd cryptominisat && mkdir -p build && cd build && cmake -DENABLE_PYTHON_INTERFACE=OFF ..
+cadical:
+	git clone -b mate-only-libraries-1.8.0 https://github.com/meelgroup/cadical
+
+compile_cadical: cadical
+	cd cadical && ./configure && make
+	echo "Removing this file will make Make compile cadical again." >"$@"
+
+cadiback:
+	git clone -b mate https://github.com/meelgroup/cadiback
+
+compile_cadiback: cadiback
+	cd cadiback && ./configure && make
+	echo "Removing this file will make Make compile cadiback again." >"$@"
+
+compile_cryptominisat: cryptominisat compile_cadical compile_cadiback
+	cd cryptominisat && mkdir -p build && cd build && cmake ..
 	$(MAKE) -C cryptominisat/build
-	echo "Removing this file will make Make compile CryptoMiniSat again." > "$@"
+	echo "Removing this file will make Make compile CryptoMiniSat again." >"$@"
 
 compile_lingeling: lingeling
 	cd lingeling && ./configure.sh
 	$(MAKE) -C lingeling
-	echo "Removing this file will make Make compile lingeling again." > "$@"
+	echo "Removing this file will make Make compile lingeling again." >"$@"
 
 compile_picosat: picosat
 	cd picosat && ./configure.sh
 	$(MAKE) -C picosat
-	echo "Removing this file will make Make compile PicoSAT again." > "$@"
+	echo "Removing this file will make Make compile PicoSAT again." >"$@"
 
 compile_all: compile_minisat compile_cryptominisat compile_lingeling compile_picosat
+
+clean:
+	$(RM) -f compile_minisat compile_cryptominisat compile_lingeling compile_picosat
+	$(RM) -rf minisat cryptominisat lingeling picosat
+	$(RM) -f compile_cadical compile_cadiback
+	$(RM) -rf cadical cadiback

test/CMakeLists.txt

@@ -2,26 +2,26 @@ include_directories("${PROJECT_SOURCE_DIR}/test/bandit")
 
 if(USE_MINISAT)
 	include_directories("${MINISAT_INCLUDE_DIR}")
-	add_executable(test_minisat minisat.cc)
+	add_executable(test_minisat minisat.cc tests.cc)
 	target_link_libraries(test_minisat ${MINISAT_LIBRARY})
 endif(USE_MINISAT)
 
 if(USE_CRYPTOMINISAT)
 	find_package(Threads)
 	include_directories("${CRYPTOMINISAT_INCLUDE_DIR}")
-	add_executable(test_cryptominisat cryptominisat.cc)
+	add_executable(test_cryptominisat cryptominisat.cc tests.cc)
 	target_link_libraries(test_cryptominisat
 	    ${CRYPTOMINISAT_LIBRARY} ${CMAKE_THREAD_LIBS_INIT})
 endif(USE_CRYPTOMINISAT)
 
 if(USE_LINGELING)
 	include_directories("${LINGELING_INCLUDE_DIR}")
-	add_executable(test_lingeling lingeling.cc)
+	add_executable(test_lingeling lingeling.cc tests.cc)
 	target_link_libraries(test_lingeling ${LINGELING_LIBRARY})
 endif(USE_LINGELING)
 
 if(USE_PICOSAT)
 	include_directories("${PICOSAT_INCLUDE_DIR}")
-	add_executable(test_picosat picosat.cc)
+	add_executable(test_picosat picosat.cc tests.cc)
 	target_link_libraries(test_picosat ${PICOSAT_LIBRARY})
 endif(USE_PICOSAT)

test/tests.cc

@@ -0,0 +1,49 @@
+#include "tests.h"
+
+#include <bandit/assertion_frameworks/snowhouse/snowhouse.h>
+#include <commonsat/commonsat.h>
+
+using namespace snowhouse;
+
+void test_satisfiable(commonsat::SolverInterface &solver)
+{
+	solver.add_clause({1, 2});
+	solver.add_clause({1, -2, 3});
+	solver.add_clause({-1, 2});
+	solver.add_clause({-1, -2});
+	bool isSatisfiable = solver.solve();
+	AssertThat(isSatisfiable, IsTrue());
+}
+
+void test_unsatisfiable(commonsat::SolverInterface &solver)
+{
+	solver.add_clause({1, 2});
+	solver.add_clause({1, -2, 3});
+	solver.add_clause({-1, 2});
+	solver.add_clause({-1, -2});
+	solver.add_clause({-3});
+	bool isSatisfiable = solver.solve();
+	AssertThat(isSatisfiable, IsFalse());
+}
+
+void test_assignment(commonsat::SolverInterface &solver)
+{
+	for (int i = 0; i < 7; ++i) {
+		commonsat::clause_t clause = {1, 2, 3};
+		for (int j = 0; j < 3; ++j) {
+			if ((i >> j) & 1) {
+				clause[j] = -clause[j];
+			}
+		}
+		solver.add_clause(clause);
+	}
+
+	bool isSatisfiable = solver.solve();
+	AssertThat(isSatisfiable, IsTrue());
+	AssertThat(solver.is_assigned(1), IsTrue());
+	AssertThat(solver.is_assigned(2), IsTrue());
+	AssertThat(solver.is_assigned(3), IsTrue());
+	AssertThat(solver.is_true(1), IsTrue());
+	AssertThat(solver.is_true(2), IsTrue());
+	AssertThat(solver.is_true(3), IsTrue());
+}