[arch-commits] Commit in maude/trunk (PKGBUILD maude-cvc4-1.5.patch)

[Antonio Rojas]

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