From 1c6d8e67d0e1bd7a052891c0f6b22361919eaaee Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Fri, 21 May 2010 15:21:11 +0000 Subject: [PATCH] * The bvsmod operation can now be output by the printers. * Output the status i.e. sat, unsat if known. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@773 e59a4935-1847-0410-ae03-e826735625c1 --- src/printer/SMTLIB1Printer.cpp | 13 +++++++++++++ src/printer/SMTLIB2Printer.cpp | 15 ++++++++++++++- src/printer/SMTLIBPrinter.cpp | 2 ++ 3 files changed, 29 insertions(+), 1 deletion(-) diff --git a/src/printer/SMTLIB1Printer.cpp b/src/printer/SMTLIB1Printer.cpp index a8875df..7ff2097 100644 --- a/src/printer/SMTLIB1Printer.cpp +++ b/src/printer/SMTLIB1Printer.cpp @@ -37,6 +37,14 @@ namespace printer else os << ":logic QF_BV" << endl; + if (input_status == TO_BE_SATISFIABLE) { + os << ":status sat" << endl; + } + else if (input_status == TO_BE_UNSATISFIABLE) { + os << ":status unsat" << endl; + } + else + os << ":status unknown" << endl; ASTNodeSet visited, symbols; buildListOfSymbols(n, visited, symbols); @@ -196,6 +204,11 @@ void printSMTLIB1VarDeclsToStream(ASTNodeSet& symbols, ostream& os) break; default: { + if ((kind == AND || kind == OR|| kind == XOR) && n.Degree() != 2) + { + FatalError("Wrong number of arguments to operation (must be two).", n); + } + // SMT-LIB only allows these functions to have two parameters. if ((BVPLUS == kind || kind == BVOR || kind == BVAND) && n.Degree() > 2) { diff --git a/src/printer/SMTLIB2Printer.cpp b/src/printer/SMTLIB2Printer.cpp index 1d983e6..2494c51 100644 --- a/src/printer/SMTLIB2Printer.cpp +++ b/src/printer/SMTLIB2Printer.cpp @@ -33,7 +33,15 @@ void SMTLIB2_PrintBack(ostream &os, const ASTNode& n) os << "(set-logic QF_BV)"<< endl; os << "(set-info :smt-lib-version 2.0)"<< endl; - os << "(set-info :status unknown)"<< endl; + + + if (input_status == TO_BE_SATISFIABLE) { + os << "(set-info :status sat)"<< endl; + } + else if (input_status == TO_BE_UNSATISFIABLE) { + os << "(set-info :status unsat)"<< endl; + } else + os << "(set-info :status unknown)"<< endl; ASTNodeSet visited, symbols; buildListOfSymbols(n, visited, symbols); @@ -193,6 +201,11 @@ void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os) break; default: { + if ((kind == AND || kind == OR|| kind == XOR) && n.Degree() != 2) + { + FatalError("Wrong number of arguments to operation (must be two).", n); + } + // SMT-LIB only allows these functions to have two parameters. if ((BVPLUS == kind || kind == BVOR || kind == BVAND) && n.Degree() > 2) { diff --git a/src/printer/SMTLIBPrinter.cpp b/src/printer/SMTLIBPrinter.cpp index a3b7bcb..6245a04 100644 --- a/src/printer/SMTLIBPrinter.cpp +++ b/src/printer/SMTLIBPrinter.cpp @@ -247,6 +247,8 @@ static string tolower(const char * name) return "bvsdiv"; case SBVREM: return "bvsrem"; + case SBVMOD: + return "bvsmod"; default: { -- 2.47.3