/
stp.rb
88 lines (78 loc) 路 3.23 KB
/
stp.rb
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
class Stp < Formula
desc "Simple Theorem Prover, an efficient SMT solver for bitvectors"
homepage "https://stp.github.io/"
url "https://github.com/stp/stp/archive/refs/tags/2.3.3.tar.gz"
sha256 "ea6115c0fc11312c797a4b7c4db8734afcfce4908d078f386616189e01b4fffa"
license "MIT"
revision 9
head "https://github.com/stp/stp.git", branch: "master"
livecheck do
url :stable
regex(/^(?:stp[._-])?v?(\d+(?:\.\d+)+)$/i)
end
bottle do
sha256 cellar: :any, arm64_sonoma: "af259bce456b7f1f1269ee4eb197595f548b2244121b515e65b6ddec73afb3f7"
sha256 cellar: :any, arm64_ventura: "0b6f933623aa208cd85648200e096e2f198aa29a7ea239d9aa518957886555be"
sha256 cellar: :any, arm64_monterey: "e86254768238af80a8b296360899c0cefd6998a874bfe023af2e611849437efc"
sha256 cellar: :any, sonoma: "b6df750106655bc6a56bdce7bde676fdb1520cc95bad5c268659094d4cfa06e4"
sha256 cellar: :any, ventura: "0163fc3b8fdf0abc81a956684c54de143d1e91b908dac9c4190783f52be48872"
sha256 cellar: :any, monterey: "24ca98b6832488b7e7530fd5031c4556983c6ca9982d340ab1d646a6f249e39b"
sha256 cellar: :any_skip_relocation, x86_64_linux: "c13b033b4156a4d75e6692682f041ec1d39d52ec4ff5d920e5b47b99a4d5ce1d"
end
# stp refuses to build with system bison and flex
depends_on "bison" => :build
depends_on "cmake" => :build
depends_on "flex" => :build
depends_on "python-setuptools" => :build
depends_on "boost"
depends_on "cryptominisat"
depends_on "minisat"
depends_on "python@3.12"
uses_from_macos "perl"
def install
python = "python3.12"
site_packages = prefix/Language::Python.site_packages(python)
site_packages.mkpath
inreplace "lib/Util/GitSHA1.cpp.in", "@CMAKE_CXX_COMPILER@", ENV.cxx
system "cmake", "-S", ".", "-B", "build",
"-DPYTHON_EXECUTABLE=#{Formula["python@3.12"].opt_bin}/#{python}",
"-DPYTHON_LIB_INSTALL_DIR=#{site_packages}",
*std_cmake_args
system "cmake", "--build", "build"
system "cmake", "--install", "build"
end
test do
(testpath/"prob.smt").write <<~EOS
(set-logic QF_BV)
(assert (= (bvsdiv (_ bv3 2) (_ bv2 2)) (_ bv0 2)))
(check-sat)
(exit)
EOS
assert_equal "sat", shell_output("#{bin}/stp --SMTLIB2 prob.smt").chomp
(testpath/"test.c").write <<~EOS
#include "stp/c_interface.h"
#include <assert.h>
int main() {
VC vc = vc_createValidityChecker();
Expr c = vc_varExpr(vc, "c", vc_bvType(vc, 32));
Expr a = vc_bvConstExprFromInt(vc, 32, 5);
Expr b = vc_bvConstExprFromInt(vc, 32, 6);
Expr xp1 = vc_bvPlusExpr(vc, 32, a, b);
Expr eq = vc_eqExpr(vc, xp1, c);
Expr eq2 = vc_notExpr(vc, eq);
int ret = vc_query(vc, eq2);
assert(ret == false);
vc_printCounterExample(vc);
vc_Destroy(vc);
return 0;
}
EOS
expected_output = <<~EOS
COUNTEREXAMPLE BEGIN:\s
ASSERT( c = 0x0000000B );
COUNTEREXAMPLE END:\s
EOS
system ENV.cc, "test.c", "-I#{include}", "-L#{lib}", "-lstp", "-o", "test"
assert_equal expected_output.chomp, shell_output("./test").chomp
end
end