search

Barnard-PL-Labs / tsltools

Library and tools for the TSL specification format
Other
7 stars 4 forks source link

TSL-MT and/or SyGuS doesnt support EUF #64

Open santolucito opened 11 months ago

santolucito commented 11 months ago

test/regression/ModuloTheories/euf.tslmt doesn't generate any assumptions.

When I log the smt queries that are made (will push this logging feature soon), and try to run directly with cvc5 i get

(error "Parse Error: tmp/tmp_10.smt2:1.12: Illegal argument detected
void cvc5::internal::LogicInfo::setLogicString(std::string)

  `logicString' is a bad argument
LogicInfo::setLogicString(): cannot parse logic string: EUF")

At least need to be throwing a warning to this effect in the toolchain, ideally we can actually fix it too lol

santolucito commented 10 months ago

its not clear to me that EUF in fact is or ever was a thing in CVC5. https://smtlib.cs.uiowa.edu/logics.shtml

I think we just can use UF, or even better QF_UF