diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-07-20 13:28:01 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-07-20 13:28:01 -0500 |
commit | f827fb06c949d421fb32f6629c2c353ca7bd026e (patch) | |
tree | 04b3563aa2467784517193dd22ef95f2ce1e612a /src/printer | |
parent | daf2eca9a4bb32680cbf35945bb09cfd13be76a7 (diff) |
Infrastructure for storing and printing heap models for separation logic. Ensure value of sep.nil is correct in models. Print instantiations as sexprs.
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 4cdf5a9fb..7b7d569b7 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1068,6 +1068,15 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m) const throw() { while( std::getline( c, ln ) ){ out << "; " << ln << std::endl; } + //print the heap model, if it exists + Expr h, neq; + if( m.getHeapModel( h, neq ) ){ + // description of the heap+what nil is equal to fully describes model + out << "(heap" << endl; + out << h << endl; + out << neq << endl; + out << ")" << std::endl; + } //print the model out << "(model" << endl; this->Printer::toStream(out, m); |