package asp;

import de.dhbwstuttgart.parser.NullToken;
import de.dhbwstuttgart.sat.asp.writer.ASPGenerator;
import de.dhbwstuttgart.sat.asp.Clingo;
import de.dhbwstuttgart.syntaxtree.ClassOrInterface;
import de.dhbwstuttgart.syntaxtree.factory.ASTFactory;
import de.dhbwstuttgart.syntaxtree.type.TypePlaceholder;
import de.dhbwstuttgart.typeinference.constraints.ConstraintSet;
import de.dhbwstuttgart.typeinference.constraints.Pair;
import de.dhbwstuttgart.typeinference.unify.model.PairOperator;
import org.junit.Test;

import java.io.*;
import java.util.*;

public class ClingoTest {
    public static final String rootDirectory = "~/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/unifyWithoutWildcards";
    public static final String tempDirectory = "/tmp/";

    @Test
    public void test() throws IOException, InterruptedException, ClassNotFoundException {
        String content = "";
        content = new ASPGenerator(this.getPairs(), this.getFC()).getASP();
        
        PrintWriter writer = new PrintWriter(tempDirectory + "test.lp", "UTF-8");
        writer.println(content);
        writer.close();

        Clingo clingo = new Clingo(Arrays.asList(new File(tempDirectory + "test.lp")));
        System.out.println(clingo.runClingo());
    }

    public Collection<ClassOrInterface> getFC() {
        Set<ClassOrInterface> ret = new HashSet<>();
        ret.add(ASTFactory.createObjectClass());
        ret.add(ASTFactory.createClass(java.util.List.class));
        return ret;
    }

    public ConstraintSet<Pair> getPairs() {
        ConstraintSet<Pair> ret = new ConstraintSet<>();
        ret.addUndConstraint(new Pair(TypePlaceholder.fresh(new NullToken()), ASTFactory.createObjectType(), PairOperator.SMALLERDOT));
        return ret;
    }
}