mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 02:16:40 +00:00
Code Activity

add recfuns to model

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-10-27 13:26:32 -05:00
parent 51a0022450
commit 80acf8ed79
9 changed files with 45 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/rewriter/rewriter_def.h
View file

@ -212,6 +212,7 @@ bool rewriter_tpl<Config>::constant_fold(app * t, frame & fr) {
return false;
}
template<typename Config>
template<bool ProofGen>
void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
@ -338,15 +339,12 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
// TODO: add rewrite rules support
expr * def = nullptr;
proof * def_pr = nullptr;
quantifier * def_q = nullptr;
// When get_macro succeeds, then
// we know that:
// forall X. f(X) = def[X]
// and def_pr is a proof for this quantifier.
//
// Remark: def_q is only used for proof generation.
// It is the quantifier forall X. f(X) = def[X]
if (get_macro(f, def, def_q, def_pr)) {
if (get_macro(f, def, def_pr)) {
SASSERT(!f->is_associative() || !flat_assoc(f));
SASSERT(new_num_args == t->get_num_args());
SASSERT(m().get_sort(def) == m().get_sort(t));