From: trevor_hansen Date: Sat, 10 Jul 2010 14:49:13 +0000 (+0000) Subject: A QF_ABV division has been added to the smt-lib. Update parser to read, update printe... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=e40f2cac168708b53b96d524afdce80e6a9bc267;p=francis%2Fstp.git A QF_ABV division has been added to the smt-lib. Update parser to read, update printer to write it. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@951 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/parser/smtlib2.y b/src/parser/smtlib2.y index a94bd6c..8d138fd 100644 --- a/src/parser/smtlib2.y +++ b/src/parser/smtlib2.y @@ -226,6 +226,7 @@ cmdi: LPAREN_TOK LOGIC_TOK FORMID_TOK RPAREN_TOK { if (!(0 == strcmp($3->GetName(),"QF_BV") || + 0 == strcmp($3->GetName(),"QF_ABV") || 0 == strcmp($3->GetName(),"QF_AUFBV"))) { yyerror("Wrong input logic:"); } diff --git a/src/printer/SMTLIB2Printer.cpp b/src/printer/SMTLIB2Printer.cpp index b723211..dc15389 100644 --- a/src/printer/SMTLIB2Printer.cpp +++ b/src/printer/SMTLIB2Printer.cpp @@ -27,7 +27,7 @@ namespace printer void SMTLIB2_PrintBack(ostream &os, const ASTNode& n) { if (containsArrayOps(n)) - os << "(set-logic QF_AUFBV)" << endl; + os << "(set-logic QF_ABV)" << endl; else os << "(set-logic QF_BV)"<< endl;