diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-26 13:11:01 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-26 13:11:01 +0100 |
commit | edd8886e56c8bb84f3fd85fc6f697d870bc0a3b7 (patch) | |
tree | 1fe3e8699f3c4831a302a369b377396ae5a347a4 /src/theory/theory_engine.cpp | |
parent | f3045ccce9d30114f6e90cfa72de176da344cb1f (diff) |
Output solutions for synthesis conjectures with --dump-synth. Minor refactor of previous commit.
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 22bf37470..74a8fab73 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1224,6 +1224,14 @@ void TheoryEngine::printInstantiations( std::ostream& out ) { } } +void TheoryEngine::printSynthSolution( std::ostream& out ) { + if( d_quantEngine ){ + d_quantEngine->printSynthSolution( out ); + }else{ + out << "Internal error : synth solution not available when quantifiers are not present." << std::endl; + } +} + static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) { std::set<TNode> all; |