Go to the documentation of this file.00001
00019 package com.microsoft.z3;
00020
00024 public class Params extends Z3Object
00025 {
00029 public void add(Symbol name, boolean value) throws Z3Exception
00030 {
00031 Native.paramsSetBool(getContext().nCtx(), getNativeObject(),
00032 name.getNativeObject(), (value) ? true : false);
00033 }
00034
00038 public void add(Symbol name, double value) throws Z3Exception
00039 {
00040 Native.paramsSetDouble(getContext().nCtx(), getNativeObject(),
00041 name.getNativeObject(), value);
00042 }
00043
00047 public void add(Symbol name, String value) throws Z3Exception
00048 {
00049
00050 Native.paramsSetSymbol(getContext().nCtx(), getNativeObject(),
00051 name.getNativeObject(),
00052 getContext().mkSymbol(value).getNativeObject());
00053 }
00054
00058 public void add(Symbol name, Symbol value) throws Z3Exception
00059 {
00060
00061 Native.paramsSetSymbol(getContext().nCtx(), getNativeObject(),
00062 name.getNativeObject(), value.getNativeObject());
00063 }
00064
00068 public void add(String name, boolean value) throws Z3Exception
00069 {
00070 Native.paramsSetBool(getContext().nCtx(), getNativeObject(),
00071 getContext().mkSymbol(name).getNativeObject(), value);
00072 }
00073
00077 public void add(String name, int value) throws Z3Exception
00078 {
00079 Native.paramsSetUint(getContext().nCtx(), getNativeObject(), getContext()
00080 .mkSymbol(name).getNativeObject(), value);
00081 }
00082
00086 public void add(String name, double value) throws Z3Exception
00087 {
00088 Native.paramsSetDouble(getContext().nCtx(), getNativeObject(), getContext()
00089 .mkSymbol(name).getNativeObject(), value);
00090 }
00091
00095 public void add(String name, Symbol value) throws Z3Exception
00096 {
00097 Native.paramsSetSymbol(getContext().nCtx(), getNativeObject(), getContext()
00098 .mkSymbol(name).getNativeObject(), value.getNativeObject());
00099 }
00100
00104 public void add(String name, String value) throws Z3Exception
00105 {
00106
00107 Native.paramsSetSymbol(getContext().nCtx(), getNativeObject(),
00108 getContext().mkSymbol(name).getNativeObject(),
00109 getContext().mkSymbol(value).getNativeObject());
00110 }
00111
00115 public String toString()
00116 {
00117 try
00118 {
00119 return Native.paramsToString(getContext().nCtx(), getNativeObject());
00120 } catch (Z3Exception e)
00121 {
00122 return "Z3Exception: " + e.getMessage();
00123 }
00124 }
00125
00126 Params(Context ctx) throws Z3Exception
00127 {
00128 super(ctx, Native.mkParams(ctx.nCtx()));
00129 }
00130
00131 void incRef(long o) throws Z3Exception
00132 {
00133 getContext().params_DRQ().incAndClear(getContext(), o);
00134 super.incRef(o);
00135 }
00136
00137 void decRef(long o) throws Z3Exception
00138 {
00139 getContext().params_DRQ().add(o);
00140 super.decRef(o);
00141 }
00142 }