src/main/scala/app/Main.scala

@@ -12,6 +12,7 @@ object Main {
 
     var maxSearchDepth: Int = 4
     var printDebug: Boolean = false
+    var innerDebug: Boolean = false
 
     println("Spróbuj wpisać jakie co, na przykład:")
     println("Paradoks barowy: jeśli jeden pije, to wszyscy piją")
@@ -29,13 +30,15 @@ object Main {
         if input == "debug" then {
           printDebug = !printDebug
           println(s"Debug mode ${if printDebug then "enabled" else "disabled"}")
+        } else if input == "odpluskw" then {
+          innerDebug = !innerDebug
         } else input.toIntOption match
           case Some(newBound) =>
             println(s"Nowa głębokość poszukiwań: $newBound (było: $maxSearchDepth)")
             maxSearchDepth = newBound
           case None =>
             val startTime = System.nanoTime()
-            val tree = new Tree(input)
+            val tree = new Tree(input, innerDebug)
             val proven = tree.solve(maxSearchDepth)
             val endTime = System.nanoTime()
             val response = if proven then s"To prawda, że ${tree.formula}"

src/main/scala/lang/Formula.scala

@@ -4,32 +4,31 @@ package lang
 import lang.Term.{NamedVar, Variable}
 import util.Printing
 
-sealed trait Formula
+sealed trait Formula {
+  override def toString: String = Printing.toString(this)
+}
 
 sealed trait NormalizedHeadFormula extends Formula
 
 object Formula {
-  /**
-   * Equality. If the equality symbol is considered part of logic, and t1 and t2 are terms, then t1 = t2 is a formula.
-   */
-  case class Equal(a: Term, b: Term) { // TODO implement equality handling
-    override def toString: String = s"($a = $b)"
-  }
+  case class Predicate(name: PredicateName, args: Seq[Term]) extends NormalizedHeadFormula
 
-  /**
-   * Predicate symbols. If P is an n-ary predicate symbol and t1, ..., tn are terms then P(t1,...,tn) is a formula.
-   */
-  case class Predicate(name: PredicateName, args: Seq[Term]) extends NormalizedHeadFormula {
+  case class Not(formula: Formula) extends NormalizedHeadFormula
 
-    def arity: Int = args.size
+  case class ForAll(variable: Variable, body: Formula) extends NormalizedHeadFormula
 
-    def isAtomic: Boolean = arity == 0
+  case class Exists(variable: Variable, body: Formula) extends NormalizedHeadFormula
 
-    override def toString: String = Printing.printFunctionLike(name.name, args)
+  case class And(a: Formula, b: Formula) extends NormalizedHeadFormula
+
+  case class Or(a: Formula, b: Formula) extends NormalizedHeadFormula
+
+  case class Equivalent(a: Formula, b: Formula) extends Formula
+
+  case class Implies(premise: Formula, conclusion: Formula) extends Formula
 
-    def jName: String = name.name.name
-  }
 
+  // helper stuff, end of actual AST defintion
   object Predicate {
     def apply(name: PredicateName, arg: Term): Predicate = Predicate(name, Seq(arg))
 
@@ -45,43 +44,4 @@ object Formula {
   object PredicateName {
     def apply(name: String): PredicateName = PredicateName(NamedVar(name))
   }
-
-  /**
-   * Negation. If φ \varphi is a formula, then ¬ φ {\displaystyle \lnot \varphi } is a formula.
-   */
-  case class Not(formula: Formula) extends NormalizedHeadFormula {
-
-    override def toString: String = "(¬" + formula + ")"
-  }
-
-  case class ForAll(variable: Variable, body: Formula) extends NormalizedHeadFormula {
-    override def toString: String = "∀" + variable + ".(" + body + ")"
-  }
-
-  case class Exists(variable: Variable, body: Formula) extends NormalizedHeadFormula {
-    override def toString: String = "∃" + variable + ".(" + body + ")"
-  }
-
-  case class And(a: Formula, b: Formula) extends NormalizedHeadFormula {
-    override def toString: String = "(" + a + " ∧ " + b + ")"
-  }
-
-  case class Or(a: Formula, b: Formula) extends NormalizedHeadFormula {
-    override def toString: String = "(" + a + " ∨ " + b + ")"
-  }
-
-  case class Equivalent(a: Formula, b: Formula) extends Formula {
-
-    override def toString: String = "(" + a + " ⇔ " + b + ")"
-  }
-
-  case class Implies(premise: Formula, conclusion: Formula) extends Formula {
-
-    override def toString: String = s"($premise ⇒ $conclusion)"
-  }
 }
-
-/*
-Binary connectives. If φ \varphi and ψ \psi are formulas, then ( φ → ψ \varphi \rightarrow \psi ) is a formula. Similar rules apply to other binary logical connectives.
-Quantifiers. If φ \varphi is a formula and x is a variable, then ∀ x φ \forall x\varphi (for all x, φ \varphi holds) and ∃ x φ \exists x\varphi (there exists x such that φ \varphi ) are formulas.
-*/

src/main/scala/lang/Term.scala

@@ -39,8 +39,6 @@ object Term {
     def isAtom: Boolean = arity == 0
 
     override def toString: String = Printing.printFunctionLike(name.name, args)
-
-    def jName: Variable = name.name
   }
 
   object Function {

src/main/scala/tree/Node.scala

@@ -11,74 +11,35 @@ import unification.{FormulaInterop, Unifier}
 import util.Gensym
 
 import scala.annotation.tailrec
+import scala.collection.immutable.LazyList
 import scala.collection.mutable
 
-final class Node private(var formula: Formula, val parent: Option[Node], val originator: Option[Node]) {
+final class Node private(val formula: Formula, val parent: Option[Node], val originator: Option[Node]) {
 
   def this(formula: Formula, parent: Node, originator: Node) = this(formula, Some(parent), Some(originator))
 
   val id = new NodeId()
 
-  val originalFormula: Formula = formula
-
-  private val backup = new mutable.Stack[Formula]()
+  def isTip: Boolean = children.isEmpty
 
-  def pushBackup(): Unit = backup.push(formula)
+  def ruleType: RuleType = RuleType(formula)
 
-  def popBakcup(): Unit = formula = backup.pop()
+  def children: Seq[Node] = children_
 
   private var hasExpanded: Boolean = false
 
   var closedForFree: Boolean = false
 
-  var children: Seq[Node] = Seq()
-  var originated: Seq[Node] = Seq()
+  private var children_ : Seq[Node] = Seq()
 
-  var blocked = false
+  private def addChild(child: Node): Unit = children_ = children_ :+ child
 
-  /** applies to nodes whose originator is gamma type, otherwise is none. */
-  def substitution(): Option[Term] = {
-    def findPredicates(f: Formula): LazyList[Formula.Predicate] = f match
-      case p: Formula.Predicate => LazyList(p)
-      case Formula.Not(formula) => findPredicates(formula)
-      case ForAll(variable, body) => findPredicates(body)
-      case Formula.Exists(variable, body) => findPredicates(body)
-      case Formula.And(a, b) => findPredicates(a) ++ findPredicates(b)
-      case Formula.Or(a, b) => findPredicates(a) ++ findPredicates(b)
-      case Formula.Equivalent(a, b) => findPredicates(a) ++ findPredicates(b)
-      case Formula.Implies(premise, conclusion) => findPredicates(premise) ++ findPredicates(conclusion)
-
-
-    originator //.filter (_.ruleType==Gamma)
-      .map(_.formula).collect { case fa: ForAll => fa }.map { parentForall =>
-      val (unifiable, expanded) = Expansion.gammaExpansion(parentForall)
-      val flexiblePreds = findPredicates(expanded)
-      val rigidPreds = findPredicates(this.formula)
-      val pairs = flexiblePreds.zip(rigidPreds)
-
-      @tailrec
-      def findUnified(pairs: LazyList[(Predicate, Predicate)]): Term =
-        if pairs.isEmpty then throw new ShouldNotHappenException()
-        else {
-          val (a, b) = pairs.head
-          Unifier.unify(FormulaInterop.apply(a), FormulaInterop.apply(b)) match
-            case UnificationResult.UnificationFailure => throw new ShouldNotHappenException()
-            case UnificationResult.UnificationSuccess(substitution) =>
-              substitution.headOption match
-                case Some((uVar, uTerm)) =>
-                  val term = FormulaInterop.toLogicTerm(uTerm)
-                  if term == unifiable then FormulaInterop.toLogicTerm(uVar) else term
-                case None => findUnified(pairs.tail)
-        }
+  var originated: Seq[Node] = Seq()
 
-      findUnified(pairs)
-    }
-  }
+  var blocked = false
 
   def canExpand: Boolean = !blocked && (!hasExpanded || RuleType(formula) == Gamma)
 
-  def restoreOriginalFormula(): Unit = formula = originalFormula
-
   def expand(): Boolean = {
     val willExpand = canExpand
     if willExpand then {
@@ -91,7 +52,7 @@ final class Node private(var formula: Formula, val parent: Option[Node], val ori
           newBranch.formulas.foreach { newFormula =>
             val newNode = new Node(newFormula, currentTip, Node.this)
             originated = newNode +: originated
-            currentTip.children = newNode +: currentTip.children
+            currentTip.addChild(newNode)
             currentTip = newNode
           }
         }
@@ -100,10 +61,6 @@ final class Node private(var formula: Formula, val parent: Option[Node], val ori
     willExpand
   }
 
-  def isTip: Boolean = children.isEmpty
-
-
-  def ruleType: RuleType = RuleType(formula)
 
   def findTips: Seq[Node] = {
     def find(n: Node): Seq[Node] =
@@ -114,6 +71,44 @@ final class Node private(var formula: Formula, val parent: Option[Node], val ori
   }
 
   override def toString: String = {
+    def substitution(): Option[Term] = {
+      def findPredicates(f: Formula): LazyList[Formula.Predicate] = f match
+        case p: Formula.Predicate => LazyList(p)
+        case Formula.Not(formula) => findPredicates(formula)
+        case ForAll(variable, body) => findPredicates(body)
+        case Formula.Exists(variable, body) => findPredicates(body)
+        case Formula.And(a, b) => findPredicates(a) ++ findPredicates(b)
+        case Formula.Or(a, b) => findPredicates(a) ++ findPredicates(b)
+        case Formula.Equivalent(a, b) => findPredicates(a) ++ findPredicates(b)
+        case Formula.Implies(premise, conclusion) => findPredicates(premise) ++ findPredicates(conclusion)
+
+
+      originator
+        .map(_.formula).collect { case fa: ForAll => fa }.map { parentForall =>
+        val (unifiable, expanded) = Expansion.gammaExpansion(parentForall)
+        val flexiblePreds = findPredicates(expanded)
+        val rigidPreds = findPredicates(this.formula)
+        val pairs = flexiblePreds.zip(rigidPreds)
+
+        @tailrec
+        def findUnified(pairs: LazyList[(Predicate, Predicate)]): Term =
+          if pairs.isEmpty then throw new ShouldNotHappenException()
+          else {
+            val (a, b) = pairs.head
+            Unifier.unify(FormulaInterop.apply(a), FormulaInterop.apply(b)) match
+              case UnificationResult.UnificationFailure => throw new ShouldNotHappenException()
+              case UnificationResult.UnificationSuccess(substitution) =>
+                substitution.headOption match
+                  case Some((uVar, uTerm)) =>
+                    val term = FormulaInterop.toLogicTerm(uTerm)
+                    if term == unifiable then FormulaInterop.toLogicTerm(uVar) else term
+                  case None => findUnified(pairs.tail)
+          }
+
+        findUnified(pairs)
+      }
+    }
+
     def idOpt(nodeOpt: Option[Node]): String = nodeOpt.map(_.id.toString).getOrElse("")
 
     s"$formula <$id> [${idOpt(parent)}] {${idOpt(originator)}} ${substitution().map(t => s"..::$t::..").getOrElse("")}"

src/main/scala/tree/Tree.scala

@@ -166,18 +166,22 @@ final class Tree(val formula: Formula, debug: Boolean) {
       println(wasPointless.toString + " " + szs)
     }
     val doomedAlready = cnds.exists(_.isEmpty)
-    val ok = !doomedAlready && hardcoreSolve(cnds)
-    if ok then true else if maxGammaExpansions == 0 then {
-      doDebug {
-        printTree()
-        printLinear()
+    val okSub: Option[Substitution] = if !doomedAlready then hardcoreSolve(cnds) else None
+    okSub match
+      case Some(value) =>
+        doDebug(println(s"Winning sub: $value"))
+        true
+      case None => if maxGammaExpansions == 0 then {
+        doDebug {
+          printTree()
+          printLinear()
+        }
+        false
+      } else {
+        doDebug(println("expanding gammas!!!!!"))
+        val worthTryingAgain = expandGammaOnce()
+        if worthTryingAgain then solve(maxGammaExpansions - 1) else false
       }
-      false
-    } else {
-      doDebug(println("expanding gammas!!!!!"))
-      val worthTryingAgain = expandGammaOnce()
-      if worthTryingAgain then solve(maxGammaExpansions - 1) else false
-    }
   }
 
   private def hasFreeUnif(v: Seq[(Unifier.UnifierTerm, Unifier.UnifierTerm)]): Boolean =
@@ -216,37 +220,29 @@ final class Tree(val formula: Formula, debug: Boolean) {
   /**
    * This is v bad to fix later. This is also the hottest inner-loop that runs in exponential
    *
-   * @return true if ok
+   * @return working substitution, or none if no solution
    */
-  private def hardcoreSolve(candidates: Seq[Seq[(Unifier.UnifierTerm, Unifier.UnifierTerm)]]): Boolean =
+  private def hardcoreSolve(candidates: Seq[Seq[(Unifier.UnifierTerm, Unifier.UnifierTerm)]]): Option[Substitution] =
     if candidates.isEmpty then {
       doDebug(println("koniec"))
-      true
+      Some(Substitution.empty())
     } else {
       val myPart = candidates.head
 
 
       @tailrec
-      def loop(myC: Seq[(Unifier.UnifierTerm, Unifier.UnifierTerm)]): Boolean = {
-        if (myC.isEmpty) false //no candidates :(
+      def loop(myC: Seq[(Unifier.UnifierTerm, Unifier.UnifierTerm)]): Option[Substitution] = {
+        if (myC.isEmpty) None //no candidates :(
         else {
           val (candA, candB) = myC.head
           Unifier.unify(candA, candB) match {
             case UnificationResult.UnificationFailure => loop(myC.tail)
             case UnificationResult.UnificationSuccess(substitution) =>
-              backupFormulas(rootNode)
-              propc(rootNode, substitution)
-              val rest = candidates.tail.map(propcHHH(_, substitution))
-
-              val ok = hardcoreSolve(rest)
-              if ok then {
-                doDebug(println(s"znalazłem $candA - $candB"))
-                true
-              } //solution found
-              else {
-                revertlol(rootNode)
-                loop(myC.tail)
-              }
+              val rest = candidates.tail.map(propagateChanges(_, substitution))
+              hardcoreSolve(rest) match
+                case Some(subRest) => doDebug(println(s"znalazłem $candA - $candB"))
+                  Some(substitution.concat(subRest))
+                case None => loop(myC.tail)
           }
         }
       }
@@ -260,67 +256,22 @@ final class Tree(val formula: Formula, debug: Boolean) {
 
   private def doDebug(code: => Unit): Unit = if debug then code
 
-  // todo ohyda
-  private def backupFormulas(node: Node): Unit = {
-    node.pushBackup()
-    node.children.foreach(backupFormulas)
-  }
-
-  private def revertlol(node: Node): Unit = {
-    node.popBakcup()
-    node.children.foreach(revertlol)
-  }
-
-  private def propc(node: Node, sub: Substitution): Unit = {
-    val s = FormulaInterop.fixSub(sub)
-
-    def lp(n: Node): Unit = {
-      n.formula = subFormula(n.formula, s)
-      n.children.foreach(lp)
-    }
 
-    lp(node)
-  }
-
-  private def subFormula(formula: Formula, m: Map[Term.Unifiable, Term]) = {
-    def lpT(t: Term): Term = {
-      t match
-        case Term.NamedVar(name) => Term.NamedVar(name)
-        case u: Term.Unifiable => m.getOrElse(u, u)
-        case i: Term.InternVar => i
-        case Term.Function(name, args) => Term.Function(name, args.map(lpT))
-    }
-
-    def lpF(f: Formula): Formula = {
-      f match
-        case Predicate(name, args) => Predicate(name, args.map(lpT))
-        case Not(formula) => Not(lpF(formula))
-        case ForAll(variable, body) => ForAll(variable, lpF(body))
-        case Exists(variable, body) => Exists(variable, lpF(body))
-        case And(a, b) => And(lpF(a), lpF(b))
-        case Or(a, b) => Or(lpF(a), lpF(b))
-        case Equivalent(a, b) => Equivalent(lpF(a), lpF(b))
-        case Implies(premise, conclusion) => Implies(lpF(premise), lpF(conclusion))
-    }
-
-    lpF(formula)
-  }
-
-  private def propcHHH(value: Seq[(Unifier.UnifierTerm, Unifier.UnifierTerm)], substitution: Unifier.Substitution):
-  Seq[(Unifier.UnifierTerm, Unifier.UnifierTerm)] = {
-    //  Unifier.applySubstitution
+  private def propagateChanges(
+                                value: Seq[(Unifier.UnifierTerm, Unifier.UnifierTerm)],
+                                substitution: Unifier.Substitution
+                              ): Seq[(Unifier.UnifierTerm, Unifier.UnifierTerm)] =
     value.map {
       case (a, b) => (Unifier.applySubstitution(a, substitution), Unifier.applySubstitution(b, substitution))
     }
-  }
 
   def findNode(id: Int): Option[Node] = {
-    def lp(n: Node): Option[Node] = {
+    def loop(n: Node): Option[Node] = {
       if (n.id.id == id) Some(n)
-      else n.children.flatMap(lp).headOption
+      else n.children.flatMap(loop).headOption
     }
 
-    lp(rootNode)
+    loop(rootNode)
   }
 }
 

src/main/scala/unification/FormulaInterop.scala

@@ -1,9 +1,9 @@
 package pl.wojciechkarpiel.tableaux
 package unification
 
-import lang.Formula.Predicate
-import lang.{Formula, Term}
+import lang.Formula.*
 import lang.Term.{Function, FunctionName, NamedVar, Variable}
+import lang.{Formula, Term}
 import unification.Unifier
 import unification.Unifier.UnificationResult.{UnificationFailure, UnificationSuccess}
 import unification.Unifier.UnifierTerm.{Tree, Unifiable}
@@ -20,12 +20,34 @@ object FormulaInterop {
     case variable: Term.InternVar => Tree(variable, Seq(), MetadataHolder(false))
     case Term.Function(name, args) => Tree(name.name, args.map(apply), MetadataHolder(true))
 
-  def fixSub(substitution: Substitution): Map[Term.Unifiable, Term] =
-    substitution.map((a, b) => a.id -> toLogicTerm(b)).toMap
-
   def toLogicTerm(t: UnifierTerm): Term = t match
     case UnifierTerm.Tree(name, branches, meta) =>
       if meta.isFunction then Function(FunctionName(name), branches.map(toLogicTerm)) else name
     case UnifierTerm.Unifiable(id) => id
 
+
+  private def substitute(formula: Formula, substitution: Substitution) = {
+    def substituteTerm(t: Term): Term = {
+      t match
+        case Term.NamedVar(name) => Term.NamedVar(name)
+        case u: Term.Unifiable => substitution.find(Unifiable(u)).map(toLogicTerm).getOrElse(u)
+        case i: Term.InternVar => i
+        case Term.Function(name, args) => Term.Function(name, args.map(substituteTerm))
+    }
+
+    def substituteFormula(f: Formula): Formula = {
+      f match
+        case Predicate(name, args) => Predicate(name, args.map(substituteTerm))
+        case Not(formula) => Not(substituteFormula(formula))
+        case ForAll(variable, body) => ForAll(variable, substituteFormula(body))
+        case Exists(variable, body) => Exists(variable, substituteFormula(body))
+        case And(a, b) => And(substituteFormula(a), substituteFormula(b))
+        case Or(a, b) => Or(substituteFormula(a), substituteFormula(b))
+        case Equivalent(a, b) => Equivalent(substituteFormula(a), substituteFormula(b))
+        case Implies(premise, conclusion) => Implies(substituteFormula(premise), substituteFormula(conclusion))
+    }
+
+    substituteFormula(formula)
+  }
+
 }

src/main/scala/unification/Unifier.scala

@@ -3,7 +3,7 @@ package unification
 
 import lang.Formula.Predicate
 import lang.Term
-import lang.Term.{NamedVar, Variable, Constant}
+import lang.Term.{Constant, NamedVar, Variable}
 import unification.Unifier.UnificationResult.{UnificationFailure, UnificationSuccess}
 import unification.Unifier.UnifierTerm.*
 import util.MetadataHolder
@@ -35,7 +35,7 @@ object Unifier {
 
     def headOption: Option[(Unifiable, UnifierTerm)] = substitution.headOption
 
-    private def concat(other: Substitution): Substitution = substitution ++ other
+    def concat(other: Substitution): Substitution = substitution ++ other
   }
 
   object Substitution {

src/main/scala/util/Printing.scala

@@ -1,8 +1,10 @@
 package pl.wojciechkarpiel.tableaux
 package util
 
+import lang.Formula
+import lang.Formula.*
 import lang.Term
-import lang.Term.Constant
+import lang.Term.*
 
 object Printing {
   def printFunctionLike(funName: Constant, args: Seq[Term]): String = {
@@ -16,5 +18,14 @@ object Printing {
     sb.toString()
   }
 
+  def toString(formula: Formula): String = formula match
+    case Predicate(name, args) => printFunctionLike(name.name, args)
+    case Not(formula) => "(¬" + formula + ")"
+    case ForAll(variable, body) => "∀" + variable + ".(" + body + ")"
+    case Exists(variable, body) => "∃" + variable + ".(" + body + ")"
+    case And(a, b) => "(" + a + " ∧ " + b + ")"
+    case Or(a, b) => "(" + a + " ∨ " + b + ")"
+    case Equivalent(a, b) => "(" + a + " ⇔ " + b + ")"
+    case Implies(premise, conclusion) => s"($premise ⇒ $conclusion)"
 
 }