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/theory/quantifiers_engine.cpp | |
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/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index da8233fc1..2975d2e70 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -1340,21 +1340,21 @@ void QuantifiersEngine::printInstantiations( std::ostream& out ) { for( BoolMap::iterator it = d_skolemized.begin(); it != d_skolemized.end(); ++it ){ Node q = (*it).first; printed = true; - out << "Skolem constants of " << q << " : " << std::endl; + out << "(skolem " << q << std::endl; out << " ( "; for( unsigned i=0; i<d_term_db->d_skolem_constants[q].size(); i++ ){ - if( i>0 ){ out << ", "; } + if( i>0 ){ out << " "; } out << d_term_db->d_skolem_constants[q][i]; } out << " )" << std::endl; - out << std::endl; + out << ")" << std::endl; } if( options::incrementalSolving() ){ for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){ bool firstTime = true; it->second->print( out, it->first, firstTime, useUnsatCore, active_lemmas ); if( !firstTime ){ - out << std::endl; + out << ")" << std::endl; } printed = printed || !firstTime; } @@ -1363,13 +1363,13 @@ void QuantifiersEngine::printInstantiations( std::ostream& out ) { bool firstTime = true; it->second.print( out, it->first, firstTime, useUnsatCore, active_lemmas ); if( !firstTime ){ - out << std::endl; + out << ")" << std::endl; } printed = printed || !firstTime; } } if( !printed ){ - out << "No instantiations." << std::endl; + out << "No instantiations" << std::endl; } } |