/dports/math/cvc4/CVC4-1.7/test/regress/regress0/lemmas/ |
H A D | clocksynchro_5clocks.main_invar.base.model.smt | 94 :assumption (=x_76 1) 95 :assumption (=x_76 1) 96 :assumption (=x_0 0) 97 :assumption (=x_0 0) 100 :assumption (=x_70 1) 101 :assumption (=x_70 1) 102 :assumption (=x_75 1) 103 :assumption (=x_75 1) 104 :assumption (=x_69 1) 105 :assumption (=x_69 1) [all …]
|
/dports/math/cvc4/CVC4-1.7/test/regress/regress4/ |
H A D | comb2.shuffled-as.sat03-420.smt | 33512 :assumption (or x69 x454) 34185 :assumption (or x2945 x16) 35271 :assumption (or x405 x288) 36118 :assumption (or x147 x529) 36888 :assumption (or x3576 x6) 58297 :assumption (or x310 x77) 80758 :assumption (or x7708 x6) 88540 :assumption (or x655 x15) 100309 :assumption (or x575 x98) 104899 :assumption (or x9 x5025) [all …]
|
/dports/math/cvc4/CVC4-1.7/test/regress/regress0/ |
H A D | bug2.smt | 2930 :assumption (or x116 x21) 2964 :assumption (or x123 x21) 3838 :assumption (or x303 x24) 3842 :assumption (or x304 x25) 3847 :assumption (or x305 x26) 3865 :assumption (or x311 x25) 3869 :assumption (or x312 x26) 3886 :assumption (or x316 x26) 3901 :assumption (or x320 x26) 3915 :assumption (or x136 x26) [all …]
|
/dports/math/stp/stp-2.3.3/tests/query-files/sample-smt-tests/ |
H A D | convert-tiff2jpg-query-1831.smt_68.smt | 13 :assumption 16 :assumption 19 :assumption 22 :assumption 26 :assumption 29 :assumption 32 :assumption 35 :assumption 38 :assumption 42 :assumption [all …]
|
H A D | working_55.smt | 10 :assumption (= sym1 (sign_extend[63] bv1[1])) 11 :assumption (= sym1 (bvnot bv0[64])) 15 :assumption (= sym2 (zero_extend[63] bv1[1])) 18 :assumption (= sym1 (zero_extend[0] sym1)) 19 :assumption (= sym1 (sign_extend[0] sym1)) 23 :assumption (= sym3 (bvshl bv1[64] bv63[64])) 25 :assumption (= sym4 (bvlshr bv1[64] bv63[64])) 29 :assumption (= sym6 (zero_extend[1] sym7)) 30 :assumption (= sym6 (sign_extend[1] sym7)) 35 ;:assumption (= sym5 (bvshl sym4 sym4))
|
/dports/math/cvc4/CVC4-1.7/test/regress/regress0/fmf/ |
H A D | Arrow_Order-smtlib.778341.smt | 88 :assumption (not (= f1 f2)) 92 :assumption (not (= f12 f1)) 96 :assumption (= (f13 f14) f1) 97 :assumption (= (f15 f14) f1) 183 :assumption (= (f17 f72 f16) f16) 198 :assumption (= f11 f54) 199 :assumption (= f8 f53) 200 :assumption (= f5 f52) 207 :assumption (= f54 f11) 208 :assumption (= f53 f8) [all …]
|
H A D | QEpres-uf.855035.smt | 43 :assumption (not (= f1 f2)) 44 :assumption (not (not (= (f3 f4 f5) f6))) 46 :assumption (= (f7 f5 (f8 (f10 f11 f9))) f1) 47 :assumption (forall (?v0 S4) (iff (= f6 ?v0) (= ?v0 f6)) ) 48 :assumption (= (f12 f13 f6) f6) 52 :assumption (= (f18 f6 f19) f1) 53 :assumption (= (f20 f6) f1) 59 :assumption (forall (?v0 S4) (= (f18 (f12 f13 ?v0) f27) f1) ) 60 :assumption (= (f12 f28 f6) f6) 63 :assumption (= (f18 f6 f27) f1) [all …]
|
/dports/math/py-mathics/Mathics3-2.2.0/mathics/builtin/ |
H A D | inference.py | 150 for assumption in assumptions_list: 151 if assumption.is_symbol(): 152 if assumption.is_true(): 159 if assumption.is_numeric(): 208 for assumption in assumptions_list: 209 assumption, applied = assumption.apply_rules( 217 for assumption in assumptions_list: 232 leaves = assumption.leaves() 233 head = assumption.get_head() 239 elif assumption.has_form( [all …]
|
/dports/math/cvc4/CVC4-1.7/test/regress/regress0/aufbv/ |
H A D | no_init_multi_delete14.smt | 12 :assumption 16 :assumption 20 :assumption 24 :assumption 28 :assumption 32 :assumption 35 :assumption 38 :assumption 41 :assumption 44 :assumption [all …]
|
/dports/math/yices/yices-2.6.2/examples/ |
H A D | example_unsat_core.c | 130 term_t assumption[3]; in unsat_core_test() local 141 assumption[0] = yices_arith_lt_atom(x, y); // x < y in unsat_core_test() 142 assumption[1] = yices_arith_gt_atom(x, y); // x > y in unsat_core_test() 143 assumption[2] = yices_arith_eq_atom(x, y); // x = y in unsat_core_test() 154 check_and_get_core(ctx, 3, assumption); in unsat_core_test() 159 assumption[0] = yices_not(assumption[0]); // x >= y in unsat_core_test() 160 assumption[1] = yices_not(assumption[1]); // x <= y in unsat_core_test() 161 assumption[2] = yices_not(assumption[2]); // x != y in unsat_core_test() 166 check_and_get_core(ctx, 3, assumption); in unsat_core_test() 171 check_and_get_core(ctx, 2, assumption); in unsat_core_test()
|
H A D | tst_bvmodel2.smt | 8 :assumption (= a (bvor b c)) 9 :assumption (= d (bvmul a bv23[16])) 10 :assumption (bvuge (extract[7:0] d) bv10[8]) 11 :assumption (= b (sign_extend[8] x)) 12 :assumption (= (extract[7:7] x) bv1[1])
|
/dports/devel/fatal/fatal-2021.12.27.00/fatal/debug/ |
H A D | assume.h | 356 assumption.print(out); 372 assumption.print(out); 385 std::size_t count_assumptions(T &&assumption) { return assumption.eval(); } 398 if (!assumption.eval()) { 431 if (assumption.eval()) { 457 if (!assumption.eval()) { 461 std::forward<T>(assumption), 483 if (assumption.eval()) { 487 std::forward<T>(assumption), 516 assumption.eval(), [all …]
|
/dports/math/boolector/boolector-3.2.2/examples/api/c/memcpy/ |
H A D | memcpy.c | 110 assumption = cmp; in main() 113 tmp = boolector_and (btor, assumption, cmp); in main() 114 boolector_release (btor, assumption); in main() 116 assumption = tmp; in main() 130 boolector_release (btor, assumption); in main() 132 assumption = tmp; in main() 139 boolector_release (btor, assumption); in main() 141 assumption = tmp; in main() 150 boolector_release (btor, assumption); in main() 152 assumption = tmp; in main() [all …]
|
/dports/www/flexget/Flexget-3.2.18/flexget/plugins/metainfo/ |
H A D | assume_quality.py | 95 key=lambda assumption: self.precision(assumption.target), reverse=True 97 for assumption in self.assumptions: 99 'Target {} - Priority {}', assumption.target, self.precision(assumption.target) 106 for assumption in self.assumptions: 107 logger.debug('Trying {} - {}', assumption.target, assumption.quality) 108 if assumption.target.allows(entry.get('quality')): 109 logger.debug('Match: {}', assumption.target) 110 self.assume(entry, assumption.quality)
|
/dports/math/cvc4/CVC4-1.7/test/regress/regress0/bv/core/ |
H A D | equality-02.smt | 12 :assumption (= x0 x1) 13 :assumption (= x1 x2) 14 :assumption (= x2 x3) 15 :assumption (= y0 y1) 16 :assumption (= y1 y2) 17 :assumption (= y2 y3) 18 :assumption (= x0 y0)
|
H A D | slice-04.smt | 11 :assumption (= x1 (concat x2 x2)) 12 :assumption (= x2 (concat x3 x3)) 13 :assumption (= x3 (concat x4 x4)) 14 :assumption (= x4 (concat x5 x5)) 15 :assumption (= x5 (concat x6 x6)) 16 :assumption (= x6 (concat x7 x7))
|
H A D | slice-05.smt | 11 :assumption (= x1 (concat x2 x2)) 12 :assumption (= x2 (concat x3 x3)) 13 :assumption (= x3 (concat x4 x4)) 14 :assumption (= x4 (concat x5 x5)) 15 :assumption (= x5 (concat x6 x6)) 16 :assumption (= x6 (concat x7 x7))
|
H A D | slice-06.smt | 11 :assumption (= x1 (concat x2 x2)) 12 :assumption (= x2 (concat x3 x3)) 13 :assumption (= x3 (concat x4 x4)) 14 :assumption (= x4 (concat x5 x5)) 15 :assumption (= x5 (concat x6 x6)) 16 :assumption (= x6 (concat x7 x7))
|
H A D | slice-20.smt | 10 :assumption (= x1 y1) 11 :assumption (= x1 (concat x2 x2)) 12 :assumption (= x2 (concat x3 x3)) 13 :assumption (= y1 (concat y2 y2)) 14 :assumption (= y2 (concat y3 y3))
|
H A D | slice-17.smt | 6 :assumption (= y (extract[11:0] x)) 7 :assumption (= y (extract[15:4] x)) 8 :assumption (= (extract[3:1] y) (extract[2:0] y)) 9 :assumption (= (extract[0:0] x) bv1[1])
|
/dports/math/cvc4/CVC4-1.7/test/regress/regress1/fmf/ |
H A D | Hoare-z3.931718.smt | 27 :assumption (not (= f1 f2)) 28 :assumption (forall (?v0 S2) (?v1 S2) (iff (= (f3 (f4 f5 ?v0) ?v1) f1) (= ?v0 ?v1)) ) 29 :assumption (not (= (f6 f7 (f8 (f9 (f10 (f11 (f12 f13 f14) f15) f16)) f7)) f1)) 30 :assumption (= (f6 f7 (f8 (f9 (f10 (f11 (f12 f13 f5) f15) (f17 f15))) f7)) f1) 31 :assumption (= (f18 f7 (f8 (f9 (f10 (f11 (f12 f13 f14) f15) f16)) f7)) f1) 32 :assumption (forall (?v0 S5) (= (f6 ?v0 f7) f1) ) 33 :assumption (forall (?v0 S4) (?v1 S10) (?v2 S4) (?v3 S4) (?v4 S10) (?v5 S4) (iff (= (f10 (f11 (f12 … 34 :assumption (forall (?v0 S5) (?v1 S5) (implies (= (f6 ?v0 ?v1) f1) (= (f18 ?v0 ?v1) f1)) ) 35 :assumption (forall (?v0 S5) (?v1 S5) (?v2 S5) (implies (= (f6 ?v0 ?v1) f1) (implies (= (f6 ?v2 ?v0… 36 :assumption (forall (?v0 S5) (?v1 S7) (?v2 S5) (implies (= (f6 ?v0 (f8 (f9 ?v1) f7)) f1) (implies (… [all …]
|
/dports/math/yices/yices-2.6.2/tests/regress/bv/ |
H A D | tst_bvmodel2.smt | 8 :assumption (= a (bvor b c)) 9 :assumption (= d (bvmul a bv23[16])) 10 :assumption (bvuge (extract[7:0] d) bv10[8]) 11 :assumption (= b (sign_extend[8] x)) 12 :assumption (= (extract[7:7] x) bv1[1])
|
/dports/math/cvc4/CVC4-1.7/test/regress/regress0/uflia/ |
H A D | diseqprop.06.smt | 12 :assumption (= x1 x2) 13 :assumption (= y1 y2) 15 :assumption (= x2 1) 16 :assumption (= y2 2) 18 :assumption (= (f x1) (f y1))
|
H A D | diseqprop.05.smt | 12 :assumption (= x1 x2) 13 :assumption (= y1 y2) 15 :assumption (= (f x1) (f y1)) 16 :assumption (= x2 1) 17 :assumption (= y2 2)
|
/dports/shells/zsh/zsh-5.8.1/Completion/Unix/Command/ |
H A D | _nkf | 25 '($inputs)-J[Input assumption is JIS 7 bit]' \ 26 '($inputs)-E[Input assumption is Shift JIS]' \ 27 '($inputs)-S[Input assumption is EUC-JP]' \ 28 '($inputs)-W[Input assumption is UTF-8 (No BOM)]' \ 29 '($inputs)-W8[Input assumption is UTF-8 (BOM)]' \ 30 '($inputs)-W16[Input assumption is UTF-16 (BigEndian; No BOM)]' \ 31 '($inputs)-W16b[Input assumption is UTF-16 (BigEndian; BOM)]' \ 32 '($inputs)-W16l0[Input assumption is UTF-16 (Little Endian; No BOM)]' \ 33 '($inputs)-W16l[Input assumption is UTF-16 (Little Endian; BOM)]' \
|