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# 18from pysmt.shortcuts import * 19from pysmt.typing import REAL, INT 20from pysmt.test import TestCase, skipIfSolverNotAvailable, main 21from pysmt.exceptions import NoSolverAvailableError 22from pysmt.logics import UFLIRA 23 24 25class TestInterpolation(TestCase): 26 def test_selection(self): 27 with self.assertRaises(NoSolverAvailableError): 28 Interpolator(logic=UFLIRA) 29 30 with self.assertRaises(NoSolverAvailableError): 31 Interpolator(name="nonexistent") 32 33 @skipIfSolverNotAvailable('msat') 34 def test_binary_interpolant_msat(self): 35 self._test_binary_interpolant('msat') 36 37 @skipIfSolverNotAvailable('msat') 38 def test_sequence_interpolant_msat(self): 39 self._test_sequence_interpolant('msat') 40 41 def _test_binary_interpolant(self, name): 42 itp = Interpolator(name=name) 43 self._bool_example(itp, True) 44 self._real_example(itp, True) 45 self._int_example(itp, True) 46 47 def _test_sequence_interpolant(self, name): 48 itp = Interpolator(name=name) 49 self._bool_example(itp, False) 50 self._real_example(itp, False) 51 self._int_example(itp, False) 52 53 @skipIfSolverNotAvailable('msat') 54 def test_context(self): 55 with Interpolator() as itp: 56 self._bool_example(itp, False) 57 58 def _bool_example(self, itp, binary): 59 # Bool Example 60 x, y, z = Symbol("bx"), Symbol("by"), Symbol("bz") 61 62 a = And(x, Not(y)) 63 b = And(Implies(z, y), z) 64 65 if binary: 66 i = itp.binary_interpolant(a, b) 67 else: 68 i = itp.sequence_interpolant([a, b]) 69 70 self.assertTrue(i is not None) 71 if not binary: 72 self.assertTrue(hasattr(i, '__len__')) 73 self.assertTrue(len(i) == 1) 74 i = i[0] 75 76 self.assertTrue(i.get_free_variables() == set([y])) 77 self.assertValid(Implies(a, i)) 78 self.assertUnsat(And(i, b)) 79 80 81 def _real_example(self, itp, binary): 82 # Real Example 83 x, y, z = Symbol("rx", REAL), Symbol("ry", REAL), Symbol("rz", REAL) 84 85 a = And(LE(x, Real(0)), LE(y, x)) 86 b = And(GE(y, z), Equals(z, Real(1))) 87 88 if binary: 89 i = itp.binary_interpolant(a, b) 90 else: 91 i = itp.sequence_interpolant([a, b]) 92 93 self.assertTrue(i is not None) 94 if not binary: 95 self.assertTrue(hasattr(i, '__len__')) 96 self.assertTrue(len(i) == 1) 97 i = i[0] 98 99 self.assertTrue(i.get_free_variables() == set([y])) 100 self.assertValid(Implies(a, i)) 101 self.assertUnsat(And(i, b)) 102 103 104 def _int_example(self, itp, binary): 105 # Int Example 106 x, y, z = Symbol("ix", INT), Symbol("iy", INT), Symbol("iz", INT) 107 108 a = And(LE(x, Int(1)), LT(y, x)) 109 b = And(GE(y, z), GT(z, Int(0))) 110 111 if binary: 112 i = itp.binary_interpolant(a, b) 113 else: 114 i = itp.sequence_interpolant([a, b]) 115 116 self.assertTrue(i is not None) 117 if not binary: 118 self.assertTrue(hasattr(i, '__len__')) 119 self.assertTrue(len(i) == 1) 120 i = i[0] 121 122 self.assertTrue(i.get_free_variables() == set([y])) 123 self.assertValid(Implies(a, i)) 124 self.assertUnsat(And(i, b)) 125 126 127if __name__ == '__main__': 128 main() 129