Z3
src/api/java/Params.java
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 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines