From d7d93965efa936d4043e7330da6907630556e5a7 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 12 Mar 2012 04:06:44 +0000 Subject: [PATCH] Add the ability to tell the SMTLIB2 printer whether it contains arrays or not. The array check can be very expensive. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1589 e59a4935-1847-0410-ae03-e826735625c1 --- src/printer/SMTLIB2Printer.cpp | 22 +++++++++++----------- src/printer/printers.h | 4 +--- 2 files changed, 12 insertions(+), 14 deletions(-) diff --git a/src/printer/SMTLIB2Printer.cpp b/src/printer/SMTLIB2Printer.cpp index dc15389..351f000 100644 --- a/src/printer/SMTLIB2Printer.cpp +++ b/src/printer/SMTLIB2Printer.cpp @@ -24,32 +24,32 @@ namespace printer void SMTLIB2_Print1(ostream& os, const BEEV::ASTNode n, int indentation, bool letize); void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os); -void SMTLIB2_PrintBack(ostream &os, const ASTNode& n) +void SMTLIB2_PrintBack(ostream &os, const ASTNode& n, const bool definately_bv) { - if (containsArrayOps(n)) - os << "(set-logic QF_ABV)" << endl; + if (!definately_bv && containsArrayOps(n)) + os << "(set-logic QF_ABV)\n"; else - os << "(set-logic QF_BV)"<< endl; + os << "(set-logic QF_BV)\n"; - os << "(set-info :smt-lib-version 2.0)"<< endl; + os << "(set-info :smt-lib-version 2.0)\n"; if (input_status == TO_BE_SATISFIABLE) { - os << "(set-info :status sat)"<< endl; + os << "(set-info :status sat)\n"; } else if (input_status == TO_BE_UNSATISFIABLE) { - os << "(set-info :status unsat)"<< endl; + os << "(set-info :status unsat)\n"; } else - os << "(set-info :status unknown)"<< endl; + os << "(set-info :status unknown)\n"; ASTNodeSet visited, symbols; buildListOfSymbols(n, visited, symbols); printVarDeclsToStream(symbols, os); os << "(assert "; SMTLIB_Print(os, n, 0, &SMTLIB2_Print1, false); - os << ")" << endl; - os << "(check-sat)" << endl; - os << "(exit)" << endl; + os << ")\n"; + // os << "(check-sat)" << endl; + // os << "(exit)\n"; } void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os) diff --git a/src/printer/printers.h b/src/printer/printers.h index da15251..f70f314 100644 --- a/src/printer/printers.h +++ b/src/printer/printers.h @@ -38,9 +38,7 @@ namespace printer void SMTLIB1_PrintBack(ostream &os, const BEEV::ASTNode& n ); - void SMTLIB2_PrintBack(ostream &os, - const BEEV::ASTNode& n ); - + void SMTLIB2_PrintBack(ostream &os, const ASTNode& n, bool definately_bv=false); ostream& GDL_Print(ostream &os, const BEEV::ASTNode n); ostream& GDL_Print(ostream &os, const ASTNode n, string (*annotate)(const ASTNode&)); -- 2.47.3