Support for syntactic simplifications
Nessuno ha ancora preso questa issue.
Valutazione
- Difficoltà
- 5/5
- Tempo stimato
- Più di una settimana
- Idoneità per principianti
- 35/100
- Tipo di issue
- Funzionalità
- Chiarezza
- Abbastanza chiara
- Stato di attività
- Ferma
- Ambito
- backend
Direzione di ricerca
Start by tracing how the backend parses and applies simplifications, then inspect the frontend handling for modules marked [symbolic]. Determine how a syntactic list of positive clause indices should affect requires checking, including variables first introduced in syntactic clauses. Done means both examples are accepted and the selected clauses are checked only syntactically without changing other simplifications.
Scritto dal modello di indicizzazione a partire dal testo della issue.
Descrizione
To improve the simplification mechanism of the backend, we require the addition of a syntactic attribute in simplifications, which takes a list of positive integers. These integers would then indicate to the backend that the corresponding clauses in the requires should be checked only syntactically. Two examples of this would be:
rule X <=Int Y => X <Int Y
requires notBool (X ==Int Y)
[simplification, syntactic(1)]
and
rule X <=Int Y => true
requires X <=Int Z
andBool Z <=Int Y
[simplification, concrete(Y, Z), syntactic(1)]
Note that, in the second example, there is a symbolic variable Z introduced in the first clause that is not present in the LHS. This appears to be supported by the front-end if the corresponding module is marked as [symbolic]. Optionally, we would like such variables to be supported also if the clause in they first appear is marked as syntactic.
- Lingua principale
- Python
- Stelle
- 591
- Fork
- 163
- Metriche di merge delle PR
- Nessuna PR unita negli ultimi 30g
Preparare l'ambiente
Come iniziare
- Leggi tutta la issue e poi la guida ai contributi del progetto.
- Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
- Fai un fork del repository e lavora su un branch.
- Apri una pull request che faccia riferimento al numero della issue.
Altre issue di runtimeverification/k
-
Introduce composable symbolic execution interface in pyxForse di nuovo libera @Stevengre l’ha presa 99 giorni fa e non c’è nessuna pull request aperta. Aperta
runtimeverification/k#4939 · 1 assegnatario ·
-
Concolic ExplorerAperta
Difficoltà 5/5 Più di una settimana Idoneità per principianti 32/100
runtimeverification/k#4937 ·
-
Difficoltà 5/5 Più di una settimana Idoneità per principianti 30/100
runtimeverification/k#4936 ·
-
Accelerating all-path reachability proofs with one-path reachability proofsForse di nuovo libera @Stevengre l’ha presa 104 giorni fa e non c’è nessuna pull request aperta. Apertatype:epic
runtimeverification/k#4934 · 4 commenti · 1 assegnatario ·
-
Support progressive depth halving as a generic policy in `Prover.advance_proof`Forse di nuovo libera @Stevengre l’ha presa 124 giorni fa e non c’è nessuna pull request aperta. Aperta
runtimeverification/k#4924 · 1 assegnatario ·
Tutte le issue di runtimeverification/k
Issue simili
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 78/100
I maintainer di solito rispondono entro 1 giorno
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 85/100
kornia/kornia#5263 · 1 commento ·
I maintainer di solito rispondono entro 1 giorno
-
approved correction metadata
Difficoltà 1/5 Meno di un'ora Idoneità per principianti 88/100
acl-org/acl-anthology#10133 · 1 commento ·
I maintainer di solito rispondono entro 1 giorno
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 78/100
BasedHardware/omi#20084 ·
I maintainer di solito rispondono entro 1 giorno
-
bug needs-acceptance wg/evaluation-quality
Difficoltà 2/5 1-3 ore Idoneità per principianti 76/100
vllm-project/semantic-router#4424 ·
I maintainer di solito rispondono entro 1 giorno