mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

fixed potential performance problem with fully interpreted sorts in the quantifier instantiation.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2013-09-27 16:55:05 +01:00
parent daaab05923
commit 3d910028bf
1 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/smt/smt_model_finder.cpp
View file

@ -975,9 +975,11 @@ namespace smt {
// Moreover, a model assigns an arbitrary intepretation to these sorts using "model_values" a model value.
// If these module values "leak" inside the logical context, they may affect satisfiability.
//
// n->insert(m_model->get_some_value(n->get_sort()), 0);
// TODO: we can use get_some_value if the sort n->get_sort() does not depend on any uninterpreted sorts.
n->insert(m_manager.mk_fresh_const("elem", n->get_sort()), 0);
sort * ns = n->get_sort();
if (m_manager.is_fully_interp(ns))
n->insert(m_model->get_some_value(ns), 0);
else
n->insert(m_manager.mk_fresh_const("elem", ns), 0);
}
}
}