java-smt
java-smt copied to clipboard
Define the difference between Plain Symbols and Nullary UFs.
All solvers allow to define nullary UFs, i.e., UFs without arguments. For some solvers, the returned formula can be used just like a plain symbol/variable and is even comparable, i.e. identical. For other solvers, a nullary UF is different from a plain symbol and appears to be a separate object.
We should document, which solvers allow this and provide more tests for this (see fb0de870f61047f92ce872d3718bce6c4673872f). Or we could return plain variables when requesting a nullary UF (or vice versa).