From 6de3e39ec71c31fe54fdebd65d80e9f41e598506 Mon Sep 17 00:00:00 2001 From: wallgrenen Date: Wed, 6 Nov 2024 11:02:16 +0100 Subject: [PATCH 1/2] Add type declarations --- src/main/scala/lazabs/horn/symex/ConstraintSimplifier.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/scala/lazabs/horn/symex/ConstraintSimplifier.scala b/src/main/scala/lazabs/horn/symex/ConstraintSimplifier.scala index a7364f84..793913f3 100644 --- a/src/main/scala/lazabs/horn/symex/ConstraintSimplifier.scala +++ b/src/main/scala/lazabs/horn/symex/ConstraintSimplifier.scala @@ -54,14 +54,14 @@ trait ConstraintSimplifierUsingConjunctEliminator extends ConstraintSimplifier { order: TermOrder) extends ConjunctEliminator(constraint, localSymbols, Set(), order) { - override protected def nonUniversalElimination(f: Conjunction) = {} + override protected def nonUniversalElimination(f: Conjunction): Unit = {} // todo: check if this eliminates function applications // e.g., unused select and stores protected def universalElimination(m: ModelElement): Unit = {} - override protected def addDivisibility(f: Conjunction) = {} + override protected def addDivisibility(f: Conjunction): Unit = {} override protected def isEliminationCandidate(t: Term): Boolean = localSymbols contains t From 3066e72e9fb101e6a8ad800d10ace65f43edfced Mon Sep 17 00:00:00 2001 From: wallgrenen Date: Wed, 6 Nov 2024 11:04:38 +0100 Subject: [PATCH 2/2] Bugfix: Only negated universal quantifiers are disjunctions, not negated existential quantifiers --- .../scala/lazabs/horn/symex/ConstraintSimplifier.scala | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/main/scala/lazabs/horn/symex/ConstraintSimplifier.scala b/src/main/scala/lazabs/horn/symex/ConstraintSimplifier.scala index 793913f3..c620f211 100644 --- a/src/main/scala/lazabs/horn/symex/ConstraintSimplifier.scala +++ b/src/main/scala/lazabs/horn/symex/ConstraintSimplifier.scala @@ -80,7 +80,8 @@ trait ConstraintSimplifierUsingConjunctEliminator extends ConstraintSimplifier { symex_sf.reducer(Conjunction.TRUE)(constraint) else constraint - if (constraint.negatedConjs.isEmpty) { + if (constraint.negatedConjs.isEmpty || + constraint.negatedConjs.forall(x => x.quans.head != ap.terfor.conjunctions.Quantifier.ALL)) { /** * If the constraint is a conjunction, we can use the * [[ConjunctEliminator]] class for simplification. @@ -91,8 +92,8 @@ trait ConstraintSimplifierUsingConjunctEliminator extends ConstraintSimplifier { .eliminate(ComputationLogger.NonLogger) } else { /** - * If there are disjunctions, then try another method of - * simplification. + * If there are disjunctions (negated universal quantifiers), + * then try another method of simplification. */ // quantify local symbols val sortedLocalSymbols =