Implement standard-compliant handling of inequality operators with more than 2 arguments

usi-verification-and-security / opensmt

The opensmt solver

Other

78 stars 18 forks source link

Implement standard-compliant handling of inequality operators with more than 2 arguments #146

Open blishko opened 4 years ago

blishko commented 4 years ago

Follow up on issue #137 and PR #138 The proper handling of multiple arguments should be extended from equality also to inequality operators according to the SMT-LIB definitions of theories of Reals and Integers.

aehyvari commented 4 years ago

This affects also xor. In smtlib2 standard xor is marked as left-assoc, meaning that the term (xor a b c) should be interpreted as (xor (xor a b) c).

blishko commented 3 years ago

The same applies to / and div.