Conversation
… tests to see how it works
… to terms with loose DB indices
| // MY_GEN_RULE, MY_GEN_TESTER, LIST_ALPHA_SUGAR, | ||
| // Generation::SymmetricTest() | ||
| // .options(options("all")) | ||
| // .inputs({ clause({ cons(a, nil()) != cons(x, nil()), |
There was a problem hiding this comment.
@joe-hauns do you have some idea how to fix this test? The reason I commented this is due to x having two different sorts in the input clause, violating the new variable sort consistency check I added.
| fte++; | ||
| ASS_EQ(fte->_tag(), FlatTerm::FUN_TERM_PTR); | ||
| ASS(fte->_term()); | ||
| if constexpr (higherOrder) { |
There was a problem hiding this comment.
This is the important bit, where we do something differently for HOL.
| } else { | ||
| doAssignVar(); | ||
| } | ||
| shouldBacktrack=!doAssignVar(); |
There was a problem hiding this comment.
We might backtrack here now, but this never happens with higherOrder==false and hopefully gets optimized away.
| (*this)[i] = lits[i]; | ||
| } | ||
|
|
||
| #if VDEBUG |
There was a problem hiding this comment.
This is the variable sort consistency check I mentioned in the summary. I think it's worth having it, as we get an error much earlier, avoiding well-sortedness errors later seemingly coming out of nowhere.
There was a problem hiding this comment.
Debug builds have always been glacial (and only got worse recently when I turned on all the sanitisers), so I think this is sensible.
There was a problem hiding this comment.
We could have it as a "turn on when you get weird typing errors" but then nobody would find it, so I guess this is as good as it gets. (Sidenote: I wonder how much performance impact the well-sortedness check has. Probably not much as it is only performed for to-be-shared terms.)
MichaelRawson
left a comment
MichaelRawson
left a comment
There was a problem hiding this comment.
Cool! Nice sensible change, much better than I thought it would be.
General thought: we could at some point run experiments to see if the template for HOL is worth the template parameter or whether treating everything as maybe-HOLy is OK.
except I commented function definition introduction, as that still causes a lot of trouble
Ugh. Do you have a nice short crash for me? I could look into why/how this happens.
| op=entry; | ||
| Base::ft=ft_; | ||
| Base::tp=0; | ||
| Base::op=Base::entry; |
There was a problem hiding this comment.
No objection, but why do we need to have this Base thing now? Is the compiler not smart enough to figure it out inside a templated class or something?
There was a problem hiding this comment.
Because of the usual C++ crap. I could also use this-> everywhere, but I decided to add some often used names as using and use Base:: for the rest.
There was a problem hiding this comment.
Thanks for the explanation, I learned something. 😷
| (*this)[i] = lits[i]; | ||
| } | ||
|
|
||
| #if VDEBUG |
There was a problem hiding this comment.
Debug builds have always been glacial (and only got worse recently when I turned on all the sanitisers), so I think this is sensible.
I agree about this, my plan is to add some more sensible HO matching, where the templating matters, so that hopefully this gets justified in the future. |
I will look at this again soon, I just didn't want to spagettify this PR too much. I think it might be as simple as changing |
2 participants
Adapting code trees and structures that use them to HOL matching. The is mostly just shoving a compile-time flag into all of these structures and then disallowing:
Some minor improvements:
FOL regression showed no difference, and a couple of rounds of debug sampling only showed problems with other, not yet touched inferences. HOL regression showed that a few dozens crashes are now avoided and we get the following figures:
Discount:
Otter: