When we want to include a complicated constraint with and in the CHC body, e.g., ($x (and (= r1 x1) (= r2 x2))), it will raise an error saying “only one first-order logic constraint is allowed.”
The current workaround is to use (not (not (and (= r1 x1) (= r2 x2)))) or (and (and (= r1 x1) (= r2 x2))).
When we want to include a complicated constraint with
andin the CHC body, e.g.,($x (and (= r1 x1) (= r2 x2))), it will raise an error saying “only one first-order logic constraint is allowed.”The current workaround is to use
(not (not (and (= r1 x1) (= r2 x2))))or(and (and (= r1 x1) (= r2 x2))).