Reexamine patching back DEs not mentioned in theory

[ryandancy]

In #140, setting model.user_functions=false causes Z3 not to regurgitate user-specified definitions. However, it then does not generate definitions for DEs which are not mentioned in the theory. So, we have to manually patch them back (see the hack in the above PR).

The most common (only?) place where DEs might exist but not be mentioned in the theory on the Portus level is when translating one sigs which are the only sig in their sort (with the non-datatype compilers). They're translated to a single DE in their own sort, and then the constants axiom and the other axioms are optimized out and they end up not being mentioned in the theory at all aside from a declare-const directive. This occurs e.g. with ertms_1A.als in the expert models.

The current fix is in core/src/main/scala/fortress/solvers/SMTLIBCliSolver.scala, but may not be the best way to fix this issue. Reevaluate this.