Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
116 changes: 27 additions & 89 deletions Formula/c/cryptominisat.rb
Original file line number Diff line number Diff line change
@@ -1,25 +1,25 @@
class Cryptominisat < Formula
desc "Advanced SAT solver"
homepage "https://www.msoos.org/cryptominisat5/"
url "https://github.com/msoos/cryptominisat/archive/refs/tags/release/5.13.0.tar.gz"
sha256 "1bfcd8a314706b3ac7831f215bae50251d9b61f3bbe90cbdcbed190741f6ee54"
url "https://github.com/msoos/cryptominisat/archive/refs/tags/release/v5.14.2.tar.gz"
sha256 "8ffe7da6ed6716b83a7f4ec26b89d680d7afbb390bc3628d68898d3bc36a9d27"
# Everything that's needed to run/build/install/link the system is MIT licensed. This allows
# easy distribution and running of the system everywhere.
license "MIT"
revision 1
compatibility_version 1

livecheck do
url :stable
regex(%r{^(?:release/)?v?(\d+(?:\.\d+)+)$}i)
end

bottle do
sha256 cellar: :any, arm64_tahoe: "d56074a77028dcfdb9d9d59b2fcd57aad7e2df80c9f99df8f5c4286ef16c3b7f"
sha256 cellar: :any, arm64_sequoia: "bf9b8dbe11fa244c8f7f6b052f12630a38040f9c02d17be2e075306eb98e2b02"
sha256 cellar: :any, arm64_sonoma: "cbd9e3001b700ea908fe9873fd9b059d634f437818ea3ccc2e38a6fa21195cb8"
sha256 cellar: :any, sonoma: "50c0d3151e24e96ec77ce11263d701b9c2e911dd4a9eb1fbfb9173cc85777500"
sha256 cellar: :any_skip_relocation, arm64_linux: "1f973a7d348b3dc75f6bc4ef3c4d243617103a1e18e42be3c927ca075b8029de"
sha256 cellar: :any_skip_relocation, x86_64_linux: "a14f3873914b9f6631948386fe1a9ef164d7a5812597e508117aab2ea83f382c"
sha256 cellar: :any, arm64_tahoe: "1f616764d075894c180a60ed93683a82e79954292c3600d07be10afcdb7de1f3"
sha256 cellar: :any, arm64_sequoia: "557300de80471bc78009251d973f5789f2a3365b50d91d5acc3097cc6d5babc3"
sha256 cellar: :any, arm64_sonoma: "219191f361770cf83e0d5a365cb48822698810e73f87c0b4e1761b3f83410568"
sha256 cellar: :any, sonoma: "c9e10a84c97f5032c9e750222038553a4c86a906d9f9673d7f0c0dcdb18ffb62"
sha256 cellar: :any_skip_relocation, arm64_linux: "6d4c7cd1f36648a97af46e599c76a929b05920cee3b13e28acc6921e304c2b66"
sha256 cellar: :any_skip_relocation, x86_64_linux: "1c00665e16db04514a98fc6175032b5b5c6746709b7d61ce54ca570d2f9b1b78"
end

depends_on "cmake" => :build
Expand All @@ -32,12 +32,12 @@ class Cryptominisat < Formula

# Currently using revision in flake.lock
resource "cadical" do
url "https://github.com/meelgroup/cadical/archive/8fcb8139c453e7cb85c470cea5d783db8e229518.tar.gz"
version "8fcb8139c453e7cb85c470cea5d783db8e229518"
sha256 "9880d09a7ff3d9dc4b633fa8230ff168b089c78a4c1811efd467925eb9972f9b"
url "https://github.com/meelgroup/cadical/archive/25c12aac83fd2f8627ca5c9a82cd864feea8783f.tar.gz"
version "25c12aac83fd2f8627ca5c9a82cd864feea8783f"
sha256 "d36995e5bac5feb6503ae76f201a618da26cbca414284a6caf33c71a9a835f54"

livecheck do
url "https://raw.githubusercontent.com/msoos/cryptominisat/refs/tags/release/#{LATEST_VERSION}/flake.lock"
url "https://raw.githubusercontent.com/msoos/cryptominisat/refs/tags/release/v#{LATEST_VERSION}/flake.lock"
strategy :json do |json|
json.dig("nodes", "cadical", "locked", "rev")
end
Expand All @@ -47,26 +47,17 @@ class Cryptominisat < Formula
# Currently using revision in flake.lock
resource "cadiback" do
url "https://github.com/meelgroup/cadiback.git",
revision: "c24a73f62da2f984df6d3f1cf37283b1ca1c9f9e"
version "c24a73f62da2f984df6d3f1cf37283b1ca1c9f9e"
revision: "798d069b99e030ddb4e612fb6ef7ccaaa2d3a5e5"
version "798d069b99e030ddb4e612fb6ef7ccaaa2d3a5e5"

