Remove Formula
#326
Remove Formula
#326
Conversation
Co-Authored-By: Sacha Ayoun <sachaayoun@gmail.com>
| | Eq (left_list, right_list) | ||
| when (match | ||
| ( Typing.type_lexpr gamma left_list, | ||
| Typing.type_lexpr gamma right_list ) | ||
| with | ||
| | (Some Type.ListType, _), (Some Type.ListType, _) -> true | ||
| | _ -> false) | ||
| && | ||
| match | ||
| fe | ||
| (Expr.Infix.( - ) | ||
| (Expr.list_length left_list) | ||
| (Expr.list_length right_list)) | ||
| with | ||
| | Expr.Lit (Int k) when not (Z.equal k Z.zero) -> true | ||
| | _ -> false -> | ||
| (* If we have two lists but can reduce the equality of their lengths to false, | ||
| then we know the lists cannot be equal*) | ||
| False |
There was a problem hiding this comment.
Removed this, which seems to slightly improve perf without causing any observable difference.
| | NOp (LstCat, _), LVar y when rpfs && prefix_catch pfs re1 y -> | ||
| Eq (UnOp (LstLen, re1), UnOp (LstLen, re2)) |
There was a problem hiding this comment.
Removed this, as it incorrectly converted list equalities to list length equalities -- maybe because I removed the rpfs param? Either way it didn't seem to make that big of a difference 🤔
| else if | ||
| PFS.exists | ||
| (fun e -> | ||
| Formula.equal e (Eq (flel, fler)) | ||
| || Formula.equal e (Eq (fler, flel))) | ||
| pfs | ||
| then Lit (Bool true) | ||
| else if | ||
| PFS.mem pfs (Not (Eq (flel, fler))) | ||
| || PFS.mem pfs (Not (Eq (fler, flel))) | ||
| then Lit (Bool false) |
There was a problem hiding this comment.
I had to remove these, as attempting to reduce a = x would always reduce to true, since that formula is already in the PFS. Maybe this reduction made sense when Expr/Formula were split? Note that a similar reduction for And/Or/Impl will still work -- this is the only case where it doesn't.
|
Some more work could be done but -- tests pass after removing |
Gillian-C/lib/MonadicSVal.ml
Outdated
| forall [ (i, Some IntType) ] zero <= i_e | ||
| && i_e < size ==> (Expr.list_nth_e arr_exp i_e == Lit Undefined) |
There was a problem hiding this comment.
(Hi, I wrote the ocamlformat formatting change for the hash operators that's probably the reason for this PR. I was just curious to see what you were doing in response).
I believe this change alters the formula, because the precedence in the initial source code is confusing. When I renamed these operators, it resulted in this instead (the link doesn't seem to navigate to the proper file for some reason? but you can search for forall). (forall i. zero) <= i && .. vs forall i, (zero <= i && ..) IIUC. I made that diff by parsing the source file with ocamlformat, modifying the ast, and printing the ast back.
Anyway, just a random remark to say it seems it'd reduce the risk of regression to incorporate my linked commit or something similar, before your further refactoring.
There was a problem hiding this comment.
Hi!
Thanks for checking it out :) Yes indeed I didn't notice, these expressions were wrong, thank you for pointing it out, just fixed it in 8111475. It was because the precedence of #.. operators is higher than that of function application so when updating the syntax I missed it. (Un)luckily these bits of code were never run so I didn't notice :p
Yeah the change is partly due by the ocamlformat change, though in general I think it makes more sense to define operators that have sensible precedence from the get go :)
|
Closed because of the PR removing |
(Not done, but opening as draft for now)
the changes include those from #316
Partial Changelog:
Remove
Formula.t, usingExpr.tanywhere it was used:The only difference at this point was a slightly different AST and the fact an
Expr.tis not always a boolean expression, but it's not actually that big of a deal it seems.The biggest downside I got so far is that it's slightly more verbose:
Eq (e1, e2)becomesBinOp (e1, Equals, e2),Not fbecomesUnOp (Not, e), etc.Add patterns from
reduce_formulaintoreduce_lexpr, cleaning up a bit, and removereduce_formulaThere are a few rules that I commented out, as they do not seem to stop the tests from passing and they caused errors after the merge -- I'll highlight these in the PR, to see if I'm correct in removing them.
BinOp: renameBAnd→And,BOr→Or,BImpl→Impl,SLessThan→StrLess,BSetMem→SetMem,BSetSub→SetSubUnOp: renameUNot→Not, addIsIntfrom FormulaRename all symbolic infix operators (
#==,#<,#&&...) to remove the hash, becoming==,<, etc. This deeply embeds theExproperators which I found nicer and also means the operators actually have different precedence! Because all operators starting with#have the same precedence which made using them annoying due to parenthesis.For GIL I didn't remove any of the existing syntax, but all
Formulanow compile asExpr, meaning that some operators have two equivalent symbols (eg.=and==,<#and<,/\and&&,--e--and-e-...)The only difference is that pure formulae must be enclosed in parenthesis, and all other assertions must not be in parenthesis, ie.
pred isTrue(+b: Boolean): b = true;must becomepred isTrue(+b: Boolean): (b = true);. This is to allow distinguishing the assertion*operator from the expression's multiplication. (In reality this change only affected a handful of definitions).Remove the types
vt,standaction_retfrom the signature of the typeSMemory, since their value was already set anyways (I think this doesn't change anything about the module type?) by usingtype _ := _instead.