1# 2# This file is part of pySMT. 3# 4# Copyright 2014 Andrea Micheli and Marco Gario 5# 6# Licensed under the Apache License, Version 2.0 (the "License"); 7# you may not use this file except in compliance with the License. 8# You may obtain a copy of the License at 9# 10# http://www.apache.org/licenses/LICENSE-2.0 11# 12# Unless required by applicable law or agreed to in writing, software 13# distributed under the License is distributed on an "AS IS" BASIS, 14# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. 15# See the License for the specific language governing permissions and 16# limitations under the License. 17# 18import os 19from tempfile import mkstemp 20 21from six.moves import cStringIO 22 23import pysmt.logics as logics 24from pysmt.test import TestCase, skipIfNoSolverForLogic, main 25from pysmt.test.examples import get_example_formulae 26from pysmt.smtlib.parser import SmtLibParser, Tokenizer 27from pysmt.smtlib.script import smtlibscript_from_formula 28from pysmt.shortcuts import Iff 29from pysmt.shortcuts import read_smtlib, write_smtlib, get_env 30from pysmt.exceptions import PysmtSyntaxError 31 32class TestSMTParseExamples(TestCase): 33 34 def test_parse_examples(self): 35 fs = get_example_formulae() 36 37 for (f_out, _, _, logic) in fs: 38 if logic == logics.QF_BV: 39 # See test_parse_examples_bv 40 continue 41 buf = cStringIO() 42 script_out = smtlibscript_from_formula(f_out) 43 script_out.serialize(outstream=buf) 44 #print(buf) 45 46 buf.seek(0) 47 parser = SmtLibParser() 48 script_in = parser.get_script(buf) 49 f_in = script_in.get_last_formula() 50 self.assertEqual(f_in.simplify(), f_out.simplify()) 51 52 53 @skipIfNoSolverForLogic(logics.QF_BV) 54 def test_parse_examples_bv(self): 55 """For BV we represent a superset of the operators defined in SMT-LIB. 56 57 We verify the correctness of the serialization process by 58 checking the equivalence of the original and serialized 59 expression. 60 """ 61 fs = get_example_formulae() 62 63 for (f_out, _, _, logic) in fs: 64 if logic != logics.QF_BV: 65 continue 66 buf_out = cStringIO() 67 script_out = smtlibscript_from_formula(f_out) 68 script_out.serialize(outstream=buf_out) 69 70 buf_in = cStringIO(buf_out.getvalue()) 71 parser = SmtLibParser() 72 script_in = parser.get_script(buf_in) 73 f_in = script_in.get_last_formula() 74 75 self.assertValid(Iff(f_in, f_out)) 76 77 def test_parse_examples_daggified(self): 78 fs = get_example_formulae() 79 80 for (f_out, _, _, logic) in fs: 81 if logic == logics.QF_BV: 82 # See test_parse_examples_daggified_bv 83 continue 84 buf_out = cStringIO() 85 script_out = smtlibscript_from_formula(f_out) 86 script_out.serialize(outstream=buf_out, daggify=True) 87 buf_in = cStringIO(buf_out.getvalue()) 88 parser = SmtLibParser() 89 script_in = parser.get_script(buf_in) 90 f_in = script_in.get_last_formula() 91 self.assertEqual(f_in.simplify(), f_out.simplify()) 92 93 @skipIfNoSolverForLogic(logics.QF_BV) 94 def test_parse_examples_daggified_bv(self): 95 fs = get_example_formulae() 96 97 for (f_out, _, _, logic) in fs: 98 if logic != logics.QF_BV: 99 # See test_parse_examples_daggified 100 continue 101 buf_out = cStringIO() 102 script_out = smtlibscript_from_formula(f_out) 103 script_out.serialize(outstream=buf_out, daggify=True) 104 buf_in = cStringIO(buf_out.getvalue()) 105 parser = SmtLibParser() 106 script_in = parser.get_script(buf_in) 107 f_in = script_in.get_last_formula() 108 self.assertValid(Iff(f_in, f_out), f_in.serialize()) 109 110 def test_dumped_logic(self): 111 # Dumped logic matches the logic in the example 112 fs = get_example_formulae() 113 114 for (f_out, _, _, logic) in fs: 115 buf_out = cStringIO() 116 script_out = smtlibscript_from_formula(f_out) 117 script_out.serialize(outstream=buf_out) 118 buf_in = cStringIO(buf_out.getvalue()) 119 parser = SmtLibParser() 120 script_in = parser.get_script(buf_in) 121 for cmd in script_in: 122 if cmd.name == "set-logic": 123 logic_in = cmd.args[0] 124 if logic == logics.QF_BOOL: 125 self.assertEqual(logic_in, logics.QF_UF) 126 elif logic == logics.BOOL: 127 self.assertEqual(logic_in, logics.LRA) 128 else: 129 self.assertEqual(logic_in, logic, script_in) 130 break 131 else: # Loops exited normally 132 print("-"*40) 133 print(script_in) 134 135 def test_read_and_write_shortcuts(self): 136 fs = get_example_formulae() 137 138 fdi, tmp_fname = mkstemp() 139 os.close(fdi) # Close initial file descriptor 140 for (f_out, _, _, _) in fs: 141 write_smtlib(f_out, tmp_fname) 142 # with open(tmp_fname) as fin: 143 # print(fin.read()) 144 145 f_in = read_smtlib(tmp_fname) 146 self.assertEqual(f_out.simplify(), f_in.simplify()) 147 # Clean-up 148 os.remove(tmp_fname) 149 150 def test_incomplete_stream(self): 151 txt = """ 152 (declare-fun A () Bool) 153 (declare-fun B () Bool) 154 (assert (and A 155 """ 156 parser = SmtLibParser() 157 with self.assertRaises(PysmtSyntaxError): 158 parser.get_script(cStringIO(txt)) 159 160 def test_parse_consume(self): 161 smt_script = """ 162 (model 163 (define-fun STRING_cmd_line_arg_1_1000 () String "AAAAAAAAAAAA") 164 ) 165 """ 166 tokens = Tokenizer(cStringIO(smt_script), interactive=True) 167 parser = SmtLibParser() 168 tokens.consume() 169 tokens.consume() 170 next_token = tokens.consume() 171 tokens.add_extra_token(next_token) 172 tokens.consume() 173 174 def test_parser_params(self): 175 txt = """ 176 (define-fun x ((y Int)) Bool (> y 0)) 177 (declare-fun z () Int) 178 (declare-fun y () Bool) 179 (assert (and y (x z))) 180 """ 181 parser = SmtLibParser() 182 script = parser.get_script(cStringIO(txt)) 183 self.assertEqual(len(get_env().formula_manager.get_all_symbols()), 184 len(script.get_declared_symbols()) + len(script.get_define_fun_parameter_symbols())) 185 186 @skipIfNoSolverForLogic(logics.QF_ABV) 187 def test_nary_bvconcat(self): 188 txt = """ 189 (set-logic QF_BV ) 190 (declare-fun INPUT () (Array (_ BitVec 32) (_ BitVec 8) ) ) 191 (declare-fun A () (_ BitVec 64))(assert (= A (bvor #x0000000000000000 (bvshl ((_ zero_extend 32) ((_ zero_extend 24) (select INPUT #x00000000))) #x0000000000000000)))) 192 (declare-fun B () (_ BitVec 64))(assert (= B (concat ((_ extract 63 56) (bvor #x0000000000000000 (bvshl ((_ zero_extend 32) ((_ zero_extend 24) ((_ extract 7 0) (bvor #x0000000000000000 (bvshl ((_ zero_extend 32) ((_ zero_extend 24) (select INPUT #x00000000))) #x0000000000000000))))) #x0000000000000000))) ((_ extract 55 48) (bvor #x0000000000000000 (bvshl ((_ zero_extend 32) ((_ zero_extend 24) ((_ extract 7 0) (bvor #x0000000000000000 (bvshl ((_ zero_extend 32) ((_ zero_extend 24) (select INPUT #x00000000))) #x0000000000000000))))) #x0000000000000000))) ((_ extract 47 40) (bvor #x0000000000000000 (bvshl ((_ zero_extend 32) ((_ zero_extend 24) ((_ extract 7 0) (bvor #x0000000000000000 (bvshl ((_ zero_extend 32) ((_ zero_extend 24) (select INPUT #x00000000))) #x0000000000000000))))) #x0000000000000000))) ((_ extract 39 32) (bvor #x0000000000000000 (bvshl ((_ zero_extend 32) ((_ zero_extend 24) ((_ extract 7 0) (bvor #x0000000000000000 (bvshl ((_ zero_extend 32) ((_ zero_extend 24) (select INPUT #x00000000))) #x0000000000000000))))) #x0000000000000000))) ((_ extract 31 24) (bvor #x0000000000000000 (bvshl ((_ zero_extend 32) ((_ zero_extend 24) ((_ extract 7 0) (bvor #x0000000000000000 (bvshl ((_ zero_extend 32) ((_ zero_extend 24) (select INPUT #x00000000))) #x0000000000000000))))) #x0000000000000000))) ((_ extract 23 16) (bvor #x0000000000000000 (bvshl ((_ zero_extend 32) ((_ zero_extend 24) ((_ extract 7 0) (bvor #x0000000000000000 (bvshl ((_ zero_extend 32) ((_ zero_extend 24) (select INPUT #x00000000))) #x0000000000000000))))) #x0000000000000000))) ((_ extract 15 8) (bvor #x0000000000000000 (bvshl ((_ zero_extend 32) ((_ zero_extend 24) ((_ extract 7 0) (bvor #x0000000000000000 (bvshl ((_ zero_extend 32) ((_ zero_extend 24) (select INPUT #x00000000))) #x0000000000000000))))) #x0000000000000000))) ((_ extract 7 0) (bvor #x0000000000000000 (bvshl ((_ zero_extend 32) ((_ zero_extend 24) ((_ extract 7 0) (bvor #x0000000000000000 (bvshl ((_ zero_extend 32) ((_ zero_extend 24) (select INPUT #x00000000))) #x0000000000000000))))) #x0000000000000000)))))) 193 (assert (= A B)) 194 (check-sat)""" 195 parser = SmtLibParser() 196 script = parser.get_script(cStringIO(txt)) 197 f_in = script.get_last_formula() 198 self.assertSat(f_in) 199 200if __name__ == "__main__": 201 main() 202