ValueError: Token('LP', '(')

[pauljurczak]

I'm trying a simple example with PyGuS and Python 3.11.4. This script:

from interpret.smt_interpreter import interpret_smt

syg = '''(
(define-fun f ((color Int) (sortAsc Int) (sortDesc Int)) Int (ite (<= 1 sortAsc) (ite (<= 1 sortDesc) 0 2) 3))
)'''

print(interpret_smt(syg))

produces this error:

  File "/home/paul/cvc5/PyGuS/main.py", line 7, in <module>
    print(interpret_smt(syg))
          ^^^^^^^^^^^^^^^^^^
  File "/home/paul/cvc5/PyGuS/interpret/smt_interpreter.py", line 12, in interpret_smt
    python_prog = parser.parse(tokens).eval()
                  ^^^^^^^^^^^^^^^^^^^^
  File "/home/paul/cvc5/PyGuS/.venv/lib/python3.11/site-packages/rply/parser.py", line 60, in parse
    self.error_handler(lookahead)
  File "/home/paul/cvc5/PyGuS/interpret/smt_parser.py", line 65, in error_handle
    raise ValueError(tks)
ValueError: Token('LP', '(')

The SyGuS string I'm using was produced by CLI version of cvc5.

[pauljurczak]

I also tried syg = '(lambda ((x Int) (y Int)) (+ x y))' produced by Base Python API of cvc5 and got this error:

ValueError: Token('VAR', 'lambda')

[yiming-fang]

Hi Paul,

For your first example, it should work if you remove the outermost parens. The lambda keyword is not supported, and all functions need to be in the format of define-fun.

[pauljurczak]

Thank you for prompt response. I tried:

from interpret.smt_interpreter import interpret_smt

syg = '(define-fun f ((color Int) (sortAsc Int) (sortDesc Int)) Int (ite (<= 1 sortAsc) (ite (<= 1 sortDesc) 0 2) 3))'
print(interpret_smt(syg))

and got:

Traceback (most recent call last):
  File "/home/paul/cvc5/PyGuS/main.py", line 4, in <module>
    print(interpret_smt(syg))
          ^^^^^^^^^^^^^^^^^^
  File "/home/paul/cvc5/PyGuS/interpret/smt_interpreter.py", line 12, in interpret_smt
    python_prog = parser.parse(tokens).eval()
                  ^^^^^^^^^^^^^^^^^^^^
  File "/home/paul/cvc5/PyGuS/.venv/lib/python3.11/site-packages/rply/parser.py", line 32, in parse
    lookahead = next(tokenizer)
                ^^^^^^^^^^^^^^^
  File "/home/paul/cvc5/PyGuS/.venv/lib/python3.11/site-packages/rply/lexer.py", line 62, in __next__
    return self.next()
           ^^^^^^^^^^^
  File "/home/paul/cvc5/PyGuS/.venv/lib/python3.11/site-packages/rply/lexer.py", line 58, in next
    raise LexingError(None, SourcePosition(
rply.errors.LexingError: (None, SourcePosition(idx=32, lineno=1, colno=29))