From efcc2b81cdb681d2a9c248347cba63115dd96f3c Mon Sep 17 00:00:00 2001 From: Markus Triska Date: Fri, 8 Sep 2023 22:37:18 +0200 Subject: [PATCH 1/7] add licensing information, addressing part of #1798 --- src/lib/clpb.pl | 27 +++++++++++++++++++++++---- 1 file changed, 23 insertions(+), 4 deletions(-) diff --git a/src/lib/clpb.pl b/src/lib/clpb.pl index 9d90ecd7..fdf1cfce 100644 --- a/src/lib/clpb.pl +++ b/src/lib/clpb.pl @@ -1,10 +1,29 @@ /* CLP(B): Constraint Logic Programming over Boolean Variables - Copyright (C): 2019-2023 Markus Triska - All rights reserved. - + Author: Markus Triska E-mail: triska@metalevel.at - WWW: http://www.metalevel.at + WWW: https://www.metalevel.at + Copyright (C): 2019-2023 Markus Triska + + Permission is hereby granted, free of charge, to any person + obtaining a copy of this software and associated documentation + files (the "Software"), to deal in the Software without + restriction, including without limitation the rights to use, copy, + modify, merge, publish, distribute, sublicense, and/or sell copies + of the Software, and to permit persons to whom the Software is + furnished to do so, subject to the following conditions: + + The above copyright notice and this permission notice shall be + included in all copies or substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, + EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF + MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT + HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, + WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER + DEALINGS IN THE SOFTWARE. */ From 672979c515703ad5c2aa2ef18b1c2451ced512a9 Mon Sep 17 00:00:00 2001 From: Markus Triska Date: Fri, 8 Sep 2023 22:40:50 +0200 Subject: [PATCH 2/7] shorter include/3 and exclude/3, relying on improved indexing --- src/lib/clpb.pl | 32 ++++++++++++-------------------- 1 file changed, 12 insertions(+), 20 deletions(-) diff --git a/src/lib/clpb.pl b/src/lib/clpb.pl index fdf1cfce..311d6115 100644 --- a/src/lib/clpb.pl +++ b/src/lib/clpb.pl @@ -1949,29 +1949,21 @@ Compatibility predicates. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ -include(Goal, List, Is) :- - include_(List, Goal, Is). - -include_([], _, []). -include_([X1|Xs1], P, Is) :- - ( call(P, X1) - -> Is = [X1|Is1] - ; Is = Is1 +include(_, [], []). +include(Goal, [L|Ls0], Ls) :- + ( call(Goal, L) -> + Ls = [L|Rest] + ; Ls = Rest ), - include_(Xs1, P, Is1). + include(Goal, Ls0, Rest). - -exclude(Goal, List, Is) :- - exclude_(List, Goal, Is). - -exclude_([], _, []). -exclude_([X1|Xs1], P, Is) :- - ( call(P, X1) - -> Is = Is1 - ; Is = [X1|Is1] +exclude(_, [], []). +exclude(Goal, [L|Ls0], Ls) :- + ( call(Goal, L) -> + Ls = Rest + ; Ls = [L|Rest] ), - exclude_(Xs1, P, Is1). - + exclude(Goal, Ls0, Rest). partition(Pred, List, Less, Equal, Greater) :- partition_(List, Pred, Less, Equal, Greater). From ad4c17fbb6590b7bd04cd058e0d5d755d5dc14c3 Mon Sep 17 00:00:00 2001 From: Markus Triska Date: Fri, 8 Sep 2023 22:41:49 +0200 Subject: [PATCH 3/7] add meta_predicate/1 declaration for include/3 and exclude/3 --- src/lib/clpb.pl | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/lib/clpb.pl b/src/lib/clpb.pl index 311d6115..b5deff81 100644 --- a/src/lib/clpb.pl +++ b/src/lib/clpb.pl @@ -1949,6 +1949,8 @@ Compatibility predicates. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ +:- meta_predicate(include(1, ?, ?)). + include(_, [], []). include(Goal, [L|Ls0], Ls) :- ( call(Goal, L) -> @@ -1957,6 +1959,8 @@ include(Goal, [L|Ls0], Ls) :- ), include(Goal, Ls0, Rest). +:- meta_predicate(exclude(1, ?, ?)). + exclude(_, [], []). exclude(Goal, [L|Ls0], Ls) :- ( call(Goal, L) -> From ec67752db480c5c9b96711ade6f5d72f6d433471 Mon Sep 17 00:00:00 2001 From: Markus Triska Date: Fri, 8 Sep 2023 22:47:59 +0200 Subject: [PATCH 4/7] shorter partition/5, relying on first instantiated argument indexing --- src/lib/clpb.pl | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/src/lib/clpb.pl b/src/lib/clpb.pl index b5deff81..d2e63db0 100644 --- a/src/lib/clpb.pl +++ b/src/lib/clpb.pl @@ -1969,17 +1969,16 @@ exclude(Goal, [L|Ls0], Ls) :- ), exclude(Goal, Ls0, Rest). -partition(Pred, List, Less, Equal, Greater) :- - partition_(List, Pred, Less, Equal, Greater). +:- meta_predicate(partition(2,?,?,?,?)). -partition_([], _, [], [], []). -partition_([H|T], Pred, L, E, G) :- +partition(_, [], [], [], []). +partition(Pred, [H|T], L, E, G) :- call(Pred, H, Diff), partition_(Diff, H, Pred, T, L, E, G). partition_(<, H, Pred, T, [H|Rest], E, G) :- - partition_(T, Pred, Rest, E, G). + partition(Pred, T, Rest, E, G). partition_(=, H, Pred, T, L, [H|Rest], G) :- - partition_(T, Pred, L, Rest, G). + partition(Pred, T, L, Rest, G). partition_(>, H, Pred, T, L, E, [H|Rest]) :- - partition_(T, Pred, L, E, Rest). + partition(Pred, T, L, E, Rest). From b38a56e7d35c692923c892f0b155f2eb3dba9056 Mon Sep 17 00:00:00 2001 From: Markus Triska Date: Fri, 8 Sep 2023 23:12:33 +0200 Subject: [PATCH 5/7] move compatibility predicates and meta_predicate/1 declarations so that they are correctly taken into account --- src/lib/clpb.pl | 85 +++++++++++++++++++++++++------------------------ 1 file changed, 44 insertions(+), 41 deletions(-) diff --git a/src/lib/clpb.pl b/src/lib/clpb.pl index d2e63db0..ec31b298 100644 --- a/src/lib/clpb.pl +++ b/src/lib/clpb.pl @@ -110,6 +110,46 @@ domain_error(Expectation, Term) :- type_error(Expectation, Term) :- type_error(Expectation, Term, unknown(Term)-1). +/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - +Compatibility predicates. +- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ + +:- meta_predicate(include(1, ?, ?)). + +include(_, [], []). +include(Goal, [L|Ls0], Ls) :- + ( call(Goal, L) -> + Ls = [L|Rest] + ; Ls = Rest + ), + include(Goal, Ls0, Rest). + +:- meta_predicate(exclude(1, ?, ?)). + +exclude(_, [], []). +exclude(Goal, [L|Ls0], Ls) :- + ( call(Goal, L) -> + Ls = Rest + ; Ls = [L|Rest] + ), + exclude(Goal, Ls0, Rest). + +:- meta_predicate(partition(2,?,?,?,?)). + +partition(_, [], [], [], []). +partition(Pred, [H|T], L, E, G) :- + call(Pred, H, Diff), + partition_(Diff, H, Pred, T, L, E, G). + +partition_(<, H, Pred, T, [H|Rest], E, G) :- + partition(Pred, T, Rest, E, G). +partition_(=, H, Pred, T, L, [H|Rest], G) :- + partition(Pred, T, L, Rest, G). +partition_(>, H, Pred, T, L, E, [H|Rest]) :- + partition(Pred, T, L, E, Rest). + +:- meta_predicate(partition(1,?,?,?)). + partition(Pred, Ls0, As, Bs) :- include(Pred, Ls0, As), exclude(Pred, Ls0, Bs). @@ -466,6 +506,10 @@ non_monotonic(X) :- ; true ). +:- meta_predicate(bdd_nodes(1, ?, ?)). +:- meta_predicate(bdd_nodes_(1, ?, ?, ?)). +:- meta_predicate(with_aux(1, ?)). + /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - Rewriting to canonical expressions. Atoms are converted to variables with a special attribute. @@ -1941,44 +1985,3 @@ clpb_atom_var(Atom, Var) :- put_assoc(Atom, A0, Var, A), b_setval('$clpb_atoms', A) ). - - - -/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -Compatibility predicates. -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ - - -:- meta_predicate(include(1, ?, ?)). - -include(_, [], []). -include(Goal, [L|Ls0], Ls) :- - ( call(Goal, L) -> - Ls = [L|Rest] - ; Ls = Rest - ), - include(Goal, Ls0, Rest). - -:- meta_predicate(exclude(1, ?, ?)). - -exclude(_, [], []). -exclude(Goal, [L|Ls0], Ls) :- - ( call(Goal, L) -> - Ls = Rest - ; Ls = [L|Rest] - ), - exclude(Goal, Ls0, Rest). - -:- meta_predicate(partition(2,?,?,?,?)). - -partition(_, [], [], [], []). -partition(Pred, [H|T], L, E, G) :- - call(Pred, H, Diff), - partition_(Diff, H, Pred, T, L, E, G). - -partition_(<, H, Pred, T, [H|Rest], E, G) :- - partition(Pred, T, Rest, E, G). -partition_(=, H, Pred, T, L, [H|Rest], G) :- - partition(Pred, T, L, Rest, G). -partition_(>, H, Pred, T, L, E, [H|Rest]) :- - partition(Pred, T, L, E, Rest). From 6fe85c5779d3ac81cdea1020852a1535697fde7c Mon Sep 17 00:00:00 2001 From: Markus Triska Date: Fri, 8 Sep 2023 23:19:10 +0200 Subject: [PATCH 6/7] remove more attributes so that they do not appear in residual goals --- src/lib/clpb.pl | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/lib/clpb.pl b/src/lib/clpb.pl index ec31b298..213d684a 100644 --- a/src/lib/clpb.pl +++ b/src/lib/clpb.pl @@ -1729,7 +1729,8 @@ attribute_goals(Var) --> del_clpb(Var) :- del_attr(Var, clpb), - del_attr(Var, clpb_hash). + del_attr(Var, clpb_hash), + del_attr(Var, clpb_atom). /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - To make residual projection work with recorded constraints, the @@ -1883,7 +1884,8 @@ booleans([B|Bs]) --> boolean(B), booleans(Bs). boolean(Var) --> { del_clpb(Var) }, - ( { get_attr(Var, clpb_omit_boolean, true) } -> [] + ( { get_attr(Var, clpb_omit_boolean, true) } -> + { put_atts(Var, -clpb_omit_boolean(_)) } ; [clpb:sat(Var =:= Var)] ). From 85cc4a80d083bb911708d3ddeb198163db15eeff Mon Sep 17 00:00:00 2001 From: Markus Triska Date: Sat, 9 Sep 2023 07:23:34 +0200 Subject: [PATCH 7/7] remove code that is not needed in Scryer Prolog --- src/lib/clpb.pl | 27 +-------------------------- 1 file changed, 1 insertion(+), 26 deletions(-) diff --git a/src/lib/clpb.pl b/src/lib/clpb.pl index 213d684a..4dde600b 100644 --- a/src/lib/clpb.pl +++ b/src/lib/clpb.pl @@ -1697,8 +1697,7 @@ attribute_goals(Var) --> { bdd_nodes(BDD, Nodes), phrase(nodes(Nodes), Ns) }, [clpb:'$clpb_bdd'(Ns)] - ; { prepare_global_variables(BDD), - phrase(sat_ands(Formula), Ands0), + ; { phrase(sat_ands(Formula), Ands0), ands_fusion(Ands0, Ands), maplist(formula_anf, Ands, ANFs0), sort(ANFs0, ANFs1), @@ -1732,34 +1731,10 @@ del_clpb(Var) :- del_attr(Var, clpb_hash), del_attr(Var, clpb_atom). -/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - To make residual projection work with recorded constraints, the - global counters must be adjusted so that new variables and nodes - also get new IDs. Also, clpb_next_id/2 is used to actually create - these counters, because creating them with b_setval/2 would make - them [] on backtracking, which is quite unfortunate in itself. -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ - b_setval(K, T) :- bb_b_put(K, T). nb_setval(K, T) :- bb_put(K, T). b_getval(K, T) :- bb_get(K, T). -prepare_global_variables(BDD) :- - clpb_next_id('$clpb_next_var', V0), - clpb_next_id('$clpb_next_node', N0), - bdd_nodes(BDD, Nodes), - foldl(max_variable_node, Nodes, V0-N0, MaxV0-MaxN0), - MaxV is MaxV0 + 1, - MaxN is MaxN0 + 1, - b_setval('$clpb_next_var', MaxV), - b_setval('$clpb_next_node', MaxN). - -max_variable_node(Node, V0-N0, V-N) :- - node_id(Node, N1), - node_varindex(Node, V1), - N is max(N0,N1), - V is max(V0,V1). - /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - Fuse formulas that share the same variables into single conjunctions. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */