replaced the Tree class with ap.basetypes.Tree

uuverifiers · Mar 11, 2024 · e1bb651 · e1bb651
1 parent 4345836
commit e1bb651
Show file tree

Hide file tree

Showing 9 changed files with 17 additions and 88 deletions.
diff --git a/src/main/scala/lazabs/horn/Util.scala b/src/main/scala/lazabs/horn/Util.scala
@@ -29,8 +29,7 @@
 
 package lazabs.horn
 
-import lazabs.prover.Tree
-
+import ap.basetypes.Tree
 import ap.terfor.conjunctions.Conjunction
 
 import scala.collection.mutable.{HashMap => MHashMap}

diff --git a/src/main/scala/lazabs/horn/bottomup/HornWrapper.scala b/src/main/scala/lazabs/horn/bottomup/HornWrapper.scala
@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2011-2023 Hossein Hojjat and Philipp Ruemmer.
+ * Copyright (c) 2011-2024 Hossein Hojjat and Philipp Ruemmer.
  * All rights reserved.
  * 
  * Redistribution and use in source and binary forms, with or without
@@ -35,6 +35,7 @@ import IExpression._
 import ap.SimpleAPI
 import ap.SimpleAPI.ProverStatus
 import ap.types.MonoSortedPredicate
+import ap.basetypes.Tree
 
 import lazabs.GlobalParameters
 import lazabs.ParallelComputation
@@ -46,7 +47,6 @@ import lazabs.horn.global._
 import lazabs.utils.Manip._
 import lazabs.prover.PrincessWrapper
 import PrincessWrapper._
-import lazabs.prover.Tree
 import lazabs.types.Type
 import lazabs.horn.Util._
 import lazabs.horn.predgen.Interpolators

diff --git a/src/main/scala/lazabs/horn/predgen/BSTreeInterpolator.scala b/src/main/scala/lazabs/horn/predgen/BSTreeInterpolator.scala
@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2011-2023 Philipp Ruemmer. All rights reserved.
+ * Copyright (c) 2011-2024 Philipp Ruemmer. All rights reserved.
  * 
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are met:
@@ -29,15 +29,14 @@
 
 package lazabs.horn.predgen
 
+import ap.basetypes.Tree
 import ap.interpolants.{ProofSimplifier, InterpolationContext, Interpolator}
 import ap.parser.{PartName, IInterpolantSpec}
 import ap.proof.certificates.Certificate
 import ap.terfor.conjunctions.Conjunction
 import ap.terfor.{TermOrder, ConstantTerm}
 import ap.terfor.substitutions.ConstantSubst
 
-import lazabs.prover.Tree
-
 import scala.collection.mutable.{ArrayBuffer, HashSet => MHashSet,
                                  HashMap => MHashMap}
 

diff --git a/src/main/scala/lazabs/horn/predgen/DagInterpolator.scala b/src/main/scala/lazabs/horn/predgen/DagInterpolator.scala
@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2011-2023 Philipp Ruemmer. All rights reserved.
+ * Copyright (c) 2011-2024 Philipp Ruemmer. All rights reserved.
  * 
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are met:
@@ -30,6 +30,7 @@
 package lazabs.horn.predgen
 
 import ap.basetypes.{IdealInt, UnionFind}
+import ap.basetypes.{Tree, Leaf}
 import ap.parser._
 import ap.Signature
 import ap.theories.{Theory, TheoryCollector}
@@ -40,7 +41,6 @@ import ap.terfor.substitutions.{ConstantSubst, VariableSubst}
 import ap.proof.{ModelSearchProver, QuantifierElimProver}
 import ap.util.Seqs
 
-import lazabs.prover.{Tree, Leaf}
 import lazabs.horn.Util._
 import DisjInterpolator.predicateGenerator
 import PredicateGenerator.{AndOrNode, AndNode, OrNode}

diff --git a/src/main/scala/lazabs/horn/predgen/DisjInterpolator.scala b/src/main/scala/lazabs/horn/predgen/DisjInterpolator.scala
@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2011-2023 Philipp Ruemmer. All rights reserved.
+ * Copyright (c) 2011-2024 Philipp Ruemmer. All rights reserved.
  * 
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are met:
@@ -29,6 +29,7 @@
 
 package lazabs.horn.predgen
 
+import ap.basetypes.{Tree, Leaf}
 import ap.theories.{Theory, TheoryCollector}
 import ap.terfor.conjunctions.{Conjunction, ReduceWithConjunction,
                                LazyConjunction}
@@ -41,7 +42,6 @@ import ap.Signature
 import ap.util.Timeout
 import IExpression.{ConstantTerm, Predicate}
 
-import lazabs.prover.{Tree, Leaf}
 import lazabs.horn.Util._
 
 import lazabs.horn.bottomup.HornClauses._

diff --git a/src/main/scala/lazabs/horn/predgen/LinTreeInterpolator.scala b/src/main/scala/lazabs/horn/predgen/LinTreeInterpolator.scala
@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2011-2023 Philipp Ruemmer. All rights reserved.
+ * Copyright (c) 2011-2024 Philipp Ruemmer. All rights reserved.
  * 
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are met:
@@ -29,6 +29,7 @@
 
 package lazabs.horn.predgen
 
+import ap.basetypes.Tree
 import ap.interpolants.{ProofSimplifier, InterpolationContext, Interpolator}
 import ap.parser.{PartName, IInterpolantSpec}
 import ap.proof.certificates.Certificate
@@ -38,8 +39,6 @@ import ap.util.Timeout
 
 import ap.proof.certificates.{CertificatePrettyPrinter, CertFormula}
 
