From: Andrew Reynolds Date: Tue, 14 May 2013 20:18:29 +0000 (-0500) Subject: Add support for quantifier patterns in smt2 printer. X-Git-Tag: cvc5-1.0.0~7287^2~120 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5762731a21d3c4e115708f96c4eb0301e00f3dd7;p=cvc5.git Add support for quantifier patterns in smt2 printer. --- diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index c59df6269..a2fe96271 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -214,7 +214,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, bool stillNeedToPrintParams = true; // operator - if(n.getNumChildren() != 0) out << '('; + if(n.getNumChildren() != 0 && n.getKind()!=kind::INST_PATTERN_LIST) out << '('; switch(Kind k = n.getKind()) { // builtin theory case kind::APPLY: break; @@ -312,12 +312,29 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, break; // quantifiers - case kind::FORALL: out << "forall "; break; - case kind::EXISTS: out << "exists "; break; + case kind::FORALL: + case kind::EXISTS: + if( k==kind::FORALL ){ + out << "forall "; + }else{ + out << "exists "; + } + for( unsigned i=0; i<2; i++) { + out << n[i] << " "; + if( i==0 && n.getNumChildren()==3 ){ + out << "(! "; + } + } + if( n.getNumChildren()==3 ){ + out << n[2]; + out << ")"; + } + out << ")"; + return; + break; case kind::BOUND_VAR_LIST: // the left parenthesis is already printed (before the switch) - for(TNode::iterator i = n.begin(), - iend = n.end(); + for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ) { out << '('; toStream(out, (*i), toDepth < 0 ? toDepth : toDepth - 1, types); @@ -334,8 +351,13 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, out << ')'; return; case kind::INST_PATTERN: + break; case kind::INST_PATTERN_LIST: // TODO user patterns + for(unsigned i=0; i