var fileName = "";

const fs = require('fs');

function readFormula(fileName) {

    let text = fs.readFileSync(fileName, 'utf8').split("\n")//  an array containing lines of text extracted from the file.

    let qtVariables = 0;
    let qtClauses = 0;
    let lineOfClauses = "";

    for (let i = 0; i < text.length; i++) {

        let firstChar = text[i].charAt(0);

        if (firstChar == "c"){
            //does NOTHING
        } else if(firstChar == "p") {
            //  coloca cada elemento da linha em pos.
            let pos = text[i].split(" ");

            // determina como inteiro a quantidade de variaveis e clausulas.

            qtVariables = parseInt(pos[2]);
            qtClauses = parseInt(pos[3]);

        } else {
            lineOfClauses = lineOfClauses.concat(" ", text[i]);
        };

        let clauseLine = lineOfClauses.split("0");
    };



    let clauses = readClauses(clauseLine)
    let variables = readVariables(clauses)

    // In the following line, text is passed as an argument so that the function
    // is able to extract the problem specification.

    let specOk = checkProblemSpecification(lineOfClauses, qtClauses, qtVariables)

    let result = { 'clauses': [], 'variables': [] }
    if (specOk) {
        result.clauses = clauses
        result.variables = variables
    }
    return result
}

function readClauses (clauseLine){

    let clauses = [];

    for (let i = 0; i < clauseLine.length; i++) {


        let eachVariable = clauseLine[i].split(" ");


        for (let j = 0; j < eachVariable.length; j++){

            if (eachVariable[j] != ""){
                eachVariable.push(parseInt(eachVariable[j], 10));
            };

        };

        clauses.push(eachVariable);
    };

    return clauses;

}

function readVariables(qntVariables){

    let allZeros = [];

    for (let i = 0; i < qntVariables; i++){

        allZeros.push("0");

    };

    return allZeros;

}

function checkProblemSpecification(lineOfClauses, qtClauses, qtVariables) {

    lineOfClauses = lineOfClauses.replace(/-/g, "");

    let highest = highestValue(lineOfClauses);

    let splitClauses = lineOfClauses.split(" 0");

    splitClauses.pop();

    let specOk = false;

    if (qtClauses == splitClauses.length){

        if (qtVariables == highest){

            specOk = true;

        } else {
            specOk = false;
        };
    } else {

            specOk = false;
    };

    return specOk;

}

function highestValue(lineOfClauses) {

    var arr = lineOfClauses.split(" ").map(Number);

    var largest = arr[0];

    for (var i = 1; i < arr.length; i++) {
        if (arr[i] > largest) {
            largest = arr[i];
        };
    } ;

    return largest;
}

function nextAssignment(variables) {

    let newVector = variables;

    if(newVector[newVector.length-1] == 0){

        newVector[newVector.length-1] = 1;


    } else {

        let checar;
        let contador = 1;
        let tempArray[];

        tempArray = newVector;

        tempArray.pop();

        while (checar = false) {

            if (tempArray[tempArray.length - 1] = 1) {

                tempArray.pop();
                contador++;
            } else {
                checar = true;
            }

        }

        newVector = tempArray;
        newVector[newVector.length - 1] = 1;

        while (contador > 0) {
            newVector.push("0");
            contador--;
        };

    }