Implements partial refactor to allow for Boolean & Numeric interop (via FormulaTerm wrapper)
#95
Conversation
…akes the Boolean types a core builtin
… to reflect API changes to FSTRIPS *Effect(s)
… domain lists in rddl instance
…y`" workaround This is a bit of an ugly workaround, but it will work for now. we have a special `Pass` type that is EXACTLY only ever used when we need to construct or check against an FSTRIPS effect that is not a conditional effect. Previously, the condition had been set as a default parameter to `Tautology` for any regular FSTRIPS effect. However, since *Effects are built outside of the context of a language, this did not work after we needed a language for Tautology and Contradiction (so that other Formula types could inherit them). There are a few more permanent approaches to this. We could either break the API and build Effects in the context of a language, or we could figure out another way to have a universal Tautology that somehow does not need to be in the context of a language. Notably this problem will STILL BE AN ISSUE if we go to a fully boolean-valued Function refactor (eliminating Predicates, etc), rather than the current partial refactor that involves wrappers between Formula and Term.
miquelramirez
added
contribution
|
Hi @mejrpete, cheers for the PR, mate. Miquel. |
…lean sort being attached to the language
Codecov Report
@@ Coverage Diff @@
## devel #95 +/- ##
==========================================
+ Coverage 98.30% 98.46% +0.15%
==========================================
Files 47 48 +1
Lines 3014 3257 +243
Branches 114 114
==========================================
+ Hits 2963 3207 +244
+ Misses 41 40 -1
Partials 10 10
Continue to review full report at Codecov.
|
|
Hi @mejrpete, thanks for the PR! Maybe you could give me write access to Cheers, BTW don't worry too much about the |
|
@gfrances Understood completely on time availability! I think I'm now generally familiar enough with the If it's ok with you, I think my having write access to the feature branch here is probably cleaner in terms of version history, etc (and would mean that the current project I'm working on with @emilkeyder-invitae could point to the feature branch on the If that's ok with you, I'll resubmit this PR (no longer as a draft) to the new branch, and then we can start working there. I'll close this PR in the meantime and should have the new one submitted before tomorrow! Thanks! |
|
Sure, let's go with that |
NOTE: this is submitted as a PR to
devel, but given the scope of the changes (and some of the existing hacks) it would probably be better for this to be submitted as a PR to a new feature branch dedicated to this refactor (which I think would have to be added to the upstream and then this PR would have to be re-submitted against that branch).As discussed in #91. This implementation is not the full SMT-like representation that we eventually want. Rather, I implemented a wrapper class
FormulaTermwhich allowsFormulaobjects to be wrapped asTermsin such a way that Boolean-valued Formula objects can be automatically cast as 0/1 numeric values for arithmetic, etc.The primary motivation for this refactor is to allow for the common patterns used in RDDL (which commonly includes numeric arithmetic over Boolean-valued state and action fluents).
This implementation
Arithmetictheory is included in a language (and a standalone child ofObjectotherwise)FormulaTermwrapper class, which is used as a container forFormulaobjects that must be treated asTermobjects for arithmetic, etc.Predicate,Formula,Term,Functionobjects are now associated with aFirstOrderLanguage(previously onlyFunctionandTermobjects had a language property). Languages are inherited up from "subterms", when, for example, aCompoundFormulais constructed. This is essential for being able to constructFormulaTermwrappers when needed, sinceTermobjects always need an associated language.While the
FormulaTermwrapper strategy for interop betweenTermandFormulaobjects falls short of the full SMT-like representation that we want, I think it is progress in the right direction. Additionally, this strategy, along with a few notable hacks that need to be addressed allowed me to almost entirely preserve the public tarski API (which also allowed for use of the existing test suite during the refactor without a ton of changes).The following are the key "hacks" that absolutely need to be addressed
ContradictionandTautologyobjects now require aFirstOrderLanguageas a parameter when they are constructed. This is due to the fact thatFormulaobjects withContradictionandTautologyobjects as subterms must be able to extract their ownFirstOrderLanguagefrom their subterms. This breaks the common direct use of Tautology and Contradiction where they are not associated with a language. From a mathematical perspective, it is a bit weird to forceTautologyandContradictionto be associated with a FOL, since there is no need formally. This is something that bears more discussion.Tautology, it was no longer possible to construct non-conditional FSTRIPS*Effectobjects withTautologyas their condition, as*Effectobjects are built outside the scope of a FOL. As a quick hack to make things work, I introduced aPassclass, which behaves exactly asTautologyis supposed to in this case, but without a language. This is a pretty terrible hack, but allowed me to work around the issue without making major API changes to FSTRIPS*Effectconstruction before this PR was filed.Booleantheory. It no longer does anything, since theBooleansort is always attached to a FOL, either as a child ofNaturalsorObjectdepending on whether or not there are numeric sorts attached to the language. This is more minor than the above two issues, but is included to motivate a discussion on which API components are flexible in the full SMT-like representation moving forward.Formula(and related) are no longer hashable, and must be treated the same way asTermobjects where you usesymreffor use in associative containers.These hacks were included specifically because I wanted to avoid arbitrarily changing the public API for
tarskiwithout discussion. The following are the API components that caused difficulty, and I believe (although I may be wrong) will require modification to avoid these kinds of hacks moving forward.*Effectconstruction outside the context of a FOL (while using something likeTautologyas a condition if they are not conditional effects)TautologyandContradictionobjects needing a FOL passed in at construction. (This is a change that was made, but is a little gross).Finally, I have also included tests that demonstrate appropriate interoperability between Predicate/Formula objects and Function/Term objects through the FormulaTerm wrapper class --- meaning that (as currently tested) numeric interpretation of Boolean-valued objects works as expected for all basic arithmetic, if then else, and sumterm operators. I've also added a large integration test in
tests/io/test_rddl_writer.pythat uses a significant chunk of the new functionality to generate one of the academic-advising RDDL domain instances used in IPPC-2018 (instance 1).This refactor is passing all tests that I was able to get working in my local configuration (which includes the base tests and all the benchmark tests). I have not been able to run tests associated with the
sddextra or which require thegringobinary for ASP reachability testing. Finally, I disabled one test related to shorthands forContradictionandTautologythat no longer makes sense in context of the changes to those classes.I fully admit that portions of this are really ugly! My hope is that we can discuss what is allowed to change in the API (or find better workarounds than I found) that will allow me to cut out the hacks that were used to make all of this work. Additionally, I still think that moving to a full SMT-like representation is strictly better than the
FormulaTermwrapper strategy used here (although I hope that this version could be used as the starting point for that refactor, since some of the changes --- including those made to theBooleansort, would need to be made regardless!)