summaryrefslogtreecommitdiff
path: root/src/printer
diff options
context:
space:
mode:
Diffstat (limited to 'src/printer')
-rw-r--r--src/printer/ast/ast_printer.cpp4
-rw-r--r--src/printer/ast/ast_printer.h2
-rw-r--r--src/printer/cvc/cvc_printer.cpp83
-rw-r--r--src/printer/cvc/cvc_printer.h2
-rw-r--r--src/printer/dagification_visitor.cpp1
-rw-r--r--src/printer/printer.cpp6
-rw-r--r--src/printer/printer.h8
-rw-r--r--src/printer/smt/smt_printer.cpp4
-rw-r--r--src/printer/smt/smt_printer.h2
-rw-r--r--src/printer/smt2/smt2_printer.cpp89
-rw-r--r--src/printer/smt2/smt2_printer.h2
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback