From 459cb24dafae7b6253476cfae07a54fc5a4a9166 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Fri, 13 Oct 2017 14:28:47 -0700 Subject: [PATCH] CBQI BV: Added EXTRACT handling. (#1240) This adds inverse handling for BITVECTOR_EXTRACT. Fixes previously disabled regressions. These regressions are now enabled. --- src/theory/quantifiers/bv_inverter.cpp | 29 +++++++++++-------- test/regress/regress0/quantifiers/Makefile.am | 8 ++--- 2 files changed, 20 insertions(+), 17 deletions(-) diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index 0795c3068..8a65338a6 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -34,7 +34,10 @@ static Node dropChild(Node n, unsigned index) { unsigned nchildren = n.getNumChildren(); Assert(index < nchildren); Kind k = n.getKind(); - Assert(k == AND || k == OR || k == BITVECTOR_MULT || k == BITVECTOR_PLUS); + Assert(k == BITVECTOR_AND + || k == BITVECTOR_OR + || k == BITVECTOR_MULT + || k == BITVECTOR_PLUS); NodeBuilder<> nb(NodeManager::currentNM(), k); for (unsigned i = 0; i < nchildren; ++i) { if (i == index) continue; @@ -268,6 +271,7 @@ Node BvInverter::solve_bv_constraint(Node sv, Node sv_t, Node t, Kind rk, Assert(index < sv_t.getNumChildren()); path.pop_back(); Kind k = sv_t.getKind(); + unsigned nchildren = sv_t.getNumChildren(); /* inversions */ if (k == BITVECTOR_CONCAT) { @@ -280,17 +284,22 @@ Node BvInverter::solve_bv_constraint(Node sv, Node sv_t, Node t, Kind rk, upper = bv::utils::getSize(t) - 1; lower = 0; NodeBuilder<> nb(nm, BITVECTOR_CONCAT); - for (unsigned i = 0; i < sv_t.getNumChildren(); i++) { + 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 if (k == BITVECTOR_EXTRACT) { + Trace("bv-invert") << "bv-invert : Unsupported for index " << index + << ", from " << sv_t << std::endl; + return Node::null(); + } else if (k == BITVECTOR_NEG || k == BITVECTOR_NOT) { + t = NodeManager::currentNM()->mkNode(k, t); } else { - Node s = sv_t.getNumChildren() == 2 - ? sv_t[1 - index] - : dropChild(sv_t, index); + Assert (nchildren >= 2); + Node s = nchildren == 2 ? sv_t[1 - index] : dropChild(sv_t, index); /* Note: All n-ary kinds except for CONCAT (i.e., AND, OR, MULT, PLUS) * are commutative (no case split based on index). */ if (k == BITVECTOR_PLUS) { @@ -327,9 +336,7 @@ Node BvInverter::solve_bv_constraint(Node sv, Node sv_t, Node t, Kind rk, Node x = getSolveVariable(solve_tn); Node scl, scr; if (index == 0) { - /* x % s = t - * with side condition: - * TODO */ + /* x % s = t is rewritten to x - x / y * y */ Trace("bv-invert") << "bv-invert : Unsupported for index " << index << ", from " << sv_t << std::endl; return Node::null(); @@ -501,10 +508,8 @@ Node BvInverter::solve_bv_constraint(Node sv, Node sv_t, Node t, Kind rk, Node skv = getInversionNode(sc, solve_tn); /* now solving with the skolem node as the RHS */ t = skv; - } else if (k == BITVECTOR_NEG || k == BITVECTOR_NOT) { - t = NodeManager::currentNM()->mkNode(k, t); - //}else if( k==BITVECTOR_ASHR ){ - // TODO + //}else if( k==BITVECTOR_ASHR ){ + // TODO } else { Trace("bv-invert") << "bv-invert : Unknown kind for bit-vector term " << k diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index ec24fdd8b..a2f5c18b5 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -104,11 +104,9 @@ TESTS = \ qbv-test-urem-rewrite.smt2 \ qbv-inequality2.smt2 \ qbv-test-invert-bvult-1.smt2 \ - intersection-example-onelane.proof-node22337.smt2 - -# solved, but fail an assertion due to unhandled EXTRACT case -# nested9_true-unreach-call.i_575.smt2 -# small-pipeline-fixpoint-3.smt2 + intersection-example-onelane.proof-node22337.smt2 \ + nested9_true-unreach-call.i_575.smt2 \ + small-pipeline-fixpoint-3.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine -- 2.30.2