From ece582951a8cd904c08cbd264c963494140ca91e Mon Sep 17 00:00:00 2001 From: wallgrenen Date: Wed, 6 Nov 2024 10:40:08 +0100 Subject: [PATCH 1/2] Only generate counterexample if the user asks for it --- src/main/scala/lazabs/horn/HornWrapper.scala | 1 + src/main/scala/lazabs/horn/symex/Symex.scala | 16 ++++++++++++++-- 2 files changed, 15 insertions(+), 2 deletions(-) diff --git a/src/main/scala/lazabs/horn/HornWrapper.scala b/src/main/scala/lazabs/horn/HornWrapper.scala index d23e6372..4c687c3f 100644 --- a/src/main/scala/lazabs/horn/HornWrapper.scala +++ b/src/main/scala/lazabs/horn/HornWrapper.scala @@ -629,6 +629,7 @@ class SymexHornWrapper(unsimplifiedClauses : Seq[Clause], "--------------------------------------") symex.printInfo = lazabs.GlobalParameters.get.log + symex.generateCounterExample = lazabs.GlobalParameters.get.plainCEX || lazabs.GlobalParameters.get.simplifiedCEX symex.solve() } diff --git a/src/main/scala/lazabs/horn/symex/Symex.scala b/src/main/scala/lazabs/horn/symex/Symex.scala index 821b6a83..cf2a4d16 100644 --- a/src/main/scala/lazabs/horn/symex/Symex.scala +++ b/src/main/scala/lazabs/horn/symex/Symex.scala @@ -56,6 +56,10 @@ abstract class Symex[CC](iClauses: Iterable[CC])( import Symex._ var printInfo = false + + // This might be set to true in SymexHornWrapper + var generateCounterExample = false + def printInfo(s : String, newLine : Boolean = true) : Unit = { if (printInfo) print(s + (if (newLine) "\n" else "")) @@ -227,7 +231,11 @@ abstract class Symex[CC](iClauses: Iterable[CC])( val proverStatus = checkFeasibility(newElectron.constraint) if (hasContradiction(newElectron, proverStatus)) { // false :- true unitClauseDB.add(newElectron, (nucleus, electrons)) - result = Right(buildCounterExample(newElectron)) + if (generateCounterExample) { + result = Right(buildCounterExample(newElectron)) + } else { + result = Right(DagEmpty) + } } else if (constraintIsFalse(newElectron, proverStatus)) { printInfo("") handleFalseConstraint(nucleus, electrons) @@ -277,7 +285,11 @@ abstract class Symex[CC](iClauses: Iterable[CC])( } else toUnitClause(clause) unitClauseDB.add(cuc, (clause, Nil)) if (hasContradiction(cuc, checkFeasibility(cuc.constraint))) { - result = Right(buildCounterExample(cuc)) + if (generateCounterExample) { + result = Right(buildCounterExample(cuc)) + } else { + result = Right(DagEmpty) + } } } if (result == null) { // none of the assertions failed, so this is SAT From 6d720d1bf6a6bdd0ed1a0c86a7dfc90cce8e043b Mon Sep 17 00:00:00 2001 From: wallgrenen Date: Wed, 6 Nov 2024 15:29:12 +0100 Subject: [PATCH 2/2] Fix PR comment: remove local variable. Check for needFullCEX instead of plainCEX --- src/main/scala/lazabs/horn/HornWrapper.scala | 3 +-- src/main/scala/lazabs/horn/symex/Symex.scala | 10 +++++----- 2 files changed, 6 insertions(+), 7 deletions(-) diff --git a/src/main/scala/lazabs/horn/HornWrapper.scala b/src/main/scala/lazabs/horn/HornWrapper.scala index 4c687c3f..082eb759 100644 --- a/src/main/scala/lazabs/horn/HornWrapper.scala +++ b/src/main/scala/lazabs/horn/HornWrapper.scala @@ -629,7 +629,6 @@ class SymexHornWrapper(unsimplifiedClauses : Seq[Clause], "--------------------------------------") symex.printInfo = lazabs.GlobalParameters.get.log - symex.generateCounterExample = lazabs.GlobalParameters.get.plainCEX || lazabs.GlobalParameters.get.simplifiedCEX symex.solve() } @@ -646,7 +645,7 @@ class SymexHornWrapper(unsimplifiedClauses : Seq[Clause], HornWrapper.verifySolution(fullSol, unsimplifiedClauses) fullSol } else { - // only keep relation symbols that were also part of the orginal problem + // only keep relation symbols that were also part of the original problem res filterKeys allPredicates(unsimplifiedClauses) } } diff --git a/src/main/scala/lazabs/horn/symex/Symex.scala b/src/main/scala/lazabs/horn/symex/Symex.scala index cf2a4d16..3362eee5 100644 --- a/src/main/scala/lazabs/horn/symex/Symex.scala +++ b/src/main/scala/lazabs/horn/symex/Symex.scala @@ -37,6 +37,7 @@ import ap.terfor._ import ap.terfor.conjunctions.Conjunction import ap.terfor.substitutions.ConstantSubst import ap.theories.{Theory, TheoryCollector} +import lazabs.GlobalParameters import lazabs.horn.bottomup.{HornClauses, NormClause, RelationSymbol} import lazabs.horn.bottomup.HornClauses.ConstraintClause import lazabs.horn.Util.{Dag, DagEmpty, DagNode} @@ -57,9 +58,6 @@ abstract class Symex[CC](iClauses: Iterable[CC])( var printInfo = false - // This might be set to true in SymexHornWrapper - var generateCounterExample = false - def printInfo(s : String, newLine : Boolean = true) : Unit = { if (printInfo) print(s + (if (newLine) "\n" else "")) @@ -231,7 +229,8 @@ abstract class Symex[CC](iClauses: Iterable[CC])( val proverStatus = checkFeasibility(newElectron.constraint) if (hasContradiction(newElectron, proverStatus)) { // false :- true unitClauseDB.add(newElectron, (nucleus, electrons)) - if (generateCounterExample) { + if (GlobalParameters.get.needFullCEX || lazabs.GlobalParameters.get.simplifiedCEX) { + // Only generate a counterexample when it is asked for result = Right(buildCounterExample(newElectron)) } else { result = Right(DagEmpty) @@ -285,7 +284,8 @@ abstract class Symex[CC](iClauses: Iterable[CC])( } else toUnitClause(clause) unitClauseDB.add(cuc, (clause, Nil)) if (hasContradiction(cuc, checkFeasibility(cuc.constraint))) { - if (generateCounterExample) { + if (GlobalParameters.get.needFullCEX || lazabs.GlobalParameters.get.simplifiedCEX) { + // Only generate a counterexample when it is asked for result = Right(buildCounterExample(cuc)) } else { result = Right(DagEmpty)