Add interface in sygus to get synthesis solution Nodes (#1552)

1 files changed, 17 insertions, 3 deletions

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index b54ce4805..dc359d252 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -310,14 +310,28 @@ void CegInstantiation::getCRefEvaluationLemmas( CegConjecture * conj, std::vecto
 }
 
 void CegInstantiation::printSynthSolution( std::ostream& out ) {
-  if( d_conj->isAssigned() ){
-    // print the conjecture
+  if( d_conj->isAssigned() )
+  {
     d_conj->printSynthSolution( out, d_last_inst_si );
-  }else{
+  }
+  else
+  {
     Assert( false );
   }
 }
 
+void CegInstantiation::getSynthSolutions(std::map<Node, Node>& sol_map)
+{
+  if (d_conj->isAssigned())
+  {
+    d_conj->getSynthSolutions(sol_map, d_last_inst_si);
+  }
+  else
+  {
+    Assert(false);
+  }
+}
+
 void CegInstantiation::preregisterAssertion( Node n ) {
   //check if it sygus conjecture
   if( QuantAttributes::checkSygusConjecture( n ) ){