search

ufmg-smite / carcara

Apache License 2.0
31 stars 11 forks source link

Handling of unary conjuncts/disjuncts #27

Closed rodrigo7491 closed 10 months ago

rodrigo7491 commented 10 months ago

In https://github.com/ufmg-smite/carcara/commit/c537c7525f51a1c234216d70697e8ccecbbde256 and, or, and xor were restricted to accurately follow SMT-LIB. Despite not being in the standard, many SMT benchmarks are currently written using unary conjuncts/disjuncts. Would it be possible to relax this input restriction, maybe under a special flag?

rodrigo7491 commented 10 months ago

See https://github.com/ufmg-smite/carcara/discussions/28. @blisko is also interested in this :)

HanielB commented 10 months ago

I think this is sensible. I think the best is to have a --strict flag or something like that that rejects non-SMT-LIB compliant terms, and that is on by default, but that can be disabled by the user. What do you think, @bpandreotti?

bpandreotti commented 10 months ago

Sounds good to me. Since we already have a --strict flag, I think we can also use it for that.

bpandreotti commented 10 months ago

Fixed by 71c1edc1cf990172d139519b5b9f16349b3471b7.