livecheck do
url "https://raw.githubusercontent.com/msoos/cryptominisat/refs/tags/release/#{LATEST_VERSION}/flake.lock"
url "https://raw.githubusercontent.com/msoos/cryptominisat/refs/tags/release/v#{LATEST_VERSION}/flake.lock"
strategy :json do |json|
json.dig("nodes", "cadiback", "locked", "rev")
end
end
end

# Apply modified Arch Linux patch to avoid rebuilding C++ library for Python bindings
patch :DATA

# Apply Arch Linux patch to avoid paths to non-installed static libraries in CMake config file
patch do
url "https://gitlab.archlinux.org/archlinux/packaging/packages/cryptominisat/-/raw/f8e0e60b7d4fd9aa185a1a1a55dcd2b7ea123d58/link-private.patch"
sha256 "a5006f49e8adf1474725d2a3e4205cdd65beb2f100f5538b2f89e14de0613e0f"
end

def python3
"python3.14"
end
Expand All @@ -91,12 +82,19 @@ def install
system "make", "libcadiback.a"
end

system "cmake", "-S", name, "-B", "build", "-DMIT=ON", "-DCMAKE_INSTALL_RPATH=#{rpath}", *std_cmake_args
site_packages = prefix/Language::Python.site_packages(python3)
args = %W[
-DBUILD_PYTHON_EXTENSION=ON
-DCMAKE_INSTALL_RPATH=#{rpath};#{rpath(source: site_packages)}
-DMIT=ON
-Dcadiback_DIR=#{buildpath}/cadiback
-Dcadical_DIR=#{buildpath}/cadical/build
]

system "cmake", "-S", name, "-B", "build", *args, *std_cmake_args
system "cmake", "--build", "build"
system "cmake", "--install", "build"

ENV.append "LDFLAGS", "-Wl,-rpath,#{rpath(source: prefix/Language::Python.site_packages(python3))}"
system python3, "-m", "pip", "install", *std_pip_args(build_isolation: true), "./#{name}"
site_packages.install prefix.glob("pycryptosat.*.so")
end

test do
Expand All @@ -121,63 +119,3 @@ def install
assert_equal "(None, True, False, True)\n", shell_output("#{python3} test.py")
end
end

__END__
diff --git a/setup.py b/setup.py
index 537d78313..2e9a58ffd 100644
--- a/setup.py
+++ b/setup.py
@@ -58,51 +58,9 @@ def gen_modules(version):
include_dirs = ["src/", "./"],
sources = ["python/src/pycryptosat.cpp",
"python/src/GitSHA1.cpp",
- "src/backbone.cpp",
- "src/cardfinder.cpp",
- "src/ccnr_cms.cpp",
- "src/ccnr.cpp",
- "src/clauseallocator.cpp",
- "src/clausecleaner.cpp",
- "src/cnf.cpp",
- "src/completedetachreattacher.cpp",
- "src/cryptominisat_c.cpp",
- "src/cryptominisat.cpp",
- "src/datasync.cpp",
- "src/distillerbin.cpp",
- "src/distillerlitrem.cpp",
- "src/distillerlong.cpp",
- "src/distillerlongwithimpl.cpp",
- "src/gatefinder.cpp",
- "src/gaussian.cpp",
- "src/get_clause_query.cpp",
- "src/hyperengine.cpp",
- "src/idrup.cpp",
- "src/intree.cpp",
- "src/lucky.cpp",
- "src/matrixfinder.cpp",
- "src/occsimplifier.cpp",
- "src/packedrow.cpp",
- "src/propengine.cpp",
- "src/reducedb.cpp",
- "src/sccfinder.cpp",
- "src/searcher.cpp",
- "src/searchstats.cpp",
- "src/sls.cpp",
- "src/solutionextender.cpp",
- "src/solverconf.cpp",
- "src/solver.cpp",
- "src/str_impl_w_impl.cpp",
- "src/subsumeimplicit.cpp",
- "src/subsumestrengthen.cpp",
- "src/vardistgen.cpp",
- "src/varreplacer.cpp",
- "src/xorfinder.cpp",
- "src/oracle/oracle.cpp",
- "src/oracle_use.cpp",
- "src/probe.cpp",
],
- libraries = ['/usr/lib/libcadiback.so'], #, 'libgmpxx.so', 'libgmp.so'
+ library_dirs = ["../build/lib"],
+ libraries = ['cryptominisat5', '/usr/lib/libcadiback.so'], #, 'libgmpxx.so', 'libgmp.so'
extra_compile_args = extra_compile_args_val,
define_macros=define_macros_val,
language = "c++",
13 changes: 6 additions & 7 deletions Formula/k/klee.rb
Original file line number Diff line number Diff line change
Expand Up @@ -7,16 +7,15 @@ class Klee < Formula
url "https://github.com/klee/klee/archive/refs/tags/v3.2.tar.gz"
sha256 "83d9b9ce0ba187e48c0e55623bf1a68b5eb61376da7ce82551c9d885715a21dd"
license "NCSA"
revision 1
revision 2
head "https://github.com/klee/klee.git", branch: "master"

