Package com.microsoft.z3

Class Model

java.lang.Object
com.microsoft.z3.Z3Object
com.microsoft.z3.Model
public class Model extends Z3Object
A Model contains interpretations (assignments) of constants and functions.

  • Method Details

    • getConstInterp

      public <R extends Sort> Expr<R> getConstInterp(Expr<R> a)
      Retrieves the interpretation (the assignment) of a in the model.
      Parameters:
      a - A Constant
      Returns:
      An expression if the constant has an interpretation in the model, null otherwise.
      Throws:
      Z3Exception

    • getConstInterp

      public <R extends Sort> Expr<R> getConstInterp(FuncDecl<R> f)
      Retrieves the interpretation (the assignment) of f in the model.
      Parameters:
      f - A function declaration of zero arity
      Returns:
      An expression if the function has an interpretation in the model, null otherwise.
      Throws:
      Z3Exception

    • getFuncInterp

      public <R extends Sort> FuncInterp<R> getFuncInterp(FuncDecl<R> f)
      Retrieves the interpretation (the assignment) of a non-constant f in the model.
      Parameters:
      f - A function declaration of non-zero arity
      Returns:
      A FunctionInterpretation if the function has an interpretation in the model, null otherwise.
      Throws:
      Z3Exception

    • getNumConsts

      public int getNumConsts()
      The number of constants that have an interpretation in the model.

    • getConstDecls

      public FuncDecl<?>[] getConstDecls()
      The function declarations of the constants in the model.
      Throws:
      Z3Exception

    • getNumFuncs

      public int getNumFuncs()
      The number of function interpretations in the model.

    • getFuncDecls

      public FuncDecl<?>[] getFuncDecls()
      The function declarations of the function interpretations in the model.
      Throws:
      Z3Exception

    • getDecls

      public FuncDecl<?>[] getDecls()
      All symbols that have an interpretation in the model.
      Throws:
      Z3Exception

    • eval

      public <R extends Sort> Expr<R> eval(Expr<R> t, boolean completion)
      Evaluates the expression t in the current model. Remarks: This function may fail if t contains quantifiers, is partial (MODEL_PARTIAL enabled), or if t is not well-sorted. In this case a ModelEvaluationFailedException is thrown.
      Parameters:
      t - the expression to evaluate
      completion - An expression completion When this flag is enabled, a model value will be assigned to any constant or function that does not have an interpretation in the model.
      Returns:
      The evaluation of t in the model.
      Throws:
      Z3Exception

    • evaluate

      public <R extends Sort> Expr<R> evaluate(Expr<R> t, boolean completion)
      Alias for Eval.
      Throws:
      Z3Exception

    • getNumSorts

      public int getNumSorts()
      The number of uninterpreted sorts that the model has an interpretation for.

    • getSorts

      public Sort[] getSorts()
      The uninterpreted sorts that the model has an interpretation for. Remarks: Z3 also provides an interpretation for uninterpreted sorts used in a formula. The interpretation for a sort is a finite set of distinct values. We say this finite set is the "universe" of the sort.
      Throws:
      Z3Exception
      See Also:

    • getSortUniverse

      public <R extends Sort> Expr<R>[] getSortUniverse(R s)
      The finite set of distinct values that represent the interpretation for sort s.
      Parameters:
      s - An uninterpreted sort
      Returns:
      An array of expressions, where each is an element of the universe of s
      Throws:
      Z3Exception

    • toString

      public String toString()
      Conversion of models to strings.
      Overrides:
      toString in class Object
      Returns:
      A string representation of the model.