clpb test ok

parent b449e702
......@@ -283,23 +283,17 @@ sat_roots(Sat, Roots) :-
%% sat(+Expr) is semidet.
%
% True iff Expr is a satisfiable Boolean expression.
sat(Sat0) :-
( phrase(sat_ands(Sat0), Ands), Ands = [_,_|_] ->
maplist(sat, Ands)
; parse_sat(Sat0, Sat),
write(1),
sat_bdd(Sat, BDD),
write(2),
sat_roots(Sat, Roots),
write(3),
roots_and(Roots, Sat0-BDD, And-BDD1),
write(4),
maplist(del_bdd, Roots),
write(5),
maplist(=(Root), Roots),
write(6),
root_put_formula_bdd(Root, And, BDD1),
write(7),
satisfiable_bdd(BDD1)
).
......@@ -983,7 +977,7 @@ var_u(Node, VNum, Index) :-
attribute_goals(Var) -->
{ var_index_root(Var, _, Root) },
( { root_get_formula_bdd(Root, Formula, BDD) } ->
{ del_bdd(Root),
{ del_bdd(Root),
phrase(sat_ands(Formula), Ands),
maplist(formula_anf, Ands, ANFs0),
sort(ANFs0, ANFs1),
......@@ -1057,7 +1051,7 @@ xors(Node) -->
list2([]) --> [].
list2([L|Ls]) --> [L], list(Ls).
list2([L|Ls]) --> [L], list2(Ls).
with_var(Var, Ls, [Var|Ls]).
......
......@@ -14,35 +14,38 @@
(compile-prolog-string
"
k(V,L,LL) :- var(V) -> (attvar(V) -> L=[V|LL] ; L=LL) ; L=LL.
k([A|B],L,LL) :- k(A,L,LX),k(B,LX,LL).
k(X,L,LL) :- X=..[Q|U] -> k([Q|U],L,LL) ; L=LL.
k(V,L,LL) :- (var(V),!) -> (attvar(V) -> L=[V|LL] ; L=LL).
k([A|B],L,LL) :- !,k(A,L,LX),k(B,LX,LL).
k([],L,L).
k(X,L,LL) :- atomic(X) -> L=LL ;
X=..[X|U] -> k([Q|U],L,LL) ;
L=LL.
")
(<define> (project_the_attributes v)
(<define> (project_the_attributes q)
(<var> (l)
(k v l '())
(k q l '())
(<recur> lp ((v vlist-null) (l l))
(<<match>> (#:mode -) (l)
((x . l)
(<let> ((x (<lookup> x)))
(if (attvar? x)
(if (gp-attvar-raw? x S)
(<recur> lp2 ((v v) (d (gp-att-data x S)))
(<match> (#:mode -) (d)
(((a . _) . d)
(<let*> ((a (<lookup> a))
(f (ref-attribute-projector a)))
(if (and a (not (vhashq-ref v a #f)))
(lp2 (vhash-consq a #t v) d)
(if (and f (not (vhashq-ref v f #f)))
(lp2 (vhash-consq f #t v) d)
(lp2 v d))))
(()
(lp v l))))
(lp v l))))
(()
(<recur> lp ((u (map car (vhash->assoc v))))
(<recur> lp ((u (map car (vhash->assoc v))))
(<<match>> (#:mode -) (u)
((x . u)
(<and>
((<lookup> x) v l)
(<or> (<and> ((<lookup> x) q l) <cut>) <cc>)
(lp u)))
(() <cc>))))))))
......@@ -67,6 +67,7 @@
add_term_expansion_temp
add_goal_expansion
add_goal_expansion_temp
group_pairs_by_key
expand_term
callable
......
......@@ -126,7 +126,10 @@
(args< lx ly)
(<cc> 1)))))
(() ()
(() (_ . _)
(<cut> (<cc> 1)))
(_ _
(<cut> <fail>))))
(<define> (term00< x y)
......
......@@ -37,6 +37,7 @@
pairs_keys_values
same_length
same_term
group_pairs_by_key
transpose))
(define term_variables
......@@ -372,7 +373,7 @@
(<define> (pairs_keys_values pairs keys values)
(<recur> lp ((pairs pairs) (keys keys) (values values))
(<<match>> (#:mode + #:name 'pairs-key-values) (pairs keys values)
((#((_ key val)) . pairs) (+ + (,key . keys)) (+ + (,val . values))
((#((,gop2- key val)) . pairs) (+ + (,key . keys)) (+ + (,val . values))
(lp pairs keys values))
(() (+ + ()) (+ + ())
<cc>))))
......@@ -409,3 +410,18 @@
(<=> y ())))))
(<define> (group_pairs_by_key pairs groups)
(<<match>> (#:mode -) (pairs)
((#(("op2-" k v)) . u)
(<recur> lp ((k k) (p u) (dg (list v)) (g '()))
(<<match>> (#:mode -) (p)
((#(("op2-" ,k v)) . u)
(lp k u (cons v dg) g))
((#(("op2-" kk v)) . u)
(lp kk u (list v) (cons (vector (list op2- k (reverse dg))) g)))
(()
(<=> groups
,(reverse (cons (vector (list op2- k (reverse dg))) g)))))))
(()
(<=> groups ()))))
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment