From d77c5daaa030ae5ff6b81eb7e77752526a8c0bb8 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Fri, 11 Nov 2016 14:41:51 -0800 Subject: [PATCH] Enable eager bitblasting for QF_ABV when no stores are present. --- src/smt/smt_engine.cpp | 6 ++++-- src/theory/bv/theory_bv.cpp | 37 ++++++++++++++++++++++++++----------- 2 files changed, 30 insertions(+), 13 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index e46511e59..38347508c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1291,7 +1291,8 @@ void SmtEngine::setDefaults() { } else if (options::solveIntAsBV() > 0) { d_logic = LogicInfo("QF_BV"); - } else if (d_logic.getLogicString() == "QF_UFBV" && + } else if ((d_logic.getLogicString() == "QF_UFBV" || + d_logic.getLogicString() == "QF_ABV") && options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { d_logic = LogicInfo("QF_BV"); } @@ -3871,7 +3872,8 @@ void SmtEnginePrivate::processAssertions() { if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && !d_smt.d_logic.isPure(THEORY_BV) && - d_smt.d_logic.getLogicString() != "QF_UFBV") { + d_smt.d_logic.getLogicString() != "QF_UFBV" && + d_smt.d_logic.getLogicString() != "QF_ABV") { throw ModalException("Eager bit-blasting does not currently support theory combination. " "Note that in a QF_BV problem UF symbols can be introduced for division. " "Try --bv-div-zero-const to interpret division by zero as a constant."); diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 869e59502..139559125 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -194,6 +194,11 @@ void TheoryBV::collectFunctionSymbols(TNode term, TNodeSet& seen) { if (term.getKind() == kind::APPLY_UF) { TNode func = term.getOperator(); storeFunction(func, term); + } else if (term.getKind() == kind::SELECT) { + TNode func = term[0]; + storeFunction(func, term); + } else if (term.getKind() == kind::STORE) { + AlwaysAssert(false, "Cannot use eager bitblasting on QF_ABV formula with stores"); } for (unsigned i = 0; i < term.getNumChildren(); ++i) { collectFunctionSymbols(term[i], seen); @@ -233,20 +238,30 @@ void TheoryBV::mkAckermanizationAsssertions(std::vector& assertions) { for(NodeSet::const_iterator it2 = it1; it2 != args.end(); ++it2) { TNode args1 = *it1; TNode args2 = *it2; + Node args_eq; + + if (args1.getKind() == kind::APPLY_UF) { + AlwaysAssert (args1.getKind() == kind::APPLY_UF && + args1.getOperator() == func); + AlwaysAssert (args2.getKind() == kind::APPLY_UF && + args2.getOperator() == func); + AlwaysAssert (args1.getNumChildren() == args2.getNumChildren()); - AlwaysAssert (args1.getKind() == kind::APPLY_UF && - args1.getOperator() == func); - AlwaysAssert (args2.getKind() == kind::APPLY_UF && - args2.getOperator() == func); - AlwaysAssert (args1.getNumChildren() == args2.getNumChildren()); - - std::vector eqs(args1.getNumChildren()); + std::vector eqs(args1.getNumChildren()); - for (unsigned i = 0; i < args1.getNumChildren(); ++i) { - eqs[i] = nm->mkNode(kind::EQUAL, args1[i], args2[i]); + for (unsigned i = 0; i < args1.getNumChildren(); ++i) { + eqs[i] = nm->mkNode(kind::EQUAL, args1[i], args2[i]); + } + args_eq = eqs.size() == 1 ? eqs[0] : nm->mkNode(kind::AND, eqs); + } else { + AlwaysAssert (args1.getKind() == kind::SELECT && + args1[0] == func); + AlwaysAssert (args2.getKind() == kind::SELECT && + args2[0] == func); + AlwaysAssert (args1.getNumChildren() == 2); + AlwaysAssert (args2.getNumChildren() == 2); + args_eq = nm->mkNode(kind::EQUAL, args1[1], args2[1]); } - - Node args_eq = eqs.size() == 1 ? eqs[0] : nm->mkNode(kind::AND, eqs); Node func_eq = nm->mkNode(kind::EQUAL, args1, args2); Node lemma = nm->mkNode(kind::IMPLIES, args_eq, func_eq); assertions.push_back(lemma); -- 2.30.2