Searched refs:QF_NIA (Results 1 – 25 of 34) sorted by relevance
12
| /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,
169 (QF_NIA, "small_set/QF_NIA/aproveSMT3509292547826641386.smt2.bz2", SAT),
170 (QF_NIA, "small_set/QF_NIA/problem-000158.cvc.2.smt2.bz2", UNSAT),
171 (QF_NIA, "small_set/QF_NIA/term-DtOD2C.smt2.bz2", SAT),
|
| H A D | test_parser_qf_nia.py | 19 from pysmt.logics import QF_NIA
25 if logic == QF_NIA:
|
| /dports/math/yices/yices-2.6.2/src/api/ |
| H A D | smt_logic_codes.c | 164 QF_NIA,
712 QF_NIA,
751 QF_NIA,
|
| H A D | smt_logic_codes.h | 116 QF_NIA, // non-linear integer arithmetic enumerator
|
| /dports/math/cvc4/CVC4-1.7/test/regress/regress1/arith/ |
| H A D | bug547.1.smt2 | 3 (set-logic QF_NIA)
|
| H A D | mod.02.smt2 | 2 (set-logic QF_NIA)
|
| H A D | mod.03.smt2 | 2 (set-logic QF_NIA)
|
| H A D | div.03.smt2 | 2 (set-logic QF_NIA)
|
| H A D | div.08.smt2 | 1 (set-logic QF_NIA)
|
| /dports/math/cvc4/CVC4-1.7/test/regress/regress0/arith/ |
| H A D | div.02.smt2 | 2 (set-logic QF_NIA)
|
| H A D | bug547.2.smt2 | 3 (set-logic QF_NIA)
|
| H A D | mod.01.smt2 | 2 (set-logic QF_NIA)
|
| H A D | div.01.smt2 | 1 (set-logic QF_NIA)
|
| /dports/math/cvc4/CVC4-1.7/test/regress/regress0/bv/ |
| H A D | bv-abstr-bug2.smt2 | 2 (set-logic QF_NIA)
|
| /dports/math/cvc4/CVC4-1.7/test/regress/regress1/nl/ |
| H A D | nl-eq-infer.smt2 | 1 (set-logic QF_NIA)
|
| H A D | disj-eval.smt2 | 3 (set-logic QF_NIA)
|
| H A D | rewriting-sums.smt2 | 3 (set-logic QF_NIA)
|
| /dports/math/cvc4/CVC4-1.7/test/regress/regress2/nl/ |
| H A D | siegel-nl-bases.smt2 | 3 (set-logic QF_NIA)
|
| /dports/math/cvc4/CVC4-1.7/contrib/ |
| H A D | run-script-smtcomp2016-application | 31 ANIA|QF_ANIA|QF_NIA|QF_UFNIA)
|
| H A D | run-script-smtcomp2017-application | 37 ANIA|QF_ANIA|QF_NIA|QF_UFNIA|QF_NRA)
|
| H A D | run-script-smtcomp2018-application | 37 ANIA|QF_ANIA|QF_NIA|QF_UFNIA|QF_NRA)
|
| /dports/security/hs-cryptol/cryptol-2.11.0/_cabal_deps/sbv-8.12/Data/SBV/Control/ |
| H A D | Types.hs | 196 | QF_NIA -- ^ Quantifier-free integer arithmetic. constructor
230 show QF_NIA = "QF_NIA"
|
| /dports/math/cvc4/CVC4-1.7/src/parser/smt1/ |
| H A D | smt1.h | 56 QF_NIA, enumerator
|
| H A D | smt1.cpp | 36 logicMap["QF_NIA"] = QF_NIA; in newLogicMap()
194 case QF_NIA: in setLogic()
|
| /dports/math/cvc4/CVC4-1.7/test/regress/regress0/nl/ |
| H A D | nia-wrong-tl.smt2 | 3 (set-logic QF_NIA)
|
12