Var methods and ExtendFormula to make it easier to construct formulas

manual/src/lib/basic.md

@@ -11,29 +11,30 @@ let mut solver = Solver::new();
 
 ## Loading a Formula
 
-We can load a formula by adding individual clauses:
+The solver also implements the `ExtendFormula` trait, so we already know how to
+add clauses from the previous chapter.
 
 ```rust
 # extern crate varisat;
 # use varisat::Solver;
 # let mut solver = Solver::new();
-use varisat::Lit;
+use varisat::ExtendFormula;
 
-let (x, y, z) = (Lit::from_dimacs(1), Lit::from_dimacs(2), Lit::from_dimacs(3));
+let (x, y, z) = solver.new_lits();
 
 solver.add_clause(&[x, y, z]);
 solver.add_clause(&[!x, !y]);
 solver.add_clause(&[!y, !z]);
 ```
 
-By adding a formula:
+We can also load a `CnfFormula` with a single call of the `add_formula` method.
 
 ```rust
 # extern crate varisat;
-# use varisat::{Lit, Solver};
+# use varisat::Solver;
 # let mut solver = Solver::new();
-# let (x, y, z) = (Lit::from_dimacs(1), Lit::from_dimacs(2), Lit::from_dimacs(3));
-use varisat::CnfFormula;
+# let (x, y, z) = solver.new_lits();
+use varisat::{CnfFormula, ExtendFormula};
 let mut formula = CnfFormula::new();
 formula.add_clause(&[x, y, z]);
 formula.add_clause(&[!x, !y]);
@@ -42,9 +43,10 @@ formula.add_clause(&[!y, !z]);
 solver.add_formula(&formula);
 ```
 
-Or by directly loading a [DIMACS CNF][dimacs] from anything that implements
-`std::io::Read`. This uses incremental parsing, making it more efficient than
-reading the whole formula into a `CnfFormula`.
+If our formula is stored as [DIMACS CNF][dimacs] in a file, or in another way
+that supports `std::io::Read`, we can load it into the solver with
+`add_dimacs_cnf`. This uses incremental parsing, making it more efficient than
+reading the whole formula into a `CnfFormula` first.
 
 ```rust
 # extern crate varisat;
@@ -79,10 +81,9 @@ query the solver for a set of assignments that make all clauses true.
 
 ```rust
 # extern crate varisat;
-# use varisat::Solver;
-# use varisat::Lit;
+# use varisat::{Solver, ExtendFormula};
 # let mut solver = Solver::new();
-# let (x, y, z) = (Lit::from_dimacs(1), Lit::from_dimacs(2), Lit::from_dimacs(3));
+# let (x, y, z) = solver.new_lits();
 # let dimacs_cnf = b"1 2 3 0\n-1 -2 0\n-2 -3 0\n";
 # solver.add_dimacs_cnf(&dimacs_cnf[..]).expect("parse error");
 # let solution = solver.solve().unwrap();

manual/src/lib/formulas.md

@@ -41,10 +41,13 @@ assert_eq!(x.to_dimacs(), 1);
 assert!(Lit::from_dimacs(2).is_positive());
 assert!(Lit::from_dimacs(-3).is_negative());
 
-assert_eq!(Lit::positive(x), Lit::from_var(x, true));
-assert_eq!(Lit::negative(x), Lit::from_var(x, false));
+assert_eq!(Lit::positive(x), x.lit(true));
+assert_eq!(Lit::negative(x), x.lit(false));
 
-assert_eq!(Lit::negative(x), !Lit::positive(x));
+assert_eq!(x.positive(), Lit::from_var(x, true));
+assert_eq!(x.negative(), Lit::from_var(x, false));
+
+assert_eq!(x.positive(), !x.negative());
 
 assert_eq!(Lit::from_index(6, true).code(), 12);
 assert_eq!(Lit::from_index(6, false).code(), 13);
@@ -81,10 +84,13 @@ Instead Varisat provides the `CnfFormula` type, which stores all literals in a
 single `Vec`. When iterating over a `CnfFormula` the clauses can be accessed as
 slices.
 
