Skip to content

Simplify Boolean Expressions By Removing Redundant Literals #57

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

Closed
rcosta358 wants to merge 1 commit into from
Closed

Simplify Boolean Expressions By Removing Redundant Literals #57

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
20 changes: 10 additions & 10 deletions liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,21 +27,21 @@ public static <T> void printError(CtElement var, Predicate expectedType, Predica

public static <T> void printError(CtElement var, String moreInfo, Predicate expectedType, Predicate cSMT,
HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
String resumeMessage = "Type expected:" + expectedType.toString(); // + "; " +"Refinement found:" +
String resumeMessage = "Type expected: " + expectedType.toString(); // + "; " +"Refinement found:" +
// cSMT.toString();

StringBuilder sb = new StringBuilder();
sb.append("______________________________________________________\n");
// title
StringBuilder sbtitle = new StringBuilder();
sbtitle.append("Failed to check refinement at: \n\n");
sbtitle.append("Failed to check refinement at:\n\n");
if (moreInfo != null)
sbtitle.append(moreInfo + "\n");
sbtitle.append(var.toString());
// all message
sb.append(sbtitle.toString() + "\n\n");
sb.append("Type expected:" + expectedType.toString() + "\n");
sb.append("Refinement found:" + cSMT.toString() + "\n");
sb.append("Type expected: " + expectedType.toString() + "\n");
sb.append("Refinement found: " + cSMT.toString() + "\n");
sb.append(printMap(map));
sb.append("Location: " + var.getPosition() + "\n");
sb.append("______________________________________________________\n");
Expand All @@ -65,7 +65,7 @@ public static void printStateMismatch(CtElement element, String method, VCImplic
sbtitle.append(element + "\n\n");

sb.append(sbtitle.toString());
sb.append("Expected possible states:" + states + "\n");
sb.append("Expected possible states: " + states + "\n");
sb.append("\nState found:\n");
sb.append(printLine());
sb.append("\n" + constraintForErrorMsg /* .toConjunctions() */.toString() + "\n");
Expand Down Expand Up @@ -120,7 +120,7 @@ public static <T> void printErrorArgs(CtElement var, Predicate expectedType, Str
sb.append("______________________________________________________\n");
String title = "Error in ghost invocation: " + msg + "\n";
sb.append(title);
sb.append(var + "\nError in refinement:" + expectedType.toString() + "\n");
sb.append(var + "\nError in refinement: " + expectedType.toString() + "\n");
sb.append(printMap(map));
sb.append("Location: " + var.getPosition() + "\n");
sb.append("______________________________________________________\n");
Expand Down Expand Up @@ -151,8 +151,8 @@ public static void printSameStateSetError(CtElement element, Predicate p, String
sbtitle.append("Error found multiple disjoint states from a State Set in a refinement\n\n");
sbtitle.append(element + "\n\n");
sb.append(sbtitle.toString());
sb.append("In predicate:" + p.toString() + "\n");
sb.append("In class:" + name + "\n");
sb.append("In predicate: " + p.toString() + "\n");
sb.append("In class: " + name + "\n");
sb.append(printMap(map));
sb.append("Location: " + element.getPosition() + "\n");
sb.append("______________________________________________________\n");
Expand All @@ -163,10 +163,10 @@ public static void printSameStateSetError(CtElement element, Predicate p, String
public static void printErrorConstructorFromState(CtElement element, CtLiteral<String> from, ErrorEmitter errorl) {
StringBuilder sb = new StringBuilder();
sb.append("______________________________________________________\n");
String s = " Error found constructor with FROM state (Constructor's should only have a TO state)\n\n";
String s = "Error found constructor with 'from' state (Constructors must only have a 'to' state)\n\n";
sb.append(s);
sb.append(element + "\n\n");
sb.append("State found:" + from + "\n");
sb.append("State found: " + from + "\n");
sb.append("Location: " + element.getPosition() + "\n");
sb.append("______________________________________________________\n");

Expand Down
15 changes: 15 additions & 0 deletions liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@
import liquidjava.processor.facade.AliasDTO;
import liquidjava.rj_language.ast.BinaryExpression;
import liquidjava.rj_language.ast.Expression;
import liquidjava.rj_language.ast.LiteralBoolean;
import liquidjava.rj_language.ast.FunctionInvocation;
import liquidjava.rj_language.ast.GroupExpression;
import liquidjava.rj_language.ast.Ite;
Expand Down Expand Up @@ -189,11 +190,25 @@ public Expression getExpression() {
return exp;
}

private static boolean isBooleanLiteral(Expression expr, boolean value) {
return expr instanceof LiteralBoolean && ((LiteralBoolean) expr).isBooleanTrue() == value;
}

public static Predicate createConjunction(Predicate c1, Predicate c2) {
// simplification: (true && x) = x, (false && x) = false
if (isBooleanLiteral(c1.getExpression(), true)) return c2;
if (isBooleanLiteral(c2.getExpression(), true)) return c1;
if (isBooleanLiteral(c1.getExpression(), false)) return c1;
if (isBooleanLiteral(c2.getExpression(), false)) return c2;
return new Predicate(new BinaryExpression(c1.getExpression(), Utils.AND, c2.getExpression()));
}

public static Predicate createDisjunction(Predicate c1, Predicate c2) {
// simplification: (false || x) = x, (true || x) = true
if (isBooleanLiteral(c1.getExpression(), false)) return c2;
if (isBooleanLiteral(c2.getExpression(), false)) return c1;
if (isBooleanLiteral(c1.getExpression(), true)) return c1;
if (isBooleanLiteral(c2.getExpression(), true)) return c2;
return new Predicate(new BinaryExpression(c1.getExpression(), Utils.OR, c2.getExpression()));
}

Expand Down