From 32a905bc8b9792cc7b42242e393433a5d33846df Mon Sep 17 00:00:00 2001
From: Vitor Santos Costa <vitor@mint32.(none)>
Date: Mon, 23 Apr 2012 07:13:25 -0500
Subject: [PATCH] ddnnf support

---
 packages/bdd/ddnnf.yap    | 24 +++++++-----------------
 packages/bdd/simpbool.yap |  2 +-
 2 files changed, 8 insertions(+), 18 deletions(-)

diff --git a/packages/bdd/ddnnf.yap b/packages/bdd/ddnnf.yap
index 3ff1af26f..63e4440c5 100644
--- a/packages/bdd/ddnnf.yap
+++ b/packages/bdd/ddnnf.yap
@@ -16,17 +16,19 @@
 % in DDNNF, Exs \in LVars into DDNNF with extra existential vars
 %
 cnf_to_ddnnf(CNF0, PVs, DDNNF) :-
-	term_variables(CNF0, Vars),
 	list2cnf(CNF0, CNF, []),
-	new_variables_in_term(Vars, CNF, LVars),
-	append(Vars, LVars, AllVars),
+	mkddnnf(CNF, PVs, DDNNF).
+
+mkddnnf(CNF, PVs, DDNNF) :-
+	term_variables(CNF, AllVars),
 %	(numbervars(CNF,1,_), writeln(CNF), fail ; true),
 	open(dimacs, write, S),
 	cnf_to_file(CNF, AllVars, S),
 	close(S),
 	% execute c2d at this point, but we're lazy%
 %	unix(system('c2d -dt_method 3 -in dimacs')),
-	unix(system('c2d -visualize -in dimacs')),
+%	unix(system('c2d -visualize -in dimacs')),
+	unix(system('dsharp -Fnnf dimacs.nnf  dimacs')),
 	open('dimacs.nnf',read,R),
 	SVars =.. [v|AllVars],
 %	ones(LVars),
@@ -100,19 +102,7 @@ disj(A, NO) -->
 ddnnf(List, PVs, DDNNF) :-
 	exps2conj(List, Conj),
 	cnf(Conj, CNF),
-%	(numbervars(CNF,1,_), writeln(Vars:CNF), fail ; true),
-	open(dimacs, write, S),
-	variables_in_term(PVs, CNF, LVars),
-	append(PVs, LVars, AllVars),
-	cnf_to_file(CNF, AllVars, S),
-	close(S),
-	% execute c2d at this point, but we're lazy
-	unix(system('c2d -in dimacs')),
-	open('dimacs.nnf',read,R),
-	SVars =.. [v|AllVars],
-%	ones(LVars),
-	input_ddnnf(R, SVars, PVs, DDNNF),
-	close(R).
+	mkddnnf(CNF, PVs, DDNNF).
 
 exps2conj((C1,C2), CC1*CC2) :- !,
 	exps2conj(C1, CC1),
diff --git a/packages/bdd/simpbool.yap b/packages/bdd/simpbool.yap
index bf7f80db3..7dafa4d82 100644
--- a/packages/bdd/simpbool.yap
+++ b/packages/bdd/simpbool.yap
@@ -6,7 +6,7 @@
 :- module(simplify_boolean, 
 	[simplify_exp/2]).
 
-%simplify_exp(V,V) :- !.
+%simplify_exp(V,V) :- writeln(V), fail, !.
 simplify_exp(V,V) :- var(V), !.
 simplify_exp(S1+S2,NS) :- !,
 	simplify_exp(S1, SS1),