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