Support and testing for equality-atom and if-then-else based RDDL-style boolean interoperability

[mejrpete]

Note that this PR is submitted as a draft, since the true PR should probably be opened against a separate feature branch, rather than devel.

Boolean interop for RDDL requires the ability to move from Term -> Formula and from Formula -> Term within the AST built in Tarski as discussed in #91. In general, we need the ability to construct nested formulae which include both logical operations on expressions with atoms based on the numerically-derived Boolean sort, and direct mathematical operations on these items.

To accomplish this in practice, two patterns can be used.

1) Term -> Formula:

Given a Term with sort Boolean, we can use the typical equality predicate and a constant True/1 value to wrap to a Formula (for a language which has both the Boolean and Equality theories attached)

a = lang.function('a', lang.Boolean)
b = lang.function('b', lang.Boolean)
bool_t = lang.constant(1, lang.Boolean)
logical_formula = (a == bool_t) | (b == bool_t)

2) Formula -> Term:

Given a Formula, we can wrap out to a Term with sort Boolean using the IfThenElse term, and corresponding boolean constants.

a = lang.function('a', lang.Boolean)
b = lang.function('b', lang.Boolean)
bool_t = lang.constant(1, lang.Boolean)
logical_formula = (a == bool_t) | (b == bool_t)
math_included = ite(logical_formula, bool_t, lang.constant(0, lang.Boolean)) + 1 

With these two patterns, we can arbitrarily move back and forth between Formula and Term objects depending on the operations needed when building the AST in Tarski. Additionally, because these patterns are easily identifiable with simple pattern matching, when performing write-side IO for an RDDL domain which includes these wrappers within the Tarski representation, we can remove the wrappers accordingly, and generate legal RDDL which does not include the additional representational overhead involved with the wrapper patterns discussed above.

The Tarski modeling approach for RDDL using these patterns involves representing Boolean RDDL values as Boolean (sort) codomain functions, with equality-based atoms as the basic logical type (e.g. (a == lang.constant(1, lang.Boolean)). This is in contrast to the approach explored in the rddl-support branch (#96), which assumed the use of Predicate for representation of Boolean RDDL values. One additional advantage of this change is that while the closed-world assumption prohibits the declaration of false-valued non-fluents and initial-state state-fluents (necessary in RDDL, since Boolean valued fluents can be declared with default values of true) in an implementation based on Predicate representations for these fluents (as in #96), the use of Boolean codomain functions in this alternate approach trivially avoids this issue.

Included changes/additions:

1. Incorporating a Boolean sort descended from Natural when the Boolean theory is attached to a FirstOrderLanguage
2. Addition of Bernoulli as a builtin for the Random theory
3. Implementation additions in RDDL write IO in order to "unwrap" the two major patterns used to translate back and forth between Formula and Term items when using the Boolean sort as described.
4. Minor changes to write true and false literals rather than 0/1 when writing RDDL from our representation (needed as far as I know for appropriate behavior with both the PROST and rddlsim RDDL parsers)
5. Test additions & modifications to test RDDL write-side IO support, along with tests for the Boolean theory changes

Omissions/Necessary future discussion

1. Current tests are focused on write-side RDDL IO. Neither the read-side tests, nor the read-side RDDL IO code has been modified to automatically wrap back and forth using the two patterns above.
2. From a user perspective (when using Tarski as a tool to directly construct the AST and domain/instance models for RDDL-specified problems) requiring the explicit use of these wrappers puts significant onus on the user to understand the distinction between Formula and Term within Tarski in order to appropriately use these wrappers and correctly construct their domain/instance. While this is potentially workable, it would be preferable from the user's perspective to have some level of "automatic" injection of wrappers in instances where there is a mismatch between input to an operator and the expected object type (e.g. when dispatching a lor called from a Formula where the argument is a Term with sort Boolean). This would involve building recovery logic with knowledge of the Boolean sort into Tarski's operator dispatching implementation, which may or may not be acceptable from a design standpoint. This may be a worthwhile point of discussion!