Skip to content

[Symex] Bugfix in ConstraintSimplifier for constraints with negated universal quantifiers #68

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
dawa6183 wants to merge 2 commits into
base: master
Choose a base branch
from
Draft

[Symex] Bugfix in ConstraintSimplifier for constraints with negated universal quantifiers #68

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
6de3e39
Add type declarations
wallgrenen Nov 6, 2024
3066e72
Bugfix: Only negated universal quantifiers are disjunctions, not nega…
wallgrenen Nov 6, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 6 additions & 5 deletions src/main/scala/lazabs/horn/symex/ConstraintSimplifier.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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.
Expand All @@ -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 =
Expand Down