From 438ba8d513af8efefcce5dac73fb7186ec848db2 Mon Sep 17 00:00:00 2001 From: martin Date: Fri, 6 Oct 2017 14:53:33 +0100 Subject: [PATCH 1/2] Avoid generating redundant constraints by iterating over n^2/2 rather than n^2 pairs. Ackermann constaints are symmetric so we don't need to consider every pair of indexes, only every ordered pair. This can halve the number of constraints generated which can be a significant saving in terms of problem size but also saves significant time when used in the string solver. --- src/solvers/flattening/arrays.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp index 854ca4156b1..912799754d4 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -316,7 +316,7 @@ void arrayst::add_array_Ackermann_constraints() i1!=index_set.end(); i1++) for(index_sett::const_iterator - i2=index_set.begin(); + i2=i1; i2!=index_set.end(); i2++) if(i1!=i2) From 7c545c81dee5c3613238a1ad1708d58f47f8c744 Mon Sep 17 00:00:00 2001 From: martin Date: Fri, 6 Oct 2017 15:16:23 +0100 Subject: [PATCH 2/2] Switch (!a | b) for (a => b) to clarrify the intent of the code. --- src/solvers/flattening/arrays.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp index 912799754d4..8a1fcfc328c 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -348,7 +348,7 @@ void arrayst::add_array_Ackermann_constraints() // add constraint lazy_constraintt lazy(lazy_typet::ARRAY_ACKERMANN, - or_exprt(literal_exprt(!indices_equal_lit), values_equal)); + implies_exprt(literal_exprt(indices_equal_lit), values_equal)); add_array_constraint(lazy, true); // added lazily #if 0 // old code for adding, not significantly faster