From 7b12b1e8307295e68cb389eaa7692036fae6e872 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 22 Jan 2018 10:06:26 -0800 Subject: [PATCH] Add previous concat handling for CBQI BV as heuristic for EQ. (#1528) Previously, we computed an inverse for s1 o x, x o s2, s1 o x o s2 while disregarding that invertibility depends on si. This adds this handling as an optional heuristic for concats over (dis)equality since it improves performance on a considerable number of benchmarks. --- src/options/quantifiers_options | 2 ++ src/theory/quantifiers/bv_inverter.cpp | 27 +++++++++++++++++++++++++- 2 files changed, 28 insertions(+), 1 deletion(-) diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 2376409e0..c6eb1cd5e 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -355,6 +355,8 @@ option cbqiBvRmExtract --cbqi-bv-rm-extract bool :read-write :default true replaces extract terms with variables for counterexample-guided instantiation for bit-vectors option cbqiBvLinearize --cbqi-bv-linear bool :read-write :default true linearize adder chains for variables +option cbqiBvConcInv cbqi-bv-concat-inv --cbqi-bv-concat-inv bool :read-write :default true + compute inverse for concat over equalities rather than producing an invertibility condition ### local theory extensions options diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index 3a7568196..cf16efbfa 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -2939,7 +2939,32 @@ Node BvInverter::solveBvLit(Node sv, } else if (k == BITVECTOR_CONCAT) { - sc = getScBvConcat(pol, litk, index, x, sv_t, t); + if (litk == EQUAL && options::cbqiBvConcInv()) + { + /* Compute inverse for s1 o x, x o s2, s1 o x o s2 + * (while disregarding that invertibility depends on si) + * rather than an invertibility condition (the proper handling). + * This improves performance on a considerable number of benchmarks. + * + * x = t[upper:lower] + * where + * upper = getSize(t) - 1 - sum(getSize(sv_t[i])) for i < index + * lower = getSize(sv_t[i]) for i > index */ + unsigned upper, lower; + upper = bv::utils::getSize(t) - 1; + lower = 0; + NodeBuilder<> nb(BITVECTOR_CONCAT); + for (unsigned i = 0; i < nchildren; i++) + { + if (i < index) { upper -= bv::utils::getSize(sv_t[i]); } + else if (i > index) { lower += bv::utils::getSize(sv_t[i]); } + } + t = bv::utils::mkExtract(t, upper, lower); + } + else + { + sc = getScBvConcat(pol, litk, index, x, sv_t, t); + } } else if (k == BITVECTOR_SIGN_EXTEND) { -- 2.30.2