NativeObject (reference) in projects: dports

Project(s)

Full Search
Definition
Symbol
File Path
History
Type

Searched refs:NativeObject (Results 1 – 25 of 1188) sorted by relevance

12 3 4 5 6 7 8 9 10 >>...48

/dports/math/z3/z3-z3-4.8.13/src/api/dotnet/
H A D	Params.cs	37 … Native.Z3_params_set_bool(Context.nCtx, NativeObject, name.NativeObject, (byte)(value ? 1 : 0)); in Add() 48 Native.Z3_params_set_uint(Context.nCtx, NativeObject, name.NativeObject, value); in Add() 59 Native.Z3_params_set_double(Context.nCtx, NativeObject, name.NativeObject, value); in Add() 70 …Native.Z3_params_set_symbol(Context.nCtx, NativeObject, name.NativeObject, Context.MkSymbol(value)… in Add() 82 … Native.Z3_params_set_symbol(Context.nCtx, NativeObject, name.NativeObject, value.NativeObject); in Add() 92 …Native.Z3_params_set_bool(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, (byte)(… in Add() 101 … Native.Z3_params_set_uint(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value); in Add() 110 …Native.Z3_params_set_double(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value… in Add() 121 …Native.Z3_params_set_symbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value… in Add() 133 …_params_set_symbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, Context.MkSymb… in Add() [all …]
H A D	Fixedpoint.cs	39 return Native.Z3_fixedpoint_get_help(Context.nCtx, NativeObject); 52 Native.Z3_fixedpoint_set_params(Context.nCtx, NativeObject, value.NativeObject); 76 Native.Z3_fixedpoint_assert(Context.nCtx, NativeObject, a.NativeObject); in Assert() 96 Native.Z3_fixedpoint_register_relation(Context.nCtx, NativeObject, f.NativeObject); in RegisterRelation() 107 …Native.Z3_fixedpoint_add_rule(Context.nCtx, NativeObject, rule.NativeObject, AST.GetNativeObject(n… in AddRule() 119 …Native.Z3_fixedpoint_add_fact(Context.nCtx, NativeObject, pred.NativeObject, (uint)args.Length, ar… in AddFact() 133 … Z3_lbool r = (Z3_lbool)Native.Z3_fixedpoint_query(Context.nCtx, NativeObject, query.NativeObject); in Query() 172 …Native.Z3_fixedpoint_update_rule(Context.nCtx, NativeObject, rule.NativeObject, AST.GetNativeObjec… in UpdateRule() 199 … return Native.Z3_fixedpoint_get_num_levels(Context.nCtx, NativeObject, predicate.NativeObject); in GetNumLevels() 207 …s = Native.Z3_fixedpoint_get_cover_delta(Context.nCtx, NativeObject, level, predicate.NativeObject… in GetCoverDelta() [all …]
H A D	Context.cs	493 t.NativeObject, v.NativeObject)); in MkUpdateField() 901 …return Expr.Create(this, Native.Z3_mk_ite(nCtx, t1.NativeObject, t2.NativeObject, t3.NativeObject)… in MkITE() 2119 …return new ArrayExpr(this, Native.Z3_mk_store(nCtx, a.NativeObject, i.NativeObject, v.NativeObject… in MkStore() 2560 … new SeqExpr(this, Native.Z3_mk_seq_replace(nCtx, s.NativeObject, src.NativeObject, dst.NativeObje… in MkReplace() 3520 …eturn new Tactic(this, Native.Z3_tactic_cond(nCtx, p.NativeObject, t1.NativeObject, t2.NativeObjec… in Cond() 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() [all …]
H A D	Solver.cs	54 Native.Z3_solver_set_params(Context.nCtx, NativeObject, value.NativeObject); 126 Native.Z3_solver_push(Context.nCtx, NativeObject); in Push() 136 Native.Z3_solver_pop(Context.nCtx, NativeObject, n); in Pop() 145 Native.Z3_solver_reset(Context.nCtx, NativeObject); in Reset() 159 Native.Z3_solver_assert(Context.nCtx, NativeObject, a.NativeObject); in Assert() 201 …tive.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraints[i].NativeObject, ps[i].Nat… in AssertAndTrack() 222 …Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraint.NativeObject, p.NativeObj… in AssertAndTrack() 230 Native.Z3_solver_from_file(Context.nCtx, NativeObject, file); in FromFile() 338 …Z3_solver_get_consequences(Context.nCtx, NativeObject, asms.NativeObject, vars.NativeObject, resul… in Consequences() 434 … = new ASTVector(Context, Native.Z3_solver_cube(Context.nCtx, NativeObject, cv.NativeObject, lvl)); in Cube() [all …]
H A D	FPNum.cs	39 … return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_sign_bv(Context.nCtx, NativeObject)); 54 if (Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref res) == 0) 71 return Native.Z3_fpa_get_numeral_significand_string(Context.nCtx, NativeObject); 88 … if (Native.Z3_fpa_get_numeral_significand_uint64(Context.nCtx, NativeObject, ref result) == 0) 104 …turn new BitVecExpr(Context, Native.Z3_fpa_get_numeral_significand_bv(Context.nCtx, NativeObject)); 113 …return Native.Z3_fpa_get_numeral_exponent_string(Context.nCtx, NativeObject, (byte)(biased ? 1 : 0… in Exponent() 141 …public bool IsNaN { get { return Native.Z3_fpa_is_numeral_nan(Context.nCtx, NativeObject) != 0; } } 146 …public bool IsInf { get { return Native.Z3_fpa_is_numeral_inf(Context.nCtx, NativeObject) != 0; } } 151 …public bool IsZero{ get { return Native.Z3_fpa_is_numeral_zero(Context.nCtx, NativeObject) != 0; }… 156 … bool IsNormal { get { return Native.Z3_fpa_is_numeral_normal(Context.nCtx, NativeObject) != 0; } } [all …]
H A D	Optimize.cs	39 return Native.Z3_optimize_get_help(Context.nCtx, NativeObject); 52 Native.Z3_optimize_set_params(Context.nCtx, NativeObject, value.NativeObject); 148 Native.Z3_optimize_assert(Context.nCtx, NativeObject, a.NativeObject); in AddConstraints() 216 …e.Z3_optimize_assert_soft(Context.nCtx, NativeObject, constraint.NativeObject, weight.ToString(), … in AssertSoft() 246 Native.Z3_optimize_push(Context.nCtx, NativeObject); in Push() 256 Native.Z3_optimize_pop(Context.nCtx, NativeObject); in Pop() 305 … return new Handle(this, Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject)); in MkMaximize() 314 … return new Handle(this, Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject)); in MkMinimize() 371 return Native.Z3_optimize_to_string(Context.nCtx, NativeObject); in ToString() 380 Native.Z3_optimize_from_file(Context.nCtx, NativeObject, file); in FromFile() [all …]
H A D	Model.cs	57 IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject); in ConstInterp() 79 … IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject); in FuncInterp() 100 … IntPtr n = Native.Z3_model_get_func_interp(Context.nCtx, NativeObject, f.NativeObject); in FuncInterp() 113 get { return Native.Z3_model_get_num_consts(Context.nCtx, NativeObject); } 143 … IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject); 155 get { return Native.Z3_model_get_num_funcs(Context.nCtx, NativeObject); } 224 …if (Native.Z3_model_eval(Context.nCtx, NativeObject, t.NativeObject, (byte)(completion ? 1 : 0), r… in Eval() 245 return Native.Z3_get_numeral_double(Context.nCtx, r.NativeObject); in Double() 251 … public uint NumSorts { get { return Native.Z3_model_get_num_sorts(Context.nCtx, NativeObject); } } 286 …ctor(Context, Native.Z3_model_get_sort_universe(Context.nCtx, NativeObject, s.NativeObject)); … in SortUniverse() [all …]
H A D	ASTVector.cs	35 get { return Native.Z3_ast_vector_size(Context.nCtx, NativeObject); } 55 Native.Z3_ast_vector_set(Context.nCtx, NativeObject, i, value.NativeObject); 65 Native.Z3_ast_vector_resize(Context.nCtx, NativeObject, newSize); in Resize() 77 Native.Z3_ast_vector_push(Context.nCtx, NativeObject, a.NativeObject); in Push() 97 return Native.Z3_ast_vector_to_string(Context.nCtx, NativeObject); in ToString() 108 res[i] = AST.Create(this.Context, this[i].NativeObject); in ToArray() 120 res[i] = Expr.Create(this.Context, this[i].NativeObject); in ToExprArray() 132 res[i] = (BoolExpr) Expr.Create(this.Context, this[i].NativeObject); in ToBoolExprArray() 192 res[i] = (FPExpr)Expr.Create(this.Context, this[i].NativeObject); in ToFPExprArray() 204 res[i] = (FPRMExpr)Expr.Create(this.Context, this[i].NativeObject); in ToFPRMExprArray() [all …]
H A D	Goal.cs	43 get { return (Z3_goal_prec)Native.Z3_goal_precision(Context.nCtx, NativeObject); } 89 Native.Z3_goal_assert(Context.nCtx, NativeObject, c.NativeObject); in Assert() 106 get { return Native.Z3_goal_inconsistent(Context.nCtx, NativeObject) != 0; } 117 get { return Native.Z3_goal_depth(Context.nCtx, NativeObject); } 125 Native.Z3_goal_reset(Context.nCtx, NativeObject); in Reset() 133 get { return Native.Z3_goal_size(Context.nCtx, NativeObject); } 157 get { return Native.Z3_goal_num_exprs(Context.nCtx, NativeObject); } 165 get { return Native.Z3_goal_is_decided_sat(Context.nCtx, NativeObject) != 0; } 173 get { return Native.Z3_goal_is_decided_unsat(Context.nCtx, NativeObject) != 0; } 184 …eturn new Model(Context, Native.Z3_goal_convert_model(Context.nCtx, NativeObject, m.NativeObject)); in ConvertModel() [all …]
H A D	ASTMap.cs	39 return 0 != Native.Z3_ast_map_contains(Context.nCtx, NativeObject, k.NativeObject); in Contains() 53 … return new AST(Context, Native.Z3_ast_map_find(Context.nCtx, NativeObject, k.NativeObject)); in Find() 66 Native.Z3_ast_map_insert(Context.nCtx, NativeObject, k.NativeObject, v.NativeObject); in Insert() 77 Native.Z3_ast_map_erase(Context.nCtx, NativeObject, k.NativeObject); in Erase() 85 Native.Z3_ast_map_reset(Context.nCtx, NativeObject); in Reset() 93 get { return Native.Z3_ast_map_size(Context.nCtx, NativeObject); } 103 … ASTVector res = new ASTVector(Context, Native.Z3_ast_map_keys(Context.nCtx, NativeObject)); 113 return Native.Z3_ast_map_to_string(Context.nCtx, NativeObject); in ToString()
H A D	FuncDecl.cs	42 Native.Z3_is_eq_func_decl(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0); in operator ==() 77 return Native.Z3_func_decl_to_string(Context.nCtx, NativeObject); in ToString() 85 get { return Native.Z3_get_func_decl_id(Context.nCtx, NativeObject); } 93 get { return Native.Z3_get_arity(Context.nCtx, NativeObject); } 102 get { return Native.Z3_get_domain_size(Context.nCtx, NativeObject); } 129 return Sort.Create(Context, Native.Z3_get_range(Context.nCtx, NativeObject)); 138 get { return (Z3_decl_kind)Native.Z3_get_decl_kind(Context.nCtx, NativeObject); } 148 return Symbol.Create(Context, Native.Z3_get_decl_name(Context.nCtx, NativeObject)); 157 get { return Native.Z3_get_decl_num_parameters(Context.nCtx, NativeObject); } 291 …ve.Z3_mk_func_decl(ctx.nCtx, name.NativeObject, AST.ArrayLength(domain), AST.ArrayToNative(domain)… in FuncDecl() [all …]
H A D	Quantifier.cs	36 get { return 0 != Native.Z3_is_quantifier_forall(Context.nCtx, NativeObject); } 44 get { return 0 != Native.Z3_is_quantifier_exists(Context.nCtx, NativeObject); } 52 get { return Native.Z3_get_quantifier_weight(Context.nCtx, NativeObject); } 60 get { return Native.Z3_get_quantifier_num_patterns(Context.nCtx, NativeObject); } 84 get { return Native.Z3_get_quantifier_num_no_patterns(Context.nCtx, NativeObject); } 108 get { return Native.Z3_get_quantifier_num_bound(Context.nCtx, NativeObject); } 190 NativeObject = Native.Z3_mk_quantifier(ctx.nCtx, (byte)(isForall ? 1 : 0) , weight, in Quantifier() 194 body.NativeObject); in Quantifier() 204 body.NativeObject); in Quantifier() 228 body.NativeObject); in Quantifier() [all …]
/dports/math/py-z3-solver/z3-z3-4.8.10/src/api/dotnet/
H A D	Params.cs	37 … Native.Z3_params_set_bool(Context.nCtx, NativeObject, name.NativeObject, (byte)(value ? 1 : 0)); in gen_random() 48 Native.Z3_params_set_uint(Context.nCtx, NativeObject, name.NativeObject, value); in gen_random() 59 Native.Z3_params_set_double(Context.nCtx, NativeObject, name.NativeObject, value); in gen_random() 70 …Native.Z3_params_set_symbol(Context.nCtx, NativeObject, name.NativeObject, Context.MkSymbol(value)… in gen_random() 82 … Native.Z3_params_set_symbol(Context.nCtx, NativeObject, name.NativeObject, value.NativeObject); in gen_random() 92 …Native.Z3_params_set_bool(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, (byte)(… in gen_random() 101 … Native.Z3_params_set_uint(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value); in gen_random() 110 …Native.Z3_params_set_double(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value… in gen_random() 121 …Native.Z3_params_set_symbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value… in gen_random() 133 …_params_set_symbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, Context.MkSymb… in gen_random() [all …]
H A D	Fixedpoint.cs	39 return Native.Z3_fixedpoint_get_help(Context.nCtx, NativeObject); 52 Native.Z3_fixedpoint_set_params(Context.nCtx, NativeObject, value.NativeObject); 76 Native.Z3_fixedpoint_assert(Context.nCtx, NativeObject, a.NativeObject); in Assert() 96 Native.Z3_fixedpoint_register_relation(Context.nCtx, NativeObject, f.NativeObject); in RegisterRelation() 107 …Native.Z3_fixedpoint_add_rule(Context.nCtx, NativeObject, rule.NativeObject, AST.GetNativeObject(n… in AddRule() 119 …Native.Z3_fixedpoint_add_fact(Context.nCtx, NativeObject, pred.NativeObject, (uint)args.Length, ar… in AddFact() 133 … Z3_lbool r = (Z3_lbool)Native.Z3_fixedpoint_query(Context.nCtx, NativeObject, query.NativeObject); in Query() 172 …Native.Z3_fixedpoint_update_rule(Context.nCtx, NativeObject, rule.NativeObject, AST.GetNativeObjec… in UpdateRule() 199 … return Native.Z3_fixedpoint_get_num_levels(Context.nCtx, NativeObject, predicate.NativeObject); in GetNumLevels() 207 …s = Native.Z3_fixedpoint_get_cover_delta(Context.nCtx, NativeObject, level, predicate.NativeObject… in GetCoverDelta() [all …]
H A D	Context.cs	483 t.NativeObject, v.NativeObject)); in MkUpdateField() 891 …return Expr.Create(this, Native.Z3_mk_ite(nCtx, t1.NativeObject, t2.NativeObject, t3.NativeObject)… in MkITE() 2109 …return new ArrayExpr(this, Native.Z3_mk_store(nCtx, a.NativeObject, i.NativeObject, v.NativeObject… in MkStore() 2531 … new SeqExpr(this, Native.Z3_mk_seq_replace(nCtx, s.NativeObject, src.NativeObject, dst.NativeObje… in MkReplace() 3445 …eturn new Tactic(this, Native.Z3_tactic_cond(nCtx, p.NativeObject, t1.NativeObject, t2.NativeObjec… in Cond() 4135 … new FPExpr(this, Native.Z3_mk_fpa_add(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObjec… in MkFPAdd() 4146 … new FPExpr(this, Native.Z3_mk_fpa_sub(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObjec… in MkFPSub() 4157 … new FPExpr(this, Native.Z3_mk_fpa_mul(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObjec… in MkFPMul() 4168 … new FPExpr(this, Native.Z3_mk_fpa_div(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObjec… in MkFPDiv() 4183 …xpr(this, Native.Z3_mk_fpa_fma(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject, t3.Na… in MkFPFMA() [all …]
H A D	Solver.cs	54 Native.Z3_solver_set_params(Context.nCtx, NativeObject, value.NativeObject); 126 Native.Z3_solver_push(Context.nCtx, NativeObject); 136 Native.Z3_solver_pop(Context.nCtx, NativeObject, n); 145 Native.Z3_solver_reset(Context.nCtx, NativeObject); 159 Native.Z3_solver_assert(Context.nCtx, NativeObject, a.NativeObject); 201 …tive.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraints[i].NativeObject, ps[i].Nat… 222 …Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraint.NativeObject, p.NativeObj… 230 Native.Z3_solver_from_file(Context.nCtx, NativeObject, file); 338 …Z3_solver_get_consequences(Context.nCtx, NativeObject, asms.NativeObject, vars.NativeObject, resul… 434 … = new ASTVector(Context, Native.Z3_solver_cube(Context.nCtx, NativeObject, cv.NativeObject, lvl)); [all …]
H A D	FPNum.cs	39 … return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_sign_bv(Context.nCtx, NativeObject)); 54 if (Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref res) == 0) 71 return Native.Z3_fpa_get_numeral_significand_string(Context.nCtx, NativeObject); 88 … if (Native.Z3_fpa_get_numeral_significand_uint64(Context.nCtx, NativeObject, ref result) == 0) 104 …turn new BitVecExpr(Context, Native.Z3_fpa_get_numeral_significand_bv(Context.nCtx, NativeObject)); 113 …return Native.Z3_fpa_get_numeral_exponent_string(Context.nCtx, NativeObject, (byte)(biased ? 1 : 0… in Exponent() 141 …public bool IsNaN { get { return Native.Z3_fpa_is_numeral_nan(Context.nCtx, NativeObject) != 0; } } 146 …public bool IsInf { get { return Native.Z3_fpa_is_numeral_inf(Context.nCtx, NativeObject) != 0; } } 151 …public bool IsZero{ get { return Native.Z3_fpa_is_numeral_zero(Context.nCtx, NativeObject) != 0; }… 156 … bool IsNormal { get { return Native.Z3_fpa_is_numeral_normal(Context.nCtx, NativeObject) != 0; } } [all …]
H A D	Optimize.cs	39 return Native.Z3_optimize_get_help(Context.nCtx, NativeObject); 52 Native.Z3_optimize_set_params(Context.nCtx, NativeObject, value.NativeObject); 148 Native.Z3_optimize_assert(Context.nCtx, NativeObject, a.NativeObject); 216 …e.Z3_optimize_assert_soft(Context.nCtx, NativeObject, constraint.NativeObject, weight.ToString(), … 246 Native.Z3_optimize_push(Context.nCtx, NativeObject); 256 Native.Z3_optimize_pop(Context.nCtx, NativeObject); 305 … return new Handle(this, Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject)); 314 … return new Handle(this, Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject)); 371 return Native.Z3_optimize_to_string(Context.nCtx, NativeObject); 380 Native.Z3_optimize_from_file(Context.nCtx, NativeObject, file); [all …]
H A D	Model.cs	57 IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject); in ConstInterp() 79 … IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject); in FuncInterp() 100 … IntPtr n = Native.Z3_model_get_func_interp(Context.nCtx, NativeObject, f.NativeObject); in FuncInterp() 113 get { return Native.Z3_model_get_num_consts(Context.nCtx, NativeObject); } 143 … IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject); 155 get { return Native.Z3_model_get_num_funcs(Context.nCtx, NativeObject); } 224 …if (Native.Z3_model_eval(Context.nCtx, NativeObject, t.NativeObject, (byte)(completion ? 1 : 0), r… in Eval() 245 return Native.Z3_get_numeral_double(Context.nCtx, r.NativeObject); in Double() 251 … public uint NumSorts { get { return Native.Z3_model_get_num_sorts(Context.nCtx, NativeObject); } } 286 …ctor(Context, Native.Z3_model_get_sort_universe(Context.nCtx, NativeObject, s.NativeObject)); … in SortUniverse() [all …]
H A D	ASTVector.cs	35 get { return Native.Z3_ast_vector_size(Context.nCtx, NativeObject); } 55 Native.Z3_ast_vector_set(Context.nCtx, NativeObject, i, value.NativeObject); 65 Native.Z3_ast_vector_resize(Context.nCtx, NativeObject, newSize); in Resize() 77 Native.Z3_ast_vector_push(Context.nCtx, NativeObject, a.NativeObject); in Push() 97 return Native.Z3_ast_vector_to_string(Context.nCtx, NativeObject); in ToString() 108 res[i] = AST.Create(this.Context, this[i].NativeObject); in ToArray() 120 res[i] = Expr.Create(this.Context, this[i].NativeObject); in ToExprArray() 132 res[i] = (BoolExpr) Expr.Create(this.Context, this[i].NativeObject); in ToBoolExprArray() 192 res[i] = (FPExpr)Expr.Create(this.Context, this[i].NativeObject); in ToFPExprArray() 204 res[i] = (FPRMExpr)Expr.Create(this.Context, this[i].NativeObject); in ToFPRMExprArray() [all …]
H A D	Goal.cs	43 get { return (Z3_goal_prec)Native.Z3_goal_precision(Context.nCtx, NativeObject); } 89 Native.Z3_goal_assert(Context.nCtx, NativeObject, c.NativeObject); 106 get { return Native.Z3_goal_inconsistent(Context.nCtx, NativeObject) != 0; } 117 get { return Native.Z3_goal_depth(Context.nCtx, NativeObject); } 125 Native.Z3_goal_reset(Context.nCtx, NativeObject); 133 get { return Native.Z3_goal_size(Context.nCtx, NativeObject); } 157 get { return Native.Z3_goal_num_exprs(Context.nCtx, NativeObject); } 165 get { return Native.Z3_goal_is_decided_sat(Context.nCtx, NativeObject) != 0; } 173 get { return Native.Z3_goal_is_decided_unsat(Context.nCtx, NativeObject) != 0; } 184 …eturn new Model(Context, Native.Z3_goal_convert_model(Context.nCtx, NativeObject, m.NativeObject)); [all …]
H A D	ASTMap.cs	39 return 0 != Native.Z3_ast_map_contains(Context.nCtx, NativeObject, k.NativeObject); in Contains() 53 … return new AST(Context, Native.Z3_ast_map_find(Context.nCtx, NativeObject, k.NativeObject)); in Find() 66 Native.Z3_ast_map_insert(Context.nCtx, NativeObject, k.NativeObject, v.NativeObject); in Insert() 77 Native.Z3_ast_map_erase(Context.nCtx, NativeObject, k.NativeObject); in Erase() 85 Native.Z3_ast_map_reset(Context.nCtx, NativeObject); in Reset() 93 get { return Native.Z3_ast_map_size(Context.nCtx, NativeObject); } 103 … ASTVector res = new ASTVector(Context, Native.Z3_ast_map_keys(Context.nCtx, NativeObject)); 113 return Native.Z3_ast_map_to_string(Context.nCtx, NativeObject); in ToString()
H A D	FuncDecl.cs	42 Native.Z3_is_eq_func_decl(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0); in operator ==() 77 return Native.Z3_func_decl_to_string(Context.nCtx, NativeObject); in ToString() 85 get { return Native.Z3_get_func_decl_id(Context.nCtx, NativeObject); } 93 get { return Native.Z3_get_arity(Context.nCtx, NativeObject); } 102 get { return Native.Z3_get_domain_size(Context.nCtx, NativeObject); } 129 return Sort.Create(Context, Native.Z3_get_range(Context.nCtx, NativeObject)); 138 get { return (Z3_decl_kind)Native.Z3_get_decl_kind(Context.nCtx, NativeObject); } 148 return Symbol.Create(Context, Native.Z3_get_decl_name(Context.nCtx, NativeObject)); 157 get { return Native.Z3_get_decl_num_parameters(Context.nCtx, NativeObject); } 291 …ve.Z3_mk_func_decl(ctx.nCtx, name.NativeObject, AST.ArrayLength(domain), AST.ArrayToNative(domain)… in FuncDecl() [all …]
H A D	Quantifier.cs	36 get { return 0 != Native.Z3_is_quantifier_forall(Context.nCtx, NativeObject); } 44 get { return 0 != Native.Z3_is_quantifier_exists(Context.nCtx, NativeObject); } 52 get { return Native.Z3_get_quantifier_weight(Context.nCtx, NativeObject); } 60 get { return Native.Z3_get_quantifier_num_patterns(Context.nCtx, NativeObject); } 84 get { return Native.Z3_get_quantifier_num_no_patterns(Context.nCtx, NativeObject); } 108 get { return Native.Z3_get_quantifier_num_bound(Context.nCtx, NativeObject); } 190 NativeObject = Native.Z3_mk_quantifier(ctx.nCtx, (byte)(isForall ? 1 : 0) , weight, in Quantifier() 194 body.NativeObject); in Quantifier() 204 body.NativeObject); in Quantifier() 228 body.NativeObject); in Quantifier() [all …]
/dports/lang/spidermonkey60/firefox-60.9.0/js/src/vm/
H A D	NativeObject-inl.h	37 inline bool NativeObject::canRemoveLastProperty() { in canRemoveLastProperty() 138 inline void NativeObject::initDenseElements(NativeObject* src, in initDenseElements() 413 /* static / inline NativeObject NativeObject::copy( in copy() 423 NativeObject* obj = &baseObj->as<NativeObject>(); in copy() 466 /* static / inline JS::Result<NativeObject, JS::OOM&> NativeObject::create( in create() 480 NativeObject* nobj = static_cast<NativeObject>(obj); in create() 499 size - sizeof(js::NativeObject)); in create() 551 NativeObject::dynamicSlotsCount(Shape shape) { in dynamicSlotsCount() 663 inline NativeObject* NewNativeObjectWithGivenProto( 669 inline NativeObject* NewNativeObjectWithClassProto( [all …]

12 3 4 5 6 7 8 9 10 >>...48