Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Package Functions
InterpolationContext Class Reference

The InterpolationContext is suitable for generation of interpolants. More...

+ Inheritance diagram for InterpolationContext:

Public Member Functions

 InterpolationContext () throws Z3Exception
 InterpolationContext (Map< String, String > settings) throws Z3Exception
BoolExpr MkInterpolant (BoolExpr a) throws Z3Exception
String InterpolationProfile () throws Z3Exception
 Return a string summarizing cumulative time used for interpolation.
int CheckInterpolant (Expr[] cnsts, int[] parents, Expr[] interps, String error, Expr[] theory) throws Z3Exception
 Checks the correctness of an interpolant.
int ReadInterpolationProblem (String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory) throws Z3Exception
 Reads an interpolation problem from a file.
void WriteInterpolationProblem (String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory) throws Z3Exception
 Writes an interpolation problem to a file.

Package Functions

Expr[] GetInterpolant (Expr pf, Expr pat, Params p) throws Z3Exception
Z3_lbool ComputeInterpolant (Expr pat, Params p, ASTVector interp, Model model) throws Z3Exception

Detailed Description

The InterpolationContext is suitable for generation of interpolants.

For more information on interpolation please refer too the C/C++ API, which is well documented.

Definition at line 33 of file InterpolationContext.java.


Constructor & Destructor Documentation

InterpolationContext ( ) throws Z3Exception [inline]

Constructor.

Definition at line 38 of file InterpolationContext.java.

    {
        m_ctx = Native.mkInterpolationContext(0);
        initContext(); 
    }
InterpolationContext ( Map< String, String >  settings) throws Z3Exception [inline]

Constructor.

See also:
Context.Context(Dictionary&lt;string, string&gt;)

Definition at line 49 of file InterpolationContext.java.

    { 
        long cfg = Native.mkConfig();
        for (Map.Entry<String, String> kv : settings.entrySet())
            Native.setParamValue(cfg, kv.getKey(), kv.getValue());
        m_ctx = Native.mkInterpolationContext(cfg);
        Native.delConfig(cfg);
        initContext();
    }

Member Function Documentation

int CheckInterpolant ( Expr[]  cnsts,
int[]  parents,
Expr[]  interps,
String  error,
Expr[]  theory 
) throws Z3Exception [inline]

Checks the correctness of an interpolant.

For more information on interpolation please refer too the function Z3_check_interpolant in the C/C++ API, which is well documented.

Definition at line 127 of file InterpolationContext.java.

    {
        Native.StringPtr n_err_str = new Native.StringPtr();
        int r = Native.checkInterpolant(nCtx(),
                                        cnsts.length,
                                        Expr.arrayToNative(cnsts),
                                        parents,
                                        Expr.arrayToNative(interps),
                                        n_err_str,
                                        theory.length,
                                        Expr.arrayToNative(theory));
        error = n_err_str.value;
        return r;
    }
Z3_lbool ComputeInterpolant ( Expr  pat,
Params  p,
ASTVector  interp,
Model  model 
) throws Z3Exception [inline, package]

Computes an interpolant. For more information on interpolation please refer too the function Z3_compute_interpolant in the C/C++ API, which is well documented.

Exceptions:
Z3Exception

Definition at line 97 of file InterpolationContext.java.

    {
        checkContextMatch(pat);
        checkContextMatch(p);

        Native.LongPtr n_i = new Native.LongPtr();
        Native.LongPtr n_m = new Native.LongPtr();
        int r = Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m);
        interp = new ASTVector(this, n_i.value);
        model = new Model(this, n_m.value);
        return Z3_lbool.fromInt(r);
    }
Expr [] GetInterpolant ( Expr  pf,
Expr  pat,
Params  p 
) throws Z3Exception [inline, package]

Computes an interpolant. For more information on interpolation please refer too the function Z3_get_interpolant in the C/C++ API, which is well documented.

Exceptions:
Z3Exception

Definition at line 76 of file InterpolationContext.java.

    {
        checkContextMatch(pf);
        checkContextMatch(pat);
        checkContextMatch(p);

        ASTVector seq = new ASTVector(this, Native.getInterpolant(nCtx(), pf.getNativeObject(), pat.getNativeObject(), p.getNativeObject()));
        int n = seq.size();
        Expr[] res = new Expr[n];
        for (int i = 0; i < n; i++)
            res[i] = Expr.create(this, seq.get(i).getNativeObject());
        return res;
    }
String InterpolationProfile ( ) throws Z3Exception [inline]

Return a string summarizing cumulative time used for interpolation.

For more information on interpolation please refer too the function Z3_interpolation_profile in the C/C++ API, which is well documented.

Definition at line 116 of file InterpolationContext.java.

    {
        return Native.interpolationProfile(nCtx());
    }
BoolExpr MkInterpolant ( BoolExpr  a) throws Z3Exception [inline]

Create an expression that marks a formula position for interpolation.

Exceptions:
Z3Exception

Definition at line 63 of file InterpolationContext.java.

    {
        checkContextMatch(a);        
        return new BoolExpr(this, Native.mkInterpolant(nCtx(), a.getNativeObject()));
    }
int ReadInterpolationProblem ( String  filename,
Expr[]  cnsts,
int[]  parents,
String  error,
Expr[]  theory 
) throws Z3Exception [inline]

Reads an interpolation problem from a file.

For more information on interpolation please refer too the function Z3_read_interpolation_problem in the C/C++ API, which is well documented.

Definition at line 148 of file InterpolationContext.java.

    {
        Native.IntPtr n_num = new Native.IntPtr();
        Native.IntPtr n_num_theory = new Native.IntPtr();
        Native.ObjArrayPtr n_cnsts = new Native.ObjArrayPtr();
        Native.UIntArrayPtr n_parents = new Native.UIntArrayPtr();
        Native.ObjArrayPtr n_theory = new Native.ObjArrayPtr();
        Native.StringPtr n_err_str = new Native.StringPtr();
        int r = Native.readInterpolationProblem(nCtx(), n_num, n_cnsts, n_parents, filename, n_err_str, n_num_theory, n_theory);
        int num = n_num.value;
        int num_theory = n_num_theory.value;
        error = n_err_str.value;
        cnsts = new Expr[num];
        parents = new int[num];
        theory = new Expr[num_theory];
        for (int i = 0; i < num; i++)
        {
            cnsts[i] = Expr.create(this, n_cnsts.value[i]);
            parents[i] = n_parents.value[i];
        }
        for (int i = 0; i < num_theory; i++)
            theory[i] = Expr.create(this, n_theory.value[i]);
        return r;
    }
void WriteInterpolationProblem ( String  filename,
Expr[]  cnsts,
int[]  parents,
String  error,
Expr[]  theory 
) throws Z3Exception [inline]

Writes an interpolation problem to a file.

For more information on interpolation please refer too the function Z3_write_interpolation_problem in the C/C++ API, which is well documented.

Definition at line 179 of file InterpolationContext.java.

    {
        Native.writeInterpolationProblem(nCtx(), cnsts.length, Expr.arrayToNative(cnsts), parents, filename, theory.length, Expr.arrayToNative(theory));     
    }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines