git: 0ce587185546 - main - math/symfpu: New port: Implementation of IEEE-754 / SMT-LIB floating-point

From: Yuri Victorovich <yuri_at_FreeBSD.org>
Date: Wed, 04 Jan 2023 10:52:05 UTC
The branch main has been updated by yuri:

URL: https://cgit.FreeBSD.org/ports/commit/?id=0ce58718554603ba9b178a44857e3b088ed0bb0f

commit 0ce58718554603ba9b178a44857e3b088ed0bb0f
Author:     Yuri Victorovich <yuri@FreeBSD.org>
AuthorDate: 2023-01-04 08:29:55 +0000
Commit:     Yuri Victorovich <yuri@FreeBSD.org>
CommitDate: 2023-01-04 10:51:59 +0000

    math/symfpu: New port: Implementation of IEEE-754 / SMT-LIB floating-point
---
 math/Makefile                                      |  1 +
 math/symfpu/Makefile                               | 32 ++++++++++++++++++++++
 math/symfpu/distinfo                               |  3 ++
 .../files/patch-baseTypes_simpleExecutable.cpp     | 11 ++++++++
 .../files/patch-baseTypes_simpleExecutable.h       | 15 ++++++++++
 math/symfpu/pkg-descr                              |  8 ++++++
 math/symfpu/pkg-plist                              | 19 +++++++++++++
 7 files changed, 89 insertions(+)

diff --git a/math/Makefile b/math/Makefile
index 7493281fb77c..c5b0cf9072d9 100644
--- a/math/Makefile
+++ b/math/Makefile
@@ -1140,6 +1140,7 @@
     SUBDIR += superlu
     SUBDIR += superlu-dist
     SUBDIR += symengine
+    SUBDIR += symfpu
     SUBDIR += symmetrica
     SUBDIR += symphony
     SUBDIR += sympol
diff --git a/math/symfpu/Makefile b/math/symfpu/Makefile
new file mode 100644
index 000000000000..c3a04d80a98f
--- /dev/null
+++ b/math/symfpu/Makefile
@@ -0,0 +1,32 @@
+PORTNAME=	symfpu
+DISTVERSION=	g20190517
+CATEGORIES=	math
+
+MAINTAINER=	yuri@FreeBSD.org
+COMMENT=	Implementation of IEEE-754 / SMT-LIB floating-point
+WWW=		https://github.com/martin-cs/symfpu
+
+LICENSE=	GPLv3
+LICENSE_FILE=	${WRKSRC}/LICENSE
+
+USES=		gmake
+
+USE_GITHUB=	yes
+GH_ACCOUNT=	martin-cs
+GH_TAGNAME=	c3acaf6
+
+CXXFLAGS+=	-I${WRKSRC}
+
+ALL_TARGET=	subdirs symfpu.a
+
+MAKE_ARGS=	SUBDIRS=baseTypes
+
+do-install:
+	${MKDIR} \
+		${STAGEDIR}${PREFIX}/include/symfpu/core \
+		${STAGEDIR}${PREFIX}/include/symfpu/utils
+	${CP} ${WRKSRC}/core/*.h ${STAGEDIR}${PREFIX}/include/symfpu/core
+	${CP} ${WRKSRC}/utils/*.h ${STAGEDIR}${PREFIX}/include/symfpu/utils
+	${INSTALL_DATA} ${WRKSRC}/symfpu.a ${STAGEDIR}${PREFIX}/lib
+
+.include <bsd.port.mk>
diff --git a/math/symfpu/distinfo b/math/symfpu/distinfo
new file mode 100644
index 000000000000..1a502917e5c9
--- /dev/null
+++ b/math/symfpu/distinfo
@@ -0,0 +1,3 @@
+TIMESTAMP = 1672799708
+SHA256 (martin-cs-symfpu-g20190517-c3acaf6_GH0.tar.gz) = 3cc3bda6357e98c348abe4b9e72be9ddca918acdcb1f19406e6a35dc939d9f24
+SIZE (martin-cs-symfpu-g20190517-c3acaf6_GH0.tar.gz) = 77560
diff --git a/math/symfpu/files/patch-baseTypes_simpleExecutable.cpp b/math/symfpu/files/patch-baseTypes_simpleExecutable.cpp
new file mode 100644
index 000000000000..b48373872b11
--- /dev/null
+++ b/math/symfpu/files/patch-baseTypes_simpleExecutable.cpp
@@ -0,0 +1,11 @@
+--- baseTypes/simpleExecutable.cpp.orig	2023-01-04 05:09:43 UTC
++++ baseTypes/simpleExecutable.cpp
+@@ -28,7 +28,7 @@
+ */
+ 
+ 
+-#include "symfpu/baseTypes/simpleExecutable.h"
++#include "baseTypes/simpleExecutable.h"
+ 
+ #include <assert.h>
+ #include <math.h>
diff --git a/math/symfpu/files/patch-baseTypes_simpleExecutable.h b/math/symfpu/files/patch-baseTypes_simpleExecutable.h
new file mode 100644
index 000000000000..62259ae6b1bb
--- /dev/null
+++ b/math/symfpu/files/patch-baseTypes_simpleExecutable.h
@@ -0,0 +1,15 @@
+--- baseTypes/simpleExecutable.h.orig	2023-01-04 05:11:39 UTC
++++ baseTypes/simpleExecutable.h
+@@ -34,9 +34,9 @@
+ **
+ */
+ 
+-#include "symfpu/utils/properties.h"
+-#include "symfpu/core/ite.h"
+-#include "symfpu/baseTypes/shared.h"
++#include "utils/properties.h"
++#include "core/ite.h"
++#include "baseTypes/shared.h"
+ 
+ #include <assert.h>
+ #include <stdint.h>
diff --git a/math/symfpu/pkg-descr b/math/symfpu/pkg-descr
new file mode 100644
index 000000000000..4c44beef1825
--- /dev/null
+++ b/math/symfpu/pkg-descr
@@ -0,0 +1,8 @@
+SymFPU is an implementation of the SMT-LIB / IEEE-754 operations in terms of
+bit-vector operations. It is templated in terms of the bit-vectors,
+propositions, floating-point formats and rounding mode types used. This allow
+the same code to be executed as an arbitrary precision "SoftFloat" library
+(although it's performance would not be good) or to be used to build symbolic
+representation of floating-point operations suitable for use in "bit-blasting"
+SMT solvers (you could also generate circuits from them but again, performance
+will likely not be good).
diff --git a/math/symfpu/pkg-plist b/math/symfpu/pkg-plist
new file mode 100644
index 000000000000..14814000293a
--- /dev/null
+++ b/math/symfpu/pkg-plist
@@ -0,0 +1,19 @@
+include/symfpu/core/add.h
+include/symfpu/core/classify.h
+include/symfpu/core/compare.h
+include/symfpu/core/convert.h
+include/symfpu/core/divide.h
+include/symfpu/core/fma.h
+include/symfpu/core/ite.h
+include/symfpu/core/multiply.h
+include/symfpu/core/operations.h
+include/symfpu/core/packing.h
+include/symfpu/core/remainder.h
+include/symfpu/core/rounder.h
+include/symfpu/core/sign.h
+include/symfpu/core/sqrt.h
+include/symfpu/core/unpackedFloat.h
+include/symfpu/utils/common.h
+include/symfpu/utils/numberOfRoundingModes.h
+include/symfpu/utils/properties.h
+lib/symfpu.a