From 6edc06fb23d341b5ac485beed259c1ac13284116 Mon Sep 17 00:00:00 2001 From: Rick Guo Date: Wed, 9 Sep 2026 17:38:01 +0800 Subject: [PATCH 1/4] Add niklasso/minisat formula from Conan Center --- .../minisat/releases/2.2.0/CMakeLists.txt | 27 ++++++ niklasso/minisat/releases/2.2.0/consumer.cpp | 18 ++++ .../minisat/releases/2.2.0/minisat_llar.gox | 93 +++++++++++++++++++ ...op-default-arg-in-friend-declaration.patch | 10 ++ .../2.2.0/patches/0002-suffix-literal.patch | 13 +++ niklasso/minisat/versions.json | 4 + 6 files changed, 165 insertions(+) create mode 100644 niklasso/minisat/releases/2.2.0/CMakeLists.txt create mode 100644 niklasso/minisat/releases/2.2.0/consumer.cpp create mode 100644 niklasso/minisat/releases/2.2.0/minisat_llar.gox create mode 100644 niklasso/minisat/releases/2.2.0/patches/0001-drop-default-arg-in-friend-declaration.patch create mode 100644 niklasso/minisat/releases/2.2.0/patches/0002-suffix-literal.patch create mode 100644 niklasso/minisat/versions.json diff --git a/niklasso/minisat/releases/2.2.0/CMakeLists.txt b/niklasso/minisat/releases/2.2.0/CMakeLists.txt new file mode 100644 index 0000000..b2a136d --- /dev/null +++ b/niklasso/minisat/releases/2.2.0/CMakeLists.txt @@ -0,0 +1,27 @@ +cmake_minimum_required(VERSION 3.15) +project(minisat LANGUAGES CXX) + +find_package(ZLIB REQUIRED) + +# no Main.cc as these are the command line tools +add_library(minisat + ${MINISAT_SRC_DIR}/core/Solver.cc + ${MINISAT_SRC_DIR}/simp/SimpSolver.cc + ${MINISAT_SRC_DIR}/utils/Options.cc + ${MINISAT_SRC_DIR}/utils/System.cc +) +target_include_directories(minisat PUBLIC ${MINISAT_SRC_DIR}) +target_link_libraries(minisat PUBLIC ZLIB::ZLIB) +set_target_properties(minisat PROPERTIES WINDOWS_EXPORT_ALL_SYMBOLS ON) + +include(GNUInstallDirs) +install( + TARGETS minisat + RUNTIME DESTINATION ${CMAKE_INSTALL_BINDIR} + ARCHIVE DESTINATION ${CMAKE_INSTALL_LIBDIR} + LIBRARY DESTINATION ${CMAKE_INSTALL_LIBDIR} +) +install(DIRECTORY ${MINISAT_SRC_DIR}/mtl ${MINISAT_SRC_DIR}/utils ${MINISAT_SRC_DIR}/core ${MINISAT_SRC_DIR}/simp + DESTINATION ${CMAKE_INSTALL_INCLUDEDIR}/minisat + FILES_MATCHING PATTERN "*.h" +) diff --git a/niklasso/minisat/releases/2.2.0/consumer.cpp b/niklasso/minisat/releases/2.2.0/consumer.cpp new file mode 100644 index 0000000..46eda82 --- /dev/null +++ b/niklasso/minisat/releases/2.2.0/consumer.cpp @@ -0,0 +1,18 @@ +// Example adapted from the Conan Center test package. +#include + +using namespace Minisat; + +int main() { + Solver solver; + Var a = solver.newVar(); + Var b = solver.newVar(); + Var c = solver.newVar(); + + solver.addClause(mkLit(a), mkLit(b), mkLit(c)); + solver.addClause(~mkLit(a), mkLit(b), mkLit(c)); + solver.addClause(mkLit(a), ~mkLit(b), mkLit(c)); + solver.addClause(mkLit(a), mkLit(b), ~mkLit(c)); + + return solver.solve() ? 0 : 1; +} diff --git a/niklasso/minisat/releases/2.2.0/minisat_llar.gox b/niklasso/minisat/releases/2.2.0/minisat_llar.gox new file mode 100644 index 0000000..4d6aa42 --- /dev/null +++ b/niklasso/minisat/releases/2.2.0/minisat_llar.gox @@ -0,0 +1,93 @@ +import ( + "os" + "path/filepath" + "slices" +) + +id "niklasso/minisat" + +fromVer "releases/2.2.0" + +onRequire (proj, deps) => { + deps.require "madler/zlib", "v1.3.1" +} + +onBuild ctx => { + installDir := ctx.outputDir + formulaDir := "releases/2.2.0" + + os.writeFile( + filepath.join(ctx.SourceDir, "CMakeLists.txt"), + ctx.Proj.readFile(filepath.join(formulaDir, "CMakeLists.txt"))!, + 0o644, + )! + for patchName in ["0001-drop-default-arg-in-friend-declaration.patch", "0002-suffix-literal.patch"] { + patchPath := filepath.join(ctx.SourceDir, patchName) + os.writeFile(patchPath, ctx.Proj.readFile(filepath.join(formulaDir, "patches", patchName))!, 0o644)! + git! "-C", ctx.SourceDir, "apply", "--unidiff-zero", patchPath + } + + c := cmake.new(ctx.SourceDir, filepath.join(ctx.SourceDir, "_build"), installDir) + c.define "MINISAT_SRC_DIR", ctx.SourceDir + c.define "CMAKE_INSTALL_LIBDIR", "lib" + // Keep Conan's static, PIC defaults. LLAR matrix options also reach + // madler/zlib, whose current Formula cannot install under an option matrix. + c.defineBool "BUILD_SHARED_LIBS", false + if !slices.contains(target.require["os"], "windows") { + c.defineBool "CMAKE_POSITION_INDEPENDENT_CODE", true + } + for dep in ctx.Proj.Deps { + c.use ctx.outputDir(dep) + } + c.configure + c.build + c.install + + licenseDir := filepath.join(installDir, "licenses") + os.mkdirAll(licenseDir, 0o755)! + os.writeFile(filepath.join(licenseDir, "LICENSE"), os.readFile(filepath.join(ctx.SourceDir, "LICENSE"))!, 0o644)! + + libs := ["-L$${libdir}", "-lminisat"] + if slices.contains(target.require["os"], "linux") || slices.contains(target.require["os"], "freebsd") { + libs <- "-lm" + } + pcDir := filepath.join(installDir, "lib", "pkgconfig") + os.mkdirAll(pcDir, 0o755)! + pc := pkgconfig.new( + name = "minisat", + description = "minimalistic SAT solver", + version = "releases/2.2.0", + requires = ["zlib"], + libs = libs, + cflags = ["-I$${includedir}", "-I$${includedir}/minisat"], + )! + out := os.create(filepath.join(pcDir, "minisat.pc"))! + pc.writeTo(out)! + out.close()! + + for dep in ctx.Proj.Deps { + pkgconfig.use ctx.outputDir(dep) + } + pkgconfig.use installDir + ctx.setMetadata pkgconfig.lookup("minisat")! +} + +onTest ctx => { + installDir := ctx.outputDir + formulaDir := "releases/2.2.0" + testDir := filepath.join(ctx.SourceDir, "_llar_consumer") + os.mkdirAll(testDir, 0o755)! + + consumer := filepath.join(testDir, "consumer.cpp") + os.writeFile(consumer, ctx.Proj.readFile(filepath.join(formulaDir, "consumer.cpp"))!, 0o644)! + for dep in ctx.Proj.Deps { + pkgconfig.use ctx.outputDir(dep) + } + pkgconfig.use installDir + flagsFile := filepath.join(testDir, "minisat.flags") + os.writeFile(flagsFile, []byte(pkgconfig.lookup("minisat")!), 0o644)! + + binary := filepath.join(testDir, "consumer") + exec! "c++", "-std=c++11", consumer, "-o", binary, "@"+flagsFile + exec! binary +} diff --git a/niklasso/minisat/releases/2.2.0/patches/0001-drop-default-arg-in-friend-declaration.patch b/niklasso/minisat/releases/2.2.0/patches/0001-drop-default-arg-in-friend-declaration.patch new file mode 100644 index 0000000..c0f1f9c --- /dev/null +++ b/niklasso/minisat/releases/2.2.0/patches/0001-drop-default-arg-in-friend-declaration.patch @@ -0,0 +1,10 @@ +diff --git a/core/SolverTypes.h b/core/SolverTypes.h +index 1ebcc73..7b1d16a 100644 +--- a/core/SolverTypes.h ++++ b/core/SolverTypes.h +@@ -50 +50 @@ +- friend Lit mkLit(Var var, bool sign = false); ++ //friend Lit mkLit(Var var, bool sign = false); +@@ -58 +58 @@ +-inline Lit mkLit (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; } ++inline Lit mkLit (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; } diff --git a/niklasso/minisat/releases/2.2.0/patches/0002-suffix-literal.patch b/niklasso/minisat/releases/2.2.0/patches/0002-suffix-literal.patch new file mode 100644 index 0000000..c713554 --- /dev/null +++ b/niklasso/minisat/releases/2.2.0/patches/0002-suffix-literal.patch @@ -0,0 +1,13 @@ +diff --git a/minisat/utils/Options.h b/minisat/utils/Options.h +index 2dba10f..ea7c185 100644 +--- a/utils/Options.h ++++ b/utils/Options.h +@@ -285 +285 @@ +- fprintf(stderr, "%4"PRIi64, range.begin); ++ fprintf(stderr, "%4" PRIi64, range.begin); +@@ -291 +291 @@ +- fprintf(stderr, "%4"PRIi64, range.end); ++ fprintf(stderr, "%4" PRIi64, range.end); +@@ -293 +293 @@ +- fprintf(stderr, "] (default: %"PRIi64")\n", value); ++ fprintf(stderr, "] (default: %" PRIi64")\n", value); diff --git a/niklasso/minisat/versions.json b/niklasso/minisat/versions.json new file mode 100644 index 0000000..3fbf3c8 --- /dev/null +++ b/niklasso/minisat/versions.json @@ -0,0 +1,4 @@ +{ + "path": "niklasso/minisat", + "deps": {} +} From ff8024cd3c54d3e775533dca7638af65acdd9a56 Mon Sep 17 00:00:00 2001 From: Rick Guo Date: Thu, 10 Sep 2026 13:56:36 +0800 Subject: [PATCH 2/4] fix(minisat): use upstream Makefile archive --- .../minisat/releases/2.2.0/CMakeLists.txt | 27 --------- .../minisat/releases/2.2.0/minisat_llar.gox | 60 ++++++++++++++----- 2 files changed, 44 insertions(+), 43 deletions(-) delete mode 100644 niklasso/minisat/releases/2.2.0/CMakeLists.txt diff --git a/niklasso/minisat/releases/2.2.0/CMakeLists.txt b/niklasso/minisat/releases/2.2.0/CMakeLists.txt deleted file mode 100644 index b2a136d..0000000 --- a/niklasso/minisat/releases/2.2.0/CMakeLists.txt +++ /dev/null @@ -1,27 +0,0 @@ -cmake_minimum_required(VERSION 3.15) -project(minisat LANGUAGES CXX) - -find_package(ZLIB REQUIRED) - -# no Main.cc as these are the command line tools -add_library(minisat - ${MINISAT_SRC_DIR}/core/Solver.cc - ${MINISAT_SRC_DIR}/simp/SimpSolver.cc - ${MINISAT_SRC_DIR}/utils/Options.cc - ${MINISAT_SRC_DIR}/utils/System.cc -) -target_include_directories(minisat PUBLIC ${MINISAT_SRC_DIR}) -target_link_libraries(minisat PUBLIC ZLIB::ZLIB) -set_target_properties(minisat PROPERTIES WINDOWS_EXPORT_ALL_SYMBOLS ON) - -include(GNUInstallDirs) -install( - TARGETS minisat - RUNTIME DESTINATION ${CMAKE_INSTALL_BINDIR} - ARCHIVE DESTINATION ${CMAKE_INSTALL_LIBDIR} - LIBRARY DESTINATION ${CMAKE_INSTALL_LIBDIR} -) -install(DIRECTORY ${MINISAT_SRC_DIR}/mtl ${MINISAT_SRC_DIR}/utils ${MINISAT_SRC_DIR}/core ${MINISAT_SRC_DIR}/simp - DESTINATION ${CMAKE_INSTALL_INCLUDEDIR}/minisat - FILES_MATCHING PATTERN "*.h" -) diff --git a/niklasso/minisat/releases/2.2.0/minisat_llar.gox b/niklasso/minisat/releases/2.2.0/minisat_llar.gox index 4d6aa42..43a1289 100644 --- a/niklasso/minisat/releases/2.2.0/minisat_llar.gox +++ b/niklasso/minisat/releases/2.2.0/minisat_llar.gox @@ -2,8 +2,22 @@ import ( "os" "path/filepath" "slices" + "strings" ) +func copyHeaders(src, dst string) { + os.mkdirAll(dst, 0o755)! + for entry in os.readDir(src)! { + from := filepath.join(src, entry.name) + to := filepath.join(dst, entry.name) + if entry.isDir { + copyHeaders from, to + } else if entry.name.hasSuffix(".h") || entry.name.hasSuffix(".hpp") { + os.writeFile(to, os.readFile(from)!, 0o644)! + } + } +} + id "niklasso/minisat" fromVer "releases/2.2.0" @@ -16,37 +30,51 @@ onBuild ctx => { installDir := ctx.outputDir formulaDir := "releases/2.2.0" - os.writeFile( - filepath.join(ctx.SourceDir, "CMakeLists.txt"), - ctx.Proj.readFile(filepath.join(formulaDir, "CMakeLists.txt"))!, - 0o644, - )! for patchName in ["0001-drop-default-arg-in-friend-declaration.patch", "0002-suffix-literal.patch"] { patchPath := filepath.join(ctx.SourceDir, patchName) os.writeFile(patchPath, ctx.Proj.readFile(filepath.join(formulaDir, "patches", patchName))!, 0o644)! git! "-C", ctx.SourceDir, "apply", "--unidiff-zero", patchPath } - c := cmake.new(ctx.SourceDir, filepath.join(ctx.SourceDir, "_build"), installDir) - c.define "MINISAT_SRC_DIR", ctx.SourceDir - c.define "CMAKE_INSTALL_LIBDIR", "lib" - // Keep Conan's static, PIC defaults. LLAR matrix options also reach - // madler/zlib, whose current Formula cannot install under an option matrix. - c.defineBool "BUILD_SHARED_LIBS", false + // The release's core Makefile builds the static archive without Main.cc. + // Keep the object list explicit because GNU Make's filter-out pattern does + // not match absolute Main.o paths passed by the LLAR source workspace. + objects := []string{ + filepath.join(ctx.SourceDir, "core", "Solver.o"), + filepath.join(ctx.SourceDir, "utils", "Options.o"), + filepath.join(ctx.SourceDir, "utils", "System.o"), + } + cflags := []string{"-Wall", "-Wno-parentheses", "-std=c++11", "-I"+ctx.SourceDir, "-D__STDC_LIMIT_MACROS", "-D__STDC_FORMAT_MACROS"} if !slices.contains(target.require["os"], "windows") { - c.defineBool "CMAKE_POSITION_INDEPENDENT_CODE", true + cflags <- "-fPIC" } + a := autotools.new(filepath.join(ctx.SourceDir, "core"), filepath.join(ctx.SourceDir, "core"), installDir) for dep in ctx.Proj.Deps { - c.use ctx.outputDir(dep) + a.use ctx.outputDir(dep) } - c.configure - c.build - c.install + a.build "libs", + "MROOT="+ctx.SourceDir, + "LIB=minisat", + "CSRCS=Solver.cc", + "COBJS="+strings.join(objects, " "), + "CFLAGS="+strings.join(cflags, " ") licenseDir := filepath.join(installDir, "licenses") os.mkdirAll(licenseDir, 0o755)! os.writeFile(filepath.join(licenseDir, "LICENSE"), os.readFile(filepath.join(ctx.SourceDir, "LICENSE"))!, 0o644)! + includeDir := filepath.join(installDir, "include", "minisat") + for dir in ["mtl", "utils", "core", "simp"] { + copyHeaders filepath.join(ctx.SourceDir, dir), filepath.join(includeDir, dir) + } + libDir := filepath.join(installDir, "lib") + os.mkdirAll(libDir, 0o755)! + os.writeFile( + filepath.join(libDir, "libminisat.a"), + os.readFile(filepath.join(ctx.SourceDir, "core", "libminisat_standard.a"))!, + 0o644, + )! + libs := ["-L$${libdir}", "-lminisat"] if slices.contains(target.require["os"], "linux") || slices.contains(target.require["os"], "freebsd") { libs <- "-lm" From 797ad3a7c7fb6b3fb65dc6e1d6da13f80e15a4e7 Mon Sep 17 00:00:00 2001 From: Rick Guo Date: Thu, 10 Sep 2026 14:08:37 +0800 Subject: [PATCH 3/4] fix(minisat): include simplifier in static archive --- niklasso/minisat/releases/2.2.0/consumer.cpp | 4 ++-- niklasso/minisat/releases/2.2.0/minisat_llar.gox | 1 + 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/niklasso/minisat/releases/2.2.0/consumer.cpp b/niklasso/minisat/releases/2.2.0/consumer.cpp index 46eda82..83cd988 100644 --- a/niklasso/minisat/releases/2.2.0/consumer.cpp +++ b/niklasso/minisat/releases/2.2.0/consumer.cpp @@ -1,10 +1,10 @@ // Example adapted from the Conan Center test package. -#include +#include using namespace Minisat; int main() { - Solver solver; + SimpSolver solver; Var a = solver.newVar(); Var b = solver.newVar(); Var c = solver.newVar(); diff --git a/niklasso/minisat/releases/2.2.0/minisat_llar.gox b/niklasso/minisat/releases/2.2.0/minisat_llar.gox index 43a1289..56e2642 100644 --- a/niklasso/minisat/releases/2.2.0/minisat_llar.gox +++ b/niklasso/minisat/releases/2.2.0/minisat_llar.gox @@ -41,6 +41,7 @@ onBuild ctx => { // not match absolute Main.o paths passed by the LLAR source workspace. objects := []string{ filepath.join(ctx.SourceDir, "core", "Solver.o"), + filepath.join(ctx.SourceDir, "simp", "SimpSolver.o"), filepath.join(ctx.SourceDir, "utils", "Options.o"), filepath.join(ctx.SourceDir, "utils", "System.o"), } From c65283fc9ecd25d30aa95a4c7faf8bc665d89837 Mon Sep 17 00:00:00 2001 From: Rick Guo Date: Thu, 10 Sep 2026 14:12:33 +0800 Subject: [PATCH 4/4] fix(minisat): pass dependency headers to Make --- niklasso/minisat/releases/2.2.0/minisat_llar.gox | 1 + 1 file changed, 1 insertion(+) diff --git a/niklasso/minisat/releases/2.2.0/minisat_llar.gox b/niklasso/minisat/releases/2.2.0/minisat_llar.gox index 56e2642..eceee09 100644 --- a/niklasso/minisat/releases/2.2.0/minisat_llar.gox +++ b/niklasso/minisat/releases/2.2.0/minisat_llar.gox @@ -52,6 +52,7 @@ onBuild ctx => { a := autotools.new(filepath.join(ctx.SourceDir, "core"), filepath.join(ctx.SourceDir, "core"), installDir) for dep in ctx.Proj.Deps { a.use ctx.outputDir(dep) + cflags <- "-I"+filepath.join(ctx.outputDir(dep), "include") } a.build "libs", "MROOT="+ctx.SourceDir,