diff options
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/ast/ast_printer.cpp | 4 | ||||
-rw-r--r-- | src/printer/ast/ast_printer.h | 2 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 83 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.h | 2 | ||||
-rw-r--r-- | src/printer/dagification_visitor.cpp | 1 | ||||
-rw-r--r-- | src/printer/printer.cpp | 6 | ||||
-rw-r--r-- | src/printer/printer.h | 8 | ||||
-rw-r--r-- | src/printer/smt/smt_printer.cpp | 4 | ||||
-rw-r--r-- | src/printer/smt/smt_printer.h | 2 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 89 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.h | 2 |
11 files changed, 189 insertions, 14 deletions
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 50bd5016d..39d76728a 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -186,6 +186,10 @@ void AstPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw }/* AstPrinter::toStream(CommandStatus*) */ +void AstPrinter::toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(){ + +} + static void toStream(std::ostream& out, const EmptyCommand* c) throw() { out << "EmptyCommand(" << c->getName() << ")"; } diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h index 4dfb2c0d5..1cac966df 100644 --- a/src/printer/ast/ast_printer.h +++ b/src/printer/ast/ast_printer.h @@ -35,6 +35,8 @@ public: void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const CommandStatus* s) const throw(); + //for models + void toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(); };/* class AstPrinter */ }/* CVC4::printer::ast namespace */ diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 6a709b833..5803ad23f 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -23,6 +23,8 @@ #include "expr/command.h" #include "theory/substitutions.h" +#include "theory/model.h" + #include <iostream> #include <vector> #include <string> @@ -500,7 +502,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo out << BitVectorType(n.getType().toType()).getSize(); out << ','; toStream(out, n[child], depth, types, false); - out << ','; + out << ','; toStream(out, n[child+1], depth, types, false); while (child > 0) { out << ')'; @@ -537,7 +539,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo out << BitVectorType(n.getType().toType()).getSize(); out << ','; toStream(out, n[child], depth, types, false); - out << ','; + out << ','; toStream(out, n[child+1], depth, types, false); while (child > 0) { out << ')'; @@ -729,6 +731,83 @@ void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw }/* CvcPrinter::toStream(CommandStatus*) */ +void CvcPrinter::toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(){ + theory::TheoryModel* tm = (theory::TheoryModel*)m; + if( c_type==Model::COMMAND_DECLARE_SORT ){ + TypeNode tn = TypeNode::fromType( ((DeclareTypeCommand*)c)->getType() ); + if( tn.isSort() ){ + //print the cardinality + if( tm->d_rep_set.d_type_reps.find( tn )!=tm->d_rep_set.d_type_reps.end() ){ + out << "; cardinality of " << tn << " is " << tm->d_rep_set.d_type_reps[tn].size() << std::endl; + } + } + out << c << std::endl; + if( tn.isSort() ){ + //print the representatives + if( tm->d_rep_set.d_type_reps.find( tn )!=tm->d_rep_set.d_type_reps.end() ){ + for( size_t i=0; i<tm->d_rep_set.d_type_reps[tn].size(); i++ ){ + if( tm->d_rep_set.d_type_reps[tn][i].isVar() ){ + out << tm->d_rep_set.d_type_reps[tn][i] << " : " << tn << ";" << std::endl; + }else{ + out << "% rep: " << tm->d_rep_set.d_type_reps[tn][i] << std::endl; + } + } + } + } + }else if( c_type==Model::COMMAND_DECLARE_FUN ){ + Node n = Node::fromExpr( ((DeclareFunctionCommand*)c)->getFunction() ); + TypeNode tn = n.getType(); + out << n << " : "; + if( tn.isFunction() || tn.isPredicate() ){ + out << "("; + for( size_t i=0; i<tn.getNumChildren()-1; i++ ){ + if( i>0 ) out << ", "; + out << tn[i]; + } + out << ") -> " << tn.getRangeType(); + }else{ + out << tn; + } + out << " = "; + if( tn.isFunction() || tn.isPredicate() ){ + out << "LAMBDA ("; + for( size_t i=0; i<tn.getNumChildren()-1; i++ ){ + if( i>0 ) out << ", "; + out << "$x" << (i+1) << " : " << tn[i]; + } + out << "): "; + } + out << tm->getValue( n ); + out << ";" << std::endl; + +/* + //for table format (work in progress) + bool printedModel = false; + if( tn.isFunction() ){ + if( options::modelFormatMode()==MODEL_FORMAT_MODE_TABLE ){ + //specialized table format for functions + RepSetIterator riter( &d_rep_set ); + riter.setFunctionDomain( n ); + while( !riter.isFinished() ){ + std::vector< Node > children; + children.push_back( n ); + for( int i=0; i<riter.getNumTerms(); i++ ){ + children.push_back( riter.getTerm( i ) ); + } + Node nn = NodeManager::currentNM()->mkNode( APPLY_UF, children ); + Node val = getValue( nn ); + out << val << " "; + riter.increment(); + } + printedModel = true; + } + } +*/ + }else{ + out << c << std::endl; + } +} + static void toStream(std::ostream& out, const AssertCommand* c) throw() { out << "ASSERT " << c->getExpr() << ";"; } diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h index 7fb611a79..c868025ef 100644 --- a/src/printer/cvc/cvc_printer.h +++ b/src/printer/cvc/cvc_printer.h @@ -38,6 +38,8 @@ public: void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const CommandStatus* s) const throw(); + //for models + void toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(); };/* class CvcPrinter */ }/* CVC4::printer::cvc namespace */ diff --git a/src/printer/dagification_visitor.cpp b/src/printer/dagification_visitor.cpp index cb56c3430..40b532612 100644 --- a/src/printer/dagification_visitor.cpp +++ b/src/printer/dagification_visitor.cpp @@ -55,6 +55,7 @@ bool DagificationVisitor::alreadyVisited(TNode current, TNode parent) { // increment again (they'll be dagified anyway). return current.isVar() || current.getMetaKind() == kind::metakind::CONSTANT || + current.getNumChildren()==0 || ( ( current.getKind() == kind::NOT || current.getKind() == kind::UMINUS ) && ( current[0].isVar() || diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 0881b814b..24baafa14 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -127,4 +127,10 @@ void Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() { } }/* Printer::toStream() */ +void Printer::toStream(std::ostream& out, Model* m ) const throw(){ + for( int i=0; i<m->getNumCommands(); i++ ){ + toStream( out, m, m->getCommand( i ), m->getCommandType( i ) ); + } +} + }/* CVC4 namespace */ diff --git a/src/printer/printer.h b/src/printer/printer.h index e3b1d6f40..6fedc854c 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -23,6 +23,7 @@ #include "util/language.h" #include "util/sexpr.h" +#include "util/model.h" #include "expr/node.h" #include "expr/command.h" @@ -76,6 +77,13 @@ public: */ virtual void toStream(std::ostream& out, const Result& r) const throw(); + /** Write a Model out to a stream with this Printer. */ + virtual void toStream(std::ostream& out, Model* m ) const throw(); + + //for models + + /** write model response to command */ + virtual void toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw() = 0; };/* class Printer */ }/* CVC4 namespace */ diff --git a/src/printer/smt/smt_printer.cpp b/src/printer/smt/smt_printer.cpp index fa46523a4..14a680a1e 100644 --- a/src/printer/smt/smt_printer.cpp +++ b/src/printer/smt/smt_printer.cpp @@ -51,6 +51,10 @@ void SmtPrinter::toStream(std::ostream& out, const SExpr& sexpr) const throw() { Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr); }/* SmtPrinter::toStream() */ +void SmtPrinter::toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(){ + Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, m, c, c_type); +} + }/* CVC4::printer::smt namespace */ }/* CVC4::printer namespace */ }/* CVC4 namespace */ diff --git a/src/printer/smt/smt_printer.h b/src/printer/smt/smt_printer.h index 6e1c607bf..1cf7fcf50 100644 --- a/src/printer/smt/smt_printer.h +++ b/src/printer/smt/smt_printer.h @@ -35,6 +35,8 @@ public: void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const CommandStatus* s) const throw(); void toStream(std::ostream& out, const SExpr& sexpr) const throw(); + //for models + void toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(); };/* class SmtPrinter */ }/* CVC4::printer::smt namespace */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index ed8648c47..9400b7732 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -29,6 +29,8 @@ #include "theory/substitutions.h" #include "util/language.h" +#include "theory/model.h" + using namespace std; namespace CVC4 { @@ -306,14 +308,6 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, // TODO user patterns break; - //function models - case kind::FUNCTION_MODEL: - break; - case kind::FUNCTION_CASE_SPLIT: - break; - case kind::FUNCTION_CASE: - out << "if "; - break; default: // fall back on however the kind prints itself; this probably // won't be SMT-LIB v2 compliant, but it will be clear from the @@ -526,6 +520,76 @@ void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const thro }/* Smt2Printer::toStream(CommandStatus*) */ + +void Smt2Printer::toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(){ + theory::TheoryModel* tm = (theory::TheoryModel*)m; + if( c_type==Model::COMMAND_DECLARE_SORT ){ + TypeNode tn = TypeNode::fromType( ((DeclareTypeCommand*)c)->getType() ); + if( tn.isSort() ){ + //print the cardinality + if( tm->d_rep_set.d_type_reps.find( tn )!=tm->d_rep_set.d_type_reps.end() ){ + out << "; cardinality of " << tn << " is " << tm->d_rep_set.d_type_reps[tn].size() << std::endl; + } + } + out << c << std::endl; + if( tn.isSort() ){ + //print the representatives + if( tm->d_rep_set.d_type_reps.find( tn )!=tm->d_rep_set.d_type_reps.end() ){ + for( size_t i=0; i<tm->d_rep_set.d_type_reps[tn].size(); i++ ){ + if( tm->d_rep_set.d_type_reps[tn][i].isVar() ){ + out << "(declare-fun " << tm->d_rep_set.d_type_reps[tn][i] << " () " << tn << ")" << std::endl; + }else{ + out << "; rep: " << tm->d_rep_set.d_type_reps[tn][i] << std::endl; + } + } + } + } + }else if( c_type==Model::COMMAND_DECLARE_FUN ){ + Node n = Node::fromExpr( ((DeclareFunctionCommand*)c)->getFunction() ); + TypeNode tn = n.getType(); + out << "(define-fun " << n << " ("; + if( tn.isFunction() || tn.isPredicate() ){ + for( size_t i=0; i<tn.getNumChildren()-1; i++ ){ + if( i>0 ) out << " "; + out << "($x" << (i+1) << " " << tn[i] << ")"; + } + out << ") " << tn.getRangeType(); + }else{ + out << ") " << tn; + } + out << " "; + out << tm->getValue( n ); + out << ")" << std::endl; + +/* + //for table format (work in progress) + bool printedModel = false; + if( tn.isFunction() ){ + if( options::modelFormatMode()==MODEL_FORMAT_MODE_TABLE ){ + //specialized table format for functions + RepSetIterator riter( &d_rep_set ); + riter.setFunctionDomain( n ); + while( !riter.isFinished() ){ + std::vector< Node > children; + children.push_back( n ); + for( int i=0; i<riter.getNumTerms(); i++ ){ + children.push_back( riter.getTerm( i ) ); + } + Node nn = NodeManager::currentNM()->mkNode( APPLY_UF, children ); + Node val = getValue( nn ); + out << val << " "; + riter.increment(); + } + printedModel = true; + } + } +*/ + }else{ + out << c << std::endl; + } +} + + static void toStream(std::ostream& out, const AssertCommand* c) throw() { out << "(assert " << c->getExpr() << ")"; } @@ -687,7 +751,7 @@ static void toStream(std::ostream& out, const GetOptionCommand* c) throw() { static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) throw() { const vector<DatatypeType>& datatypes = c->getDatatypes(); - out << "(declare-datatypes ("; + out << "(declare-datatypes () ("; for(vector<DatatypeType>::const_iterator i = datatypes.begin(), i_end = datatypes.end(); i != i_end; @@ -698,14 +762,15 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) thr out << "(" << d.getName() << " "; for(Datatype::const_iterator ctor = d.begin(), ctor_end = d.end(); ctor != ctor_end; ++ctor){ - out << "(" << ctor->getName() << " "; + if( ctor!=d.begin() ) out << " "; + out << "(" << ctor->getName(); for(DatatypeConstructor::const_iterator arg = ctor->begin(), arg_end = ctor->end(); arg != arg_end; ++arg){ - out << "(" << arg->getSelector() << " " + out << " (" << arg->getSelector() << " " << static_cast<SelectorType>(arg->getType()).getRangeType() << ")"; } - out << ") "; + out << ")"; } out << ")" << endl; } diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index fd65a1efa..30c0ce647 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -35,6 +35,8 @@ public: void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const CommandStatus* s) const throw(); + //for models + void toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(); };/* class Smt2Printer */ }/* CVC4::printer::smt2 namespace */ |