-import lazabs.prover.Tree
-
 import scala.collection.mutable.{ArrayBuffer, HashSet => MHashSet,
                                  HashMap => MHashMap}
 

diff --git a/src/main/scala/lazabs/horn/predgen/TemplateInterpolator.scala b/src/main/scala/lazabs/horn/predgen/TemplateInterpolator.scala
@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2011-2023 Philipp Ruemmer and Pavle Subotic.
+ * Copyright (c) 2011-2024 Philipp Ruemmer and Pavle Subotic.
  * All rights reserved.
  * 
  * Redistribution and use in source and binary forms, with or without
@@ -37,6 +37,7 @@ import lazabs.horn.abstractions.{AbsLattice, TermSubsetLattice, ProductLattice,
 import AbstractionRecord.AbstractionMap
 
 import ap.basetypes.IdealInt
+import ap.basetypes.{Tree, Leaf}
 import ap.parser._
 import ap.theories.TheoryCollector
 import ap.terfor.{ConstantTerm, TermOrder, TerForConvenience, Term, OneTerm, Formula}
@@ -48,7 +49,6 @@ import ap.proof.{ModelSearchProver, QuantifierElimProver}
 import ap.util.Seqs
 import ap.util.Timeout
 
-import lazabs.prover.{Tree, Leaf}
 import lazabs.horn.Util._
 import PredicateGenerator.{AndOrNode, AndNode, OrNode}
 import lazabs.horn.bottomup.{NormClause, RelationSymbol, HornClauses}

diff --git a/src/main/scala/lazabs/horn/predgen/TreeInterpolator.scala b/src/main/scala/lazabs/horn/predgen/TreeInterpolator.scala
@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2011-2023 Philipp Ruemmer. All rights reserved.
+ * Copyright (c) 2011-2024 Philipp Ruemmer. All rights reserved.
  * 
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are met:
@@ -29,7 +29,7 @@
 
 package lazabs.horn.predgen
 
-import ap.basetypes.IdealInt
+import ap.basetypes.{IdealInt, Tree}
 import ap.parameters.{Param, GoalSettings}
 import ap.parser.PartName
 import ap.theories.Theory
@@ -48,8 +48,6 @@ import ap.util.Seqs
 
 import lazabs.horn.Util
 
-import lazabs.prover.Tree
-
 import scala.collection.mutable.{ArrayBuffer, HashSet => MHashSet,
                                  HashMap => MHashMap}
 

diff --git a/src/main/scala/lazabs/prover/PrincessAPI.scala b/src/main/scala/lazabs/prover/PrincessAPI.scala
@@ -32,10 +32,8 @@ package lazabs.prover
 
 import lazabs.GlobalParameters
 
-import scala.collection.mutable.ArrayBuffer
-
 import ap.SimpleAPI
-import ap.basetypes.IdealInt
+import ap.basetypes.{IdealInt, Tree}
 import ap.parser._
 import ap.parser.IExpression._
 import ap.Signature
@@ -52,71 +50,7 @@ import ap.interpolants.{Interpolator, InterpolationContext, ProofSimplifier,
 import ap.terfor.conjunctions.Quantifier
 import ap.util.LRUCache
 
-import scala.collection.mutable.{ArrayBuffer, ArrayStack}
-
-////////////////////////////////////////////////////////////////////////////////
-
-object Leaf {
-  def apply[D](d : D) = Tree(d, List())
-  def unapply[D](t : Tree[D]) : Option[D] = t match {
-    case Tree(d, List()) => Some(d)
-    case _ => None
-  }
-}
-
-case class Tree[D](d : D, children : List[Tree[D]]) {
-  def map[E](f : D => E) : Tree[E] = {
-    val newD = f(d)
-    Tree(newD, children map (_ map f))
-  }
-  def mapUpDown(f : D => D) : Tree[D] = {
-    val newD = f(d)
-    val newChildren = children map (_ map f)
-    Tree(f(newD), newChildren)
-  }
-  def foreach[U](f : D => U) : Unit = {
-    f(d)
-    for (c <- children) c foreach f
-  }
-  def zip[E](t : Tree[E]) : Tree[(D, E)] = t match {
-    case Tree(e, children2) =>
-      Tree((d, e),
-           for ((c1, c2) <- children zip children2)
-           yield (c1 zip c2))
-  }
-  def unzip[D1, D2](implicit asPair: D => (D1, D2)): (Tree[D1], Tree[D2]) = {
-    val (children1, children2) = (for (c <- children) yield c.unzip).unzip
-    val (d1, d2) = asPair(d)
-    (Tree(d1, children1), Tree(d2, children2))
-  }
-  def subtrees : Tree[Tree[D]] =
-    Tree(this, for (c <- children) yield c.subtrees)
-  def toList : List[D] = iterator.toList
-  def toSeq = toList
-  def toSet = iterator.toSet
-  def iterator = new Iterator[D] {
-    val todo = new ArrayStack[Tree[D]]
-    todo push Tree.this
-    def hasNext = !todo.isEmpty
-    def next = {
-      val Tree(data, children) = todo.pop
-      for (c <- children)
-        todo push c
-      data
-    }
-  }
-
-  def prettyPrint : Unit =
-    prettyPrint("")
-
-  def prettyPrint(indent : String) : Unit = {
-    val newIndent = indent + "   "
-    println(indent + d)
-    for (c <- children) (c prettyPrint newIndent)
-  }
-
-  def size = iterator.size
-}
+import scala.collection.mutable.ArrayBuffer
 
 ////////////////////////////////////////////////////////////////////////////////