<commit_before>package de.bmoth.backend;

import java.util.LinkedList;
import java.util.List;

import com.microsoft.z3.ArithExpr;
import com.microsoft.z3.ArrayExpr;
import com.microsoft.z3.BoolExpr;
import com.microsoft.z3.Context;
import com.microsoft.z3.DatatypeExpr;
import com.microsoft.z3.Expr;
import com.microsoft.z3.IntExpr;
import com.microsoft.z3.IntNum;
import com.microsoft.z3.Quantifier;
import com.microsoft.z3.Sort;
import com.microsoft.z3.Symbol;
import com.microsoft.z3.TupleSort;

import de.bmoth.parser.Parser;
import de.bmoth.parser.ast.AbstractVisitor;
import de.bmoth.parser.ast.nodes.DeclarationNode;
import de.bmoth.parser.ast.nodes.ExprNode;
import de.bmoth.parser.ast.nodes.ExpressionOperatorNode;
import de.bmoth.parser.ast.nodes.ExpressionOperatorNode.ExpressionOperator;
import de.bmoth.parser.ast.nodes.FormulaNode;
import de.bmoth.parser.ast.nodes.FormulaNode.FormulaType;
import de.bmoth.parser.ast.nodes.IdentifierExprNode;
import de.bmoth.parser.ast.nodes.IdentifierPredicateNode;
import de.bmoth.parser.ast.nodes.NumberNode;
import de.bmoth.parser.ast.nodes.ParallelSubstitutionNode;
import de.bmoth.parser.ast.nodes.PredicateNode;
import de.bmoth.parser.ast.nodes.PredicateOperatorNode;
import de.bmoth.parser.ast.nodes.PredicateOperatorWithExprArgsNode;
import de.bmoth.parser.ast.nodes.QuantifiedExpressionNode;
import de.bmoth.parser.ast.nodes.QuantifiedPredicateNode;
import de.bmoth.parser.ast.nodes.SelectSubstitutionNode;
import de.bmoth.parser.ast.nodes.SingleAssignSubstitution;
import de.bmoth.parser.ast.types.BoolType;
import de.bmoth.parser.ast.types.CoupleType;
import de.bmoth.parser.ast.types.IntegerType;
import de.bmoth.parser.ast.types.SequenceType;
import de.bmoth.parser.ast.types.SetType;
import de.bmoth.parser.ast.types.Type;

/**
 * This class translates a FormulaNode of the parser to a z3 backend node.
 *
 * The second parameter of the AbstractVisitor class is the method parameter of
 * each method which is inherited form the AbstractVisitor class. In the
 * FormulaTranslator this parameter is not needed. Hence, the placeholder class
 * Void is used. Furthermore, each call to a visitXXX method of the
 * AbstractVisitor class should use the argument null.
 **/
public class FormulaToZ3Translator extends AbstractVisitor<Expr, Void> {

    private Context z3Context;
    // the context which is used to create z3 objects
    private final LinkedList<BoolExpr> constraintList = new LinkedList<>();
    // A list of z3 constraints which are separately created by the translation.
    // For example, for the B keyword NATURAL an ordinary z3 identifier will be
    // created because there no corresponding keyword in z3.
    // Additionally, a constraint axiomatizing this identifier will be added to
    // this list.
    private int tempoVariablesCounter = 0;
    // used to generate unique identifiers

    public FormulaToZ3Translator(Context z3Context) {
        this.z3Context = z3Context;
    }

    private String createFreshTemporaryVariable() {
        this.tempoVariablesCounter++;
        return "$t_" + this.tempoVariablesCounter;
    }

    public static BoolExpr translatePredicate(String formula, Context z3Context) {
        FormulaNode node = Parser.getFormulaAsSemanticAst(formula);
        if (node.getFormulaType() != FormulaType.PREDICATE_FORMULA) {
            throw new RuntimeException("Expected predicate.");
        }
        FormulaToZ3Translator formulaTranslator = new FormulaToZ3Translator(z3Context);
        Expr constraint = formulaTranslator.visitPredicateNode((PredicateNode) node.getFormula(), null);
        if (!(constraint instanceof BoolExpr)) {
            throw new RuntimeException("Invalid translation. Expected BoolExpr but found " + constraint.getClass());
        }

        BoolExpr boolExpr = (BoolExpr) constraint;
        // adding all additional constraints to result
        for (BoolExpr bExpr : formulaTranslator.constraintList) {
            boolExpr = z3Context.mkAnd(boolExpr, bExpr);
        }
        return boolExpr;
    }

    @Override
    public Expr visitIdentifierExprNode(IdentifierExprNode node, Void n) {
        Type type = node.getDeclarationNode().getType();
        return z3Context.mkConst(node.getName(), bTypeToZ3Sort(type));

    }

    @Override
    public Expr visitIdentifierPredicateNode(IdentifierPredicateNode node, Void n) {
        return z3Context.mkBoolConst(node.getName());
    }

