"""
This is the template for extracting the solution for the computation problem of computing
real solution of a polynomial system of equations RR from the output of the computer
algebra system Z3.

.. moduleauthor:: Albert Heinle <albert.heinle@uwaterloo.ca>
"""

import xml.dom.minidom as dom
import re

#--------------------------------------------------
#---------------The template-----------------------
#--------------------------------------------------

def extractSolution(outpString):
    """
    This function extracts the real solutions of a polynomial system
    computed by Z3, using the executable code that was
    generated by the template in the same folder on a certain
    instance.

    It returns a string representation of the solution in XML-format.
    The XML-string will be given as follows::

      <SOL_R_poly_sys_SOL>
        <satisfiable>0 or 1, depending on true or not</satisfiable>
      </SOL_R_poly_sys_SOL>

    If there is no solution given, or something is wrong with the given string,
    a ValueError is raised.

    :param outpString: The String that was returned by the Z3-execution
    :type  outpString: str
    :returns: XML-Representation of the solution.
    :rtype: str
    :raises: ValueError
    """
    if (type(outpString) != str):
        raise ValueError("Wrong Type of argument. String type expected.")
    solBeginStr = "=====Solution Begin====="
    solEndStr   = "=====Solution End====="
    solBeginPos = outpString.index(solBeginStr) + len(solBeginStr)
    solEndStrPos   = outpString.index(solEndStr)
    solStr = outpString[solBeginPos:solEndStrPos].strip()
    if (solStr == "" and (solStr!="sat" or solStr!="unsat")):
        raise ValueError("Output is empty.")
    #From here on, we can assume that we are dealing with a valid
    #string.
    #Construction of the XML-Document
    result = dom.Document()
    result.appendChild(result.createElement("SOL_R_poly_sys_SOL"))
    tempNode = result.firstChild
    #Adding the basis
    tempNodeSolutions = tempNode.appendChild(result.createElement("satisfiable"))
    if solStr == "sat":
        tempNodeSolutions.appendChild(result.createTextNode("1"))
    else:
        tempNodeSolutions.appendChild(result.createTextNode("0"))
    return result.toprettyxml("  ")

#--------------------------------------------------
#----------------Help Functions--------------------
#--------------------------------------------------
