diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-01-04 17:30:25 -0600 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-01-04 15:30:25 -0800 |
commit | e1df8f68a90c7ba548b2746704b978555ec4283f (patch) | |
tree | b3bcea5160fdb6fa38252e20eea7f759a9bfae85 | |
parent | 256d4093ab6ac3b792c6f1f11131124d1ae6b069 (diff) |
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.
-rw-r--r-- | src/theory/builtin/theory_builtin_rewriter.cpp | 14 | ||||
-rw-r--r-- | src/theory/quantifiers/ceg_instantiator.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/ceg_t_instantiator.cpp | 19 | ||||
-rw-r--r-- | 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 |