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

math/Makefile

@@ -200,6 +200,7 @@
     SUBDIR += crlibm
     SUBDIR += cryptominisat
     SUBDIR += csdp
+    SUBDIR += ctl-sat
     SUBDIR += curv
     SUBDIR += cvc3
     SUBDIR += cvc4

math/ctl-sat/Makefile

@@ -0,0 +1,34 @@
+# $FreeBSD$
+
+PORTNAME=	ctl-sat
+DISTVERSION=	g20200210
+CATEGORIES=	math
+
+MAINTAINER=	0mp@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>

math/ctl-sat/distinfo

@@ -0,0 +1,3 @@
+TIMESTAMP = 1581352735
+SHA256 (nicolaprezza-CTLSAT-g20200210-6de41e0_GH0.tar.gz) = f285cc5ab39359b45d3a1b22c725393458624dea82f11b29ed9828cf523aa7ed
+SIZE (nicolaprezza-CTLSAT-g20200210-6de41e0_GH0.tar.gz) = 1197332

math/ctl-sat/files/patch-Makefile

@@ -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:
+ 

math/ctl-sat/pkg-descr

@@ -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