Add niklasso/minisat Formula from Conan Center

niklasso/minisat/releases/2.2.0/consumer.cpp

@@ -0,0 +1,18 @@
+// Example adapted from the Conan Center test package.
+#include <minisat/simp/SimpSolver.h>
+
+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;
+}

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
+}

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; }

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);

niklasso/minisat/versions.json

@@ -0,0 +1,4 @@
+{
+	"path": "niklasso/minisat",
+	"deps": {}
+}