Date: Friday, January 12, 2018 @ 19:28:57
Author: arojas
Revision: 281691
Rebuild with CVC4 1.5 (FS#57069)
Added:
maude/trunk/maude-cvc4-1.5.patch
Modified:
maude/trunk/PKGBUILD
----------------------+
PKGBUILD | 9 ++++++---
maude-cvc4-1.5.patch | 24 ++++++++++++++++++++++++
2 files changed, 30 insertions(+), 3 deletions(-)
Modified: PKGBUILD
===================================================================
--- PKGBUILD 2018-01-12 18:58:06 UTC (rev 281690)
+++ PKGBUILD 2018-01-12 19:28:57 UTC (rev 281691)
@@ -6,7 +6,7 @@
pkgname=maude
pkgver=2.7.1
-pkgrel=1
+pkgrel=2
pkgdesc="High-level Specification Language"
arch=('x86_64')
url="http://maude.cs.uiuc.edu";
@@ -15,14 +15,17 @@
makedepends=('flex' 'bison')
source=("http://maude.cs.illinois.edu/w/images/d/d8/Maude-$pkgver.tar.gz";
"http://maude.cs.illinois.edu/w/images/c/ca/Full-Maude-$pkgver.zip";
- maude.sh)
+ maude.sh maude-cvc4-1.5.patch)
md5sums=('aa31753f742f976940c69aa699c3d0ec'
'b365fe0fdd161880e95aeb089f166657'
- '0a51738365579574b40a3d32da6f3291')
+ '0a51738365579574b40a3d32da6f3291'
+ '9e759db427d9d6e77d35cc56b7690e0b')
prepare() {
cd "$srcdir/maude-$pkgver"
autoreconf -i
+
+ patch -p1 -i ../maude-cvc4-1.5.patch # Fix build with CVC4 1.5
}
build() {
Added: maude-cvc4-1.5.patch
===================================================================
--- maude-cvc4-1.5.patch (rev 0)
+++ maude-cvc4-1.5.patch 2018-01-12 19:28:57 UTC (rev 281691)
@@ -0,0 +1,24 @@
+diff --git a/src/Mixfix/variableGenerator.cc b/src/Mixfix/variableGenerator.cc
+index 4761dfc..086b4ee 100755
+--- a/src/Mixfix/variableGenerator.cc
++++ b/src/Mixfix/variableGenerator.cc
+@@ -312,18 +312,7 @@ VariableGenerator::dagToCVC4(DagNode* dag)
+ //
+ case SMT_Symbol::EQUALS:
+ {
+- //
+- // Bizarrely CVC4 requires the IFF be used for Boolean equality so
we need to
+- // check the SMT type associated with our first argument sort to
catch this case.
+- //
+- Sort* domainSort = s->getOpDeclarations()[0].getDomainAndRange()[0];
+- SMT_Info::SMT_Type smtType = smtInfo.getType(domainSort);
+- if (smtType == SMT_Info::NOT_SMT)
+- {
+- IssueWarning("term " << QUOTE(dag) << " does not belong to an
SMT sort.");
+- goto fail;
+- }
+- return exprManager->mkExpr(((smtType == SMT_Info::BOOLEAN) ?
kind::IFF : kind::EQUAL), exprs[0], exprs[1]);
++ return exprManager->mkExpr(kind::EQUAL, exprs[0], exprs[1]);
+ }
+ case SMT_Symbol::NOT_EQUALS:
+ {
