Invariant synthesis #100
Invariant synthesis #100
Conversation
Philipp15b
left a comment
Philipp15b
left a comment
There was a problem hiding this comment.
I left some comments. Most importantly, I think rather than adding _filtered versions to evals, the easier way is to just filter what you eval at the call site.
src/driver/smt_proof.rs
Outdated
| } | ||
|
|
||
| /// Get a model for the constraints if it exists and instantiate vc_tvars_pvars with it | ||
| pub fn update_vc_with_model<'smt, 'ctx, 'tcx: 'ctx>( |
There was a problem hiding this comment.
I recommend you split this fn into different concerns: 1. doing the query and getting the (filtered) model, 2. doing the substitution, 3. creating the new vc quant prove task.
|
|
||
| pub struct Qelim<'tcx> { | ||
| tcx: &'tcx mut TyCtx, | ||
| tcx: &'tcx TyCtx, |
There was a problem hiding this comment.
Ideally this would stay mutable since qelim could, in the future, need the TyCtx to create new fresh variables.
src/smt/partial_eval.rs
Outdated
| /// Rather than substituting recursively, wrap the VC in nested `Subst` expressions, | ||
| /// one for each variable that has a concrete model value. | ||
| pub fn instantiate_through_subst<'ctx>( |
There was a problem hiding this comment.
I would split this for different concerns again: 1. extracting the substitutions (e.g. in the form of a HashMap) from the model, 2. converting a Symbolic back into an Expr, and 3. creating the new vc expression with substitutions applied.
src/smt/symbolic.rs
Outdated
| Symbolic::Uninterpreted(_) => Err(SmtEvalError::ParseError), // TODO | ||
| } | ||
| } | ||
| pub fn eval_filtered(&self, model: &FilteredModel<'ctx>) -> Result<Box<dyn Display>, SmtEvalError> { |
There was a problem hiding this comment.
I don't think this function does what it suggests. To me, it suggests partially evaluating self based on the FilteredModel.
But instead, it only does that properly for variables, not full expressions. For expressions like x + y, this would still evaluate the full thing even if x and y were filtered out, no?
Instead, why not just filter the list of variables at the call site (currently instantiate_through_subst) and then use the normal eval`?
maditaP
force-pushed
the
invariant-synthesis
branch
from
341816e to
7348de7
Compare
2 participants
The inner loop of an invariant synthesis