class TestParserExtensibility(TestCase):

    def setUp(self):
        self.ts_parser = TSSmtLibParser()
        self.smt_parser = SmtLibParser()

    def test_wrong(self):
        txt = """
        (declare-fun A () Bool)
        (declare-fun B () Bool)
        (assert (and A B))
        (check-sat)
        (exit)
        """
        with self.assertRaises(UnknownSmtLibCommandError):
            self.ts_parser.get_ts(cStringIO(txt))
        script = self.smt_parser.get_script(cStringIO(txt))
        self.assertIsNotNone(script)

    def test_basic(self):
        txt = """
        (declare-fun A () Bool)
        (declare-fun B () Bool)
        (init (and A B))
        (trans (=> A (next A)))
        (exit)
        """
        with self.assertRaises(UnknownSmtLibCommandError):
            self.smt_parser.get_script(cStringIO(txt))
        ts = self.ts_parser.get_ts(cStringIO(txt))
        self.assertIsNotNone(ts)

 def parse(self, file_id):
     fname = SMTLIB_FILE_PATTERN % file_id
     reset_env()
     parser = SmtLibParser()
     script = parser.get_script_fname(fname)
     self.assertIsNotNone(script)
     return script

 def test_parse_bvconst_width(self):
     smtlib_input = "(assert (> #x10 #x10))"
     parser = SmtLibParser()
     buffer_ = cStringIO(smtlib_input)
     expr = parser.get_script(buffer_).get_last_formula()
     const = expr.args()[0]
     self.assertEqual(const.bv_width(), 8, const.bv_width())

    def test_dumped_logic(self):
        # Dumped logic matches the logic in the example
        fs = get_example_formulae()

        for (f_out, _, _, logic) in fs:
            buf_out = cStringIO()
            script_out = smtlibscript_from_formula(f_out)
            script_out.serialize(outstream=buf_out)

            buf_in = cStringIO(buf_out.getvalue())
            parser = SmtLibParser()
            script_in = parser.get_script(buf_in)
            for cmd in script_in:
                if cmd.name == "set-logic":
                    logic_in = cmd.args[0]
                    if logic == logics.QF_BOOL:
                        self.assertEqual(logic_in, logics.QF_UF)
                    elif logic == logics.BOOL:
                        self.assertEqual(logic_in, logics.LRA)
                    else:
                        self.assertEqual(logic_in, logic, script_in)
                    break
            else: # Loops exited normally
                print("-"*40)
                print(script_in)

    def __init__(self, env=None, interactive=False):
        SmtLibParser.__init__(self, env, interactive)

        # Add new commands
        #
        # The mapping function takes care of consuming the command
        # name from the input stream, e.g., '(init' . Therefore,
        # _cmd_init will receive the rest of the stream, in our
        # example, '(and A B)) ...'
        self.commands["init"] = self._cmd_init
        self.commands["trans"] = self._cmd_trans

        # Remove unused commands
        #
        # If some commands are not compatible with the extension, they
        # can be removed from the parser. If found, they will cause
        # the raising of the exception UnknownSmtLibCommandError
        del self.commands["check-sat"]
        del self.commands["get-value"]
        # ...

        # Add 'next' function
        #
        # New operators can be added similarly as done for commands.
        # e.g., 'next'. The helper function _operator_adapter,
        # simplifies the writing of such extensions.  In this example,
        # we will rewrite the content of the next without the need of
        # introducing a new pySMT operator. If you are interested in a
        # simple way of handling new operators in pySMT see
        # pysmt.test.test_dwf.
        self.interpreted["next"] = self._operator_adapter(self._next_var)

 def test_define_funs_arg_and_fun(self):
     smtlib_script = "\n".join(['(define-fun f ((n Int)) Int n)', '(declare-fun n () Real)'])
     stream = cStringIO(smtlib_script)
     parser = SmtLibParser()
     _ = parser.get_script(stream)
     # No exceptions are thrown
     self.assertTrue(True)

 def test_smtlib_define_fun_serialization(self):
     smtlib_input = "(define-fun init ((x Bool)) Bool (and x (and x (and x (and x (and x (and x x)))))))"
     parser = SmtLibParser()
     buffer_ = cStringIO(smtlib_input)
     s = parser.get_script(buffer_)
     for c in s:
         res = c.serialize_to_string(daggify=False)
     self.assertEqual(res.replace('__x0', 'x'), smtlib_input)

 def test_define_funs_same_args(self):
     # n is defined once as an Int and once as a Real
     smtlib_script = "\n".join(['(define-fun f ((n Int)) Int n)', '(define-fun f ((n Real)) Real n)'])
     stream = cStringIO(smtlib_script)
     parser = SmtLibParser()
     _ = parser.get_script(stream)
     # No exceptions are thrown
     self.assertTrue(True)

 def test_parse_declare_const(self):
     smtlib_input = """
     (declare-const s Int)
     (check-sat)"""
     parser = SmtLibParser()
     buffer_ = cStringIO(smtlib_input)
     script = parser.get_script(buffer_)
     self.assertIsNotNone(script)

    def smtlib_solver(self, stream):
        smt_parser = SmtLibParser()
        name = self.args.solver
        if name == "auto":
            solver = Solver()
        else:
            solver = Solver(name=name)

        for cmd in smt_parser.get_command_generator(stream):
            r = evaluate_command(cmd, solver)
            self.print_result(cmd, r)

    def test_complex_annotations_values(self):
        source ="""\
(declare-fun |"v__AT0"| () Bool)
(define-fun .def_1 () Bool (! |"v__AT0"| :next (+ 1     meaningless)))
"""
        buf = StringIO(source)
        parser = SmtLibParser()
        script = parser.get_script(buf)
        ann = script.annotations
        v0 = self.env.formula_manager.get_symbol('"v__AT0"')
        v1_str = next(iter(ann[v0]["next"]))
        self.assertEquals(v1_str, "(+ 1     meaningless)")

 def test_parse_exception(self):
     from pysmt.exceptions import PysmtSyntaxError
     smtlib_input = "(declare-const x x x Int)" +\
                    "(check-sat)"
     parser = SmtLibParser()
     buffer_ = cStringIO(smtlib_input)
     try:
         parser.get_script(buffer_)
         self.assertFalse(True)
     except PysmtSyntaxError as ex:
         self.assertEqual(ex.pos_info[0], 0)
         self.assertEqual(ex.pos_info[1], 19)

    def test_annotations_colon_values(self):
        source ="""\
(declare-fun |"v__AT0"| () Bool)
(define-fun .def_1 () Bool (! |"v__AT0"| :next :this_is_considered_a_value))
"""
        buf = StringIO(source)
        parser = SmtLibParser()
        script = parser.get_script(buf)
        ann = script.annotations
        v0 = self.env.formula_manager.get_symbol('"v__AT0"')
        v1_str = next(iter(ann[v0]["next"]))
        self.assertEquals(v1_str, ":this_is_considered_a_value")

    def test_all_parsing(self):
        # Create a small file that tests all commands of smt-lib 2
        parser = SmtLibParser()

        nie = 0
        for cmd in DEMO_SMTSCRIPT:
            try:
                next(parser.get_command_generator(cStringIO(cmd)))
            except NotImplementedError:
                nie += 1
        # There are currently 3 not-implemented commands
        self.assertEquals(nie, 3)

    def test_string_constant_quote_escaping_parsing(self):
        script = """
        (declare-const x String)
        (assert (= x "a""b"))
        (assert (= x "\"\""))
        (assert (= x "\"\"\"\""))
        """

        p = SmtLibParser()
        buffer = cStringIO(script)
        s = p.get_script(buffer)
        self.assertEqual('a"b', s.commands[1].args[0].arg(1).constant_value())
        self.assertEqual('"', s.commands[2].args[0].arg(1).constant_value())
        self.assertEqual('""', s.commands[3].args[0].arg(1).constant_value())

    def __init__(self, env=None, interactive=False):
        SmtLibParser.__init__(self, env, interactive)

        # Add new commands
        self.commands["init"] = self._cmd_init
        self.commands["trans"] = self._cmd_trans

        # Remove unused commands
        del self.commands["check-sat"]
        del self.commands["get-value"]
        # ...

        # Add 'next' function
        self.interpreted["next"] = self._operator_adapter(self._next_var)

    def test_interpreting_annotations(self):
        source ="""\
(declare-fun |"v__AT0"| () Bool)
(declare-fun |"v__AT1"| () Bool)
(define-fun .def_1 () Bool (! |"v__AT0"| :next |"v__AT1"|))
"""
        buf = StringIO(source)
        parser = SmtLibParser()
        script = parser.get_script(buf)
        ann = script.annotations
        v0 = self.env.formula_manager.get_symbol('"v__AT0"')
        v1_str = next(iter(ann[v0]["next"]))
        self.env.formula_manager.get_symbol(v1_str)
        self.assertEquals(v1_str, '"v__AT1"')

    def test_parse_examples_daggified_bv(self):
        fs = get_example_formulae()

        for (f_out, _, _, logic) in fs:
            if logic != logics.QF_BV:
                # See test_parse_examples_daggified
                continue
            buf_out = cStringIO()
            script_out = smtlibscript_from_formula(f_out)
            script_out.serialize(outstream=buf_out, daggify=True)
            buf_in = cStringIO(buf_out.getvalue())
            parser = SmtLibParser()
            script_in = parser.get_script(buf_in)
            f_in = script_in.get_last_formula()
            self.assertValid(Iff(f_in, f_out), f_in.serialize())

    def __init__(self, args, environment, logic, LOGICS=None, **options):
        Solver.__init__(self,
                        environment,
                        logic=logic,
                        **options)
        self.to = self.environment.typeso
        if LOGICS is not None: self.LOGICS = LOGICS
        self.args = args
        self.declared_vars = set()
        self.declared_sorts = set()
        self.solver = Popen(args, stdout=PIPE, stderr=PIPE, stdin=PIPE,
                            bufsize=-1)
        # Give time to the process to start-up
        time.sleep(0.01)
        self.parser = SmtLibParser(interactive=True)
        if PY2:
            self.solver_stdin = self.solver.stdin
            self.solver_stdout = self.solver.stdout
        else:
            self.solver_stdin = TextIOWrapper(self.solver.stdin)
            self.solver_stdout = TextIOWrapper(self.solver.stdout)

        # Initialize solver
        self.options(self)
        self.set_logic(logic)

    def test_parse_examples(self):
        fs = get_example_formulae()

        for (f_out, _, _, logic) in fs:
            if logic == logics.QF_BV:
                # See test_parse_examples_bv
                continue
            buf_out = cStringIO()
            script_out = smtlibscript_from_formula(f_out)
            script_out.serialize(outstream=buf_out)

            buf_in = cStringIO(buf_out.getvalue())
            parser = SmtLibParser()
            script_in = parser.get_script(buf_in)
            f_in = script_in.get_last_formula()
            self.assertEqual(f_in.simplify(), f_out.simplify())