| Server IP : 82.208.35.60 / Your IP : 216.73.216.238 Web Server : Apache/2.4.55 (FreeBSD) OpenSSL/1.1.1q-freebsd PHP/7.3.31 System : FreeBSD server7.d2m.cz 12.4-RELEASE-p9 FreeBSD 12.4-RELEASE-p9 GENERIC amd64 User : studiokobylisy_cz ( 1008) PHP Version : 7.3.31 Disable Function : NONE MySQL : OFF | cURL : ON | WGET : OFF | Perl : OFF | Python : OFF | Sudo : OFF | Pkexec : OFF Directory : /usr/ports/lang/maude/files/ |
Upload File : |
kind::IFF was removed in CVC4 1.6
--- src/Mixfix/variableGenerator.cc.orig 2018-09-17 10:44:35 UTC
+++ 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:
{