diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
commit | 1d18e5ebed9a5b20ed6a8fe21d11842acf6fa7ea (patch) | |
tree | 7074f04453914bc377ff6aeb307dd17b82b76ff3 /src/printer/cvc | |
parent | 74770f1071e6102795393cf65dd0c651038db6b4 (diff) |
Merge from my post-smtcomp branch. Includes:
Dumping infrastructure. Can dump preprocessed queries and clauses. Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc. For a
full list of options see --dump=help.
CUDD building much cleaner.
Documentation and assertion fixes.
Printer improvements, printing of commands in language-defined way, etc.
Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.
CVC3 compatibility layer (builds as libcompat).
SWIG detection and language binding support (infrastructure).
Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).
Copyright and file headers regenerated.
Diffstat (limited to 'src/printer/cvc')
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 98 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.h | 2 |
2 files changed, 83 insertions, 17 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 8e089a8a3..0f3d635bd 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -28,6 +28,7 @@ #include <typeinfo> #include <algorithm> #include <iterator> +#include <stack> using namespace std; @@ -172,6 +173,15 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, return; } else if(n.getMetaKind() == kind::metakind::PARAMETERIZED) { switch(n.getKind()) { + case kind::SORT_TYPE: { + std::string name; + if(n.getAttribute(expr::VarNameAttr(), name)) { + out << name; + } else { + goto default_case; + } + break; + } case kind::BITVECTOR_EXTRACT: out << n[0] << n.getOperator().getConst<BitVectorExtract>(); break; @@ -192,6 +202,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, break; default: + default_case: out << n.getOperator(); if(n.getNumChildren() > 0) { out << '('; @@ -231,9 +242,24 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, case kind::SELECT: out << n[0] << '[' << n[1] << ']'; break; - case kind::STORE: - out << n[0] << " WITH [" << n[1] << "] = " << n[2]; + case kind::STORE: { + stack<TNode> stk; + stk.push(n); + while(stk.top()[0].getKind() == kind::STORE) { + stk.push(stk.top()[0]); + } + out << '('; + TNode x = stk.top(); + out << x[0] << " WITH [" << x[1] << "] := " << x[2]; + stk.pop(); + while(!stk.empty()) { + x = stk.top(); + out << ", [" << x[1] << "] := " << x[2]; + stk.pop(); + } + out << ')'; break; + } case kind::TUPLE_TYPE: out << '['; @@ -301,7 +327,9 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, // infix binary operator out << '(' << n[0] << ' ' << n.getOperator() << ' ' << n[1] << ')'; } else if(n.getKind() == kind::AND || - n.getKind() == kind::OR) { + n.getKind() == kind::OR || + n.getKind() == kind::PLUS || + n.getKind() == kind::MULT) { // infix N-ary operator TNode::iterator i = n.begin(); out << '(' << *i++; @@ -347,9 +375,12 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c, tryToStream<CheckSatCommand>(out, c) || tryToStream<QueryCommand>(out, c) || tryToStream<QuitCommand>(out, c) || + tryToStream<DeclarationSequence>(out, c) || tryToStream<CommandSequence>(out, c) || - tryToStream<DeclarationCommand>(out, c) || + tryToStream<DeclareFunctionCommand>(out, c) || tryToStream<DefineFunctionCommand>(out, c) || + tryToStream<DeclareTypeCommand>(out, c) || + tryToStream<DefineTypeCommand>(out, c) || tryToStream<DefineNamedFunctionCommand>(out, c) || tryToStream<SimplifyCommand>(out, c) || tryToStream<GetValueCommand>(out, c) || @@ -361,7 +392,8 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c, tryToStream<GetInfoCommand>(out, c) || tryToStream<SetOptionCommand>(out, c) || tryToStream<GetOptionCommand>(out, c) || - tryToStream<DatatypeDeclarationCommand>(out, c)) { + tryToStream<DatatypeDeclarationCommand>(out, c) || + tryToStream<CommentCommand>(out, c)) { return; } @@ -385,16 +417,22 @@ static void toStream(std::ostream& out, const CheckSatCommand* c) { BoolExpr e = c->getExpr(); if(!e.isNull()) { out << "CHECKSAT " << e << ";"; + } else { + out << "CHECKSAT;"; } - out << "CHECKSAT;"; } static void toStream(std::ostream& out, const QueryCommand* c) { - out << "QUERY " << c->getExpr() << ";"; + BoolExpr e = c->getExpr(); + if(!e.isNull()) { + out << "QUERY " << e << ";"; + } else { + out << "QUERY TRUE;"; + } } static void toStream(std::ostream& out, const QuitCommand* c) { - Unhandled("quit command"); + //out << "EXIT;"; } static void toStream(std::ostream& out, const CommandSequence* c) { @@ -405,14 +443,22 @@ static void toStream(std::ostream& out, const CommandSequence* c) { } } -static void toStream(std::ostream& out, const DeclarationCommand* c) { - const vector<string>& declaredSymbols = c->getDeclaredSymbols(); - Type declaredType = c->getDeclaredType(); - Assert(declaredSymbols.size() > 0); - copy( declaredSymbols.begin(), declaredSymbols.end() - 1, - ostream_iterator<string>(out, ", ") ); - out << declaredSymbols.back(); - out << " : " << declaredType << ";"; +static void toStream(std::ostream& out, const DeclarationSequence* c) { + DeclarationSequence::const_iterator i = c->begin(); + for(;;) { + DeclarationDefinitionCommand* dd = + static_cast<DeclarationDefinitionCommand*>(*i++); + if(i != c->end()) { + out << dd->getSymbol() << ", "; + } else { + out << *dd; + break; + } + } +} + +static void toStream(std::ostream& out, const DeclareFunctionCommand* c) { + out << c->getSymbol() << " : " << c->getType() << ";"; } static void toStream(std::ostream& out, const DefineFunctionCommand* c) { @@ -430,6 +476,22 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c) { out << "): " << formula << ";"; } +static void toStream(std::ostream& out, const DeclareTypeCommand* c) { + if(c->getArity() > 0) { + Unhandled("Don't know how to print parameterized type declaration " + "in CVC language:\n%s", c->toString().c_str()); + } + out << c->getSymbol() << " : TYPE;"; +} + +static void toStream(std::ostream& out, const DefineTypeCommand* c) { + if(c->getParameters().size() > 0) { + Unhandled("Don't know how to print parameterized type definition " + "in CVC language:\n%s", c->toString().c_str()); + } + out << c->getSymbol() << " : TYPE = " << c->getType() << ";"; +} + static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) { toStream(out, static_cast<const DefineFunctionCommand*>(c)); } @@ -484,6 +546,10 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) { } } +static void toStream(std::ostream& out, const CommentCommand* c) { + out << "% " << c->getComment(); +} + template <class T> static bool tryToStream(std::ostream& out, const Command* c) { if(typeid(*c) == typeid(T)) { diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h index d794c82e8..fd478dbe5 100644 --- a/src/printer/cvc/cvc_printer.h +++ b/src/printer/cvc/cvc_printer.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing |