Searched refs:QF_AUFLIA (Results 1 – 25 of 52) sorted by relevance
123
| /dports/math/py-pysmt/pysmt-0.9.0/pysmt/test/smtlib/ |
| H A D | parser_utils.py | 26 QF_ALIA, QF_ABV, QF_AUFLIA, QF_AUFBV, QF_NRA, QF_NIA,
158 (QF_AUFLIA, "small_set/QF_AUFLIA/array_incompleteness1.smt2.bz2", UNSAT),
159 (QF_AUFLIA, "small_set/QF_AUFLIA/swap_invalid_t1_pp_nf_ai_00002_002.cvc.smt2.bz2", SAT),
|
| /dports/math/yices/yices-2.6.2/src/api/ |
| H A D | smt_logic_codes.c | 152 QF_AUFLIA,
735 QF_AUFLIA,
774 QF_AUFLIA,
|
| H A D | smt_logic_codes.h | 145 QF_AUFLIA, // arrays + uninterpreted functions + linear integer arithmetic enumerator
|
| /dports/math/py-pysmt/pysmt-0.9.0/pysmt/test/ |
| H A D | test_array.py | 21 from pysmt.logics import QF_AUFLIA, QF_AUFBV
56 @skipIfNoSolverForLogic(QF_AUFLIA)
61 self.assertSat(formula, logic=QF_AUFLIA)
|
| H A D | test_rewritings.py | 29 from pysmt.logics import BOOL, QF_NRA, QF_LRA, QF_AUFLIA
87 @skipIfNoSolverForLogic(QF_AUFLIA)
99 @skipIfNoSolverForLogic(QF_AUFLIA)
113 @skipIfNoSolverForLogic(QF_AUFLIA)
150 @skipIfNoSolverForLogic(QF_AUFLIA)
|
| /dports/math/cvc4/CVC4-1.7/test/regress/regress1/ |
| H A D | bug472.smt2 | 1 (set-logic QF_AUFLIA)
|
| /dports/math/cvc4/CVC4-1.7/test/regress/regress0/auflia/ |
| H A D | error72.delta2.smt | 2 :logic QF_AUFLIA
|
| H A D | a17.smt | 2 :logic QF_AUFLIA
|
| H A D | fuzz04.smt | 2 :logic QF_AUFLIA
|
| H A D | fuzz03.smt | 2 :logic QF_AUFLIA
|
| H A D | x2.smt | 2 :logic QF_AUFLIA
|
| H A D | bug336.smt2 | 1 (set-logic QF_AUFLIA)
|
| /dports/math/cvc4/CVC4-1.7/test/regress/regress0/ |
| H A D | bug544.smt2 | 4 (set-logic QF_AUFLIA)
|
| H A D | bug421.smt2 | 4 (set-logic QF_AUFLIA)
|
| H A D | bug421b.smt2 | 8 (set-logic QF_AUFLIA)
|
| /dports/math/yices/yices-2.6.2/tests/regress/mantis/ |
| H A D | 0036.smt2 | 2 (set-logic QF_AUFLIA)
|
| /dports/math/cvc4/CVC4-1.7/contrib/ |
| H A D | run-script-smtcomp2016-application | 37 QF_AUFLIA)
|
| H A D | run-script-smtcomp2017-application | 43 QF_AUFLIA)
|
| H A D | run-script-smtcomp2015-application | 44 QF_AUFLIA|QF_AX)
|
| H A D | run-script-smtcomp2018-application | 43 QF_AUFLIA)
|
| H A D | run-script-smtcomp2014-application | 44 QF_AUFLIA|QF_AX)
|
| /dports/security/hs-cryptol/cryptol-2.11.0/_cabal_deps/sbv-8.12/Data/SBV/Control/ |
| H A D | Types.hs | 190 …| QF_AUFLIA -- ^ Quantifier-free linear formulas over the theory of integer arrays extend… constructor
224 show QF_AUFLIA = "QF_AUFLIA"
|
| /dports/math/cvc4/CVC4-1.7/src/parser/smt1/ |
| H A D | smt1.h | 49 QF_AUFLIA, enumerator
|
| H A D | smt1.cpp | 55 logicMap["QF_AUFLIA"] = QF_AUFLIA; in newLogicMap()
270 case QF_AUFLIA: in setLogic()
|
| /dports/math/cvc4/CVC4-1.7/test/regress/regress0/decision/ |
| H A D | pp-regfile.delta01.smt | 5 :logic QF_AUFLIA
|
123