feat: Special Binary Relation FuncDecls

z3-sys/src/lib.rs

@@ -2256,6 +2256,21 @@ unsafe extern "C" {
         body: Z3_ast,
     );
 
+    /// Create a `FuncDecl` representing a partial order
+    pub fn Z3_mk_partial_order(c: Z3_context, a: Z3_sort, id: usize) -> Z3_func_decl;
+
+    /// Create a `FuncDecl` representing a piecewise linear order
+    pub fn Z3_mk_piecewise_linear_order(c: Z3_context, a: Z3_sort, id: usize) -> Z3_func_decl;
+
+    /// Create a `FuncDecl` representing a linear order
+    pub fn Z3_mk_linear_order(c: Z3_context, a: Z3_sort, id: usize) -> Z3_func_decl;
+
+    /// Create a `FuncDecl` representing a tree order
+    pub fn Z3_mk_tree_order(c: Z3_context, a: Z3_sort, id: usize) -> Z3_func_decl;
+
+    /// Create a `FuncDecl` representing a transitive closure
+    pub fn Z3_mk_transitive_closure(c: Z3_context, f: Z3_func_decl) -> Z3_func_decl;
+
     /// Create an AST node representing `true`.
     pub fn Z3_mk_true(c: Z3_context) -> Z3_ast;
 

z3/src/func_decl.rs

@@ -1,3 +1,4 @@
+use std::borrow::Borrow;
 use std::convert::TryInto;
 use std::ffi::CStr;
 use std::fmt;
@@ -38,6 +39,140 @@ impl FuncDecl {
         }
     }
 
+    /// 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
+    ///
+    /// ```
+    /// # use z3::{FuncDecl, Sort, Solver, SatResult, Symbol};
+    /// # use z3::ast::{Bool, Int};
+    ///
+    ///   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`](Self::piecewise_linear_order)
+    /// - [`linear_order`](Self::linear_order)
+    /// - [`tree_order`](Self::tree_order)
+    /// - [`transitive_closure`](Self::transitive_closure)
+    pub fn partial_order<A: Borrow<Sort>>(a: A, id: usize) -> Self {
+        let a = a.borrow();
+        let ctx = &a.ctx;
+        unsafe { Self::wrap(ctx, Z3_mk_partial_order(ctx.z3_ctx.0, a.z3_sort, id)) }
+    }
+
+    /// 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`](Self::partial_order)
+    /// - [`linear_order`](Self::linear_order)
+    /// - [`tree_order`](Self::tree_order)
+    /// - [`transitive_closure`](Self::transitive_closure)
+    pub fn piecewise_linear_order<A: Borrow<Sort>>(a: A, id: usize) -> Self {
+        let a = a.borrow();
+        let ctx = &a.ctx;
+        unsafe {
+            Self::wrap(
+                ctx,
+                Z3_mk_piecewise_linear_order(ctx.z3_ctx.0, a.z3_sort, id),
+            )
+        }
+    }
+
+    /// 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`](Self::partial_order)
+    /// - [`piecewise_linear_order`](Self::piecewise_linear_order)
+    /// - [`tree_order`](Self::tree_order)
+    /// - [`transitive_closure`](Self::transitive_closure)
+    pub fn linear_order<A: Borrow<Sort>>(a: A, id: usize) -> Self {
+        let a = a.borrow();
+        let ctx = &a.ctx;
+        unsafe { Self::wrap(ctx, Z3_mk_linear_order(ctx.z3_ctx.0, a.z3_sort, id)) }
+    }
+
+    /// 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`](Self::partial_order)
+    /// - [`piecewise_linear_order`](Self::piecewise_linear_order)
+    /// - [`linear_order`](Self::linear_order)
+    /// - [`transitive_closure`](Self::transitive_closure)
+    pub fn tree_order<A: Borrow<Sort>>(a: A, id: usize) -> Self {
+        let a = a.borrow();
+        let ctx = &a.ctx;
+        unsafe { Self::wrap(ctx, Z3_mk_tree_order(ctx.z3_ctx.0, a.z3_sort, id)) }
+    }
+
+    /// 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`](Self::partial_order)
+    /// - [`piecewise_linear_order`](Self::piecewise_linear_order)
+    /// - [`linear_order`](Self::linear_order)
+    /// - [`tree_order`](Self::tree_order)
+    pub fn transitive_closure<A: Borrow<FuncDecl>>(a: A) -> Self {
+        let a = a.borrow();
+        let ctx = &a.ctx;
+        unsafe { Self::wrap(ctx, Z3_mk_transitive_closure(ctx.z3_ctx.0, a.z3_func_decl)) }
+    }
+
     /// Return the number of arguments of a function declaration.
     ///
     /// If the function declaration is a constant, then the arity is `0`.