Selaa lähdekoodia

fix indentation

i think this is emacs vs vim, but not quite sure.
Lucas Stadler 10 vuotta sitten
vanhempi
commit
e1df0ff76c
2 muutettua tiedostoa jossa 76 lisäystä ja 76 poistoa
  1. 63 63
      rust/dpll/src/cnf.rs
  2. 13 13
      rust/dpll/src/main.rs

+ 63 - 63
rust/dpll/src/cnf.rs

@ -3,71 +3,71 @@
3 3
//! `CNF` stands for conjunctive normal form, i.e. a logic formula that
4 4
//! consists of a conjunction of disjunctions.
5 5
6
 pub struct CNF {
7
	  pub num_vars: u32,
8
	  pub num_clauses: u32,
9
	  pub clauses: Vec<Vec<i32>>
10
 }
6
pub struct CNF {
7
	pub num_vars: u32,
8
		 pub num_clauses: u32,
9
		 pub clauses: Vec<Vec<i32>>
10
}
11 11
12
 /// Parses a CNF formula in DIMAC format.
13
 ///
14
 /// # Examples
15
 ///
16
 /// A simple example for a formula in DIMAC format is below:
17
 ///
18
 /// ```text
19
 /// p cnf 5 3
20
 /// 1 2 3 0
21
 /// -2 3 4 0
22
 /// 4 5 0
23
 /// ```
24
 ///
25
 /// The above represents a formula with 5 variables and 3 clauses.  The first
26
 /// line specifies this.  Each following line represents a clause with possibly
27
 /// negated literals, terminated by 0 and a newline.
28
 pub fn parse_dimac(dimac: &str) -> Result<CNF, String> {
29
	  let mut lines = dimac.lines();
30
	  let mut num_vars;
31
	  let mut num_clauses;
32
	  
33
	  match lines.next() {
34
			None => { return Err("expected cnf description".to_string()) }
35
			Some(line) => {
36
				 let desc: Vec<&str> = line.split(" ").collect();
37
				 if desc.len() != 4 || desc[0] != "p" || desc[1] != "cnf" {
38
					  return Err("cnf description must be of the form 'p cnf <num vars> <num clauses>'".to_string())
39
				 }
40
				 match desc[2].parse::<u32>() {
41
					  Ok(n) => { num_vars = n }
42
					  Err(e) => { return Err(format!("<num vars> must be a positive integer: {}", e)) }
43
				 }
44
				 
45
				 match desc[3].parse::<u32>() {
46
					  Ok(n) => { num_clauses = n }
47
					  Err(e) => { return Err(format!("<num clauses> must be a positive integer: {}", e)) }
48
				 }
49
			}
50
	  }
51
52
	  let clause_lines: Vec<&str> = lines.collect();
53
	  if clause_lines.len() as u32 != num_clauses {
54
			return Err(format!("Wrong number of clauses: Expected {}, but got {}", num_clauses, clause_lines.len()))
55
	  }
12
/// Parses a CNF formula in DIMAC format.
13
///
14
/// # Examples
15
///
16
/// A simple example for a formula in DIMAC format is below:
17
///
18
/// ```text
19
/// p cnf 5 3
20
/// 1 2 3 0
21
/// -2 3 4 0
22
/// 4 5 0
23
/// ```
24
///
25
/// The above represents a formula with 5 variables and 3 clauses.  The first
26
/// line specifies this.  Each following line represents a clause with possibly
27
/// negated literals, terminated by 0 and a newline.
28
pub fn parse_dimac(dimac: &str) -> Result<CNF, String> {
29
	let mut lines = dimac.lines();
30
	let mut num_vars;
31
	let mut num_clauses;
56 32
57
	  let mut clauses: Vec<Vec<i32>> = Vec::with_capacity(num_clauses as usize);
58
	  for clause_line in clause_lines {
59
			let mut vars: Vec<i32> = clause_line.split(" ").map(|x| x.parse::<i32>().unwrap()).collect();
60
			if vars.is_empty() {
61
				 return Err("empty clause".to_string())
33
	match lines.next() {
34
		None => { return Err("expected cnf description".to_string()) }
35
		Some(line) => {
36
			let desc: Vec<&str> = line.split(" ").collect();
37
			if desc.len() != 4 || desc[0] != "p" || desc[1] != "cnf" {
38
				return Err("cnf description must be of the form 'p cnf <num vars> <num clauses>'".to_string())
39
			}
40
			match desc[2].parse::<u32>() {
41
				Ok(n) => { num_vars = n }
42
				Err(e) => { return Err(format!("<num vars> must be a positive integer: {}", e)) }
62 43
			}
63
			if vars[vars.len()-1] != 0 {
64
				 return Err("clause must be terminated with 0".to_string())
44
45
			match desc[3].parse::<u32>() {
46
				Ok(n) => { num_clauses = n }
47
				Err(e) => { return Err(format!("<num clauses> must be a positive integer: {}", e)) }
65 48
			}
66
			let l = vars.len();
67
			vars.truncate(l - 1);
68
			clauses.push(vars)
69
	  }
49
		}
50
	}
51
52
	let clause_lines: Vec<&str> = lines.collect();
53
	if clause_lines.len() as u32 != num_clauses {
54
		return Err(format!("Wrong number of clauses: Expected {}, but got {}", num_clauses, clause_lines.len()))
55
	}
56
57
	let mut clauses: Vec<Vec<i32>> = Vec::with_capacity(num_clauses as usize);
58
	for clause_line in clause_lines {
59
		let mut vars: Vec<i32> = clause_line.split(" ").map(|x| x.parse::<i32>().unwrap()).collect();
60
		if vars.is_empty() {
61
			return Err("empty clause".to_string())
62
		}
63
		if vars[vars.len()-1] != 0 {
64
			return Err("clause must be terminated with 0".to_string())
65
		}
66
		let l = vars.len();
67
		vars.truncate(l - 1);
68
		clauses.push(vars)
69
	}
70 70
71
	  let cnf = CNF { num_vars: num_vars, num_clauses: num_clauses, clauses: clauses };
72
	  return Ok(cnf)
73
 }
71
	let cnf = CNF { num_vars: num_vars, num_clauses: num_clauses, clauses: clauses };
72
	return Ok(cnf)
73
}

+ 13 - 13
rust/dpll/src/main.rs

@ -16,17 +16,17 @@ use std::io::Read;
16 16
use solve::cnf;
17 17
18 18
fn main() {
19
    let input: &mut String = &mut String::new();
20
    match io::stdin().read_to_string(input) {
21
        Ok(_) => match cnf::parse_dimac(input) {
22
            Ok(cnf) => {
23
                println!("cnf has {} variables and {} clauses", cnf.num_vars, cnf.num_clauses);
24
                for clause in cnf.clauses {
25
                    println!("{:?}", clause);
26
                }
27
            }
28
            Err(e) => { println!("Error: {}", e) }
29
        },
30
        Err(e) => { println!("Error: {}", e) }
31
    }
19
	let input: &mut String = &mut String::new();
20
	match io::stdin().read_to_string(input) {
21
		Ok(_) => match cnf::parse_dimac(input) {
22
			Ok(cnf) => {
23
				println!("cnf has {} variables and {} clauses", cnf.num_vars, cnf.num_clauses);
24
				for clause in cnf.clauses {
25
					println!("{:?}", clause);
26
				}
27
			}
28
			Err(e) => { println!("Error: {}", e) }
29
		},
30
			Err(e) => { println!("Error: {}", e) }
31
	}
32 32
}