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#
18"""Describe all logics supported by pySMT and other logics defined in
19the SMTLIB and provides methods to compare and search for particular
20logics.
21"""
22import six
23
24from pysmt.exceptions import UndefinedLogicError, NoLogicAvailableError
25
26
27class Theory(object):
28    """Describes a theory similarly to the SMTLIB 2.0."""
29    def __init__(self,
30                 arrays = None,
31                 arrays_const = None,
32                 bit_vectors = None,
33                 floating_point = None,
34                 integer_arithmetic = None,
35                 real_arithmetic = None,
36                 integer_difference = None,
37                 real_difference = None,
38                 linear = None,
39                 uninterpreted = None,
40                 custom_type = None,
41                 strings = None):
42        self.arrays = arrays or False
43        self.arrays_const = arrays_const or False
44        self.bit_vectors = bit_vectors or False
45        self.floating_point = floating_point or False
46        self.integer_arithmetic = integer_arithmetic or False
47        self.real_arithmetic = real_arithmetic or False
48        self.integer_difference = integer_difference or False
49        self.real_difference = real_difference or False
50        self.linear = linear if linear is not None else True
51        self.uninterpreted = uninterpreted or False
52        self.custom_type = custom_type or False
53        self.strings = strings or False
54        assert not arrays_const or arrays, "Cannot set arrays_const w/o arrays"
55        return
56
57    def set_lira(self, value=True):
58        res = self.copy()
59        res.integer_arithmetic = value
60        res.real_arithmetic = value
61        return res
62
63    def set_linear(self, value=True):
64        res = self.copy()
65        res.linear = value
66        return res
67
68    def set_strings(self, value=True):
69        res = self.copy()
70        res.strings = value
71        return res
72
73    def set_difference_logic(self, value=True):
74        res = self.copy()
75        if res.integer_arithmetic:
76            res.integer_difference = value
77        if res.real_arithmetic:
78            res.real_difference = value
79        return res
80
81    def set_arrays(self, value=True):
82        res = self.copy()
83        res.arrays = value
84        return res
85
86    def set_arrays_const(self, value=True):
87        if not self.arrays and value:
88            res = self.set_arrays()
89        else:
90            res = self.copy()
91        res.arrays_const = value
92        return res
93
94    def copy(self):
95        new_theory = Theory(arrays = self.arrays,
96                            arrays_const = self.arrays_const,
97                            bit_vectors = self.bit_vectors,
98                            floating_point = self.floating_point,
99                            integer_arithmetic = self.integer_arithmetic,
100                            real_arithmetic = self.real_arithmetic,
101                            integer_difference = self.integer_difference,
102                            real_difference = self.real_difference,
103                            linear = self.linear,
104                            uninterpreted = self.uninterpreted,
105                            custom_type = self.custom_type,
106                            strings = self.strings)
107        return new_theory
108
109    def combine(self, other):
110        if self.integer_arithmetic and other.integer_arithmetic:
111            integer_difference = self.integer_difference and other.integer_difference
112        elif self.integer_arithmetic and not other.integer_arithmetic:
113            integer_difference = self.integer_difference
114        elif not self.integer_arithmetic and other.integer_arithmetic:
115            integer_difference = other.integer_difference
116        else:
117            assert not self.integer_arithmetic and not other.integer_arithmetic
118            integer_difference = False
119
120        if self.real_arithmetic and other.real_arithmetic:
121            real_difference = self.real_difference and other.real_difference
122        elif self.real_arithmetic and not other.real_arithmetic:
123            real_difference = self.real_difference
124        elif not self.real_arithmetic and other.real_arithmetic:
125            real_difference = other.real_difference
126        else:
127            assert not self.real_arithmetic and not other.real_arithmetic
128            real_difference = False
129
130        return Theory(
131            arrays=self.arrays or other.arrays,
132            arrays_const=self.arrays_const or other.arrays_const,
133            bit_vectors=self.bit_vectors or other.bit_vectors,
134            floating_point=self.floating_point or other.floating_point,
135            integer_arithmetic=self.integer_arithmetic or other.integer_arithmetic,
136            real_arithmetic=self.real_arithmetic or other.real_arithmetic,
137            integer_difference=integer_difference,
138            real_difference=real_difference,
139            linear=self.linear and other.linear,
140            uninterpreted=self.uninterpreted or other.uninterpreted,
141            custom_type=self.custom_type or other.custom_type,
142            strings=self.strings or other.strings)
143
144    def __eq__(self, other):
145        if other is None or (not isinstance(other, Theory)):
146            return False
147        return (self.arrays == other.arrays and
148                self.arrays_const == other.arrays_const and
149                self.bit_vectors == other.bit_vectors and
150                self.floating_point == other.floating_point and
151                self.integer_arithmetic == other.integer_arithmetic and
152                self.real_arithmetic == other.real_arithmetic and
153                self.integer_difference == other.integer_difference and
154                self.real_difference == other.real_difference and
155                self.linear == other.linear and
156                self.uninterpreted == other.uninterpreted and
157                self.custom_type == other.custom_type and
158                self.strings == other.strings)
159
160    def __ne__(self, other):
161        return not (self == other)
162
163    def __le__(self, other):
164        if self.integer_difference == other.integer_difference:
165            le_integer_difference = True
166        elif self.integer_difference and other.integer_arithmetic:
167            le_integer_difference = True
168        elif not self.integer_arithmetic and other.integer_arithmetic:
169            le_integer_difference = True
170        else:
171            le_integer_difference = False
172
173        if self.real_difference == other.real_difference:
174            le_real_difference = True
175        elif self.real_difference and other.real_arithmetic:
176            le_real_difference = True
177        elif not self.real_arithmetic and other.real_arithmetic:
178            le_real_difference = True
179        else:
180            le_real_difference = False
181
182        if self.linear == other.linear:
183            le_linear = True
184        elif self.linear and not other.linear:
185            le_linear = True
186        else:
187            le_linear = False
188
189        return (self.arrays <= other.arrays and
190                self.arrays_const <= other.arrays_const and
191                self.bit_vectors <= other.bit_vectors and
192                self.floating_point <= other.floating_point and
193                self.uninterpreted <= other.uninterpreted and
194                self.custom_type <= other.custom_type and
195                le_integer_difference and
196                self.integer_arithmetic <= other.integer_arithmetic and
197                le_real_difference and
198                self.real_arithmetic <= other.real_arithmetic and
199                le_linear and
200                self.strings <= other.strings)
201
202    def __str__(self):
203        return ("Arrays: %s, " % self.arrays +
204                "ArraysConst: %s, " % self.arrays_const +
205                "BV: %s, " % self.bit_vectors +
206                "FP: %s, " % self.floating_point +
207                "IA: %s, " % self.integer_arithmetic +
208                "RA: %s, " % self.real_arithmetic +
209                "ID: %s, " % self.integer_difference +
210                "RD: %s, " % self.real_difference +
211                "Linear: %s, " % self.linear +
212                "EUF: %s, " % self.uninterpreted +
213                "Type: %s, " % self.custom_type +
214                "String: %s"% self.strings)
215
216    __repr__ = __str__
217
218
219class Logic(object):
220    """Describes a Logic similarly to the way they are defined in the SMTLIB 2.0
221
222    Note: We define more Logics than the ones defined in the SMTLib
223    2.0.  See LOGICS for a list of all the logics and SMTLIB2_LOGICS
224    for the restriction to the ones defined in SMTLIB2.0
225    """
226
227    def __init__(self, name, description,
228                 quantifier_free = False,
229                 theory=None,
230                 **theory_kwargs):
231        self.name = name
232        self.description = description
233        self.quantifier_free = quantifier_free
234        if theory is None:
235            self.theory = Theory(**theory_kwargs)
236        else:
237            self.theory = theory
238        return
239
240    def get_quantified_version(self):
241        """Returns the quantified version of logic."""
242        if self.quantifier_free:
243            return self
244        target_logic = Logic(name="", description="",
245                             quantifier_free=False,
246                             theory=self.theory)
247        return get_closer_pysmt_logic(target_logic)
248
249    def is_quantified(self):
250        """Return whether the logic supports quantifiers."""
251        return not self.quantifier_free
252
253    def __str__(self):
254        return self.name
255
256    def __repr__(self):
257        return str(self)
258
259    def __eq__(self, other):
260        if other is None or (not isinstance(other, Logic)):
261            return False
262
263        return (self.name == other.name and
264                self.quantifier_free == other.quantifier_free and
265                self.theory == other.theory)
266
267    def __ne__(self, other):
268        return not (self == other)
269
270    def __lt__(self, other):
271        return (self != other) and (self.__le__(other))
272
273    def __le__(self, other):
274        return (self.theory <= other.theory and
275                self.quantifier_free >= other.quantifier_free)
276
277    def __ge__(self, other):
278        return (other.__le__(self))
279
280    def __gt__(self, other):
281        return (other.__lt__(self))
282
283    def __hash__(self):
284        return hash(self.name)
285
286# Logics
287
288QF_BOOL = Logic(name="QF_BOOL",
289                description=\
290                """The simplest logic: quantifier-free boolean logic.""",
291                quantifier_free=True)
292
293BOOL = Logic(name="BOOL",
294             description=\
295             """Quantified boolean logic.""")
296QBF=BOOL # Provide additional name for consistency with literature
297
298
299QF_BOOLt = Logic(name="QF_BOOLt",
300                description=\
301                """Quantifier-free boolean logic with custom sorts.""",
302                 quantifier_free=True,
303                 custom_type=True)
304
305
306AUFLIA = Logic(name="AUFLIA",
307               description=\
308"""Closed formulas over the theory of linear integer arithmetic and
309arrays extended with free sort and function symbols but restricted to
310arrays with integer indices and values.""",
311               arrays=True,
312               integer_arithmetic=True,
313               uninterpreted=True)
314
315ALIA = Logic(name="ALIA",
316             description=\
317"""Closed formulas over the theory of linear integer arithmetic and
318arrays.""",
319             arrays=True,
320             integer_arithmetic=True)
321
322
323AUFLIRA = Logic(name="AUFLIRA",
324                description=\
325"""Closed linear formulas with free sort and function symbols over
326one- and two-dimentional arrays of integer index and real value.""",
327                arrays=True,
328                integer_arithmetic=True,
329                real_arithmetic=True,
330                uninterpreted=True)
331
332
333AUFNIRA = Logic(name="AUFNIRA",
334                description=\
335"""Closed formulas with free function and predicate symbols over a
336theory of arrays of arrays of integer index and real value.""",
337                arrays=True,
338                integer_arithmetic=True,
339                real_arithmetic=True,
340                linear=False,
341                uninterpreted=True)
342
343
344LRA = Logic(name="LRA",
345            description=\
346"""Closed linear formulas in linear real arithmetic.""",
347            real_arithmetic=True)
348
349
350LIA = Logic(name="LIA",
351            description=\
352"""Closed linear formulas in linear integer arithmetic.""",
353            integer_arithmetic=True)
354
355
356UFLIRA = Logic(name="UFLIRA",
357                description=\
358"""Closed linear formulas with free sort and function symbols in
359linear and real arithmetic.""",
360                integer_arithmetic=True,
361                real_arithmetic=True,
362                linear=True,
363                uninterpreted=True)
364
365
366QF_UFLIRA = Logic(name="QF_UFLIRA",
367                description=\
368"""Quantifier-free, closed linear formulas with free sort and function symbols in
369linear and real arithmetic.""",
370                integer_arithmetic=True,
371                real_arithmetic=True,
372                linear=True,
373                quantifier_free=True,
374                uninterpreted=True)
375
376
377NIA = Logic(name="NIA",
378            description=\
379"""Closed formulas in non-linear integer arithmetic.""",
380            integer_arithmetic=True,
381            linear=False)
382
383
384NRA = Logic(name="NRA",
385            description=\
386"""Closed formulas in non-linear real arithmetic.""",
387            real_arithmetic=True,
388            linear=False)
389
390
391QF_ABV = Logic(name="QF_ABV",
392               description=\
393"""Closed quantifier-free formulas over the theory of bitvectors and
394bitvector arrays.""",
395               quantifier_free=True,
396               arrays=True,
397               bit_vectors=True)
398
399
400QF_AUFBV = Logic(name="QF_AUFBV",
401                 description=\
402"""Closed quantifier-free formulas over the theory of bitvectors and
403bitvector arrays extended with free sort and function symbols.""",
404                 quantifier_free=True,
405                 arrays=True,
406                 bit_vectors=True,
407                 uninterpreted=True)
408
409
410QF_AUFLIA = Logic(name="QF_AUFLIA",
411                  description=\
412"""Closed quantifier-free linear formulas over the theory of integer
413arrays extended with free sort and function symbols.""",
414                  quantifier_free=True,
415                  arrays=True,
416                  integer_arithmetic=True,
417                  uninterpreted=True)
418
419
420QF_ALIA = Logic(name="QF_ALIA",
421                description=\
422"""Closed quantifier-free linear formulas over the theory of integer
423arrays.""",
424                quantifier_free=True,
425                arrays=True,
426                integer_arithmetic=True)
427
428
429QF_AX = Logic(name="QF_AX",
430              description=\
431"""Closed quantifier-free formulas over the theory of arrays with
432extensionality.""",
433              quantifier_free=True,
434              arrays=True)
435
436
437QF_BV = Logic(name="QF_BV",
438              description=\
439"""Closed quantifier-free formulas over the theory of fixed-size
440bitvectors.""",
441              quantifier_free=True,
442              bit_vectors=True)
443
444BV = Logic(name="BV",
445           description=\
446"""Closed formulas over the theory of fixed-size
447bitvectors.""",
448           bit_vectors=True)
449
450UFBV = Logic(name="UFBV",
451             description=\
452"""Closed formulas over the theory of fixed-size bitvectors
453 and uninterpreted functions.""",
454             bit_vectors=True,
455             uninterpreted=True)
456
457QF_IDL = Logic(name="QF_IDL",
458               description=\
459"""Difference Logic over the integers. In essence, Boolean
460combinations of inequations of the form x - y < b where x and y are
461integer variables and b is an integer constant.""",
462               quantifier_free=True,
463               integer_arithmetic=True,
464               integer_difference=True)
465
466
467QF_LIA = Logic(name="QF_LIA",
468               description=\
469"""Unquantified linear integer arithmetic. In essence, Boolean
470combinations of inequations between linear polynomials over integer
471variables.""",
472               quantifier_free=True,
473               integer_arithmetic=True)
474
475
476QF_LRA = Logic(name="QF_LRA",
477               description=\
478"""Unquantified linear real arithmetic. In essence, Boolean
479combinations of inequations between linear polynomials over real
480variables.""",
481               quantifier_free=True,
482               real_arithmetic=True)
483
484QF_NIA = Logic(name="QF_NIA",
485               description=\
486"""Quantifier-free integer arithmetic.""",
487               quantifier_free=True,
488               integer_arithmetic=True,
489               linear=False)
490
491
492QF_NRA = Logic(name="QF_NRA",
493               description=\
494"""Quantifier-free real arithmetic.""",
495               quantifier_free=True,
496               real_arithmetic=True,
497               linear=False)
498
499
500QF_RDL = Logic(name="QF_RDL",
501               description=\
502"""Difference Logic over the reals. In essence, Boolean combinations
503of inequations of the form x - y < b where x and y are real variables
504and b is a rational constant.""",
505               real_arithmetic=True,
506               quantifier_free=True,
507               real_difference=True)
508
509
510QF_UF = Logic(name="QF_UF",
511              description=\
512"""Unquantified formulas built over a signature of uninterpreted
513(i.e., free) sort and function symbols.""",
514              quantifier_free=True,
515              uninterpreted=True)
516
517UF = Logic(name="UF",
518           description=\
519"""Quantified formulas built over a signature of uninterpreted
520(i.e., free) sort and function symbols.""",
521           uninterpreted=True)
522
523
524QF_UFBV = Logic(name="QF_UFBV",
525                description=\
526"""Unquantified formulas over bitvectors with uninterpreted sort
527function and symbols.""",
528                quantifier_free=True,
529                bit_vectors=True,
530                uninterpreted=True)
531
532
533QF_UFIDL = Logic(name="QF_UFIDL",
534                 description=\
535"""Difference Logic over the integers (in essence) but with
536uninterpreted sort and function symbols?""",
537                 quantifier_free=True,
538                 integer_arithmetic=True,
539                 integer_difference=True,
540                 uninterpreted=True)
541
542
543QF_UFLIA = Logic(name="QF_UFLIA",
544                 description=\
545"""Unquantified linear integer arithmetic with uninterpreted sort and
546function symbols.""",
547                 quantifier_free=True,
548                 integer_arithmetic=True,
549                 uninterpreted=True)
550
551
552QF_UFLRA = Logic(name="QF_UFLRA",
553                 description=\
554"""Unquantified linear real arithmetic with uninterpreted sort and
555function symbols.""",
556                 quantifier_free=True,
557                 real_arithmetic=True,
558                 uninterpreted=True)
559
560
561QF_UFNRA = Logic(name="QF_UFNRA",
562                 description=\
563"""Unquantified non-linear real arithmetic with uninterpreted sort and
564function symbols.""",
565                 quantifier_free=True,
566                 real_arithmetic=True,
567                 linear=False,
568                 uninterpreted=True)
569
570
571QF_UFNIA = Logic(name="QF_UFNIA",
572                 description=\
573"""Unquantified non-linear integer arithmetic with uninterpreted sort and
574function symbols.""",
575                 quantifier_free=True,
576                 integer_arithmetic=True,
577                 linear=False,
578                 uninterpreted=True)
579
580
581UFLRA = Logic(name="UFLRA",
582              description=\
583"""Linear real arithmetic with uninterpreted sort and function
584symbols.""",
585              real_arithmetic=True,
586              uninterpreted=True)
587
588
589UFNIA = Logic(name="UFNIA",
590              description=\
591"""Non-linear integer arithmetic with uninterpreted sort and function
592symbols.""",
593              integer_difference=True,
594              linear=False,
595              uninterpreted=True)
596
597
598QF_SLIA = Logic(name="QF_SLIA",
599                description=\
600                """Extension of LIA including theory of Strings.""",
601                integer_arithmetic=True,
602                quantifier_free=True,
603                uninterpreted=True,
604                strings=True)
605
606
607QF_AUFBVLIRA = Logic(name="QF_AUFBVLIRA",
608                     description=\
609                     """Quantifier free Arrays, Bitvectors and LIRA""",
610                     linear=True,
611                     uninterpreted=True,
612                     quantifier_free=True,
613                     arrays=True,
614                     bit_vectors=True,
615                     integer_arithmetic=True,
616                     real_arithmetic=True)
617
618
619AUTO = Logic(name="Auto",
620             description="Special logic used to indicate that the logic to be used depends on the formula.")
621
622SMTLIB2_LOGICS = frozenset([ AUFLIA,
623                             AUFLIRA,
624                             AUFNIRA,
625                             ALIA,
626                             LRA,
627                             LIA,
628                             NIA,
629                             NRA,
630                             UFLRA,
631                             UFNIA,
632                             UFLIRA,
633                             QF_ABV,
634                             QF_AUFBV,
635                             QF_AUFLIA,
636                             QF_ALIA,
637                             QF_AX,
638                             QF_BV,
639                             QF_IDL,
640                             QF_LIA,
641                             QF_LRA,
642                             QF_NIA,
643                             QF_NRA,
644                             QF_RDL,
645                             QF_UF,
646                             QF_UFBV ,
647                             QF_UFIDL,
648                             QF_UFLIA,
649                             QF_UFLRA,
650                             QF_UFNRA,
651                             QF_UFNIA,
652                             QF_UFLIRA,
653                             QF_SLIA
654                         ])
655
656LOGICS = SMTLIB2_LOGICS | frozenset([ QF_BOOL, BOOL, QF_AUFBVLIRA])
657
658QF_LOGICS = frozenset(_l for _l in LOGICS if _l.quantifier_free)
659
660#
661# This is the set of logics supported by the current version of pySMT
662#
663PYSMT_LOGICS = frozenset([QF_BOOL, QF_IDL, QF_LIA, QF_LRA, QF_RDL, QF_UF, QF_UFIDL,
664                          QF_UFLIA, QF_UFLRA, QF_UFLIRA,
665                          BOOL, LRA, LIA, UFLIRA, UFLRA,
666                          QF_BV, QF_UFBV,
667                          QF_SLIA,
668                          QF_BV, QF_UFBV,
669                          QF_ABV, QF_AUFBV, QF_AUFLIA, QF_ALIA, QF_AX,
670                          QF_AUFBVLIRA,
671                          QF_NRA, QF_NIA, UFBV, BV,
672                      ])
673
674# PySMT Logics includes additional features:
675#  - constant arrays: QF_AUFBV  becomes QF_AUFBV*
676#  - theories without custom types (no-name) QF_AUFBV QF_AUFBVt
677#
678
679ext_logics = set()
680for l in PYSMT_LOGICS:
681    if not l.theory.custom_type:
682        new_theory = l.theory.copy()
683        new_theory.custom_type = True
684        nl = Logic(name=l.name+"t",
685                   description=l.description+" (with Custom Types)",
686                   quantifier_free=l.quantifier_free,
687                   theory=new_theory)
688        ext_logics.add(nl)
689
690    if l.theory.arrays:
691        new_theory = l.theory.copy()
692        new_theory.arrays_const = True
693        nl = Logic(name=l.name+"*",
694                   description=l.description+" (Extended with Const Arrays)",
695                   quantifier_free=l.quantifier_free,
696                   theory=new_theory)
697        ext_logics.add(nl)
698
699
700
701LOGICS = LOGICS | frozenset(ext_logics)
702PYSMT_LOGICS = PYSMT_LOGICS | frozenset(ext_logics)
703
704
705PYSMT_QF_LOGICS = frozenset(_l for _l in PYSMT_LOGICS if _l.quantifier_free)
706
707BV_LOGICS = frozenset(_l for _l in PYSMT_LOGICS if _l.theory.bit_vectors)
708ARRAYS_LOGICS = frozenset(_l for _l in PYSMT_LOGICS if _l.theory.arrays)
709ARRAYS_CONST_LOGICS = frozenset(_l for _l in PYSMT_LOGICS \
710                                if _l.theory.arrays_const)
711
712
713def get_logic_by_name(name):
714    """Returns the Logic that matches the provided name."""
715    for logic in LOGICS:
716        if logic.name.lower() == name.lower(): return logic
717    raise UndefinedLogicError(name)
718
719
720def convert_logic_from_string(name):
721    """Helper function to parse function arguments.
722
723    This takes a logic or a string or None, and returns a logic or None.
724    """
725    if name is not None and isinstance(name, six.string_types):
726        name = get_logic_by_name(name)
727    return name
728
729
730def get_logic_name(**logic_kwargs):
731    """Returns the name of the Logic that matches the given properties.
732
733    See get_logic for the list of parameters.
734    """
735    return get_logic(**logic_kwargs).name
736
737
738def get_logic(quantifier_free=False,
739              arrays=False,
740              arrays_const=False,
741              bit_vectors=False,
742              floating_point=False,
743              integer_arithmetic=False,
744              real_arithmetic=False,
745              integer_difference=False,
746              real_difference=False,
747              linear=True,
748              uninterpreted=False,
749              custom_type=False,
750              strings=False):
751    """Returns the Logic that matches the given properties.
752
753    Equivalent (but better) to executing get_logic_by_name(get_logic_name(...))
754    """
755
756    for logic in LOGICS:
757        if (logic.quantifier_free == quantifier_free and
758            logic.theory.arrays == arrays and
759            logic.theory.arrays_const == arrays_const and
760            logic.theory.bit_vectors == bit_vectors and
761            logic.theory.floating_point == floating_point and
762            logic.theory.integer_arithmetic == integer_arithmetic and
763            logic.theory.real_arithmetic == real_arithmetic and
764            logic.theory.integer_difference == integer_difference and
765            logic.theory.real_difference == real_difference and
766            logic.theory.linear == linear and
767            logic.theory.uninterpreted == uninterpreted and
768            logic.theory.custom_type == custom_type and
769            logic.theory.strings == strings):
770            return logic
771    raise UndefinedLogicError
772
773
774def most_generic_logic(logics):
775    """Given a set of logics, return the most generic one.
776
777    If a unique most generic logic does not exists, throw an error.
778    """
779    res = [ l for l in logics if all(l >= x for x in logics)]
780    if len(res) != 1:
781        raise NoLogicAvailableError("Could not find the most generic "
782                                    "logic for %s." % str(logics))
783    return res[0]
784
785
786def get_closer_logic(supported_logics, logic):
787    """
788    Returns the smaller supported logic that is greater or equal to
789    the given logic. Raises NoLogicAvailableError if the solver
790    does not support the given logic.
791
792    """
793    res = [l for l in supported_logics if logic <= l]
794    if len(res) == 0:
795        raise NoLogicAvailableError("Logic %s is not supported" % logic)
796    return min(res)
797
798
799def get_closer_pysmt_logic(target_logic):
800    """Returns the closer logic supported by PYSMT."""
801    return get_closer_logic(PYSMT_LOGICS, target_logic)
802
803
804def get_closer_smtlib_logic(target_logic):
805    """Returns the closer logic supported by SMT-LIB 2.0."""
806    if target_logic == QF_BOOL:
807        return QF_UF
808    if target_logic == BOOL:
809        return LRA
810    return get_closer_logic(SMTLIB2_LOGICS, target_logic)
811