Struct FuncDecl 

pub struct FuncDecl { /* private fields */ }

Function declaration. Every constant and function have an associated declaration.

The declaration assigns a name, a sort (i.e., type), and for function the sort (i.e., type) of each of its arguments. Note that, in Z3, a constant is a function with 0 arguments.

See also:

• RecFuncDecl

Implementations

impl FuncDecl

pub fn new<S: Into<Symbol>>(name: S, domain: &[&Sort], range: &Sort) -> Self

pub fn partial_order<A: Borrow<Sort>>(a: A, id: usize) -> Self

Create a partial order FuncDecl “Special Relation” over the given Sort.

The Sort may have many partial orders derived this way, distinguished by the second integer argument to this call, which represents the “id” of the partial order. Calling this twice with the same ID will yield the same partial order FuncDecl.

See https://microsoft.github.io/z3guide/docs/theories/Special%20Relations/ for more info.

A partial order is a binary relation that is reflexive, antisymmetric, and transitive.

Example

  let sort = Sort::int();
  let partial_order = FuncDecl::partial_order(&sort, 0);
  // Create a solver to assert properties of the partial order.
  let solver = Solver::new();
  let x = Int::new_const("x");
  let y = Int::new_const("y");
  let z = Int::new_const("z");

  solver.assert(&partial_order.apply(&[&x, &x]).as_bool().unwrap());
  // test reflexivity
  assert_eq!(
      solver.check_assumptions(&[partial_order.apply(&[&x, &x]).as_bool().unwrap().not()]),
      SatResult::Unsat
  );

  // test antisymmetry
  assert_eq!(
      solver.check_assumptions(&[
          partial_order.apply(&[&x, &y]).as_bool().unwrap(),
          partial_order.apply(&[&y, &x]).as_bool().unwrap(),
          x.eq(&y).not()
      ]),
      SatResult::Unsat
  );

  // test transitivity
  assert_eq!(
      solver.check_assumptions(&[
          partial_order.apply(&[&x, &y]).as_bool().unwrap(),
          partial_order.apply(&[&y, &z]).as_bool().unwrap(),
          partial_order.apply(&[&x, &z]).as_bool().unwrap().not(),
      ]),
      SatResult::Unsat
  );

See also

• piecewise_linear_order
• linear_order
• tree_order
• transitive_closure

pub fn piecewise_linear_order<A: Borrow<Sort>>(a: A, id: usize) -> Self

Create a piecewise linear order FuncDecl “Special Relation” over the given Sort.

See https://microsoft.github.io/z3guide/docs/theories/Special%20Relations/ for more info.

See also

• partial_order
• linear_order
• tree_order
• transitive_closure

pub fn linear_order<A: Borrow<Sort>>(a: A, id: usize) -> Self

Create a linear order FuncDecl “Special Relation” over the given Sort.

See https://microsoft.github.io/z3guide/docs/theories/Special%20Relations/ for more info.

See also

• partial_order
• piecewise_linear_order
• tree_order
• transitive_closure

pub fn tree_order<A: Borrow<Sort>>(a: A, id: usize) -> Self

Create a tree order FuncDecl “Special Relation” over the given Sort.

See https://microsoft.github.io/z3guide/docs/theories/Special%20Relations/ for more info.

See also

• partial_order
• piecewise_linear_order
• linear_order
• transitive_closure

pub fn transitive_closure<A: Borrow<FuncDecl>>(a: A) -> Self

Create a transitive closure FuncDecl “Special Relation” over the given FuncDecl.

See https://microsoft.github.io/z3guide/docs/theories/Special%20Relations/ for more info.

See also

• partial_order
• piecewise_linear_order
• linear_order
• tree_order

pub fn arity(&self) -> usize

Return the number of arguments of a function declaration.

If the function declaration is a constant, then the arity is 0.

let f = FuncDecl::new(
    "f",
    &[&Sort::int(), &Sort::real()],
    &Sort::int());
assert_eq!(f.arity(), 2);

pub fn apply(&self, args: &[&dyn Ast]) -> Dynamic

Create a constant (if args has length 0) or function application (otherwise).

Note that args should have the types corresponding to the domain of the FuncDecl.

pub fn kind(&self) -> DeclKind

Return the DeclKind of this FuncDecl.

pub fn name(&self) -> String

Return the name of this FuncDecl.

Strings will return the Symbol. Ints will have a "k!" prepended to the Symbol.

pub fn domain(&self, i: usize) -> Option<SortKind>

Returns the kind of the i-th domain (parameter) of this FuncDecl.

Returns None if i >= |domain|.

pub fn range(&self) -> SortKind

Returns the kind of range (output) of this FuncDecl.

Trait Implementations

impl Debug for FuncDecl

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl Display for FuncDecl

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl Drop for FuncDecl

fn drop(&mut self)

Executes the destructor for this type.

impl Translate for FuncDecl

fn translate(&self, dest: &Context) -> Self