diff options
Diffstat (limited to 'src/printer/smt2/smt2_printer.cpp')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 89 |
1 files changed, 77 insertions, 12 deletions
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; } |