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..83cd988 --- /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() { + SimpSolver 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..eceee09 --- /dev/null +++ b/niklasso/minisat/releases/2.2.0/minisat_llar.gox @@ -0,0 +1,123 @@ +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" + +onRequire (proj, deps) => { + deps.require "madler/zlib", "v1.3.1" +} + +onBuild ctx => { + installDir := ctx.outputDir + formulaDir := "releases/2.2.0" + + 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 + } + + // 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, "simp", "SimpSolver.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") { + cflags <- "-fPIC" + } + 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, + "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" + } + 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": {} +}