<commit_before>#include <iostream>
#include <map>
#include <vector>
#include <fstream>
#include <sstream>
#include <string>
#include <cstdlib>
#include <cstdio>
#include <unistd.h>
#include <ext/stdio_filebuf.h>
#include <cstring>
#include <signal.h>

using namespace std;

int iabs(int a) { return a < 0 ? -a : a; }

void exit_verifier(int result_code, int exit_code) {
    cout << endl << result_code;
    exit(exit_code);
}

int main(int argc, char* argv[]) {
    ifstream instance(argv[1]);
    ifstream solver_output(argv[2]);
    string line;

    map<int, int> variables;
    bool SAT_answer = false;
    bool UNSAT_answer = false;
    while (getline(solver_output, line)) {
        istringstream lss(line);
        string prefix;
        lss >> prefix;
        if (prefix == "s") {
            string answer;
            lss >> answer;
            if (answer == "UNKNOWN") {
                cout << "Solver reported unknown." << endl;
                exit_verifier(0, 0);
            }
            else if (answer == "SATISFIABLE") {
                cout << "Solver reported satisfiable. Checking." << endl;
                SAT_answer = true;
            }
            else if (answer == "UNSATISFIABLE") {
                cout << "Solver reported unsatisfiable. Checking." << endl;
                UNSAT_answer = true;
                break; // Proof should follow.
            }
        }
        else if (prefix == "v") {
            // read solution
            int v;
            while (lss >> v && v != 0) {
                variables[iabs(v)] = v;
            }
        }
    }
    if (SAT_answer) {
        while (getline(instance, line)) {
            if (line.substr(0, 1) == "c" || line.substr(0, 1) == "p") continue;
            istringstream lss(line);
            int v;
            bool sat_clause = false;
            int num_vars = 0;
            while (lss >> v && v != 0) {
                num_vars++;
                if (variables[iabs(v)] == v) {
                    sat_clause = true;
                    break;
                }
            }
            if (!sat_clause && num_vars > 0) {
                cout << "Clause " << line << " not satisfied" << endl;
                cout << "Wrong solution." << endl;
                exit_verifier(-1, 0);
            }
        }
        cout << "Solution verified." << endl;
        exit_verifier(11, 0);
    } else if (UNSAT_answer) {
        // Verify the solution that should be given in DRUP or TRACECHECK format following the solution line.
        
        // First line is used to detect the proof format
        string first_line;
        getline(solver_output, first_line);
        //first_line = first_line.substr(first_line.find('\t')); // skip timestamp
        istringstream lss(first_line);
        string format = "";
        /*bool trace = false;
        if (first_line.find(" 0 0") != string::npos) { // "0 0" means TRACE proof format
            trace = true;
            cout << "Detected TRACE proof format." << endl;
        } else { // DRUP format
            cout << "Detected RUP proof format." << endl;
            trace = false;
        }*/
        if (first_line.find("p proof BRUP") != string::npos) {
            format = "brup";
        } else if (first_line.find("p proof DRUP") != string::npos) {
            format = "drup";
        } else if (first_line.find("p proof TC") != string::npos) {
            format = "tc";
        } else {
            cout << "Could not find 'p proof' line with proof format identifier." << endl;
            exit_verifier(0, 0);
        }
        
        // Prepare communication pipes with checker programs
        int outfd[2];
        int infd[2];
        pipe(outfd);
        pipe(infd);

        char* checker_cmd = new char[4096];
        if (format == "brup") {
            strcpy(checker_cmd, "./brup.py");
        } else if (format == "drup") {
            strcpy(checker_cmd, "./drup-check");
        } else if (format == "tc") {
            strcpy(checker_cmd, "./stc");
        }
        
        cout << "Calling " << checker_cmd << " " << argv[1] << endl;<commit_msg>change o line<commit_after>#include <iostream>
#include <map>
#include <vector>
#include <fstream>
#include <sstream>
#include <string>
#include <cstdlib>
#include <cstdio>
#include <unistd.h>
#include <ext/stdio_filebuf.h>
#include <cstring>
#include <signal.h>

using namespace std;

int iabs(int a) { return a < 0 ? -a : a; }

void exit_verifier(int result_code, int exit_code) {
    cout << endl << result_code;
    exit(exit_code);
}

int main(int argc, char* argv[]) {
    ifstream instance(argv[1]);
    ifstream solver_output(argv[2]);
    string line;

    map<int, int> variables;
    bool SAT_answer = false;
    bool UNSAT_answer = false;
    while (getline(solver_output, line)) {
        istringstream lss(line);
        string prefix;
        lss >> prefix;
        if (prefix == "s") {
            string answer;
            lss >> answer;
            if (answer == "UNKNOWN") {
                cout << "Solver reported unknown." << endl;
                exit_verifier(0, 0);
            }
            else if (answer == "SATISFIABLE") {
                cout << "Solver reported satisfiable. Checking." << endl;
                SAT_answer = true;
            }
            else if (answer == "UNSATISFIABLE") {
                cout << "Solver reported unsatisfiable. Checking." << endl;
                UNSAT_answer = true;
                break; // Proof should follow.
            }
        }
        else if (prefix == "v") {
            // read solution
            int v;
            while (lss >> v && v != 0) {
                variables[iabs(v)] = v;
            }
        }
    }
    if (SAT_answer) {
        while (getline(instance, line)) {
            if (line.substr(0, 1) == "c" || line.substr(0, 1) == "p") continue;
            istringstream lss(line);
            int v;
            bool sat_clause = false;
            int num_vars = 0;
            while (lss >> v && v != 0) {
                num_vars++;
                if (variables[iabs(v)] == v) {
                    sat_clause = true;
                    break;
                }
            }
            if (!sat_clause && num_vars > 0) {
                cout << "Clause " << line << " not satisfied" << endl;
                cout << "Wrong solution." << endl;
                exit_verifier(-1, 0);
            }
        }
        cout << "Solution verified." << endl;
        exit_verifier(11, 0);
    } else if (UNSAT_answer) {
        // Verify the solution that should be given in DRUP or TRACECHECK format following the solution line.
        
        // First line is used to detect the proof format
        string first_line;
        getline(solver_output, first_line);
        //first_line = first_line.substr(first_line.find('\t')); // skip timestamp
        istringstream lss(first_line);
        string format = "";
        /*bool trace = false;
        if (first_line.find(" 0 0") != string::npos) { // "0 0" means TRACE proof format
            trace = true;
            cout << "Detected TRACE proof format." << endl;
        } else { // DRUP format
            cout << "Detected RUP proof format." << endl;
            trace = false;
        }*/
        if (first_line.find("o proof BDRUP") != string::npos) {
            format = "brup";
        } else if (first_line.find("o proof DRUP") != string::npos) {
            format = "drup";
        } else if (first_line.find("o proof TC") != string::npos) {
            format = "tc";
        } else {
            cout << "Could not find 'p proof' line with proof format identifier." << endl;
            exit_verifier(0, 0);
        }
        
        // Prepare communication pipes with checker programs
        int outfd[2];
        int infd[2];
        pipe(outfd);
        pipe(infd);

        char* checker_cmd = new char[4096];
        if (format == "brup") {
            strcpy(checker_cmd, "./brup.py");
        } else if (format == "drup") {
            strcpy(checker_cmd, "./drup-check");
        } else if (format == "tc") {
            strcpy(checker_cmd, "./stc");
        }
        
        cout << "Calling " << checker_cmd << " " << argv[1] << endl;
{'fraction_non_alphanumeric': 0.1343844754396604, 'fraction_numerical': 0.007519708914493633, 'mean_word_length': 1.6186090822483328, 'pattern_counts': {'":': 0, '<': 139, '<?xml version=': 0, '>': 47, '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': '116312', 'n_tokens_mistral': 2538, 'n_tokens_neox': 2452, 'n_words': 679}