Lines Matching refs:NativeObject
241 return new SeqSort(this, Native.Z3_mk_seq_sort(nCtx, s.NativeObject)); in MkSeqSort()
250 return new ReSort(this, Native.Z3_mk_re_sort(nCtx, s.NativeObject)); in MkReSort()
456 n_constr[i] = cla[i].NativeObject; in MkDatatypeSorts()
492 nCtx, field.NativeObject, in MkUpdateField()
493 t.NativeObject, v.NativeObject)); in MkUpdateField()
569 … Native.Z3_add_rec_def(nCtx, f.NativeObject, (uint)args.Length, argsNative, body.NativeObject); in AddRecDef()
649 return Expr.Create(this, Native.Z3_mk_bound(nCtx, index, ty.NativeObject)); in MkBound()
680 … return Expr.Create(this, Native.Z3_mk_const(nCtx, name.NativeObject, range.NativeObject)); in MkConst()
702 return Expr.Create(this, Native.Z3_mk_fresh_const(nCtx, prefix, range.NativeObject)); in MkFreshConst()
859 return new BoolExpr(this, Native.Z3_mk_eq(nCtx, x.NativeObject, y.NativeObject)); in MkEq()
883 return new BoolExpr(this, Native.Z3_mk_not(nCtx, a.NativeObject)); in MkNot()
901 …return Expr.Create(this, Native.Z3_mk_ite(nCtx, t1.NativeObject, t2.NativeObject, t3.NativeObject)… in MkITE()
914 return new BoolExpr(this, Native.Z3_mk_iff(nCtx, t1.NativeObject, t2.NativeObject)); in MkIff()
927 return new BoolExpr(this, Native.Z3_mk_implies(nCtx, t1.NativeObject, t2.NativeObject)); in MkImplies()
940 return new BoolExpr(this, Native.Z3_mk_xor(nCtx, t1.NativeObject, t2.NativeObject)); in MkXor()
1082 return (ArithExpr)Expr.Create(this, Native.Z3_mk_unary_minus(nCtx, t.NativeObject)); in MkUnaryMinus()
1095 … return (ArithExpr)Expr.Create(this, Native.Z3_mk_div(nCtx, t1.NativeObject, t2.NativeObject)); in MkDiv()
1109 return new IntExpr(this, Native.Z3_mk_mod(nCtx, t1.NativeObject, t2.NativeObject)); in MkMod()
1123 return new IntExpr(this, Native.Z3_mk_rem(nCtx, t1.NativeObject, t2.NativeObject)); in MkRem()
1136 … return (ArithExpr)Expr.Create(this, Native.Z3_mk_power(nCtx, t1.NativeObject, t2.NativeObject)); in MkPower()
1149 return new BoolExpr(this, Native.Z3_mk_lt(nCtx, t1.NativeObject, t2.NativeObject)); in MkLt()
1162 return new BoolExpr(this, Native.Z3_mk_le(nCtx, t1.NativeObject, t2.NativeObject)); in MkLe()
1175 return new BoolExpr(this, Native.Z3_mk_gt(nCtx, t1.NativeObject, t2.NativeObject)); in MkGt()
1188 return new BoolExpr(this, Native.Z3_mk_ge(nCtx, t1.NativeObject, t2.NativeObject)); in MkGe()
1206 return new RealExpr(this, Native.Z3_mk_int2real(nCtx, t.NativeObject)); in MkInt2Real()
1221 return new IntExpr(this, Native.Z3_mk_real2int(nCtx, t.NativeObject)); in MkReal2Int()
1232 return new BoolExpr(this, Native.Z3_mk_is_int(nCtx, t.NativeObject)); in MkIsInteger()
1246 return new BitVecExpr(this, Native.Z3_mk_bvnot(nCtx, t.NativeObject)); in MkBVNot()
1258 return new BitVecExpr(this, Native.Z3_mk_bvredand(nCtx, t.NativeObject)); in MkBVRedAND()
1270 return new BitVecExpr(this, Native.Z3_mk_bvredor(nCtx, t.NativeObject)); in MkBVRedOR()
1284 return new BitVecExpr(this, Native.Z3_mk_bvand(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVAND()
1298 return new BitVecExpr(this, Native.Z3_mk_bvor(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVOR()
1312 return new BitVecExpr(this, Native.Z3_mk_bvxor(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVXOR()
1326 … return new BitVecExpr(this, Native.Z3_mk_bvnand(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVNAND()
1340 return new BitVecExpr(this, Native.Z3_mk_bvnor(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVNOR()
1354 … return new BitVecExpr(this, Native.Z3_mk_bvxnor(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVXNOR()
1366 return new BitVecExpr(this, Native.Z3_mk_bvneg(nCtx, t.NativeObject)); in MkBVNeg()
1380 return new BitVecExpr(this, Native.Z3_mk_bvadd(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVAdd()
1394 return new BitVecExpr(this, Native.Z3_mk_bvsub(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVSub()
1408 return new BitVecExpr(this, Native.Z3_mk_bvmul(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVMul()
1427 … return new BitVecExpr(this, Native.Z3_mk_bvudiv(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVUDiv()
1450 … return new BitVecExpr(this, Native.Z3_mk_bvsdiv(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVSDiv()
1468 … return new BitVecExpr(this, Native.Z3_mk_bvurem(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVURem()
1488 … return new BitVecExpr(this, Native.Z3_mk_bvsrem(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVSRem()
1505 … return new BitVecExpr(this, Native.Z3_mk_bvsmod(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVSMod()
1521 return new BoolExpr(this, Native.Z3_mk_bvult(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVULT()
1537 return new BoolExpr(this, Native.Z3_mk_bvslt(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVSLT()
1553 return new BoolExpr(this, Native.Z3_mk_bvule(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVULE()
1569 return new BoolExpr(this, Native.Z3_mk_bvsle(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVSLE()
1585 return new BoolExpr(this, Native.Z3_mk_bvuge(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVUGE()
1601 return new BoolExpr(this, Native.Z3_mk_bvsge(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVSGE()
1617 return new BoolExpr(this, Native.Z3_mk_bvugt(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVUGT()
1633 return new BoolExpr(this, Native.Z3_mk_bvsgt(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVSGT()
1653 … return new BitVecExpr(this, Native.Z3_mk_concat(nCtx, t1.NativeObject, t2.NativeObject)); in MkConcat()
1670 return new BitVecExpr(this, Native.Z3_mk_extract(nCtx, high, low, t.NativeObject)); in MkExtract()
1686 return new BitVecExpr(this, Native.Z3_mk_sign_ext(nCtx, i, t.NativeObject)); in MkSignExt()
1703 return new BitVecExpr(this, Native.Z3_mk_zero_ext(nCtx, i, t.NativeObject)); in MkZeroExt()
1717 return new BitVecExpr(this, Native.Z3_mk_repeat(nCtx, i, t.NativeObject)); in MkRepeat()
1739 return new BitVecExpr(this, Native.Z3_mk_bvshl(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVSHL()
1761 … return new BitVecExpr(this, Native.Z3_mk_bvlshr(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVLSHR()
1785 … return new BitVecExpr(this, Native.Z3_mk_bvashr(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVASHR()
1800 return new BitVecExpr(this, Native.Z3_mk_rotate_left(nCtx, i, t.NativeObject)); in MkBVRotateLeft()
1815 return new BitVecExpr(this, Native.Z3_mk_rotate_right(nCtx, i, t.NativeObject)); in MkBVRotateRight()
1832 … return new BitVecExpr(this, Native.Z3_mk_ext_rotate_left(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVRotateLeft()
1849 …return new BitVecExpr(this, Native.Z3_mk_ext_rotate_right(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVRotateRight()
1867 return new BitVecExpr(this, Native.Z3_mk_int2bv(nCtx, n, t.NativeObject)); in MkInt2BV()
1890 … return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (byte)(signed ? 1 : 0))); in MkBV2Int()
1906 …rn new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (byte… in MkBVAddNoOverflow()
1922 …return new BoolExpr(this, Native.Z3_mk_bvadd_no_underflow(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVAddNoUnderflow()
1938 … return new BoolExpr(this, Native.Z3_mk_bvsub_no_overflow(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVSubNoOverflow()
1954 …n new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (byte… in MkBVSubNoUnderflow()
1970 …return new BoolExpr(this, Native.Z3_mk_bvsdiv_no_overflow(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVSDivNoOverflow()
1984 return new BoolExpr(this, Native.Z3_mk_bvneg_no_overflow(nCtx, t.NativeObject)); in MkBVNegNoOverflow()
2000 …rn new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (byte… in MkBVMulNoOverflow()
2016 …return new BoolExpr(this, Native.Z3_mk_bvmul_no_underflow(nCtx, t1.NativeObject, t2.NativeObject)); in MkBVMulNoUnderflow()
2065 return Expr.Create(this, Native.Z3_mk_select(nCtx, a.NativeObject, i.NativeObject)); in MkSelect()
2088 …return Expr.Create(this, Native.Z3_mk_select_n(nCtx, a.NativeObject, AST.ArrayLength(args), AST.Ar… in MkSelect()
2119 …return new ArrayExpr(this, Native.Z3_mk_store(nCtx, a.NativeObject, i.NativeObject, v.NativeObject… in MkStore()
2149 …pr(this, Native.Z3_mk_store_n(nCtx, a.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args)… in MkStore()
2168 … return new ArrayExpr(this, Native.Z3_mk_const_array(nCtx, domain.NativeObject, v.NativeObject)); in MkConstArray()
2189 …return (ArrayExpr)Expr.Create(this, Native.Z3_mk_map(nCtx, f.NativeObject, AST.ArrayLength(args), … in MkMap()
2204 return Expr.Create(this, Native.Z3_mk_array_default(nCtx, array.NativeObject)); in MkTermArray()
2217 … return Expr.Create(this, Native.Z3_mk_array_ext(nCtx, arg1.NativeObject, arg2.NativeObject)); in MkArrayExt()
2242 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject)); in MkEmptySet()
2253 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_full_set(nCtx, domain.NativeObject)); in MkFullSet()
2266 …n (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_add(nCtx, set.NativeObject, element.NativeObject)); in MkSetAdd()
2280 …n (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_del(nCtx, set.NativeObject, element.NativeObject)); in MkSetDel()
2317 …rayExpr)Expr.Create(this, Native.Z3_mk_set_difference(nCtx, arg1.NativeObject, arg2.NativeObject)); in MkSetDifference()
2328 … return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_complement(nCtx, arg.NativeObject)); in MkSetComplement()
2341 …n (BoolExpr) Expr.Create(this, Native.Z3_mk_set_member(nCtx, elem.NativeObject, set.NativeObject)); in MkSetMembership()
2354 … (BoolExpr) Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject)); in MkSetSubset()
2367 return new SeqExpr(this, Native.Z3_mk_seq_empty(nCtx, s.NativeObject)); in MkEmptySeq()
2376 return new SeqExpr(this, Native.Z3_mk_seq_unit(nCtx, elem.NativeObject)); in MkUnit()
2395 return new SeqExpr(this, Native.Z3_mk_int_to_str(nCtx, e.NativeObject)); in IntToString()
2405 return new SeqExpr(this, Native.Z3_mk_ubv_to_str(nCtx, e.NativeObject)); in UbvToString()
2414 return new SeqExpr(this, Native.Z3_mk_sbv_to_str(nCtx, e.NativeObject)); in SbvToString()
2424 return new IntExpr(this, Native.Z3_mk_str_to_int(nCtx, e.NativeObject)); in StringToInt()
2447 return (IntExpr) Expr.Create(this, Native.Z3_mk_seq_length(nCtx, s.NativeObject)); in MkLength()
2458 … return new BoolExpr(this, Native.Z3_mk_seq_prefix(nCtx, s1.NativeObject, s2.NativeObject)); in MkPrefixOf()
2469 … return new BoolExpr(this, Native.Z3_mk_seq_suffix(nCtx, s1.NativeObject, s2.NativeObject)); in MkSuffixOf()
2480 … return new BoolExpr(this, Native.Z3_mk_seq_contains(nCtx, s1.NativeObject, s2.NativeObject)); in MkContains()
2491 return new BoolExpr(this, Native.Z3_mk_str_lt(nCtx, s1.NativeObject, s2.NativeObject)); in MkStringLt()
2502 return new BoolExpr(this, Native.Z3_mk_str_le(nCtx, s1.NativeObject, s2.NativeObject)); in MkStringLe()
2513 return new SeqExpr(this, Native.Z3_mk_seq_at(nCtx, s.NativeObject, index.NativeObject)); in MkAt()
2524 … return Expr.Create(this, Native.Z3_mk_seq_nth(nCtx, s.NativeObject, index.NativeObject)); in MkNth()
2536 …w SeqExpr(this, Native.Z3_mk_seq_extract(nCtx, s.NativeObject, offset.NativeObject, length.NativeO… in MkExtract()
2548 …new IntExpr(this, Native.Z3_mk_seq_index(nCtx, s.NativeObject, substr.NativeObject, offset.NativeO… in MkIndexOf()
2560 … new SeqExpr(this, Native.Z3_mk_seq_replace(nCtx, s.NativeObject, src.NativeObject, dst.NativeObje… in MkReplace()
2569 return new ReExpr(this, Native.Z3_mk_seq_to_re(nCtx, s.NativeObject)); in MkToRe()
2581 …return new BoolExpr(this, Native.Z3_mk_seq_in_re(nCtx, s.NativeObject, re.NativeObject)); … in MkInRe()
2590 return new ReExpr(this, Native.Z3_mk_re_star(nCtx, re.NativeObject)); in MkStar()
2599 … return new ReExpr(this, Native.Z3_mk_re_loop(nCtx, re.NativeObject, lo, hi)); in MkLoop()
2608 return new ReExpr(this, Native.Z3_mk_re_plus(nCtx, re.NativeObject)); in MkPlus()
2617 return new ReExpr(this, Native.Z3_mk_re_option(nCtx, re.NativeObject)); in MkOption()
2626 return new ReExpr(this, Native.Z3_mk_re_complement(nCtx, re.NativeObject)); in MkComplement()
2672 return new ReExpr(this, Native.Z3_mk_re_empty(nCtx, s.NativeObject)); in MkEmptyRe()
2682 return new ReExpr(this, Native.Z3_mk_re_full(nCtx, s.NativeObject)); in MkFullRe()
2694 return new ReExpr(this, Native.Z3_mk_re_range(nCtx, lo.NativeObject, hi.NativeObject)); in MkRange()
2704 … return new BoolExpr(this, Native.Z3_mk_char_le(nCtx, ch1.NativeObject, ch2.NativeObject)); in MkCharLe()
2713 return new IntExpr(this, Native.Z3_mk_char_to_int(nCtx, ch.NativeObject)); in CharToInt()
2722 return new BitVecExpr(this, Native.Z3_mk_char_to_bv(nCtx, ch.NativeObject)); in CharToBV()
2731 return new Expr(this, Native.Z3_mk_char_from_bv(nCtx, bv.NativeObject)); in CharFromBV()
2740 return new BoolExpr(this, Native.Z3_mk_char_is_digit(nCtx, ch.NativeObject)); in MkIsDigit()
2825 return Expr.Create(this, Native.Z3_mk_numeral(nCtx, v, ty.NativeObject)); in MkNumeral()
2840 return Expr.Create(this, Native.Z3_mk_int(nCtx, v, ty.NativeObject)); in MkNumeral()
2855 return Expr.Create(this, Native.Z3_mk_unsigned_int(nCtx, v, ty.NativeObject)); in MkNumeral()
2870 return Expr.Create(this, Native.Z3_mk_int64(nCtx, v, ty.NativeObject)); in MkNumeral()
2885 return Expr.Create(this, Native.Z3_mk_unsigned_int64(nCtx, v, ty.NativeObject)); in MkNumeral()
2913 return new RatNum(this, Native.Z3_mk_numeral(nCtx, v, RealSort.NativeObject)); in MkReal()
2924 return new RatNum(this, Native.Z3_mk_int(nCtx, v, RealSort.NativeObject)); in MkReal()
2935 return new RatNum(this, Native.Z3_mk_unsigned_int(nCtx, v, RealSort.NativeObject)); in MkReal()
2946 return new RatNum(this, Native.Z3_mk_int64(nCtx, v, RealSort.NativeObject)); in MkReal()
2957 return new RatNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, RealSort.NativeObject)); in MkReal()
2969 return new IntNum(this, Native.Z3_mk_numeral(nCtx, v, IntSort.NativeObject)); in MkInt()
2980 return new IntNum(this, Native.Z3_mk_int(nCtx, v, IntSort.NativeObject)); in MkInt()
2991 return new IntNum(this, Native.Z3_mk_unsigned_int(nCtx, v, IntSort.NativeObject)); in MkInt()
3002 return new IntNum(this, Native.Z3_mk_int64(nCtx, v, IntSort.NativeObject)); in MkInt()
3013 return new IntNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, IntSort.NativeObject)); in MkInt()
3433 last = ts[ts.Length - 1].NativeObject; in AndThen()
3435 last = Native.Z3_tactic_and_then(nCtx, ts[i].NativeObject, last); in AndThen()
3439 last = Native.Z3_tactic_and_then(nCtx, t2.NativeObject, last); in AndThen()
3440 return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, last)); in AndThen()
3443 … return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, t2.NativeObject)); in AndThen()
3473 … return new Tactic(this, Native.Z3_tactic_or_else(nCtx, t1.NativeObject, t2.NativeObject)); in OrElse()
3487 return new Tactic(this, Native.Z3_tactic_try_for(nCtx, t.NativeObject, ms)); in TryFor()
3504 return new Tactic(this, Native.Z3_tactic_when(nCtx, p.NativeObject, t.NativeObject)); in When()
3520 …eturn new Tactic(this, Native.Z3_tactic_cond(nCtx, p.NativeObject, t1.NativeObject, t2.NativeObjec… in Cond()
3532 return new Tactic(this, Native.Z3_tactic_repeat(nCtx, t.NativeObject, max)); in Repeat()
3561 return new Tactic(this, Native.Z3_tactic_fail_if(nCtx, p.NativeObject)); in FailIf()
3584 … return new Tactic(this, Native.Z3_tactic_using_params(nCtx, t.NativeObject, p.NativeObject)); in UsingParams()
3621 … return new Tactic(this, Native.Z3_tactic_par_and_then(nCtx, t1.NativeObject, t2.NativeObject)); in ParAndThen()
3697 return new Probe(this, Native.Z3_probe_lt(nCtx, p1.NativeObject, p2.NativeObject)); in Lt()
3711 return new Probe(this, Native.Z3_probe_gt(nCtx, p1.NativeObject, p2.NativeObject)); in Gt()
3725 return new Probe(this, Native.Z3_probe_le(nCtx, p1.NativeObject, p2.NativeObject)); in Le()
3739 return new Probe(this, Native.Z3_probe_ge(nCtx, p1.NativeObject, p2.NativeObject)); in Ge()
3753 return new Probe(this, Native.Z3_probe_eq(nCtx, p1.NativeObject, p2.NativeObject)); in Eq()
3767 return new Probe(this, Native.Z3_probe_and(nCtx, p1.NativeObject, p2.NativeObject)); in And()
3781 return new Probe(this, Native.Z3_probe_or(nCtx, p1.NativeObject, p2.NativeObject)); in Or()
3793 return new Probe(this, Native.Z3_probe_not(nCtx, p.NativeObject)); in Not()
3812 return new Solver(this, Native.Z3_mk_solver_for_logic(nCtx, logic.NativeObject)); in MkSolver()
3845 return new Solver(this, Native.Z3_mk_solver_from_tactic(nCtx, t.NativeObject)); in MkSolver()
4050 return new FPNum(this, Native.Z3_mk_fpa_nan(nCtx, s.NativeObject)); in MkFPNaN()
4060 … return new FPNum(this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, (byte)(negative ? 1 : 0))); in MkFPInf()
4070 … return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, (byte)(negative ? 1 : 0))); in MkFPZero()
4080 return new FPNum(this, Native.Z3_mk_fpa_numeral_float(nCtx, v, s.NativeObject)); in MkFPNumeral()
4090 return new FPNum(this, Native.Z3_mk_fpa_numeral_double(nCtx, v, s.NativeObject)); in MkFPNumeral()
4100 return new FPNum(this, Native.Z3_mk_fpa_numeral_int(nCtx, v, s.NativeObject)); in MkFPNumeral()
4112 …Num(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, (byte)(sgn ? 1 : 0), exp, sig, s.NativeObject)); in MkFPNumeral()
4124 …this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, (byte)(sgn ? 1 : 0), exp, sig, s.NativeObject)); in MkFPNumeral()
4190 return new FPExpr(this, Native.Z3_mk_fpa_abs(this.nCtx, t.NativeObject)); in MkFPAbs()
4199 return new FPExpr(this, Native.Z3_mk_fpa_neg(this.nCtx, t.NativeObject)); in MkFPNeg()
4210 … new FPExpr(this, Native.Z3_mk_fpa_add(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObjec… in MkFPAdd()
4221 … new FPExpr(this, Native.Z3_mk_fpa_sub(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObjec… in MkFPSub()
4232 … new FPExpr(this, Native.Z3_mk_fpa_mul(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObjec… in MkFPMul()
4243 … new FPExpr(this, Native.Z3_mk_fpa_div(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObjec… in MkFPDiv()
4258 …xpr(this, Native.Z3_mk_fpa_fma(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject, t3.Na… in MkFPFMA()
4268 … return new FPExpr(this, Native.Z3_mk_fpa_sqrt(this.nCtx, rm.NativeObject, t.NativeObject)); in MkFPSqrt()
4278 … return new FPExpr(this, Native.Z3_mk_fpa_rem(this.nCtx, t1.NativeObject, t2.NativeObject)); in MkFPRem()
4289 …n new FPExpr(this, Native.Z3_mk_fpa_round_to_integral(this.nCtx, rm.NativeObject, t.NativeObject)); in MkFPRoundToIntegral()
4299 … return new FPExpr(this, Native.Z3_mk_fpa_min(this.nCtx, t1.NativeObject, t2.NativeObject)); in MkFPMin()
4309 … return new FPExpr(this, Native.Z3_mk_fpa_max(this.nCtx, t1.NativeObject, t2.NativeObject)); in MkFPMax()
4319 … return new BoolExpr(this, Native.Z3_mk_fpa_leq(this.nCtx, t1.NativeObject, t2.NativeObject)); in MkFPLEq()
4329 … return new BoolExpr(this, Native.Z3_mk_fpa_lt(this.nCtx, t1.NativeObject, t2.NativeObject)); in MkFPLt()
4339 … return new BoolExpr(this, Native.Z3_mk_fpa_geq(this.nCtx, t1.NativeObject, t2.NativeObject)); in MkFPGEq()
4349 … return new BoolExpr(this, Native.Z3_mk_fpa_gt(this.nCtx, t1.NativeObject, t2.NativeObject)); in MkFPGt()
4362 … return new BoolExpr(this, Native.Z3_mk_fpa_eq(this.nCtx, t1.NativeObject, t2.NativeObject)); in MkFPEq()
4371 return new BoolExpr(this, Native.Z3_mk_fpa_is_normal(this.nCtx, t.NativeObject)); in MkFPIsNormal()
4380 return new BoolExpr(this, Native.Z3_mk_fpa_is_subnormal(this.nCtx, t.NativeObject)); in MkFPIsSubnormal()
4389 return new BoolExpr(this, Native.Z3_mk_fpa_is_zero(this.nCtx, t.NativeObject)); in MkFPIsZero()
4398 return new BoolExpr(this, Native.Z3_mk_fpa_is_infinite(this.nCtx, t.NativeObject)); in MkFPIsInfinite()
4407 return new BoolExpr(this, Native.Z3_mk_fpa_is_nan(this.nCtx, t.NativeObject)); in MkFPIsNaN()
4416 return new BoolExpr(this, Native.Z3_mk_fpa_is_negative(this.nCtx, t.NativeObject)); in MkFPIsNegative()
4425 return new BoolExpr(this, Native.Z3_mk_fpa_is_positive(this.nCtx, t.NativeObject)); in MkFPIsPositive()
4445 …new FPExpr(this, Native.Z3_mk_fpa_fp(this.nCtx, sgn.NativeObject, sig.NativeObject, exp.NativeObje… in MkFP()
4461 … return new FPExpr(this, Native.Z3_mk_fpa_to_fp_bv(this.nCtx, bv.NativeObject, s.NativeObject)); in MkFPToFP()
4477 …Expr(this, Native.Z3_mk_fpa_to_fp_float(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject… in MkFPToFP()
4493 …PExpr(this, Native.Z3_mk_fpa_to_fp_real(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject… in MkFPToFP()
4512 …xpr(this, Native.Z3_mk_fpa_to_fp_signed(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject… in MkFPToFP()
4514 …r(this, Native.Z3_mk_fpa_to_fp_unsigned(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject… in MkFPToFP()
4529 …PExpr(this, Native.Z3_mk_fpa_to_fp_float(this.nCtx, s.NativeObject, rm.NativeObject, t.NativeObjec… in MkFPToFP()
4549 …turn new BitVecExpr(this, Native.Z3_mk_fpa_to_sbv(this.nCtx, rm.NativeObject, t.NativeObject, sz)); in MkFPToBV()
4551 …turn new BitVecExpr(this, Native.Z3_mk_fpa_to_ubv(this.nCtx, rm.NativeObject, t.NativeObject, sz)); in MkFPToBV()
4565 return new RealExpr(this, Native.Z3_mk_fpa_to_real(this.nCtx, t.NativeObject)); in MkFPToReal()
4582 return new BitVecExpr(this, Native.Z3_mk_fpa_to_ieee_bv(this.nCtx, t.NativeObject)); in MkFPToIEEEBV()
4599 …tive.Z3_mk_fpa_to_fp_int_real(this.nCtx, rm.NativeObject, exp.NativeObject, sig.NativeObject, s.Na… in MkFPToFP()
4633 return a.NativeObject; in UnwrapAST()