use dpll on the dimac formula that was parsed from stdin

rust/solve/src/dpll.rs

use std::collections::BTreeSet;
type Var = i32;
type BoundVars = BTreeSet<Var>;
type Clause = Vec<Var>;
pub type Var = i32;
pub type BoundVars = BTreeSet<Var>;
pub type Clause = Vec<Var>;
fn empty_vars() -> BoundVars {
    BTreeSet::new()
    assert!(!is_clause_unit(vars, vec!(1, 2)));
}
fn dpll(clauses: Vec<Clause>) -> Option<BoundVars> {
pub fn dpll(clauses: Vec<Clause>) -> Option<BoundVars> {
    fn dpll_inner(stack: &mut Vec<(Var, BoundVars)>, vars: &mut BoundVars, clauses: Vec<Clause>) -> Option<BoundVars> {
        if clauses.iter().all(|c| is_clause_satisfied(&vars, c.clone())) { // all clauses satisfied, success
            Some(vars.clone())

rust/solve/src/main.rs

use std::io::Read;
use solve::cnf;
use solve::dpll;
fn main() {
    let input: &mut String = &mut String::new();
	Ok(_) => match cnf::parse_dimac(input) {
	    Ok(cnf) => {
		println!("cnf has {} variables and {} clauses", cnf.num_vars, cnf.num_clauses);
		for clause in cnf.clauses {
		for clause in cnf.clauses.clone() {
		    println!("{:?}", clause);
		}
                match dpll::dpll(cnf.clauses) {
                    Some(bindings) => println!("satisfiable: {:?}", bindings),
                    None => println!("not satisfiable")
                }
	    }
	    Err(e) => { println!("Error: {}", e) }
	},