From adce815643549b5f29f9d5cd381edc84af79c6d5 Mon Sep 17 00:00:00 2001
From: Sankalp Gambhir <sankalp.gambhir47@gmail.com>
Date: Tue, 28 Mar 2023 16:40:34 +0200
Subject: [PATCH 1/2] Add stricter fresh ID gen
---
.../src/main/scala/lisa/kernel/fol/Substitutions.scala | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala
index 33f56008..f45ce911 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala
@@ -94,7 +94,7 @@ trait Substitutions extends FormulaDefinitions {
val newSubst = m - bound
val fv = m.values.flatMap(_.freeVariables).toSet
if (fv.contains(bound)) {
- val newBoundVariable = VariableLabel(freshId(fv.map(_.name), bound.name))
+ val newBoundVariable = VariableLabel(freshId(fv.map(_.name) ++ m.keys.map(_.id), bound.name))
val newInner = substituteVariables(inner, Map(bound -> VariableTerm(newBoundVariable)))
BinderFormula(label, newBoundVariable, substituteVariables(newInner, newSubst))
} else BinderFormula(label, bound, substituteVariables(inner, newSubst))
@@ -136,7 +136,7 @@ trait Substitutions extends FormulaDefinitions {
val newSubst = m - bound
val fv: Set[VariableLabel] = newSubst.flatMap { case (symbol, LambdaTermTerm(arguments, body)) => body.freeVariables }.toSet
if (fv.contains(bound)) {
- val newBoundVariable = VariableLabel(freshId(fv.map(_.name), bound.name))
+ val newBoundVariable = VariableLabel(freshId(fv.map(_.name) ++ m.keys.map(_.id), bound.name))
val newInner = substituteVariables(inner, Map(bound -> VariableTerm(newBoundVariable)))
BinderFormula(label, newBoundVariable, instantiateTermSchemas(newInner, newSubst))
} else BinderFormula(label, bound, instantiateTermSchemas(inner, newSubst))
@@ -232,7 +232,7 @@ trait Substitutions extends FormulaDefinitions {
(mPred.flatMap { case (symbol, LambdaTermFormula(arguments, body)) => body.freeVariables }).toSet ++
(mTerm.flatMap { case (symbol, LambdaTermTerm(arguments, body)) => body.freeVariables }).toSet
if (fv.contains(bound)) {
- val newBoundVariable = VariableLabel(freshId(fv.map(_.name), bound.name))
+ val newBoundVariable = VariableLabel(freshId(fv.map(_.name) ++ mTerm.keys.map(_.id), bound.name))
val newInner = substituteVariables(inner, Map(bound -> VariableTerm(newBoundVariable)))
BinderFormula(label, newBoundVariable, instantiateSchemas(newInner, mCon, mPred, newmTerm))
} else BinderFormula(label, bound, instantiateSchemas(inner, mCon, mPred, newmTerm))
--
GitLab
From 3d639377686385f8b8d5cece51d43cf71663e53d Mon Sep 17 00:00:00 2001
From: Sankalp Gambhir <sankalp.gambhir47@gmail.com>
Date: Tue, 28 Mar 2023 16:52:12 +0200
Subject: [PATCH 2/2] Added test for edge subst
---
lisa-utils/src/test/scala/lisa/kernel/SubstitutionTest.scala | 3 +++
1 file changed, 3 insertions(+)
diff --git a/lisa-utils/src/test/scala/lisa/kernel/SubstitutionTest.scala b/lisa-utils/src/test/scala/lisa/kernel/SubstitutionTest.scala
index 19c4b39c..901d6851 100644
--- a/lisa-utils/src/test/scala/lisa/kernel/SubstitutionTest.scala
+++ b/lisa-utils/src/test/scala/lisa/kernel/SubstitutionTest.scala
@@ -13,6 +13,7 @@ import org.scalatest.funsuite.AnyFunSuite
class SubstitutionTest extends AnyFunSuite {
private val x = variable
+ private val x1 = VariableLabel(Identifier("x", 1))
private val x2 = variable
private val x3 = variable
private val y = variable
@@ -85,6 +86,7 @@ class SubstitutionTest extends AnyFunSuite {
$(Q(f(f(h(x, y)))) /\ R(x, h(y, f(z))), x -> z(), h -> lambda(Seq(x, z), g(h(z, y))), z -> y()) _VS_ Q(f(f(g(h(y, y))))) /\ R(z, g(h(f(y), y))),
$(forall(x, R(x, y)), x -> z()) _VS_ forall(x, R(x, y)),
$(forall(x, R(x, y)), y -> z()) _VS_ forall(x, R(x, z)),
+ $(forall(x, P(x)), x1 -> f(x())) _VS_ forall(x, P(x)),
$(forall(x, R(x, y)) /\ P(h(x, y)), y -> z(), x -> y()) _VS_ forall(x, R(x, z)) /\ P(h(y, z)),
$(forall(x, R(x, y)) /\ P(h(x, y)), y -> x()) _VS_ forall(y, R(y, x)) /\ P(h(x, x)),
$(existsOne(x, R(x, y)) /\ P(h(x, y)), y -> x()) _VS_ existsOne(y, R(y, x)) /\ P(h(x, x))
@@ -214,6 +216,7 @@ class SubstitutionTest extends AnyFunSuite {
X -> (z === y),
P -> lambda(x2, exists(y, R(x2, y) /\ P(x)))
) _VS_ (exists(y2, Q(y2) /\ ((z === y) <=> exists(x2, P(x2) /\ exists(y, R(x, y) /\ P(x))))) /\ R(y, f(y))),
+ $(forall(x, P(x)), x1 -> f(x())) _VS_ forall(x, P(x)),
$(
forall(x, e2(c1(e2(X, P(x))) /\ R(y, f(y)), exists(x, P(x) /\ X))),
c1 -> lambda(X, exists(y, Q(y) /\ X)),
--
GitLab