mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

align format of quantifier instantiation with new core

Browse source 
So far the format is

(forall ((x Int)) body) (not (body[t/x]))

The alternative could be the clause

(not (forall ((x Int)) body)) body[t/x]

they just better be consistent between engines
This commit is contained in:
Nikolaj Bjorner 2022-10-21 15:26:00 -07:00
parent 53adc2afee
commit 7eee7914bd
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/qi_queue.cpp
View file

@ -311,8 +311,8 @@ namespace smt {
expr* gens[1] = { gen.get() };
for (unsigned i = 0; i < num_bindings; ++i)
bindings_e.push_back(bindings[i]->get_expr());
args.push_back(m.mk_not(q));
args.push_back(instance);
args.push_back(q);
args.push_back(mk_not(m, instance));
args.push_back(m.mk_app(symbol("bind"), num_bindings, bindings_e.data(), m.mk_proof_sort()));
args.push_back(m.mk_app(symbol("gen"), 1, gens, m.mk_proof_sort()));
pr1 = m.mk_app(symbol("inst"), args.size(), args.data(), m.mk_proof_sort());