mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
3f2f3138c0
That is, duplicate lemmas making use of an algebraic type (either by using a projection, a constructor or a pattern matching) which is tagged by the new meta alginst.
Also:
- Add new select metas for automatically tagging types with alginst
- edit relevent drivers so that discrimination happens before eliminate_algebraic:
- CVC5
- Z3 > 4.8.7
- Vampire 4.5.1
- why3-smt
92 lines
1.3 KiB
Plaintext
92 lines
1.3 KiB
Plaintext
theory Kept_partial
|
|
meta "enco_kept" "instantiate"
|
|
end
|
|
|
|
theory Kept_twin
|
|
meta "enco_kept" "twin"
|
|
end
|
|
|
|
theory Partial_incomplete
|
|
meta "enco_kept" "instantiate"
|
|
meta "encoding_instantiate:complete" "no"
|
|
end
|
|
|
|
theory Poly_explicit
|
|
meta "enco_poly" "explicit"
|
|
end
|
|
|
|
theory Poly_guard
|
|
meta "enco_poly" "guard"
|
|
end
|
|
|
|
theory Poly_deco
|
|
meta "enco_poly" "decorate"
|
|
end
|
|
|
|
theory Inst_none
|
|
meta "select_inst" "none"
|
|
end
|
|
|
|
theory Inst_goal
|
|
meta "select_inst" "goal"
|
|
end
|
|
|
|
theory Inst_all
|
|
meta "select_inst" "all"
|
|
end
|
|
|
|
theory Lskept_none
|
|
meta "select_lskept" "none"
|
|
end
|
|
|
|
theory Lskept_goal
|
|
meta "select_lskept" "goal"
|
|
end
|
|
|
|
theory Lskept_all
|
|
meta "select_lskept" "all"
|
|
end
|
|
|
|
theory Lsinst_none
|
|
meta "select_lsinst" "none"
|
|
end
|
|
|
|
theory Lsinst_goal
|
|
meta "select_lsinst" "goal"
|
|
end
|
|
|
|
theory Lsinst_all
|
|
meta "select_lsinst" "all"
|
|
end
|
|
|
|
theory Kept_none
|
|
meta "select_kept" "none"
|
|
end
|
|
|
|
theory Kept_goal
|
|
meta "select_kept" "goal"
|
|
end
|
|
|
|
theory Kept_all
|
|
meta "select_kept" "all"
|
|
end
|
|
|
|
theory Alginst_none
|
|
meta "select_alginst" "none"
|
|
end
|
|
|
|
theory Alginst_goal
|
|
meta "select_alginst" "goal"
|
|
end
|
|
|
|
theory Alginst_all
|
|
meta "select_alginst" "all"
|
|
end
|
|
|
|
theory KeptIntReal
|
|
use int.Int
|
|
use real.Real
|
|
meta "encoding:kept" type Int.int
|
|
meta "encoding:kept" type Real.real
|
|
end
|