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/smt2 | |
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/smt2')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 110 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.h | 2 |
2 files changed, 84 insertions, 28 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 5ce571904..5758b1101 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -23,6 +23,8 @@ #include <string> #include <typeinfo> +#include "util/boolean_simplification.h" + using namespace std; namespace CVC4 { @@ -64,6 +66,17 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, // constant if(n.getMetaKind() == kind::metakind::CONSTANT) { switch(n.getKind()) { + case kind::TYPE_CONSTANT: + switch(n.getConst<TypeConstant>()) { + case BOOLEAN_TYPE: out << "Boolean"; break; + case REAL_TYPE: out << "Real"; break; + case INTEGER_TYPE: out << "Int"; break; + default: + // fall back on whatever operator<< does on underlying type; we + // might luck out and be SMT-LIB v2 compliant + kind::metakind::NodeValueConstPrinter::toStream(out, n); + } + break; case kind::BITVECTOR_TYPE: out << "(_ BitVec " << n.getConst<BitVectorSize>().size << ")"; break; @@ -91,11 +104,20 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, return; } + if(n.getKind() == kind::SORT_TYPE) { + std::string name; + if(n.getAttribute(expr::VarNameAttr(), name)) { + out << name; + return; + } + } + bool stillNeedToPrintParams = true; // operator out << '('; switch(n.getKind()) { // builtin theory + case kind::APPLY: break; case kind::EQUAL: out << "= "; break; case kind::DISTINCT: out << "distinct "; break; case kind::TUPLE: break; @@ -111,7 +133,6 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, // uf theory case kind::APPLY_UF: break; - case kind::SORT_TYPE: break; // arith theory case kind::PLUS: out << "+ "; break; @@ -127,6 +148,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, // arrays theory case kind::SELECT: out << "select "; break; case kind::STORE: out << "store "; break; + case kind::ARRAY_TYPE: out << "Array "; break; // bv theory case kind::BITVECTOR_CONCAT: out << "concat "; break; @@ -253,8 +275,10 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c, tryToStream<QueryCommand>(out, c) || tryToStream<QuitCommand>(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) || @@ -266,7 +290,8 @@ void Smt2Printer::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; } @@ -289,13 +314,25 @@ static void toStream(std::ostream& out, const PopCommand* c) { static void toStream(std::ostream& out, const CheckSatCommand* c) { BoolExpr e = c->getExpr(); if(!e.isNull()) { - out << "(assert " << e << ")"; + out << PushCommand() << endl + << AssertCommand(e) << endl + << CheckSatCommand() << endl + << PopCommand() << endl; + } else { + out << "(check-sat)"; } - out << "(check-sat)"; } static void toStream(std::ostream& out, const QueryCommand* c) { - Unhandled("query command"); + BoolExpr e = c->getExpr(); + if(!e.isNull()) { + out << PushCommand() << endl + << AssertCommand(BooleanSimplification::negate(e)) << endl + << CheckSatCommand() << endl + << PopCommand() << endl; + } else { + out << "(check-sat)"; + } } static void toStream(std::ostream& out, const QuitCommand* c) { @@ -310,26 +347,21 @@ 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(); - for(vector<string>::const_iterator i = declaredSymbols.begin(); - i != declaredSymbols.end(); - ++i) { - if(declaredType.isFunction()) { - FunctionType ft = declaredType; - out << "(declare-fun " << *i << " ("; - const vector<Type> argTypes = ft.getArgTypes(); - if(argTypes.size() > 0) { - copy( argTypes.begin(), argTypes.end() - 1, - ostream_iterator<Type>(out, " ") ); - out << argTypes.back(); - } - out << ") " << ft.getRangeType() << ")"; - } else { - out << "(declare-fun " << *i << " () " << declaredType << ")"; +static void toStream(std::ostream& out, const DeclareFunctionCommand* c) { + Type type = c->getType(); + out << "(declare-fun " << c->getSymbol() << " ("; + if(type.isFunction()) { + FunctionType ft = type; + const vector<Type> argTypes = ft.getArgTypes(); + if(argTypes.size() > 0) { + copy( argTypes.begin(), argTypes.end() - 1, + ostream_iterator<Type>(out, " ") ); + out << argTypes.back(); } + type = ft.getRangeType(); } + + out << ") " << type << ")"; } static void toStream(std::ostream& out, const DefineFunctionCommand* c) { @@ -337,14 +369,34 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c) { const vector<Expr>& formals = c->getFormals(); Expr formula = c->getFormula(); out << "(define-fun " << func << " ("; - for(vector<Expr>::const_iterator i = formals.begin(); - i != formals.end(); - ++i) { + vector<Expr>::const_iterator i = formals.begin(); + for(;;) { out << "(" << (*i) << " " << (*i).getType() << ")"; + ++i; + if(i != formals.end()) { + out << " "; + } else { + break; + } } out << ") " << FunctionType(func.getType()).getRangeType() << " " << formula << ")"; } +static void toStream(std::ostream& out, const DeclareTypeCommand* c) { + out << "(declare-sort " << c->getSymbol() << " " << c->getArity() << ")"; +} + +static void toStream(std::ostream& out, const DefineTypeCommand* c) { + const vector<Type>& params = c->getParameters(); + out << "(define-sort " << c->getSymbol() << " ("; + if(params.size() > 0) { + copy( params.begin(), params.end() - 1, + ostream_iterator<Type>(out, " ") ); + out << params.back(); + } + out << ") " << c->getType() << ")"; +} + static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) { out << "DefineNamedFunction( "; toStream(out, static_cast<const DefineFunctionCommand*>(c)); @@ -406,6 +458,10 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) { Unhandled("datatype declaration command"); } +static void toStream(std::ostream& out, const CommentCommand* c) { + out << "(set-info :notes \"" << c->getComment() << "\")"; +} + template <class T> static bool tryToStream(std::ostream& out, const Command* c) { if(typeid(*c) == typeid(T)) { diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 4bae8a2e1..2086370ae 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_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 |