various sdd and vtree fixes

src/queries/queries.jl

@@ -245,8 +245,8 @@ Note: this function is generally intractable for large circuits.
 function isdeterministic(root::LogicCircuit)::Bool
     mgr = sdd_mgr_for(root)
     result::Bool = true
-    f_con(c) = mgr(constant(c))
-    f_lit(n) = mgr(literal(n))
+    f_con(c) = compile(mgr,constant(c))
+    f_lit(n) = compile(mgr,literal(n))
     f_a(_, cs) = reduce(&, cs)
     f_o(_, cs) = begin
         for i = 1:length(cs)

src/sdd/apply.jl

@@ -2,9 +2,9 @@
 Conjoin two SDDs
 """
 @inline conjoin(x::SddConstantNode, y::SddConstantNode) = 
-    (isfalse(x) || isfalse(y)) ? false_sdd : true_sdd  
+    ((x === false_sdd) || (y === false_sdd)) ? false_sdd : true_sdd  
 @inline conjoin(x::Sdd, y::SddConstantNode) = 
-    isfalse(y) ? false_sdd : x
+    (y === false_sdd) ? false_sdd : x
 @inline conjoin(x::SddConstantNode, y::Sdd) = 
     conjoin(y, x)
 
@@ -18,7 +18,6 @@ function conjoin(s::SddLiteralNode, t::SddLiteralNode)::Sdd
     end
 end
 
-
 # Note: attempts to make a special cache for conjunctions with literals have not yielded speedups
 
 function conjoin(s::Sdd, t::Sdd)::Sdd 

src/sdd/sdd_functions.jl

@@ -112,7 +112,7 @@ compile(::SddMgr, constant::Bool) =
 Negate an SDD
 """
 @inline negate(c::SddConstantNode) = 
-    isfalse(c) ? true_sdd : false_sdd
+    (c === false_sdd) ? true_sdd : false_sdd
 
 function negate(s::SddLiteralNode)
     if ispositive(s) 
@@ -210,7 +210,7 @@ model_count(root::StructLogicCircuit)::BigInt =
     model_count(root, length(global_scope(vtree(root))))
 
 "Decide whether one sentence logically entails another"
-entails(x::Sdd, y::Sdd) = isfalse(x & !y)
+entails(x::Sdd, y::Sdd) = ((x & !y) === false_sdd)
 
 "Decide whether two sentences are logically equivalent"
 equivalent(x::Sdd, y::Sdd) = begin

src/structured/abstract_vtrees.jl

