Merge pull request #52 from timbeurskens/feature/definitions

language support for pre-defined references to subtrees

Cargo.toml

@@ -9,7 +9,7 @@ authors = ["Tim Beurskens <[email protected]>"]
 [package]
 name = "rsbdd"
 description = "A BDD-based SAT solver"
-version = "0.13.0"
+version = "0.14.2"
 edition.workspace = true
 authors.workspace = true
 

examples/cliques.txt

@@ -31,6 +31,15 @@ only the complement of E is denoted below.
 The cliques problem shows an interesting similarity to the graph-coloring problem:
 graph coloring can be encoded as a clique in a graph of vertices VxC where V is the set of vertices in the graph to be colored, and C is the set of colors.
 a vertex pair in the clique graph is connected by an edge if the original vertices are adjacent, and they do not share the same color.
+
+more intuitive explanation:
+
+- The encoding chosen here is: 'a variable is true if it is in the clique, false if it is not in the clique'.
+- Every node is a variable.
+- A node can be in the clique if all its edges are in the clique as well.
+- Unconnected nodes can not be in the clique simultaneously.
+- Every unconnected edge (edge in the residual graph) is a new -(x & y) constraint.
+
 "
 
 -(a & f) &

src/bin/rsbdd.rs

@@ -130,7 +130,6 @@ fn main() -> anyhow::Result<()> {
     if !args.retain_choices.is_any() {
         result = input_parsed
             .env
-            .borrow()
             .retain_choice_bottom_up(result, args.retain_choices);
     }
 
@@ -145,7 +144,7 @@ fn main() -> anyhow::Result<()> {
 
     // reduce the bdd to a single path from root to a single 'true' node
     if args.model {
-        result = input_parsed.env.borrow().model(result);
+        result = input_parsed.env.model(result);
     }
 
     // show ordered variable list