From edd8886e56c8bb84f3fd85fc6f697d870bc0a3b7 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 26 Jan 2015 13:11:01 +0100
Subject: Output solutions for synthesis conjectures with --dump-synth.  Minor
 refactor of previous commit.

---
 src/theory/theory_engine.cpp | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'src/theory/theory_engine.cpp')

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;
-- 
cgit v1.2.3