diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-21 14:04:35 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-21 14:28:24 -0400 |
| commit | 16215e6e021c0fb24a6237126e17c89485dfc012 (patch) | |
| tree | 484f927a27af4d26c616d5982e0b0ce2497eaad7 /src/printer | |
| parent | 118e998b926870e817cd57c49b91fdb27948e828 (diff) | |
Some model and printing fixes for defined functions in input.
Diffstat (limited to 'src/printer')
| -rw-r--r-- | src/printer/ast/ast_printer.cpp | 2 | ||||
| -rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 2 | ||||
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 3239d5b85..42fe7801d 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -144,10 +144,10 @@ void AstPrinter::toStream(std::ostream& out, const Command* c, tryToStream<DeclarationSequence>(out, c) || tryToStream<CommandSequence>(out, c) || tryToStream<DeclareFunctionCommand>(out, c) || - tryToStream<DefineFunctionCommand>(out, c) || tryToStream<DeclareTypeCommand>(out, c) || tryToStream<DefineTypeCommand>(out, c) || tryToStream<DefineNamedFunctionCommand>(out, c) || + tryToStream<DefineFunctionCommand>(out, c) || tryToStream<SimplifyCommand>(out, c) || tryToStream<GetValueCommand>(out, c) || tryToStream<GetModelCommand>(out, c) || diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 0206c4252..2cfeaafc1 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -764,10 +764,10 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c, tryToStream<DeclarationSequence>(out, c) || tryToStream<CommandSequence>(out, c) || tryToStream<DeclareFunctionCommand>(out, c) || - tryToStream<DefineFunctionCommand>(out, c) || tryToStream<DeclareTypeCommand>(out, c) || tryToStream<DefineTypeCommand>(out, c) || tryToStream<DefineNamedFunctionCommand>(out, c) || + tryToStream<DefineFunctionCommand>(out, c) || tryToStream<SimplifyCommand>(out, c) || tryToStream<GetValueCommand>(out, c) || tryToStream<GetModelCommand>(out, c) || diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index ef4fd5fea..50cab3f53 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -506,10 +506,10 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c, tryToStream<QuitCommand>(out, c) || tryToStream<CommandSequence>(out, c) || tryToStream<DeclareFunctionCommand>(out, c) || - tryToStream<DefineFunctionCommand>(out, c) || tryToStream<DeclareTypeCommand>(out, c) || tryToStream<DefineTypeCommand>(out, c) || tryToStream<DefineNamedFunctionCommand>(out, c) || + tryToStream<DefineFunctionCommand>(out, c) || tryToStream<SimplifyCommand>(out, c) || tryToStream<GetValueCommand>(out, c) || tryToStream<GetModelCommand>(out, c) || |