mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

optimize generate_mutual_exclusion in theory_str to make only half as many subterms

Browse source
This commit is contained in:
Murphy Berzish 2016-12-06 12:59:40 -05:00
parent da61c99f9e
commit b57f04e2d2
1 changed files with 1 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/smt/theory_str.cpp
View file

@ -2449,13 +2449,8 @@ expr_ref theory_str::generate_mutual_exclusion(expr_ref_vector & terms) {
expr_ref_vector result(m);
// TODO this can probably be made more efficient
for (unsigned int majorIndex = 0; majorIndex < terms.size(); ++majorIndex) {
for (unsigned int minorIndex = 0; minorIndex < terms.size(); ++minorIndex) {
if (majorIndex == minorIndex) {
continue;
}
for (unsigned int minorIndex = majorIndex + 1; minorIndex < terms.size(); ++minorIndex) {
// generate an expression of the form
// terms[majorIndex] --> NOT(terms[minorIndex])
expr_ref ex(rewrite_implication(terms.get(majorIndex), m.mk_not(terms.get(minorIndex))), m);