Maude-help mailing list

[<bzielinski AT uni.lodz.pl>]

Dear Sir or Madame

I am looking for some information concerning the use of cvc4 smt solver from
inside Maude interpreter. I understand that Maude interpreter is compiled with
cvc4 support by default, and one even has the file smt.maude in the standard
library of tools with some hooks to cvc4. Unfortunately I cannot find any
information on functions (or even hooks) in the manual, nor from other
sources. Even the file smt.maude seems to contain only hooks linking booleans,
ints, etc with similar types and operators in cvc4, but no functions like
"check-sat", "get-model" or something like that. Where can I find the relevant
information?

I am looking forward to your reply

Best regards

Bartosz Zielinski