Skip to content

Commit

Permalink
Remove unused fully qualified names
Browse files Browse the repository at this point in the history
  • Loading branch information
hajduakos committed Sep 1, 2020
1 parent 1e232c9 commit 26313c0
Show file tree
Hide file tree
Showing 2 changed files with 17 additions and 17 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -321,7 +321,7 @@ private com.microsoft.z3.Expr transformRef(final RefExpr<?> expr) {
}

private com.microsoft.z3.Expr transformIte(final IteExpr<?> expr) {
final com.microsoft.z3.BoolExpr condTerm = (com.microsoft.z3.BoolExpr) toTerm(expr.getCond());
final BoolExpr condTerm = (BoolExpr) toTerm(expr.getCond());
final com.microsoft.z3.Expr thenTerm = toTerm(expr.getThen());
final com.microsoft.z3.Expr elzeTerm = toTerm(expr.getElse());
return context.mkITE(condTerm, thenTerm, elzeTerm);
Expand All @@ -341,56 +341,56 @@ private com.microsoft.z3.Expr transformTrue(final TrueExpr expr) {
}

private com.microsoft.z3.Expr transformNot(final NotExpr expr) {
final com.microsoft.z3.BoolExpr opTerm = (com.microsoft.z3.BoolExpr) toTerm(expr.getOp());
final BoolExpr opTerm = (BoolExpr) toTerm(expr.getOp());
return context.mkNot(opTerm);
}

private com.microsoft.z3.Expr transformImply(final ImplyExpr expr) {
final com.microsoft.z3.BoolExpr leftOpTerm = (com.microsoft.z3.BoolExpr) toTerm(expr.getLeftOp());
final com.microsoft.z3.BoolExpr rightOpTerm = (com.microsoft.z3.BoolExpr) toTerm(expr.getRightOp());
final BoolExpr leftOpTerm = (BoolExpr) toTerm(expr.getLeftOp());
final BoolExpr rightOpTerm = (BoolExpr) toTerm(expr.getRightOp());
return context.mkImplies(leftOpTerm, rightOpTerm);
}

private com.microsoft.z3.Expr transformIff(final IffExpr expr) {
final com.microsoft.z3.BoolExpr leftOpTerm = (com.microsoft.z3.BoolExpr) toTerm(expr.getLeftOp());
final com.microsoft.z3.BoolExpr rightOpTerm = (com.microsoft.z3.BoolExpr) toTerm(expr.getRightOp());
final BoolExpr leftOpTerm = (BoolExpr) toTerm(expr.getLeftOp());
final BoolExpr rightOpTerm = (BoolExpr) toTerm(expr.getRightOp());
return context.mkIff(leftOpTerm, rightOpTerm);
}

private com.microsoft.z3.Expr transformXor(final XorExpr expr) {
final com.microsoft.z3.BoolExpr leftOpTerm = (com.microsoft.z3.BoolExpr) toTerm(expr.getLeftOp());
final com.microsoft.z3.BoolExpr rightOpTerm = (com.microsoft.z3.BoolExpr) toTerm(expr.getRightOp());
final BoolExpr leftOpTerm = (BoolExpr) toTerm(expr.getLeftOp());
final BoolExpr rightOpTerm = (BoolExpr) toTerm(expr.getRightOp());
return context.mkXor(leftOpTerm, rightOpTerm);
}

private com.microsoft.z3.Expr transformAnd(final AndExpr expr) {
final com.microsoft.z3.BoolExpr[] opTerms = expr.getOps().stream()
.map(e -> (com.microsoft.z3.BoolExpr) toTerm(e))
final BoolExpr[] opTerms = expr.getOps().stream()
.map(e -> (BoolExpr) toTerm(e))
.toArray(BoolExpr[]::new);
return context.mkAnd(opTerms);
}

private com.microsoft.z3.Expr transformOr(final OrExpr expr) {
final com.microsoft.z3.BoolExpr[] opTerms = expr.getOps().stream()
.map(e -> (com.microsoft.z3.BoolExpr) toTerm(e))
final BoolExpr[] opTerms = expr.getOps().stream()
.map(e -> (BoolExpr) toTerm(e))
.toArray(BoolExpr[]::new);
return context.mkOr(opTerms);
}

private com.microsoft.z3.Expr transformExists(final ExistsExpr expr) {
env.push();
final com.microsoft.z3.Expr[] paramTerms = transformParamDecls(expr.getParamDecls());
final com.microsoft.z3.BoolExpr opTerm = (com.microsoft.z3.BoolExpr) toTerm(expr.getOp());
final com.microsoft.z3.BoolExpr result = context.mkExists(paramTerms, opTerm, 1, null, null, null, null);
final BoolExpr opTerm = (BoolExpr) toTerm(expr.getOp());
final BoolExpr result = context.mkExists(paramTerms, opTerm, 1, null, null, null, null);
env.pop();
return result;
}

private com.microsoft.z3.Expr transformForall(final ForallExpr expr) {
env.push();
final com.microsoft.z3.Expr[] paramTerms = transformParamDecls(expr.getParamDecls());
final com.microsoft.z3.BoolExpr opTerm = (com.microsoft.z3.BoolExpr) toTerm(expr.getOp());
final com.microsoft.z3.BoolExpr result = context.mkForall(paramTerms, opTerm, 1, null, null, null, null);
final BoolExpr opTerm = (BoolExpr) toTerm(expr.getOp());
final BoolExpr result = context.mkForall(paramTerms, opTerm, 1, null, null, null, null);
env.pop();
return result;
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -106,7 +106,7 @@ public boolean equals(final Object obj) {

@Override
public String toString() {
return Utils.lispStringBuilder(label.getName()).add(kind == Kind.EMIT ? "!" : "?").addAll(args).toString();
return Utils.lispStringBuilder(label.getName()).add(kind == EMIT ? "!" : "?").addAll(args).toString();
}

}

0 comments on commit 26313c0

Please sign in to comment.