3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-31 23:34:55 +00:00

replace_re axiom placeholder

@ahelwer - illustrates placeholder for one approach for axiomatizing replace_re
This commit is contained in:
Nikolaj Bjorner 2021-12-08 03:40:24 -08:00
parent 773a2ae7bc
commit a5bd115235
2 changed files with 25 additions and 0 deletions

View file

@ -106,6 +106,7 @@ namespace seq {
void unit_axiom(expr* n);
void length_axiom(expr* n);
void unroll_not_contains(expr* e);
void replace_re_axiom(expr* e);
expr_ref length_limit(expr* s, unsigned k);
expr_ref is_digit(expr* ch);