Home
last modified time | relevance | path

Searched refs:assumption (Results 1 – 25 of 5666) sorted by relevance

12345678910>>...227

/dports/math/cvc4/CVC4-1.7/test/regress/regress0/lemmas/
H A Dclocksynchro_5clocks.main_invar.base.model.smt94 :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 Dcomb2.shuffled-as.sat03-420.smt33512 :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 Dbug2.smt2930 :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 Dconvert-tiff2jpg-query-1831.smt_68.smt13 :assumption
16 :assumption
19 :assumption
22 :assumption
26 :assumption
29 :assumption
32 :assumption
35 :assumption
38 :assumption
42 :assumption
[all …]
H A Dworking_55.smt10 :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 DArrow_Order-smtlib.778341.smt88 :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 DQEpres-uf.855035.smt43 :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 Dinference.py150 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 Dno_init_multi_delete14.smt12 :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 Dexample_unsat_core.c130 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 Dtst_bvmodel2.smt8 :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 Dassume.h356 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 Dmemcpy.c110 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 Dassume_quality.py95 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 Dequality-02.smt12 :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 Dslice-04.smt11 :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 Dslice-05.smt11 :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 Dslice-06.smt11 :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 Dslice-20.smt10 :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 Dslice-17.smt6 :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 DHoare-z3.931718.smt27 :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 Dtst_bvmodel2.smt8 :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 Ddiseqprop.06.smt12 :assumption (= x1 x2)
13 :assumption (= y1 y2)
15 :assumption (= x2 1)
16 :assumption (= y2 2)
18 :assumption (= (f x1) (f y1))
H A Ddiseqprop.05.smt12 :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_nkf25 '($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)]' \

12345678910>>...227