From 4be9a1aac51c1c8675071b098c962e2cef17a296 Mon Sep 17 00:00:00 2001
From: Katja Goltsova <katja.goltsova@protonmail.com>
Date: Mon, 19 Sep 2022 18:47:57 +0200
Subject: [PATCH] Require that PredicateFormula's and ConnectorFormula's args
correspond to the label's arity
Analogous to the existing requirement in FunctionTerm.
---
.../src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala | 2 ++
lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala | 2 +-
2 files changed, 3 insertions(+), 1 deletion(-)
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
index 1e95ed08..84321108 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
@@ -23,6 +23,7 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD
* The formula counterpart of [[PredicateLabel]].
*/
sealed case class PredicateFormula(label: PredicateLabel, args: Seq[Term]) extends Formula {
+ require(label.arity == args.size)
override def freeVariables: Set[VariableLabel] = args.foldLeft(Set.empty[VariableLabel])((prev, next) => prev union next.freeVariables)
override def constantPredicates: Set[ConstantPredicateLabel] = label match {
@@ -42,6 +43,7 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD
* The formula counterpart of [[ConnectorLabel]].
*/
sealed case class ConnectorFormula(label: ConnectorLabel, args: Seq[Formula]) extends Formula {
+ require(label.arity == -1 || label.arity == args.length)
override def freeVariables: Set[VariableLabel] = args.foldLeft(Set.empty[VariableLabel])((prev, next) => prev union next.freeVariables)
override def constantFunctions: Set[ConstantFunctionLabel] = args.foldLeft(Set.empty[ConstantFunctionLabel])((prev, next) => prev union next.constantFunctions)
diff --git a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
index 33f62829..771f392a 100644
--- a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
+++ b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
@@ -38,7 +38,7 @@ class PrinterTest extends AnyFunSuite {
assert(prettyFormula(BinderFormula(Forall, x, BinderFormula(Exists, y, BinderFormula(ExistsOne, z, a)))) == "∀x. ∃y. ∃!z. a")
- assert(prettyFormula(PredicateFormula(ConstantPredicateLabel("f", 2), Seq(x, y, z))) == "f(?x, ?y, ?z)")
+ assert(prettyFormula(PredicateFormula(ConstantPredicateLabel("f", 3), Seq(x, y, z))) == "f(?x, ?y, ?z)")
}
}
--
GitLab