#include <cstdio>
#include <cstdlib>
#include <assert.h>

#include "circuit.h"
#include "clause.h"
#include "CCAnr/ccanr.h"

int main(int args, char* argv[]) {

    if(args != 2) {
        printf("usage: ./atpg <XXX.bench>\n");
        exit(1);
    }

    srand(19260817);

    Circuit* circuit = new Circuit();

    printf("parsing file %s ...", argv[1]);
    circuit->parse_from_file(argv[1]);
    circuit->init_topo_index();
    printf(" Done.\n");

    printf("====== Circuit Statistics ====== \n");
    printf("PI:\t%ld\n", circuit->PIs.size());
    printf("PO:\t%ld\n", circuit->POs.size());
    printf("Gate:\t%ld\n", circuit->name2gate.size());
    printf("Stem:\t%ld\n", circuit->stems.size());
    printf("================================ \n");

    circuit->global_fault_undetected_count = circuit->gates.size() * 2;

    CCAnr::module_init();

    // init clause local search
    ClauseLS::init_data_structs(circuit);

    while(true) {
        bool ls = circuit->local_search();
        bool is_valid = circuit->is_valid_circuit();
        printf("checking valid circuit ...");
        printf(" result: %d.\n", is_valid);
        if(!ls) break;
        if(!is_valid) break; 
        if(circuit->global_fault_undetected_count == 0) break;
    }

    return 0;
}