@@ -106,9 +106,6 @@ Base.show(io::IO, c::Vtree) = print(io, "$(typeof(c))($(join(variables(c), ','))
 # Constructors
 #############
 
-# Syntactic sugar to compile circuits using a vtree
-(vtree::Vtree)(arg) = compile(vtree, arg)
-
 # construct vtrees from other vtrees
 function (::Type{V})(vtree::Vtree)::V where V<:Vtree
     f_leaf(l) = V(variable(l))

test/sdd/sdds_test.jl

@@ -12,7 +12,7 @@ include("../helper/validate_sdd.jl")
    @test_throws Exception compile(mgr.left, cnf)
    @test_throws Exception compile(right_most_descendent(mgr), cnf)
 
-   r = mgr(cnf)
+   r = compile(mgr,cnf)
    @test compile(mgr, cnf) === r
 
    @test respects_vtree(r)

test/sdd/trimmed_apply_test.jl

@@ -16,12 +16,12 @@ using LogicCircuits
     notx_c = compile(mgr,notx)
     true_c = compile(mgr,true)
     @test true_c isa Sdd
-    @test true_c === mgr(true)
+    @test true_c === compile(mgr,true)
     @test true_c === compile(Sdd,mgr,true)
     @test true_c === (Sdd,mgr)(true)
     @test true_c === (mgr,Sdd)(true)
     false_c = compile(mgr,false)
-    @test false_c === mgr(false)
+    @test false_c === compile(mgr,false)
 
     @test false_c & true_c == false_c
     @test false_c & notx_c == false_c
@@ -139,7 +139,7 @@ using LogicCircuits
     @test model_count(f4c) == model_count(f4)
     @test f4c.vtree === f4.vtree
 
-    f4c = mgr(StructLogicCircuit(mgr,f4))
+    f4c = compile(mgr,StructLogicCircuit(mgr,f4))
     @test Sdd(mgr,f4c) === f4c
     @test f4 === f4c
     @test f4c isa Sdd

test/sdd/trimmed_sdds_test.jl

@@ -5,60 +5,60 @@ using LogicCircuits: Element # test some internals
 @testset "Trimmed SDD test" begin
 
     num_vars = 7
-    mgr = SddMgr(num_vars, :balanced)
+    manager = SddMgr(num_vars, :balanced)
 
-    @test num_variables(mgr) == num_vars
-    @test num_nodes(mgr) == 2*num_vars-1
-    @test num_edges(mgr) == 2*num_vars-2
-    @test mgr isa SddMgr
-
-    @test varsubset(left_most_descendent(mgr), mgr)
-    @test varsubset(mgr.left, mgr)
-    @test varsubset(mgr.right, mgr)
-    @test varsubset_left(mgr.left, mgr)
-    @test varsubset_left(mgr.left.left, mgr)
-    @test varsubset_left(mgr.left.right, mgr)
-    @test varsubset_right(mgr.right, mgr)
-    @test varsubset_right(mgr.right.right, mgr)
-    @test varsubset_right(mgr.right.left, mgr)
-
-    @test !varsubset(mgr, left_most_descendent(mgr))
-    @test !varsubset_left(mgr.right, mgr)
-    @test !varsubset_left(mgr.right.left, mgr)
-    @test !varsubset_left(mgr.right.right, mgr)
-    @test !varsubset_left(mgr, mgr)
-    @test !varsubset_left(mgr, mgr.left)
-    @test !varsubset_left(mgr, mgr.right)
-    @test !varsubset_right(mgr.left, mgr)
-    @test !varsubset_right(mgr.left.right, mgr)
-    @test !varsubset_right(mgr.left.left, mgr)
-    @test !varsubset_right(mgr, mgr)
-    @test !varsubset_right(mgr, mgr.left)
-    @test !varsubset_right(mgr, mgr.right)
+    @test num_variables(manager) == num_vars
+    @test num_nodes(manager) == 2*num_vars-1
+    @test num_edges(manager) == 2*num_vars-2
+    @test manager isa SddMgr
+
+    @test varsubset(left_most_descendent(manager), manager)
+    @test varsubset(manager.left, manager)
+    @test varsubset(manager.right, manager)
+    @test varsubset_left(manager.left, manager)
+    @test varsubset_left(manager.left.left, manager)
+    @test varsubset_left(manager.left.right, manager)
+    @test varsubset_right(manager.right, manager)
+    @test varsubset_right(manager.right.right, manager)
+    @test varsubset_right(manager.right.left, manager)
+
+    @test !varsubset(manager, left_most_descendent(manager))
+    @test !varsubset_left(manager.right, manager)
+    @test !varsubset_left(manager.right.left, manager)
+    @test !varsubset_left(manager.right.right, manager)
+    @test !varsubset_left(manager, manager)
+    @test !varsubset_left(manager, manager.left)
+    @test !varsubset_left(manager, manager.right)
+    @test !varsubset_right(manager.left, manager)
+    @test !varsubset_right(manager.left.right, manager)
+    @test !varsubset_right(manager.left.left, manager)
+    @test !varsubset_right(manager, manager)
+    @test !varsubset_right(manager, manager.left)
+    @test !varsubset_right(manager, manager.right)
 
     x = Var(1)
     y = Var(2)
 
-    x_c = compile(mgr, var2lit(x))
-    y_c = compile(mgr, var2lit(y))
+    x_c = compile(manager, var2lit(x))
+    y_c = compile(manager, var2lit(y))
 
     @test x_c != y_c 
 
     @test variable(x_c) == x
     @test literal(x_c) == var2lit(x)
-    @test vtree(x_c) ∈ mgr
+    @test vtree(x_c) ∈ manager
     @test ispositive(x_c)
-    @test x_c == compile(mgr, var2lit(x))
+    @test x_c == compile(manager, var2lit(x))
 
     @test variable(y_c) == y
     @test literal(y_c) == var2lit(y)
-    @test vtree(y_c) ∈ mgr
+    @test vtree(y_c) ∈ manager
     @test ispositive(y_c)
-    @test y_c == compile(mgr, var2lit(y))
+    @test y_c == compile(manager, var2lit(y))
 
     notx = -var2lit(x)
 
-    notx_c = compile(mgr,notx)
+    notx_c = compile(manager,notx)
 
     @test sat_prob(x_c) == 1//2
     @test sat_prob(notx_c) == 1//2
@@ -69,16 +69,16 @@ using LogicCircuits: Element # test some internals
 
     @test variable(notx_c) == x
     @test literal(notx_c) == notx
-    @test vtree(notx_c) ∈ mgr
+    @test vtree(notx_c) ∈ manager
     @test isnegative(notx_c)
-    @test notx_c == compile(mgr, notx)
+    @test notx_c == compile(manager, notx)
 
-    true_c = compile(mgr,true)
+    true_c = compile(manager,true)
 
     @test istrue(true_c)
     @test constant(true_c) == true
 
-    false_c = compile(mgr,false)
+    false_c = compile(manager,false)
 
     @test isfalse(false_c)
     @test constant(false_c) == false
@@ -91,26 +91,26 @@ using LogicCircuits: Element # test some internals
     @test model_count(true_c,num_vars) == BigInt(2)^(num_vars)
     @test model_count(false_c,num_vars) == BigInt(0)
 
-    v1 = compile(mgr, Lit(1))
-    v2 = compile(mgr, Lit(2))
-    v3 = compile(mgr, Lit(3))
-    v4 = compile(mgr, Lit(4))
-    v5 = compile(mgr, Lit(5))
-    v6 = compile(mgr, Lit(6))
-    v7 = compile(mgr, Lit(7))
-    @test_throws Exception compile(mgr, Lit(8))
+    v1 = compile(manager, Lit(1))
+    v2 = compile(manager, Lit(2))
+    v3 = compile(manager, Lit(3))
+    v4 = compile(manager, Lit(4))
+    v5 = compile(manager, Lit(5))
+    v6 = compile(manager, Lit(6))
+    v7 = compile(manager, Lit(7))
+    @test_throws Exception compile(manager, Lit(8))
 
     p1 = [Element(true_c,v3)]
-    @test canonicalize(p1, mgr.left.right) === v3
+    @test canonicalize(p1, manager.left.right) === v3
     p2 = [Element(v1,true_c), Element(!v1,false_c)]
-    @test canonicalize(p2, mgr.left) === v1
+    @test canonicalize(p2, manager.left) === v1
 
     p3 = [Element(v1,v4), Element(!v1,v7)]
-    n1 = canonicalize(p3, mgr)
+    n1 = canonicalize(p3, manager)
     p4 = [Element(!v1,v7), Element(v1,v4)]
-    n2 = canonicalize(p4,mgr)
-    @test n1.vtree.left === mgr.left
-    @test n1.vtree.right === mgr.right
+    n2 = canonicalize(p4,manager)
+    @test n1.vtree.left === manager.left
+    @test n1.vtree.right === manager.right
     @test n1 === n2
     @test isdeterministic(n1)
     @test n1(true, false, false, true, false, false, false)

test/structured/structured_logic_nodes_test.jl

@@ -37,7 +37,7 @@ using DataFrames: DataFrame
     @test !istrue(f)
     @test !isfalse(f)
 
-    @test literal(vtree(Lit(-5))) == Lit(-5)
+    @test literal(compile(vtree,Lit(-5))) == Lit(-5)
     @test literal((PlainStructLogicCircuit,vtree)(Lit(-5))) == Lit(-5)
     @test constant((PlainStructLogicCircuit,vtree)(false)) == false
 

test/structured/vtree_tests.jl

@@ -21,7 +21,7 @@ using LogicCircuits
     @test lca(v1,i1) == i1
     @test lca(v1,i1,v1) == i1
     @test lca(v1,v2,v3) == r
-    @test lca(vtree_safe(r(true)), vtree_safe(r(false))) === nothing
+    @test lca(vtree_safe(compile(r,true)), vtree_safe(compile(r,false))) === nothing
 
     @test_throws Exception lca(i1,PlainVtree(Var(4)))
     @test varsubset_left(v1,r)