+The `add_clause` method of the `ExtendFormula` trait allows adding new clauses
+to a `CnfFormula`.
+
 ```rust
 # extern crate varisat;
 # use varisat::{Var, Lit};
-use varisat::CnfFormula;
+use varisat::{CnfFormula, ExtendFormula};
 
 let mut formula = CnfFormula::new();
 
@@ -98,6 +104,29 @@ formula.add_clause(&[!a, !c]);
 assert_eq!(formula.iter().last().unwrap(), &[!a, !c]);
 ```
 
+## New Variables and Literals
+
+Often we don't care about the specific indices of variables. In that case,
+instead of manually computing indices, we can dynamically ask for new unused
+variables. This functionality is also also provided by the `ExtendFormula`
+trait.
+
+```rust
+# extern crate varisat;
+# use varisat::{CnfFormula, ExtendFormula, Lit, Var};
+let mut formula = CnfFormula::new();
+
+let a = formula.new_var().negative();
+let b = formula.new_lit();
+let (c, d, e) = formula.new_lits();
+let f: Vec<Lit> = formula.new_lit_iter(10).collect();
+
+formula.add_clause(&[a, b, c, d, e]);
+formula.add_clause(&f);
+
+assert_eq!(formula.var_count(), 15);
+```
+
 ## Parsing and Writing Formulas
 
 Varisat provides routines for parsing and writing Formulas in the [DIMACS
@@ -106,6 +135,7 @@ CNF][dimacs] format.
 ```rust
 # extern crate varisat;
 # use varisat::{Var, Lit};
+# use varisat::ExtendFormula;
 use varisat::dimacs::{DimacsParser, write_dimacs};
 
 let input = b"p cnf 3 2\n1 2 3 0\n-1 -3 0\n";

manual/src/lib/incremental.md

@@ -16,11 +16,12 @@ clauses that were already present prior to the last `solve` call.
 
 ```rust
 # extern crate varisat;
-use varisat::{Lit, Solver};
-
-let (x, y, z) = (Lit::from_dimacs(1), Lit::from_dimacs(2), Lit::from_dimacs(3));
+use varisat::{ExtendFormula, Solver};
 
 let mut solver = Solver::new();
+
+let (x, y, z) = solver.new_lits();
+
 solver.add_clause(&[!x, y]);
 solver.add_clause(&[!y, z]);
 assert_eq!(solver.solve().unwrap(), true);
@@ -49,12 +50,13 @@ clauses:
 
 ```rust
 # extern crate varisat;
-use varisat::{Lit, Solver};
-
-let (x, y, z) = (Lit::from_dimacs(1), Lit::from_dimacs(2), Lit::from_dimacs(3));
-let ignore_clauses = Lit::from_dimacs(4);
+use varisat::{ExtendFormula, Solver};
 
 let mut solver = Solver::new();
+
+let (x, y, z) = solver.new_lits();
+let ignore_clauses = solver.new_lit();
+
 solver.add_clause(&[!x, y]);
 solver.add_clause(&[!y, z]);
 assert_eq!(solver.solve().unwrap(), true);

varisat-dimacs/src/lib.rs

@@ -4,7 +4,7 @@ use std::borrow::Borrow;
 use std::io;
 use std::mem::replace;
 
-use varisat_formula::{CnfFormula, Lit, Var};
+use varisat_formula::{CnfFormula, ExtendFormula, Lit, Var};
 
 use failure::{Error, Fail};
 
@@ -309,10 +309,8 @@ impl DimacsParser {
                 self.partial_clause.clear();
                 self.clause_count += 1;
             } else {
-                self.partial_clause.push(Lit::from_var(
-                    Var::from_dimacs(self.partial_lit as isize),
-                    !self.negate_next_lit,
-                ));
+                self.partial_clause
+                    .push(Var::from_dimacs(self.partial_lit as isize).lit(!self.negate_next_lit));
             }
         }
     }