Cannot parse CHCs containing certain conjunctions

[WileyCorning]

The following trivial example:

(declare-term-types  ((E 0)) ((($a))))
(define-funs-rec
    ((E.Sem ((et E) (x Int) (y Int) (r Int)) Bool))
    ((! (match et (
            ($a (and (> 0 x) (= r 0)))
    )) :input (x y) :output (r))
    )
)
(synth-fun f() E)
(constraint (E.Sem f 1 2 0))
(check-synth)

throws this error during parsing:

test.sl:7:22: error: while processing `define-funs-rec`: processing definition for E.Sem: processing CHC for E.Sem: in match $a: Multiple constraints in CHC for $a in E.Sem. Only one first-order logic constraint is allowed.
Error reported here:
            ($a (and (> 0 x) (= r 0)))
---------------------^

It appears that the parser expects a certain child-term configuration to be present if the CHC contains an and.

---

Also, oddly, this file parses:

(declare-term-types  ((E 0)) ((($0)($a ($aa E)))))
(define-funs-rec
    ((E.Sem ((et E) (x Int) (y Int) (r Int)) Bool))
    ((! (match et (
            ($0 (= r 0))
            ;(($a t1) (exists ((mu Int)) (and (E.Sem t1 0 0 mu) (= r mu))))
            (($a t1) (exists ((mu Int)) (and (E.Sem t1 x y mu) (= r mu))))
    )) :input (x y) :output (r))
    )
)
(synth-fun f() E)
(constraint (E.Sem f 1 2 0))
(check-synth)

but this one doesn't, throwing the same error as above:

(declare-term-types  ((E 0)) ((($0)($a ($aa E)))))
(define-funs-rec
    ((E.Sem ((et E) (x Int) (y Int) (r Int)) Bool))
    ((! (match et (
            ($0 (= r 0))
            (($a t1) (exists ((mu Int)) (and (E.Sem t1 0 0 mu) (= r mu))))
            ;(($a t1) (exists ((mu Int)) (and (E.Sem t1 x y mu) (= r mu))))
    )) :input (x y) :output (r))
    )
)
(synth-fun f() E)
(constraint (E.Sem f 1 2 0))
(check-synth)

which suggests some difference in handling between child semantic relation queries with variable arguments vs. with literal / expression arguments.

[kjcjohnson]

I believe this has the same root cause as https://github.com/SemGuS-git/Semgus-Parser/issues/68.

The parser currently recognizes two forms: [1] <predicate> or [2] (and <sem-rel>... <predicate>).

For your first example, (and (> 0 x) (= r 0)), the parser is throwing an error because it looks like [2], but only one predicate is allowed in [2], but (> 0 x) and (= r 0) are present.

Workaround: specify all complex semantics like: (and <sem-rel>... (and <pred>...)), where there may be zero semantic relations. In your example, this would be: (and (and (> 0 x) (= r 0)))

Not sure about the second one. Is it really the same error message? That doesn't make sense to me.

[kjcjohnson]

Ah, here it is: https://github.com/SemGuS-git/Semgus-Parser/blob/6b47837cff2c7455ccbdc3e25241a6e6ad4916f3/ParserLibrary/Commands/FunctionDefinitionCommands.cs#L311

Only variables are allowed to be arguments to semantic relations currently. I think this was an initial convenience for implementation - not sure if there was a deeper reason, but it does need to be extended to literals (at least).

Workaround: introduce another variable for the constant:

(exists ((mu Int) (zero Int))
    (and (E.Sem t1 zero zero mu)
         (and (= zero 0)
              (= r mu))))