Skip to content

Commit

Permalink
eliminated a case of non-determinism
Browse files Browse the repository at this point in the history
  • Loading branch information
pruemmer committed Feb 28, 2024
1 parent e19dc69 commit ca5237d
Showing 1 changed file with 7 additions and 8 deletions.
15 changes: 7 additions & 8 deletions src/main/scala/lazabs/horn/bottomup/HornPredAbsContext.scala
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/**
* Copyright (c) 2011-2021 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:
Expand Down Expand Up @@ -40,7 +40,7 @@ import ap.types.TypeTheory
import ap.parameters.{Param, GoalSettings}
import ap.util.Timeout

import scala.collection.mutable.{LinkedHashMap, ArrayBuffer}
import scala.collection.mutable.{LinkedHashMap, ArrayBuffer, LinkedHashSet}
import scala.util.Random

trait HornPredAbsContext[CC] {
Expand Down Expand Up @@ -192,12 +192,11 @@ class HornPredAbsContextImpl[CC <% HornClauses.ConstraintClause]
implicit val sf = new SymbolFactory(theories)

val relationSymbols = {
val preds =
(for (c <- iClauses.iterator;
lit <- (Iterator single c.head) ++ c.body.iterator;
p = lit.predicate)
yield p).toSet
(for (p <- preds) yield (p -> RelationSymbol(p))).toMap
val preds = new LinkedHashSet[Predicate]
for (c <- iClauses;
lit <- (Iterator single c.head) ++ c.body.iterator)
preds += lit.predicate
(for (p <- preds.iterator) yield (p -> RelationSymbol(p))).toMap
}

// make sure that arguments constants have been instantiated
Expand Down

0 comments on commit ca5237d

Please sign in to comment.