From e1df8f68a90c7ba548b2746704b978555ec4283f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 4 Jan 2018 17:30:25 -0600 Subject: [PATCH] Improvements for CBQI (#1478) Includes: - Basic rewriting for choice functions in the builtin rewriter, - Do not consider more than one equal term in ceg instantiator (helps cases where we have a repeated pattern of duplicate instantiations), - Do not introduce dummy extract equalities in the cbqi-bv-rm-extract pass (dummy concat equalities suffice). - Do not consider extracts in nested quantified formulas in the cbqi-bv-rm-extract pass. --- .../builtin/theory_builtin_rewriter.cpp | 14 +++++++++++++ src/theory/quantifiers/ceg_instantiator.cpp | 4 ++++ src/theory/quantifiers/ceg_t_instantiator.cpp | 19 +++++++++--------- src/theory/quantifiers/ceg_t_instantiator.h | 20 +++++++++---------- 4 files changed, 36 insertions(+), 21 deletions(-) diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp index edc934d0d..b0e3aeb6f 100644 --- a/src/theory/builtin/theory_builtin_rewriter.cpp +++ b/src/theory/builtin/theory_builtin_rewriter.cpp @@ -94,6 +94,20 @@ RewriteResponse TheoryBuiltinRewriter::postRewrite(TNode node) { Trace("builtin-rewrite-debug") << "...failed to get array representation." << std::endl; } return RewriteResponse(REWRITE_DONE, node); + } + else if (node.getKind() == kind::CHOICE) + { + if (node[1].getKind() == kind::EQUAL) + { + for (unsigned i = 0; i < 2; i++) + { + if (node[1][i] == node[0][0]) + { + return RewriteResponse(REWRITE_DONE, node[1][1 - i]); + } + } + } + return RewriteResponse(REWRITE_DONE, node); }else{ return doRewrite(node); } diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index e14ae78fc..0e8b229a3 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -335,6 +335,10 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i) { return true; } + // Do not consider more than one equal term, + // this helps non-monotonic strategies that may encounter + // duplicate instantiations. + break; } } } diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp index 4b326ede6..2c71de666 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/ceg_t_instantiator.cpp @@ -1920,9 +1920,6 @@ void BvInstantiatorPreprocess::registerCounterexampleLemma( nm->mkSkolem("ek", ex.getType(), "variable to represent disjoint extract region"); - Node ceq_lem = var.eqNode(ex); - Trace("cegqi-bv-pp") << "Introduced : " << ceq_lem << std::endl; - new_lems.push_back(ceq_lem); children.push_back(var); vars.push_back(var); } @@ -1967,15 +1964,17 @@ void BvInstantiatorPreprocess::collectExtracts( if (visited.find(cur) == visited.end()) { visited.insert(cur); - - if (cur.getKind() == BITVECTOR_EXTRACT) + if (cur.getKind() != FORALL) { - extract_map[cur[0]].push_back(cur); - } + if (cur.getKind() == BITVECTOR_EXTRACT) + { + extract_map[cur[0]].push_back(cur); + } - for (const Node& nc : cur) - { - visit.push_back(nc); + for (const Node& nc : cur) + { + visit.push_back(nc); + } } } } while (!visit.empty()); diff --git a/src/theory/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/ceg_t_instantiator.h index 0648942e8..a607909cc 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.h +++ b/src/theory/quantifiers/ceg_t_instantiator.h @@ -284,27 +284,25 @@ class BvInstantiatorPreprocess : public InstantiatorPreprocess virtual ~BvInstantiatorPreprocess() {} /** register counterexample lemma * - * This method modifies the contents of lems based on removing extract terms - * when the option --cbqi-bv-rm-extract is enabled. + * This method modifies the contents of lems based on the extract terms + * it contains when the option --cbqi-bv-rm-extract is enabled. It introduces + * a dummy equality so that segments of terms t under extracts can be solved + * independently. * * For example: * P[ ((extract 7 4) t), ((extract 3 0) t)] * becomes: * P[((extract 7 4) t), ((extract 3 0) t)] ^ - * t = concat( x74, x30 ) ^ - * x74 = ((extract 7 4) t) ^ - * x30 = ((extract 3 0) t) - * where x74 and x30 are fresh variables. + * t = concat( x74, x30 ) + * where x74 and x30 are fresh variables of type BV_4. * * Another example: * P[ ((extract 7 3) t), ((extract 4 0) t)] * becomes: * P[((extract 7 4) t), ((extract 3 0) t)] ^ - * t = concat( x75, x44, x30 ) ^ - * x75 = ((extract 7 5) t) ^ - * x44 = ((extract 4 4) t) ^ - * x30 = ((extract 3 0) t) - * where x75, x44 and x30 are fresh variables. + * t = concat( x75, x44, x30 ) + * where x75, x44 and x30 are fresh variables of type BV_3, BV_1, and BV_4 + * respectively. * * Notice we leave the original conjecture alone. This is done for performance * since the added equalities ensure we are able to construct the proper -- 2.30.2