除了感叹号运算符的 <var> := ... 形式外，在 then 语句中不能引入额外的变量。规则中的 then 语句中出现的每个术语都必须等于之前 if 语句中出现的术语。绕过此限制的唯一方法是添加以下形式的语句 then <tm>!;。随后 then 语句的原子可以自由使用 <tm>。

例如，考虑以下半格理论的无效和有效规则

// Invalid: Cannot infer type of x.
rule {
    if x = x;
    then x = x;
}
// Valid (but nonsensical):
rule {
    if x: El;
    then x = x;
}

// Invalid: x and y are not introduced in an `if` statement.
rule {
    then meet(x, y)!;
}
// Valid:
rule {
    if x: El;
    if y: El;
    then meet(x, y)!;
}

// Invalid: meet(x, y) is not equal to a term occurring earlier.
rule {
    if le(z, x);
    if le(z, y);
    then le(z, meet(x, y));
}
// Valid: Assert that meet(x, y) exists in a then statement.
rule {
    if le(z, x);
    if le(z, y);
    then meet(x, y)!
    then le(z, meet(x, y));
}
// Valid: Suppose that meet(x, y) exists in if statement.
rule {
    if le(z, x);
    if le(z, y);
    if meet(x, y)!;
    then le(z, meet(x, y));
}

// Invalid: Both Meet(x, y) and Meet(y, x) do not occur earlier.
rule {
    if x: El;
    if y: El;
    then meet(x, y);
    then meet(y, x);
}

// Valid: the term on the left-hand side of the equation is introduced
// in an if statement.
rule {
    if meet(x, y)!;
    then meet(x, y);
    then meet(y, x);
}

// Valid: the term on the right-hand side of the equation is introduced
// earlier in a then statement.
rule {
    if x: El;
    if y: El;
    then meet(x, y)!;
    then meet(y, x) = meet(x, y);
}

// Invalid: meet(x, y) is not equal to a term that occurs earlier.
rule {
    if u = meet(x, meet(y, z))!;
    then meet(meet(x, y), z) = u;
}

// Valid: All of u, Meet(x, y) and z are introduced in an if statement.
rule {
    if u = meet(x, meet(y, z))!;
    if meet(x, y)!;
    then u = meet(meet(x, y), z);
}

生成的 Rust 接口

Eqlog 将每个 .eqlog 转换为 .rs 文件。Rust 文件必须在 src 目录（例如 lib.rs 或 main.rs）内声明，并使用 eqlog_runtime::eqlog_mod! 宏。

Eqlog 生成文档化的 Rust 代码。要构建和查看此文档，请运行

cargo doc --document-private-items --open

生成的 Rust 模块的公共 API 由以下符号组成

• 对于每个 Eqlog 类型，都有一个 Rust 类型 <TypeName>，用于表示该类型的元素 ID。
• 模型结构。其名称是通过将文件名转换为驼峰命名法得到的。例如，对于 semi_group.eqlog，这将变为 SemiGroup。

模型结构有以下成员函数

• fn new() -> Self
  创建一个空的模型结构。
• fn close(&mut self)
  在所有规则下关闭模型。
• pub fn close_until(&mut self, condition:impl Fn(&Self) -> bool) -> bool
  在满足条件之前，关闭所有规则下的模型。如果模型可以在所有规则下关闭但条件仍然不成立，则返回 false。
• 对于每个类型
  • fn new_<sort_name>(&mut self) -> <TypeName>
    将新元素添加到模型结构中。
  • fn equate_<sort_name>(&mut self, lhs: <TypeName>, rhs: <TypeName>)
    在模型结构中强制执行等式 lhs = rhs。
  • fn are_equal_<sort_name>(&self, lhs: <TypeName>, rhs: <TypeName>) -> bool
    如果 lhs 和 rhs 代表相同的元素，则返回 true。
  • fn root_<sort_name>(&self, el: <TypeName>) -> <TypeName>
    返回元素等价类的规范/根元素。
