From 9d33b74150ec4e36847f2ac34f634e8cd4aa2e22 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 17 Mar 2010 03:55:25 +0000 Subject: [PATCH] When outputting to SMTLIB format handle properly some cases when the number of arguments > 2. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@643 e59a4935-1847-0410-ae03-e826735625c1 --- src/printer/SMTLIBPrinter.cpp | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/printer/SMTLIBPrinter.cpp b/src/printer/SMTLIBPrinter.cpp index bc5ba00..cfe345a 100644 --- a/src/printer/SMTLIBPrinter.cpp +++ b/src/printer/SMTLIBPrinter.cpp @@ -167,10 +167,14 @@ void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os) case FALSE: os << "false"; break; - case NAND: // No NAND in smtlib format. + case NAND: // No NAND, NOR in smtlib format. + case NOR: assert(c.size() ==2); os << "(" << "not "; - os << "(" << "and "; + if (NAND == kind ) + os << "(" << "and "; + else + os << "(" << "or "; SMTLIB_Print1(os, c[0], 0, letize); os << " " ; SMTLIB_Print1(os, c[1], 0, letize); @@ -205,8 +209,8 @@ void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os) break; default: { - // SMT-LIB only allows arithmetic functions to have two parameters. - if (BVPLUS == kind && n.Degree() > 2) + // SMT-LIB only allows these functions to have two parameters. + if ((BVPLUS == kind || kind == BVOR || kind == BVAND) && n.Degree() > 2) { string close = ""; -- 2.47.3