<commit_before>/*
 * Author: <NAME> (<EMAIL>)
 */

package janala.solvers;

import janala.config.Config;
import janala.interpreters.Constraint;
import janala.interpreters.StringConstants;
import janala.interpreters.SymbolicInt;
import janala.interpreters.Value;
import janala.utils.MyLogger;

import java.io.*;
import java.util.ArrayList;
import java.util.TreeMap;
import java.util.logging.Level;
import java.util.logging.Logger;

/**
 * Author: <NAME> (<EMAIL>)
 * Date: 7/7/12
 * Time: 7:32 PM
 */
public class YicesSolver2 implements Solver {
    boolean first = true;
    ArrayList<Value> inputs;
    ArrayList<Constraint> constraints;
    private final static Logger logger = MyLogger.getLogger(YicesSolver.class.getName());
    private final static Logger tester = MyLogger.getTestLogger(Config.mainClass+"."+Config.iteration);

    public void setInputs(ArrayList<Value> inputs) {
        this.inputs = inputs;
        this.first = true;
    }

    private void initSolver(Constraint c) {
        if (first) {
            first = false;
            constraints = new ArrayList<Constraint>();
            c.not();
        }
    }

    public void visitSymbolicInt(SymbolicInt c) {
        initSolver(c);
        logger.log(Level.INFO,"{0}",c);
        constraints.add(c);
    }


    public boolean solve() {
        try {
            PrintStream out = new PrintStream(new BufferedOutputStream(new FileOutputStream(Config.formulaFile)));
            int nInputs = inputs.size();
            for (int i = 0; i < nInputs; i++) {
                out.print("(define x");
                out.print(i+1);
                out.println("::int)");
            }
            for (Constraint next : constraints) {
                out.print("(assert ");
                next.print(out);
                out.println(")");
            }
            out.println("(check)");
            out.println("(show-model)");
            out.close();


            ProcessBuilder builder = new ProcessBuilder(new String[]{Config.yicesCommand,Config.formulaFile});
            builder.redirectErrorStream(true);
            Process process = builder.start();

            (new StreamGobbler(process.getErrorStream(),"ERROR")).start();

            boolean result = true;
            InputStream is = process.getInputStream();
            InputStreamReader isr = new InputStreamReader(is);
            BufferedReader br = new BufferedReader(isr);
            String line = null;

            line = br.readLine();
            if (!line.startsWith("sat")) {
                if (!line.startsWith("unsat")) {
                    logger.log(Level.SEVERE, "Call to Yices failed (concolic.yices = "
                            + Config.yicesCommand + ")");
                    Runtime.getRuntime().halt(1);
                }
                tester.log(Level.INFO,"-- Infeasible");
                logger.log(Level.INFO,"-- Infeasible");
                result = false;
            } else {
                result = true;
                TreeMap<Integer,Long> soln = new TreeMap<Integer, Long>();
                while ((line = br.readLine()) != null) {
                    if (line.startsWith("(")) {
                        String[] tokens = line.split(" ");
                        int xi = Integer.parseInt(tokens[1].substring(1));
                        String tmp = tokens[2].trim();<commit_msg>fixed the hang problem on cygwin.<commit_after>/*
 * Author: <NAME> (<EMAIL>)
 */

package janala.solvers;

import janala.config.Config;
import janala.interpreters.Constraint;
import janala.interpreters.StringConstants;
import janala.interpreters.SymbolicInt;
import janala.interpreters.Value;
import janala.utils.MyLogger;

import java.io.*;
import java.util.ArrayList;
import java.util.TreeMap;
import java.util.logging.Level;
import java.util.logging.Logger;

/**
 * Author: <NAME> (<EMAIL>)
 * Date: 7/7/12
 * Time: 7:32 PM
 */
public class YicesSolver2 implements Solver {
    boolean first = true;
    ArrayList<Value> inputs;
    ArrayList<Constraint> constraints;
    private final static Logger logger = MyLogger.getLogger(YicesSolver.class.getName());
    private final static Logger tester = MyLogger.getTestLogger(Config.mainClass+"."+Config.iteration);

    public void setInputs(ArrayList<Value> inputs) {
        this.inputs = inputs;
        this.first = true;
    }

    private void initSolver(Constraint c) {
        if (first) {
            first = false;
            constraints = new ArrayList<Constraint>();
            c.not();
        }
    }

    public void visitSymbolicInt(SymbolicInt c) {
        initSolver(c);
        logger.log(Level.INFO,"{0}",c);
        constraints.add(c);
    }


    public boolean solve() {
        try {
            PrintStream out = new PrintStream(new BufferedOutputStream(new FileOutputStream(Config.formulaFile)));
            int nInputs = inputs.size();
            for (int i = 0; i < nInputs; i++) {
                out.print("(define x");
                out.print(i+1);
                out.println("::int)");
            }
            for (Constraint next : constraints) {
                out.print("(assert ");
                next.print(out);
                out.println(")");
            }
            out.println("(check)");
            out.println("(show-model)");
            out.close();


            ProcessBuilder builder = new ProcessBuilder(new String[]{Config.yicesCommand,Config.formulaFile});
            builder.redirectErrorStream(true);
            Process process = builder.start();

            (new StreamGobbler(process.getErrorStream(),"ERROR")).start();

            boolean result = true;
            InputStream is = process.getInputStream();
            InputStreamReader isr = new InputStreamReader(is);
            BufferedReader br = new BufferedReader(isr);
            String line = null;

            line = br.readLine();
            if (!line.startsWith("sat")) {
                if (!line.startsWith("unsat")) {
                    logger.log(Level.SEVERE, "Call to Yices failed (concolic.yices = "
                            + Config.yicesCommand + ")");
                    Runtime.getRuntime().halt(1);
                }
                tester.log(Level.INFO,"-- Infeasible");
                logger.log(Level.INFO,"-- Infeasible");
                result = false;
                while ((line = br.readLine()) != null) { }
                br.close();
            } else {
                result = true;
                TreeMap<Integer,Long> soln = new TreeMap<Integer, Long>();
                while ((line = br.readLine()) != null) {
                    if (line.startsWith("(")) {
                        String[] tokens = line.split(" ");
                        int xi = Integer.parseInt(tokens[1].substring(1));
                        String tmp = tokens[2].trim();
{'fraction_non_alphanumeric': 0.12830243760035032, 'fraction_numerical': 0.0043789227849948915, 'mean_word_length': 1.9282051282051282, 'pattern_counts': {'":': 2, '<': 25, '<?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': '6422048', 'n_tokens_mistral': 1888, 'n_tokens_neox': 1831, 'n_words': 393}