(self, outstream=None, printer=None, daggify=True)
Serializes the SmtLibCommand into outstream using the given printer.

        Exactly one of outstream or printer must be specified. When
        specifying the printer, the associated outstream will be used.
        If printer is not specified, daggify controls the printer to
        be created. If true a daggified formula is produced, otherwise
        a tree printing is done.
Serializes the SmtLibCommand into outstream using the given printer.
Serializes the SmtLibCommand into outstream using the given printer .
def serialize(self, outstream=None, printer=None, daggify=True):
        """Serializes the SmtLibCommand into outstream using the given printer.

        Exactly one of outstream or printer must be specified. When
        specifying the printer, the associated outstream will be used.
        If printer is not specified, daggify controls the printer to
        be created. If true a daggified formula is produced, otherwise
        a tree printing is done.

        """

        if (outstream is None) and (printer is not None):
            outstream = printer.stream
        elif (outstream is not None) and (printer is None):
            if daggify:
                printer = SmtDagPrinter(outstream)
            else:
                printer = SmtPrinter(outstream)
        else:
            assert (outstream is not None and printer is not None) or \
                   (outstream is None and printer is None), \
                   "Exactly one of outstream and printer must be set."

        if self.name == smtcmd.SET_OPTION:
            outstream.write("(%s %s %s)" % (self.name,self.args[0],self.args[1]))

        elif self.name == smtcmd.SET_INFO:
            outstream.write("(%s %s %s)" % (self.name,self.args[0],
                                            quote(self.args[1])))

        elif self.name == smtcmd.ASSERT:
            outstream.write("(%s " % self.name)
            printer.printer(self.args[0])
            outstream.write(")")

        elif self.name == smtcmd.GET_VALUE:
            outstream.write("(%s (" % self.name)
            for a in self.args:
                printer.printer(a)
                outstream.write(" ")
            outstream.write("))")

        elif self.name in [smtcmd.CHECK_SAT, smtcmd.EXIT,
                           smtcmd.RESET_ASSERTIONS, smtcmd.GET_UNSAT_CORE,
                           smtcmd.GET_ASSIGNMENT, smtcmd.GET_MODEL]:
            outstream.write("(%s)" % self.name)

        elif self.name == smtcmd.SET_LOGIC:
            outstream.write("(%s %s)" % (self.name, self.args[0]))

        elif self.name in [smtcmd.DECLARE_FUN, smtcmd.DECLARE_CONST]:
            symbol = self.args[0]
            type_str = symbol.symbol_type().as_smtlib()
            outstream.write("(%s %s %s)" % (self.name,
                                            quote(symbol.symbol_name()),
                                            type_str))

        elif self.name == smtcmd.DEFINE_FUN:
            name = self.args[0]
            params_list = self.args[1]
            params = " ".join(["(%s %s)" % (v, v.symbol_type()) for v in params_list])
            rtype = self.args[2]
            expr = self.args[3]
            outstream.write("(%s %s (%s) %s " % (self.name,
                                                name,
                                                params,
                                                rtype))
            printer.printer(expr)
            outstream.write(")")

        elif self.name in [smtcmd.PUSH, smtcmd.POP]:
            outstream.write("(%s %d)" % (self.name, self.args[0]))

        elif self.name == smtcmd.DEFINE_SORT:
            name = self.args[0]
            params_list = self.args[1]
            params = " ".join(params_list)
            rtype = self.args[2]
            outstream.write("(%s %s (%s) %s)" % (self.name,
                                                 name,
                                                 params,
                                                 rtype))
        elif self.name == smtcmd.DECLARE_SORT:
            type_decl = self.args[0]
            outstream.write("(%s %s %d)" % (self.name,
                                            type_decl.name,
                                            type_decl.arity))

        elif self.name in smtcmd.ALL_COMMANDS:
            raise NotImplementedError("'%s' is a valid SMT-LIB command "\
                                      "but it is currently not supported. "\
                                      "Please open a bug-report." % self.name)
        else:
            raise UnknownSmtLibCommandError(self.name)
def serialize ( self , outstream = None , printer = None , daggify = True ) : if ( outstream is None ) and ( printer is not None ) : outstream = printer . stream elif ( outstream is not None ) and ( printer is None ) : if daggify : printer = SmtDagPrinter ( outstream ) else : printer = SmtPrinter ( outstream ) else : assert ( outstream is not None and printer is not None ) or ( outstream is None and printer is None ) , "Exactly one of outstream and printer must be set." if self . name == smtcmd . SET_OPTION : outstream . write ( "(%s %s %s)" % ( self . name , self . args [ 0 ] , self . args [ 1 ] ) ) elif self . name == smtcmd . SET_INFO : outstream . write ( "(%s %s %s)" % ( self . name , self . args [ 0 ] , quote ( self . args [ 1 ] ) ) ) elif self . name == smtcmd . ASSERT : outstream . write ( "(%s " % self . name ) printer . printer ( self . args [ 0 ] ) outstream . write ( ")" ) elif self . name == smtcmd . GET_VALUE : outstream . write ( "(%s (" % self . name ) for a in self . args : printer . printer ( a ) outstream . write ( " " ) outstream . write ( "))" ) elif self . name in [ smtcmd . CHECK_SAT , smtcmd . EXIT , smtcmd . RESET_ASSERTIONS , smtcmd . GET_UNSAT_CORE , smtcmd . GET_ASSIGNMENT , smtcmd . GET_MODEL ] : outstream . write ( "(%s)" % self . name ) elif self . name == smtcmd . SET_LOGIC : outstream . write ( "(%s %s)" % ( self . name , self . args [ 0 ] ) ) elif self . name in [ smtcmd . DECLARE_FUN , smtcmd . DECLARE_CONST ] : symbol = self . args [ 0 ] type_str = symbol . symbol_type ( ) . as_smtlib ( ) outstream . write ( "(%s %s %s)" % ( self . name , quote ( symbol . symbol_name ( ) ) , type_str ) ) elif self . name == smtcmd . DEFINE_FUN : name = self . args [ 0 ] params_list = self . args [ 1 ] params = " " . join ( [ "(%s %s)" % ( v , v . symbol_type ( ) ) for v in params_list ] ) rtype = self . args [ 2 ] expr = self . args [ 3 ] outstream . write ( "(%s %s (%s) %s " % ( self . name , name , params , rtype ) ) printer . printer ( expr ) outstream . write ( ")" ) elif self . name in [ smtcmd . PUSH , smtcmd . POP ] : outstream . write ( "(%s %d)" % ( self . name , self . args [ 0 ] ) ) elif self . name == smtcmd . DEFINE_SORT : name = self . args [ 0 ] params_list = self . args [ 1 ] params = " " . join ( params_list ) rtype = self . args [ 2 ] outstream . write ( "(%s %s (%s) %s)" % ( self . name , name , params , rtype ) ) elif self . name == smtcmd . DECLARE_SORT : type_decl = self . args [ 0 ] outstream . write ( "(%s %s %d)" % ( self . name , type_decl . name , type_decl . arity ) ) elif self . name in smtcmd . ALL_COMMANDS : raise NotImplementedError ( "'%s' is a valid SMT-LIB command " "but it is currently not supported. " "Please open a bug-report." % self . name ) else : raise UnknownSmtLibCommandError ( self . name )