• 对于每个谓词
  • fn <pred_name>(&self,arg_1: <Type_1>, ...,arg_n: <Type_n>)
    检查谓词在给定参数上是否成立。
  • fn iter_<pred_name>(&self) ->impl'_ + Iterator<Item =<arity>>
    返回满足谓词的元组的迭代器。迭代器产生的项目类型由arity确定。
  • fn insert_<pred_name>(&mut self, arg_1: <Type_1>, ..., arg_n: <Type_n>)
    强制谓词对给定参数成立。
• 对于每个函数
  • fn <func_name>(&self,arg_1: <Type_1>, ...,arg_n: <Type_n>) -> Option<<ResultType>>
    在给定参数上评估函数。
  • fn iter_<func_name>(&self) ->impl'_ + Iterator<Item =<arity>>
    返回函数图的元组的迭代器。迭代器产生的项目类型由arity确定。
  • fn define_<func_name>(&mut self, arg_1: <Type_1>, ..., arg_n: <Type_n>) -> <ResultType>
    强制函数在给定参数上定义，如果需要则添加新元素。
  • fn insert_<func_name>(&mut self, arg_1: <Type_1>, ..., arg_n: <Type_n>, result: <ResultType>)
    将一个元组插入函数的图中。

例如，以下是从半格理论生成的rust模块的公共声明

struct El;
struct Semilattice;
impl Semilattice {
  fn new() -> Self;
  fn close(&mut self);
  fn close_until(&mut self, condition: impl Fn(&Self) -> bool) -> bool;

  fn new_el(&mut self) -> El;
  fn equate_el(&mut self, lhs: El, rhs: El);
  fn are_equal_el(&self, lhs: El, rhs: El) -> bool;
  fn root_el(&self, el: El) -> El;

  fn le(&self, arg0: El, arg1: El) -> bool;
  fn iter_le(&self) -> impl '_ + Iterator<Item = (El, El)>;
  fn insert_le(&mut self, arg0: El, arg1: El);

  fn meet(&self, arg0: El, arg1: El) -> Option<El>;
  fn iter_meet(&self) -> impl '_ + Iterator<Item = (El, El, El)>;
  fn define_meet(&mut self, arg0: El, arg1: El) -> El;
  fn insert_meet(&mut self, arg0: El, arg1: El, result: El);
}

数据模型和算法

标准datalog功能

eqlog生成的理论模型结构可以被视为内存中的SQL数据库，其模式由类型、谓词和函数声明给出。给定类型的元素是简单的整数ID，模型结构维护每个类型的有效ID列表。每个谓词 p 都表示为一个表，其行是谓词成立的元素的元组。函数表示为 图。例如，如果 f 是一个单参数函数，那么 f 的内部表将包含如下形式的行 (x, f(x))。

close 函数会重复枚举规则和规则中if语句的所有匹配，并将规则中then语句对应的数据附加到模型中。最终，会达到一个 不动点（除非理论包含非全射规则，见下文），算法停止。例如，对于传递性公理

rule {
    if le(x, y);
    if le(y, z);
    then le(x, z);
}

close 函数枚举了在 Le 表中所有满足 y_0 = y_1 的行 (x, y_0) 和 (y_1, z)，然后将行 (x, z) 添加到 Le。最终，Le 表将包含我们找到的所有新行 (x, z)，这意味着我们已经达到不动点并可以停止：现在 le 谓词是传递的。

rule {
    if le(x, y);
    if le(y, x);
    then x = y;
}

rule {
    if g_f(x_1, ..., x_n, y);
    if g_f(x_1, ..., x_n, z);
    then y = z;
}

type N;
zero: N;
succ: N -> N;

rule {
    then Zero()!;
}
rule {
    if n: N;
    then Succ(n)!;
}

rule {
    if x: El;
    if y : El;
    then meet(x, y)!;
}

// Match `if` statements in a rule and change the model such that the
// corresponding `then` statements holds. Returns true if the model was
// changed, i.e. if new facts were concluded.
fn adjoin_conclusions(ax: Axiom) -> bool {
  ...
}

fn close() {
  loop {
    loop {
      let model_changed = surjective_rules.iter().any(adjoin_conclusion);
      if !model_changed {
        break;
      }
    }

    let model_changed = non_surjective_rules.iter().any(adjoin_conclusion);
    if !model_changed {
      break;
    }
  }
}