use std::env;
use std::process;
use std::fs::File;
use std::io::prelude::*;
use inline_python::*;

fn main() -> std::io::Result<()> {
    let args: Vec<_> = env::args().collect();
    if args.len() < 4 { println!("Need clique size, complete graph order, and output filename."); process::exit(1); }
    let sclique: usize = args[1].clone().to_string().parse::<usize>().unwrap();
    let order: usize = args[2].clone().to_string().parse::<usize>().unwrap();
    let output_name: &String = &args[3];
    println!("{} {} {}", sclique, order, output_name);

    let mut buffer = File::create(output_name)?;
    let mut buffer2 = File::create(".a")?;

    let mut edges: Vec<[u32; 2]> = Vec::new(); 
    let c = Context::new();

    c.run(python! {
        import networkx as nx;
        import itertools as it
        G = nx.complete_graph('order);
        def issize(val):
            return len(val)<='sclique
        B = [c for c in list(it.takewhile(issize, nx.enumerate_all_cliques(G))) if len(c)=='sclique];
    });

    let cliques = c.get::<Vec<Vec<u32>>>("B");
    write!(buffer, "p cnf {} {}\n", ((order * (order - 1)) / 2), 2*cliques.len())?;
    for clique in cliques {
        /*let fedge: [u32; 2] = [clique[0], clique[1]];
        let fresult = edges.iter().position(|&val| val==fedge);
        let feindex = match fresult {
            Some(val) => val+1,
            None => {
                edges.push(fedge);
                println!("{} = {:?}", edges.len(), fedge);
                edges.len()
            }
        };*/
        //write!(buffer, "x")?;

        for a in 0..sclique {
            for b in a+1..sclique {
                //i += 1;
                let edge: [u32; 2] = [clique[a], clique[b]];
                let result = edges.iter().position(|&val| val==edge);
                let eindex = match result {
                    Some(val) => val+1,
                    None => {
                        edges.push(edge);
                        println!("{} = {:?}", edges.len(), edge);
                        edges.len()
                    }
                };
                write!(buffer, "{} ", eindex)?;
                write!(buffer2, "-{} ", eindex)?;
            }
        }
        write!(buffer, "0\n")?;
        write!(buffer2, "0\n")?;
    }
    Ok(())
}

//fn search_space() {
    // I just have to find a single counterexample.  A single example of it being possible to color
    // the graph such that none of the cliques have all edges colored the same color.
    // Finding an example of it being possible to color the graph such that a clique has all edges
    // colored the same tells me nothing.
    //
    // //identify lines that are the most idependent of each other?
    // take the first line
    // assume 9 of the edges are colored.
    // assume the same for the next line
    // continue until you've selected a coloring for every edge
    // test the coloring
    // do the same with different edges (there are 10 choose 1 = 10 ways to do this per line, but
    // the lines are obviously not independent)
    // test the colorings
    // now assume 8 of the edges are colored on the first line (there are 10 choose 2 = 45 ways to
    // do this per line)
    // count down in reverse order in octary in terms of how many edges are colored per line
    // don't bother checking whenever a line is forced to have 0 or 10 edges colored.
    // if the fpga ever returns a 1, I have found a counterexample.
    // The first lines should be edited first because they have the most control over the next
    // lines.
    // 
    // Work in reverse?
    // Find what other colorings all the edges of a specific clique being colored the same forces,
    // and try to 
//}