bottle do
rebuild 1
sha256 arm64_tahoe: "5a6b573c25130976ca751247e04d9fccb13fcaed6c509c4c6b4fdad39344c470"
sha256 arm64_sequoia: "2a75e77d76dbf1c19948be54c31e5ea6f0f555ffb61a33919cc3c2594c03559d"
sha256 arm64_sonoma: "c6e8559baf8e80ac61123eff04d32fed8523b2760dd8982f6041902b7a921f14"
sha256 sonoma: "c5da5c3aa76ee6df601a07b20bc4c2c31ed07730a80d31764338a0684cf7318a"
sha256 x86_64_linux: "92dd88ee1ef927f42257db072817fa552f0040c9cecb3128792de3643f1faf32"
sha256 arm64_tahoe: "203c689927268d04179ff379f721d67f07ed0891740c6bb594b320537e0c87bc"
sha256 arm64_sequoia: "fce18a6e0a204338ffab96d595a1970732f87c36f6fe5399c438da9ddee9375e"
sha256 arm64_sonoma: "aec64589dcd505701a20bec26fd753302044077cb312f605c149d7d92a94748a"
sha256 sonoma: "f421ee878c444e10d0baef47e564b9a4bd57172f9fbc022743c2d5aa7c98729d"
sha256 x86_64_linux: "13447a3a22f6de2d472b98c971b193ed8dd89396b370c8f5184c4e1dc96cd908"
end

depends_on "cmake" => :build
Expand Down
14 changes: 7 additions & 7 deletions Formula/s/stp.rb
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ class Stp < Formula
desc "Simple Theorem Prover, an efficient SMT solver for bitvectors"
homepage "https://stp.github.io/"
license "MIT"
revision 8
revision 9
head "https://github.com/stp/stp.git", branch: "master"

stable do
Expand All @@ -22,12 +22,12 @@ class Stp < Formula
end

bottle do
sha256 cellar: :any, arm64_tahoe: "aa08a02cc2bf05e0272644b9568aa861e7272a0368c98066c95a75877d2c303a"
sha256 cellar: :any, arm64_sequoia: "b3d18ec4ee1bfdda98b50cf653a3db4e76b83a88952bf8be3273ea50793dac9e"
sha256 cellar: :any, arm64_sonoma: "30a4268486f368e5d2d3b232812afeba87b643f5eeca6f9fe3db6bc689ec6705"
sha256 cellar: :any, sonoma: "ee33974fa9d80245ee1f586d6a7321a46d46ccbd8186aa57fa8eab6c17ce2bd4"
sha256 cellar: :any_skip_relocation, arm64_linux: "5d349289acbbeba2c7f4184598d7fe1ddd974c3c34a1ffb1d3ee3f224be8ade8"
sha256 cellar: :any_skip_relocation, x86_64_linux: "7e8b01d46340707274e6cff8df7c1510d88f7f8ab42ae41721af62682fb52c79"
sha256 cellar: :any, arm64_tahoe: "a116d5592fa317bbda40cb6b5b8704b95adea1f89322d6183a20ec695a3a609e"
sha256 cellar: :any, arm64_sequoia: "5b49ea62bc28988aee733b93243f04fe061dd9ce89275caf430391f6262f95fc"
sha256 cellar: :any, arm64_sonoma: "b677368cd71d24a6477f011838407cb2814e3efd66e35749e27824017ebac958"
sha256 cellar: :any, sonoma: "22ab44a28ba6d44ff38f6850eaa040b58ff5139ee5e7519061bb8eb6212807f3"
sha256 cellar: :any_skip_relocation, arm64_linux: "39f08ceaa72d2762cc56c642af6bd9f943bd3b8ca6ac82a57a1a53883d640d26"
sha256 cellar: :any_skip_relocation, x86_64_linux: "8a8f6222a9dcb368f00e9abfd4025b772354644b99ae3e34209690c9ac09bd86"
end

# stp refuses to build with system bison and flex
Expand Down
Loading