Various updates in preparation for Z3 version update#585
Conversation
alexanderjsummers
left a comment
alexanderjsummers
left a comment
There was a problem hiding this comment.
Most of my comments are out-of-interest; the minor fix to the one axiom seems worth doing now
| |// AS: added "reverse triggering" versions of the axioms | ||
| |axiom (forall<T> s0: Seq T, s1: Seq T, m: int :: { Seq#Index(s1, m), Seq#Append(s0,s1)} // m == n-|s0|, n == m + |s0| | ||
| | s0 != Seq#Empty() && s1 != Seq#Empty() && 0 <= m && m < Seq#Length(s1) ==> Seq#Sub(Seq#Add(m,Seq#Length(s0)),Seq#Length(s0)) == m && Seq#Index(Seq#Append(s0,s1), Seq#Add(m,Seq#Length(s0))) == Seq#Index(s1, m)); | ||
| | s0 != Seq#Empty() && s1 != Seq#Empty() && 0 <= m && m < Seq#Length(s1) && s1 != Seq#Append(s0,s1) ==> Seq#Sub(Seq#Add(m,Seq#Length(s0)),Seq#Length(s0)) == m && Seq#Index(Seq#Append(s0,s1), Seq#Add(m,Seq#Length(s0))) == Seq#Index(s1, m)); |
There was a problem hiding this comment.
Let's move this to before the inequalities (two conjuncts earlier); I think (heuristically) it can be useful to put the first-to-be-ruled-out cases first.
Also, although I don't think it's relevant for what this axiom does directly, adding s0 != Seq#Append(s0,s1) && before it should be fine and I think it might be easier to get this consistent if we follow this pattern everywhere: rule out the cases where the operator doesn't actually create new sequences, and only add the index terms under these conditions. I didn't think about it that way when making the previous changes, but I think this fits well how to make this more methodical.
| "/proverOpt:O:NNF.SK_HACK=true", | ||
| "/proverOpt:O:smt.MBQI=false", | ||
| "/proverOpt:O:smt.QI.EAGER_THRESHOLD=100", | ||
| "/proverOpt:O:smt.BV.REFLECT=true", |
There was a problem hiding this comment.
Does this option no longer exist? It seems like one that could have quite significant effects on performance but only for problems using bitvectors + quantifiers
| "/proverOpt:O:smt.ARITH.RANDOM_INITIAL_VALUE=true", | ||
| "/proverOpt:O:smt.CASE_SPLIT=3", | ||
| "/proverOpt:O:smt.DELAY_UNITS=true", | ||
| "/proverOpt:O:NNF.SK_HACK=true", |
There was a problem hiding this comment.
I assume this option has gone? Not sure what it did, to be honest
| "/proverOpt:O:smt.PHASE_SELECTION=0", | ||
| "/proverOpt:O:smt.RESTART_STRATEGY=0", | ||
| "/proverOpt:O:smt.RESTART_FACTOR=|1.5|", | ||
| "/proverOpt:O:smt.ARITH.RANDOM_INITIAL_VALUE=true", |
There was a problem hiding this comment.
looking at the docs, I'm surprised we had this one - seems good to get rid of anyway
| "/errorTrace:0", | ||
| "/errorLimit:10000000", | ||
| "/proverOpt:O:smt.AUTO_CONFIG=false", | ||
| "/proverOpt:O:smt.PHASE_SELECTION=0", |
There was a problem hiding this comment.
What's the rationale for removing these three? It might be a good thing to do, but presumably has some chance of non-trivial performance impact (maybe in either direction?)
2 participants
We might want to update our used Z3 version from 4.8.7 to 4.16.0 soon. This version leads to some issues with the current version of Carbon, which I'm trying to address in this PR:
if (*) { ... assume false }block, to prevent them from being triggered in subsequent assertions.P(x1, y1) == P(x2, y2) ==> x1 == x2 && y1 == y2to one that uses getter functions for each parameter and therefore should not be multiplicative in the same way