Declarative predicates by limiting resources

Not sure I get this. I guess the whole problem is related to the mathematical concept of countability. If all choice points are finite we have a finite set of solutions that we will nicely cover. If one is infinite it depends on the ordering. If the infinite one is the oldest, all still works fine: the finite ones will be exhausted, advancing the infinite one, etc. If the infinite is not the oldest, the choice points that are older are never explored. So with one infinite ordering can (always?) fix the problem.

With two infinite (your case), this doesn’t work. You can use call_with_depth_limit/3 to make the infinite choices finite and do iterative deepening. As long as you do not use infinite foreign choice points (e.g., repeat), this should work fine. It creates duplicates. Possibly you can solve that by demanding that the reached depth is exactly the limit? Not 100% sure.

Otherwise, I think you are stuck with normal Prolog. My intuition says delimited continuations are probably not an answer as these capture the continuation, but not the (open) choices. Possibly you can restructure to get what you want. Alternatively you can use engines and restructure the program such that each engine satisfies the rules above (at most one infinite choice point that is the oldest) and next you can takes answers from each of them and combine the result.

Finally, you can map your infinite space to another infinite state that is easily counted, i.e., make a mapping from integers to your btrees, count the integers and map each to a btree.