> > What do you mean by compatibility in this case? Are you looking for >> unsatisfiability? Do you have an efficiency concern in mind (with an >> example)? >> > > What I was trying to say can be illustrated by following examples. > > Suppose, after (lazy) negation of individual states in stream we get the > following stream: > > ((x == 1) || ... ) && ((x == 2) || ... ) && ... // here goes other > conjuncts (probably, infinitely many) > > We start folding this stream, i.e we are trying to convert it from CNF to > DNF. > > First, we try to combine (x == 1) and (x == 2). Since the formula is > unsatisfiable, we can drop it and start to proceed with other disjuncts. > > But lets consider other case: > > ((x == 1) || ... ) && ((y == 2) || ... ) && ... > > > Now (x == 1) && (y == 2) is satifiable, and we have to drag it through > other `negated` answers. In the worst case, we have to drag (x == 1) > through the whole stream. >
This sounds like you're switching search strategies to depth-first. Why not consider each of these disjuncts like any other goal in a conjunction, and benefit from interleaving? Are you noticing too much space usage? -- You received this message because you are subscribed to the Google Groups "minikanren" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/minikanren. For more options, visit https://groups.google.com/d/optout.
