diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-02-24 16:37:46 -0600 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-02-24 16:37:46 -0600 |
commit | c71ec272d5ef58bfa147507bdbb370f2e288d154 (patch) | |
tree | 8bf3b84a476fa7fff798158e6b58697399c7b966 /src/printer/smt2 | |
parent | deb304550fbb6e19346319ec24d83e0650c64e91 (diff) |
added option --model-u-dt-enum for outputting uninterpreted sorts as datatype enumerations + minor update to array rewriter to improve output for this option, minor refactoring of representative selection for quantifier instantiation, initial draft of disequality propagation option --uf-ss-deq-prop, other refactoring of uf strong solver, fixed bug 496, improvement for fmf enumeration of finite built-in sorts
Diffstat (limited to 'src/printer/smt2')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 46 |
1 files changed, 32 insertions, 14 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 000fd2fbf..8541ca6ae 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -27,8 +27,10 @@ #include "theory/substitutions.h" #include "util/language.h" #include "smt/smt_engine.h" +#include "smt/options.h" #include "theory/model.h" +#include "theory/arrays/theory_arrays_rewriter.h" using namespace std; @@ -552,21 +554,30 @@ void Smt2Printer::toStream(std::ostream& out, Model& m, const Command* c) const theory::TheoryModel& tm = (theory::TheoryModel&) m; if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) { TypeNode tn = TypeNode::fromType( ((const 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.find(tn)).second.size() << std::endl; + if( options::modelUninterpDtEnum() && tn.isSort() && + tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){ + out << "(declare-datatypes () ((" << dynamic_cast<const DeclareTypeCommand*>(c)->getSymbol() << " "; + for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){ + out << "(" << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << ")"; } - } - 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.find(tn)).second.size(); i++ ){ - if( (*tm.d_rep_set.d_type_reps.find(tn)).second[i].isVar() ){ - out << "(declare-fun " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << " () " << tn << ")" << std::endl; - }else{ - out << "; rep: " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << std::endl; + out << ")))" << std::endl; + } else { + 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.find(tn)).second.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.find(tn)).second.size(); i++ ){ + if( (*tm.d_rep_set.d_type_reps.find(tn)).second[i].isVar() ){ + out << "(declare-fun " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << " () " << tn << ")" << std::endl; + }else{ + out << "; rep: " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << std::endl; + } } } } @@ -583,6 +594,13 @@ void Smt2Printer::toStream(std::ostream& out, Model& m, const Command* c) const << " " << n.getType().getRangeType() << " " << val[1] << ")" << std::endl; } else { + if( options::modelUninterpDtEnum() && val.getKind() == kind::STORE ) { + TypeNode tn = val[1].getType(); + if (tn.isSort() && tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){ + Cardinality indexCard((*tm.d_rep_set.d_type_reps.find(tn)).second.size()); + val = theory::arrays::TheoryArraysRewriter::normalizeConstant( val, indexCard ); + } + } out << "(define-fun " << n << " () " << n.getType() << " " << val << ")" << std::endl; } |