mirror of
https://github.com/Z3Prover/z3
synced 2025-04-29 20:05:51 +00:00
dfc80d3b69
A lot of existing code in Java bindings catches exceptions just to silence them later. This is: a) Unnecessary: it is OK for a function to throw a RuntimeException without declaring it. b) Highly unidiomatic and not recommended by Java experts (see Effective Java and others) c) Confusing as has the potential to hide the existing bugs and have them resurface at the most inconvenient/unexpected moment.
63 lines
1.2 KiB
Java
63 lines
1.2 KiB
Java
/**
|
|
Copyright (c) 2012-2014 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
Pattern.java
|
|
|
|
Abstract:
|
|
|
|
Author:
|
|
|
|
@author Christoph Wintersteiger (cwinter) 2012-03-15
|
|
|
|
Notes:
|
|
|
|
**/
|
|
|
|
package com.microsoft.z3;
|
|
|
|
/**
|
|
* Patterns comprise a list of terms. The list should be non-empty. If the list
|
|
* comprises of more than one term, it is also called a multi-pattern.
|
|
**/
|
|
public class Pattern extends AST
|
|
{
|
|
/**
|
|
* The number of terms in the pattern.
|
|
**/
|
|
public int getNumTerms()
|
|
{
|
|
return Native.getPatternNumTerms(getContext().nCtx(), getNativeObject());
|
|
}
|
|
|
|
/**
|
|
* The terms in the pattern.
|
|
*
|
|
* @throws Z3Exception
|
|
**/
|
|
public Expr[] getTerms()
|
|
{
|
|
|
|
int n = getNumTerms();
|
|
Expr[] res = new Expr[n];
|
|
for (int i = 0; i < n; i++)
|
|
res[i] = Expr.create(getContext(),
|
|
Native.getPattern(getContext().nCtx(), getNativeObject(), i));
|
|
return res;
|
|
}
|
|
|
|
/**
|
|
* A string representation of the pattern.
|
|
**/
|
|
@Override
|
|
public String toString()
|
|
{
|
|
return Native.patternToString(getContext().nCtx(), getNativeObject());
|
|
}
|
|
|
|
Pattern(Context ctx, long obj)
|
|
{
|
|
super(ctx, obj);
|
|
}
|
|
}
|