Dynamic prelude

[PetarMax]

I've had an idea:

💥 The prelude should not be fixed. It should be reset dynamically, removing all uninterpreted function symbols (and associated SMT lemmas) that are not in the ground truth plus the predicates to be checked. 💥

What do we lose? Forall-quantified statements that we know are difficult for the solver to handle.
What do we gain? SATs and UNSATs instead of unknowns.

Why am I thinking of this - because I am running some new (potental engagement) tests and I am getting a real Unknown from Z3, and the constraints contain modInt because that is what the code uses. When the smt-lemma

rule chop ( I:Int ) => I modInt pow256 [concrete, smt-lemma]

is present, Z3 really returns Unknown, no matter how large I set the timeout, when it’s removed I get an instant SAT/UNSAT.

This means that that modInt in the SMT lemma is 🪄 soMehOw 🪄 interacting with the solver, it’s trying to define chop as a function and failing, but chop is not relevant to this query and there is no need for it to be there.

[goodlyrottenapple]

Would you be able to provide a bug report as a starting point for addressing this issue?

[PetarMax]

Actually, I think we can put this on hold for now. I have a way of handling it by replacing the smt-lemma with simplifications.

[jberthold]

Precompute several relations from the definition's SMT components

• function_uses_sort :: Functions x Sorts
  • directly from the argument and result sorts of the function
• lemma_uses_sort :: Lemmas x Sorts
  • sorts of the (all-quantified) variables
• lemma_uses_function :: Lemmas x Functions
  • occurrences within the lemma body expressions
    We should retain this SMT-related structure together with the definition (maybe by caching it in the Definitiontype itself) but we can recompute it for first experiments.

Iterative algorithm to select lemmas, functions, and sorts to declare:

For checkPredicates, the input is the definition, a ground truth (path condition) and a predicate.
A. filter ground truth to only include things that the predicate mentions

• variables in the predicate, and transitive closure over the mentioned variables
• this code is already there on Sam's branch
  B. Select sorts and functions to declare, and lemmas to assert

  1. start with sorts and functions from predicate and ground truth

     • used_sorts \subset Sorts, used_functions \subset Functions
     • Omitting all pre-declared things, int+bool and functions on them
     • and lemmas empty

  2. extend lemmas by considering used_sorts and used_functions

     • [ l | f <- used_functions, (l, f) <- lemma_uses_function ] <> [ l | s <- used_sorts, (l, s) <- lemma_uses_sort ]

  3. extend used_functions by [ f | l <- lemmas, (l, f) <- lemma_uses_function ]
     extend used_sorts by [s | l <- lemmas, (l, s) >- lemma_uses_sort ]

The last step should not require any loop back to 2. 🤞

Related booster code is in Booster.SMT.Translate

[jberthold]

As a first (and probably sufficient?) step, the SMT lemmas in the definition according to which functions are actually used by the predicates in question.
This requires computing a relation FunctionSymbol x SMTLemma, which will be turned into a lookup table FunctionSymbol -> Set SMTLemma to select the lemmas. Furthermore, the lemmas part of the prelude needs to be recomputed for each request, the SMT solver setup and interface will have to change to accommodate it.