svn commit: r525718 - in head/math: . ctl-sat ctl-sat/files
Mateusz Piotrowski
0mp at FreeBSD.org
Mon Feb 10 16:43:22 UTC 2020
Author: 0mp
Date: Mon Feb 10 16:43:21 2020
New Revision: 525718
URL: https://svnweb.freebsd.org/changeset/ports/525718
Log:
New port: math/ctl-sat: CTL (Computation Tree Logic) SAT solver
CTL-SAT is a CTL (Computation Tree Logic) SAT solver. The user may test
satisfiability of a CTL formula may by providing it as a command-line
argument to the ctl-sat program, e.g.:
ctl-sat "~( (A(pUq) ^ AG(q->r) ^ AG(r->EXr)) -> EFEGr )"
The worst-case time complexity is O((2^n)^3) for this SAT solver, while the
worst-case space complexity is O((2^n)^2).
WWW: https://github.com/nicolaprezza/CTLSAT
Added:
head/math/ctl-sat/
head/math/ctl-sat/Makefile (contents, props changed)
head/math/ctl-sat/distinfo (contents, props changed)
head/math/ctl-sat/files/
head/math/ctl-sat/files/patch-Makefile (contents, props changed)
head/math/ctl-sat/pkg-descr (contents, props changed)
Modified:
head/math/Makefile
Modified: head/math/Makefile
==============================================================================
--- head/math/Makefile Mon Feb 10 16:41:24 2020 (r525717)
+++ head/math/Makefile Mon Feb 10 16:43:21 2020 (r525718)
@@ -200,6 +200,7 @@
SUBDIR += crlibm
SUBDIR += cryptominisat
SUBDIR += csdp
+ SUBDIR += ctl-sat
SUBDIR += curv
SUBDIR += cvc3
SUBDIR += cvc4
Added: head/math/ctl-sat/Makefile
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ head/math/ctl-sat/Makefile Mon Feb 10 16:43:21 2020 (r525718)
@@ -0,0 +1,34 @@
+# $FreeBSD$
+
+PORTNAME= ctl-sat
+DISTVERSION= g20200210
+CATEGORIES= math
+
+MAINTAINER= 0mp at FreeBSD.org
+COMMENT= CTL (Computation Tree Logic) SAT solver
+
+LICENSE= MIT
+LICENSE_FILE= ${WRKSRC}/LICENSE
+
+USE_GITHUB= yes
+GH_ACCOUNT= nicolaprezza
+GH_PROJECT= CTLSAT
+GH_TAGNAME= 6de41e0
+
+PLIST_FILES= bin/ctl-sat
+
+PORTDOCS= README.md
+
+OPTIONS_DEFINE= DOCS
+
+pre-build:
+ @${RM} ${WRKSRC}/ctl-sat
+
+do-install:
+ ${INSTALL_PROGRAM} ${WRKSRC}/ctl-sat ${STAGEDIR}${PREFIX}/bin
+
+post-install-DOCS-on:
+ @${MKDIR} ${STAGEDIR}${DOCSDIR}
+ ${INSTALL_MAN} ${WRKSRC}/README.md ${STAGEDIR}${DOCSDIR}
+
+.include <bsd.port.mk>
Added: head/math/ctl-sat/distinfo
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ head/math/ctl-sat/distinfo Mon Feb 10 16:43:21 2020 (r525718)
@@ -0,0 +1,3 @@
+TIMESTAMP = 1581352735
+SHA256 (nicolaprezza-CTLSAT-g20200210-6de41e0_GH0.tar.gz) = f285cc5ab39359b45d3a1b22c725393458624dea82f11b29ed9828cf523aa7ed
+SIZE (nicolaprezza-CTLSAT-g20200210-6de41e0_GH0.tar.gz) = 1197332
Added: head/math/ctl-sat/files/patch-Makefile
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ head/math/ctl-sat/files/patch-Makefile Mon Feb 10 16:43:21 2020 (r525718)
@@ -0,0 +1,38 @@
+--- Makefile.orig 2015-01-07 10:27:59 UTC
++++ Makefile
+@@ -2,26 +2,15 @@
+
+ SOURCE=\
+ formulas/AllTomorrow.cpp \
+-formulas/AllTomorrow.h \
+ formulas/AllUntil.cpp \
+-formulas/AllUntil.h \
+ formulas/Atom.cpp \
+-formulas/Atom.h \
+ formulas/Conjunction.cpp \
+-formulas/Conjunction.h \
+ formulas/ExistsTomorrow.cpp \
+-formulas/ExistsTomorrow.h \
+ formulas/ExistsUntil.cpp \
+-formulas/ExistsUntil.h \
+ formulas/Formula.cpp \
+-formulas/Formula.h \
+ formulas/Negation.cpp \
+-formulas/Negation.h \
+ parser/CTLParser.cpp \
+-parser/CTLParser.h \
+ tableau/Tableau.cpp \
+-tableau/Tableau.h \
+-common.h \
+ main.cpp \
+
+
+@@ -33,7 +22,7 @@ all: $(BINARY)
+
+ $(BINARY): $(SOURCE)
+
+- g++ -march=native -mtune=generic -O3 $(SOURCE) -o $(BINARY)
++ $(CXX) $(CXXFLAGS) $(SOURCE) -o $(BINARY)
+
+ clean:
+
Added: head/math/ctl-sat/pkg-descr
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ head/math/ctl-sat/pkg-descr Mon Feb 10 16:43:21 2020 (r525718)
@@ -0,0 +1,10 @@
+CTL-SAT is a CTL (Computation Tree Logic) SAT solver. The user may test
+satisfiability of a CTL formula may by providing it as a command-line argument
+to the ctl-sat program, e.g.:
+
+ ctl-sat "~( (A(pUq) ^ AG(q->r) ^ AG(r->EXr)) -> EFEGr )"
+
+The worst-case time complexity is O((2^n)^3) for this SAT solver, while the
+worst-case space complexity is O((2^n)^2).
+
+WWW: https://github.com/nicolaprezza/CTLSAT
More information about the svn-ports-all
mailing list