|
|
@ -12,7 +12,6 @@ extern crate solve;
|
|
12
|
12
|
|
|
13
|
13
|
use std::io;
|
|
14
|
14
|
use std::io::Read;
|
|
15
|
|
use std::thread;
|
|
16
|
15
|
|
|
17
|
16
|
use solve::cnf;
|
|
18
|
17
|
use solve::dpll;
|
|
|
@ -27,12 +26,10 @@ fn main() {
|
|
27
|
26
|
println!("{:?}", clause);
|
|
28
|
27
|
}
|
|
29
|
28
|
|
|
30
|
|
thread::Builder::new().name("solver".to_string()).stack_size(100 * 1024 * 1024).spawn(move || {
|
|
31
|
|
match dpll::dpll(cnf.clauses) {
|
|
32
|
|
Some(bindings) => println!("satisfiable: {:?}", bindings),
|
|
33
|
|
None => println!("not satisfiable")
|
|
34
|
|
}
|
|
35
|
|
}).unwrap().join();
|
|
|
29
|
match dpll::dpll(cnf.clauses) {
|
|
|
30
|
Some(bindings) => println!("satisfiable: {:?}", bindings),
|
|
|
31
|
None => println!("not satisfiable")
|
|
|
32
|
}
|
|
36
|
33
|
}
|
|
37
|
34
|
Err(e) => { println!("Error: {}", e) }
|
|
38
|
35
|
},
|