    @Override
    public Expr visitPredicateOperatorWithExprArgs(PredicateOperatorWithExprArgsNode node, Void n) {
        final List<ExprNode> expressionNodes = node.getExpressionNodes();
        switch (node.getOperator()) {
        case EQUAL: {
            Expr left = visitExprNode(expressionNodes.get(0), null);
            Expr right = visitExprNode(expressionNodes.get(1), null);
            return z3Context.mkEq(left, right);
        }
        case NOT_EQUAL: {
            Expr left = visitExprNode(expressionNodes.get(0), null);
            Expr right = visitExprNode(expressionNodes.get(1), null);
            return z3Context.mkNot(z3Context.mkEq(left, right));
        }
        case ELEMENT_OF: {
            Expr left = visitExprNode(expressionNodes.get(0), null);
            ArrayExpr right = (ArrayExpr) visitExprNode(expressionNodes.get(1), null);
            return z3Context.mkSetMembership(left, right);
        }
        case LESS_EQUAL:
            break;
        case LESS: {
            ArithExpr left = (ArithExpr) visitExprNode(expressionNodes.get(0), null);
            ArithExpr right = (ArithExpr) visitExprNode(expressionNodes.get(1), null);
            return z3Context.mkLt(left, right);
        }
        case GREATER_EQUAL:
            break;
        case GREATER: {
            ArithExpr left = (ArithExpr) visitExprNode(expressionNodes.get(0), null);
            ArithExpr right = (ArithExpr) visitExprNode(expressionNodes.get(1), null);
            return z3Context.mkGt(left, right);
        }
        default:
            break;
        }
        // TODO
        throw new AssertionError("Not implemented: " + node.getOperator());
    }

    @Override
    public Expr visitExprOperatorNode(ExpressionOperatorNode node, Void n) {
        List<ExprNode> expressionNodes = node.getExpressionNodes();
        switch (node.getOperator()) {
        case PLUS: {<commit_msg>FormulaToZ3Translator (Arithmetic) - Relational Operators<commit_after>package de.bmoth.backend;

import java.util.LinkedList;
import java.util.List;

import com.microsoft.z3.ArithExpr;
import com.microsoft.z3.ArrayExpr;
import com.microsoft.z3.BoolExpr;
import com.microsoft.z3.Context;
import com.microsoft.z3.DatatypeExpr;
import com.microsoft.z3.Expr;
import com.microsoft.z3.IntExpr;
import com.microsoft.z3.IntNum;
import com.microsoft.z3.Quantifier;
import com.microsoft.z3.Sort;
import com.microsoft.z3.Symbol;
import com.microsoft.z3.TupleSort;

import de.bmoth.parser.Parser;
import de.bmoth.parser.ast.AbstractVisitor;
import de.bmoth.parser.ast.nodes.DeclarationNode;
import de.bmoth.parser.ast.nodes.ExprNode;
import de.bmoth.parser.ast.nodes.ExpressionOperatorNode;
import de.bmoth.parser.ast.nodes.ExpressionOperatorNode.ExpressionOperator;
import de.bmoth.parser.ast.nodes.FormulaNode;
import de.bmoth.parser.ast.nodes.FormulaNode.FormulaType;
import de.bmoth.parser.ast.nodes.IdentifierExprNode;
import de.bmoth.parser.ast.nodes.IdentifierPredicateNode;
import de.bmoth.parser.ast.nodes.NumberNode;
import de.bmoth.parser.ast.nodes.ParallelSubstitutionNode;
import de.bmoth.parser.ast.nodes.PredicateNode;
import de.bmoth.parser.ast.nodes.PredicateOperatorNode;
import de.bmoth.parser.ast.nodes.PredicateOperatorWithExprArgsNode;
import de.bmoth.parser.ast.nodes.QuantifiedExpressionNode;
import de.bmoth.parser.ast.nodes.QuantifiedPredicateNode;
import de.bmoth.parser.ast.nodes.SelectSubstitutionNode;
import de.bmoth.parser.ast.nodes.SingleAssignSubstitution;
import de.bmoth.parser.ast.types.BoolType;
import de.bmoth.parser.ast.types.CoupleType;
import de.bmoth.parser.ast.types.IntegerType;
import de.bmoth.parser.ast.types.SequenceType;
import de.bmoth.parser.ast.types.SetType;
import de.bmoth.parser.ast.types.Type;

/**
 * This class translates a FormulaNode of the parser to a z3 backend node.
 *
 * The second parameter of the AbstractVisitor class is the method parameter of
 * each method which is inherited form the AbstractVisitor class. In the
 * FormulaTranslator this parameter is not needed. Hence, the placeholder class
 * Void is used. Furthermore, each call to a visitXXX method of the
 * AbstractVisitor class should use the argument null.
 **/
public class FormulaToZ3Translator extends AbstractVisitor<Expr, Void> {

    private Context z3Context;
    // the context which is used to create z3 objects
    private final LinkedList<BoolExpr> constraintList = new LinkedList<>();
    // A list of z3 constraints which are separately created by the translation.
    // For example, for the B keyword NATURAL an ordinary z3 identifier will be
    // created because there no corresponding keyword in z3.
    // Additionally, a constraint axiomatizing this identifier will be added to
    // this list.
    private int tempoVariablesCounter = 0;
    // used to generate unique identifiers

    public FormulaToZ3Translator(Context z3Context) {
        this.z3Context = z3Context;
    }

    private String createFreshTemporaryVariable() {
        this.tempoVariablesCounter++;
        return "$t_" + this.tempoVariablesCounter;
    }

    public static BoolExpr translatePredicate(String formula, Context z3Context) {
        FormulaNode node = Parser.getFormulaAsSemanticAst(formula);
        if (node.getFormulaType() != FormulaType.PREDICATE_FORMULA) {
            throw new RuntimeException("Expected predicate.");
        }
        FormulaToZ3Translator formulaTranslator = new FormulaToZ3Translator(z3Context);
        Expr constraint = formulaTranslator.visitPredicateNode((PredicateNode) node.getFormula(), null);
        if (!(constraint instanceof BoolExpr)) {
            throw new RuntimeException("Invalid translation. Expected BoolExpr but found " + constraint.getClass());
        }

        BoolExpr boolExpr = (BoolExpr) constraint;
        // adding all additional constraints to result
        for (BoolExpr bExpr : formulaTranslator.constraintList) {
            boolExpr = z3Context.mkAnd(boolExpr, bExpr);
        }
        return boolExpr;
    }

    @Override
    public Expr visitIdentifierExprNode(IdentifierExprNode node, Void n) {
        Type type = node.getDeclarationNode().getType();
        return z3Context.mkConst(node.getName(), bTypeToZ3Sort(type));

    }

    @Override
    public Expr visitIdentifierPredicateNode(IdentifierPredicateNode node, Void n) {
        return z3Context.mkBoolConst(node.getName());
    }

    @Override
    public Expr visitPredicateOperatorWithExprArgs(PredicateOperatorWithExprArgsNode node, Void n) {
        final List<ExprNode> expressionNodes = node.getExpressionNodes();
        switch (node.getOperator()) {
        case EQUAL: {
            Expr left = visitExprNode(expressionNodes.get(0), null);
            Expr right = visitExprNode(expressionNodes.get(1), null);
            return z3Context.mkEq(left, right);
        }
        case NOT_EQUAL: {
            Expr left = visitExprNode(expressionNodes.get(0), null);
            Expr right = visitExprNode(expressionNodes.get(1), null);
            return z3Context.mkNot(z3Context.mkEq(left, right));
        }
        case ELEMENT_OF: {
            Expr left = visitExprNode(expressionNodes.get(0), null);
            ArrayExpr right = (ArrayExpr) visitExprNode(expressionNodes.get(1), null);
            return z3Context.mkSetMembership(left, right);
        }
        case LESS_EQUAL: {
            ArithExpr left = (ArithExpr) visitExprNode(expressionNodes.get(0), null);
            ArithExpr right = (ArithExpr) visitExprNode(expressionNodes.get(1), null);
            return z3Context.mkLe(left, right);
        }
        case LESS: {
            ArithExpr left = (ArithExpr) visitExprNode(expressionNodes.get(0), null);
            ArithExpr right = (ArithExpr) visitExprNode(expressionNodes.get(1), null);
            return z3Context.mkLt(left, right);
        }
        case GREATER_EQUAL:{
            ArithExpr left = (ArithExpr) visitExprNode(expressionNodes.get(0), null);
            ArithExpr right = (ArithExpr) visitExprNode(expressionNodes.get(1), null);
            return z3Context.mkGe(left, right);
        }
        case GREATER: {
            ArithExpr left = (ArithExpr) visitExprNode(expressionNodes.get(0), null);
            ArithExpr right = (ArithExpr) visitExprNode(expressionNodes.get(1), null);
            return z3Context.mkGt(left, right);
        }
        default:
            break;
        }
        // TODO
        throw new AssertionError("Not implemented: " + node.getOperator());
    }

    @Override
    public Expr visitExprOperatorNode(ExpressionOperatorNode node, Void n) {
        List<ExprNode> expressionNodes = node.getExpressionNodes();
        switch (node.getOperator()) {
        case PLUS: {
{'fraction_non_alphanumeric': 0.09365742499050513, 'fraction_numerical': 0.007823775161412838, 'mean_word_length': 3.4285233770602086, 'pattern_counts': {'":': 0, '<': 13, '<?xml version=': 0, '>': 13, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3629955', 'n_tokens_mistral': 3823, 'n_tokens_neox': 3717, 'n_words': 879}