From: Markus Triska <triska@metalevel.at>
Date: Sun, 23 Apr 2023 07:20:46 +0000 (+0200)
Subject: remove residual goal for ground BDD
X-Git-Tag: v0.9.2~144^2
X-Git-Url: https://git.sagredo.dev/?a=commitdiff_plain;h=2a1b8f37eca21a80ad22b22dc23304379e3d77c5;p=scryer-prolog.git

remove residual goal for ground BDD

Example:

    ?- sat(X).
       X = 1.
---

diff --git a/src/lib/clpb.pl b/src/lib/clpb.pl
index 1bdbbefc..3b7ac007 100644
--- a/src/lib/clpb.pl
+++ b/src/lib/clpb.pl
@@ -1628,6 +1628,7 @@ skip_to_var_(Var, Weight, [Var0-Weight0|VWs0], VWs) -->
 
 attribute_goals(Var) -->
         { var_index_root(Var, _, Root) },
+        !,
         (   { root_get_formula_bdd(Root, Formula, BDD) } ->
             { del_bdd(Root) },
             (   { clpb_residuals(bdd) } ->
@@ -1655,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_bdd(BDD)),
+          ground(BDD),
+          put_atts(Var, -clpb_bdd(_)) }.
 
 del_clpb(Var) :-
         del_attr(Var, clpb),