From 1c33d2a2edb85ca235f4958f7db35bcb5bf61a21 Mon Sep 17 00:00:00 2001 From: Markus Triska Date: Sun, 3 Sep 2023 21:47:58 +0200 Subject: [PATCH 1/3] remove clpb_max/1 attribute for residual goal projection Example: ?- sat(A+B), weighted_maximum([1,1], [A,B], Max). A = 1, B = 1, Max = 2. --- src/lib/clpb.pl | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/lib/clpb.pl b/src/lib/clpb.pl index 3b7ac007..868ac277 100644 --- a/src/lib/clpb.pl +++ b/src/lib/clpb.pl @@ -1656,6 +1656,10 @@ attribute_goals(Var) --> booleans(RestVs) ; boolean(Var) % the variable may have occurred only in taut/2 ). +attribute_goals(Var) --> + { get_atts(Var, clpb_max(_)), + !, + put_atts(Var, -clpb_max(_)) }. attribute_goals(Var) --> { get_atts(Var, clpb_bdd(BDD)), ground(BDD), From 1257ba165fca5d2f9c4dde8296a0b43182943fbf Mon Sep 17 00:00:00 2001 From: Markus Triska Date: Sun, 3 Sep 2023 21:57:51 +0200 Subject: [PATCH 2/3] untabify --- src/lib/clpb.pl | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/lib/clpb.pl b/src/lib/clpb.pl index 868ac277..15c7837b 100644 --- a/src/lib/clpb.pl +++ b/src/lib/clpb.pl @@ -17,8 +17,8 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ :- module(clpb, [op(300, fy, ~), - op(500, yfx, #), - sat/1, + op(500, yfx, #), + sat/1, taut/2, labeling/1, sat_count/2, From 85f4bdbe0b66742741f73bdb3dea10604f5f26bf Mon Sep 17 00:00:00 2001 From: Markus Triska Date: Sun, 3 Sep 2023 22:01:38 +0200 Subject: [PATCH 3/3] update answer --- src/lib/clpb.pl | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/lib/clpb.pl b/src/lib/clpb.pl index 15c7837b..9d90ecd7 100644 --- a/src/lib/clpb.pl +++ b/src/lib/clpb.pl @@ -1513,8 +1513,7 @@ random_bindings(VNum, Node) --> % % ``` % ?- sat(A#B), weighted_maximum([1,2,1], [A,B,C], Maximum). -% A = 0, B = 1, C = 1, Maximum = 3 -% ; false. +% A = 0, B = 1, C = 1, Maximum = 3. % ``` weighted_maximum(Ws, Vars, Max) :-