<commit_before>package de.bmoth.util;

import com.microsoft.z3.BoolExpr;
import com.microsoft.z3.Context;
import com.microsoft.z3.Solver;
import com.microsoft.z3.Status;
import de.bmoth.backend.FormulaToZ3Translator;
import org.junit.Test;

import java.util.*;

import static org.junit.Assert.assertEquals;

public class UtilMethodsTest {

    @Test
    public void testSort() throws Exception {
        Map<String, Set<String>> dependencies = new HashMap<>();
        dependencies.put("a", new HashSet<>());
        dependencies.put("b", new HashSet<>(Arrays.asList("a")));
        dependencies.put("c", new HashSet<>(Arrays.asList("a", "d")));
        dependencies.put("d", new HashSet<>(Arrays.asList("b")));
        List<String> sorted = Utils.sortByTopologicalOrder(dependencies);
        assertEquals(Arrays.asList("a", "b", "d", "c"), sorted);
    }

    public static void check(Status satisfiable, String formula, Context ctx, Solver s) {
        BoolExpr constraint = FormulaToZ3Translator.translatePredicate(formula, ctx);
        // create scope just for current constraint
        s.push();
        s.add(constraint);
        Status check = s.check();
        // clean solver stack
        s.pop();
        assertEquals(satisfiable, check);
    }

    public static void checkLaw(String law, Context ctx, Solver s) {
        BoolExpr constraint = FormulaToZ3Translator.translatePredicate(law, ctx);
        s.add(ctx.mkNot(constraint));
        Status check = s.check();
        assertEquals(Status.UNSATISFIABLE, check);
    }

    public static void checkTruthTable(Map<String, Status> map, Context ctx, Solver s) {
        for (Map.Entry<String, Status> entry : map.entrySet()) {
            check(entry.getValue(), entry.getKey(), ctx, s);
            s.reset();
        }
    }

}<commit_msg>cleanup solver<commit_after>package de.bmoth.util;

import com.microsoft.z3.BoolExpr;
import com.microsoft.z3.Context;
import com.microsoft.z3.Solver;
import com.microsoft.z3.Status;
import de.bmoth.backend.FormulaToZ3Translator;
import org.junit.Test;

import java.util.*;

import static org.junit.Assert.assertEquals;

public class UtilMethodsTest {

    @Test
    public void testSort() throws Exception {
        Map<String, Set<String>> dependencies = new HashMap<>();
        dependencies.put("a", new HashSet<>());
        dependencies.put("b", new HashSet<>(Arrays.asList("a")));
        dependencies.put("c", new HashSet<>(Arrays.asList("a", "d")));
        dependencies.put("d", new HashSet<>(Arrays.asList("b")));
        List<String> sorted = Utils.sortByTopologicalOrder(dependencies);
        assertEquals(Arrays.asList("a", "b", "d", "c"), sorted);
    }

    public static void check(Status satisfiable, String formula, Context ctx, Solver s) {
        BoolExpr constraint = FormulaToZ3Translator.translatePredicate(formula, ctx);
        // create scope just for current constraint
        s.push();
        s.add(constraint);
        Status check = s.check();
        // clean solver stack
        s.pop();
        assertEquals(satisfiable, check);
    }

    public static void checkLaw(String law, Context ctx, Solver s) {
        BoolExpr constraint = FormulaToZ3Translator.translatePredicate(law, ctx);
        s.push();
        s.add(ctx.mkNot(constraint));
        Status check = s.check();
        s.pop();
        assertEquals(Status.UNSATISFIABLE, check);
    }

    public static void checkTruthTable(Map<String, Status> map, Context ctx, Solver s) {
        for (Map.Entry<String, Status> entry : map.entrySet()) {
            check(entry.getValue(), entry.getKey(), ctx, s);
            s.reset();
        }
    }

}
{'fraction_non_alphanumeric': 0.13676148796498905, 'fraction_numerical': 0.0038293216630196935, 'mean_word_length': 3.108988764044944, 'pattern_counts': {'":': 0, '<': 23, '<?xml version=': 0, '>': 23, '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': '408055', 'n_tokens_mistral': 1085, 'n_tokens_neox': 1076, 'n_words': 253}