Merge 52acf9a into f5a5cfe

Tractables · Mar 22, 2021 · c800a3a · c800a3a
2 parents f5a5cfe + 52acf9a
commit c800a3a
Show file tree

Hide file tree

Showing 2 changed files with 32 additions and 0 deletions.
diff --git a/src/sdd/sdd_functions.jl b/src/sdd/sdd_functions.jl
@@ -227,3 +227,11 @@ import Base: xor
 "Exclusive logical disjunction (XOR)"
 xor(x::Sdd,y::Sdd) = (x ∧ ¬y) ∨ (y ∧ ¬x)
 
+"Smooth an sdd to a StructLogicCircuit"
+function smooth(root::Sdd)::StructLogicCircuit
+    lc = LogicCircuit(root)
+    plc = propagate_constants(lc, remove_unary=true)
+    slc = StructLogicCircuit(root.vtree, plc)
+    smooth(slc)
+end
+
diff --git a/test/sdd/sdds_test.jl b/test/sdd/sdds_test.jl
@@ -45,4 +45,28 @@ include("../helper/validate_sdd.jl")
 
    end
 
+end
+
+@testset "sdd smoothing test" begin
+   cnfs = [ 
+            ("easy","C17_mince",32,92,45)
+            ("easy","majority_mince",32,132,61)
+            ("easy","b1_mince",8,169,84)
+            ("easy","cm152a_mince",2048,127,62)
+            ("iscas89","s208.1.scan",262144,1942,927)
+          ]
+
+
+   for (suite, name, count, size, nodes) in cnfs
+
+      cnf = zoo_cnf("$suite/$name.cnf")
+      vtree = zoo_vtree("$suite/$name.min.vtree");
+
+      mgr = SddMgr(vtree)
+      cnfΔ = compile(mgr, cnf)
+
+      smooth_slc = smooth(cnfΔ)
+      @test issmooth(smooth_slc)
+      @test respects_vtree(smooth_slc, vtree)
+   end  
 end