From: yoni206 Date: Wed, 22 Aug 2018 21:36:13 +0000 (-0700) Subject: Generating less consistency lemmas in bv-ackermann preprocessing pass (#2253) X-Git-Tag: cvc5-1.0.0~4739 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=810bd1f79ca8416a24d21f72a18b29689d6b57f6;p=cvc5.git Generating less consistency lemmas in bv-ackermann preprocessing pass (#2253) --- diff --git a/src/preprocessing/passes/bv_ackermann.cpp b/src/preprocessing/passes/bv_ackermann.cpp index 12c1c5c21..26785f15b 100644 --- a/src/preprocessing/passes/bv_ackermann.cpp +++ b/src/preprocessing/passes/bv_ackermann.cpp @@ -23,12 +23,9 @@ #include "preprocessing/passes/bv_ackermann.h" -#include "expr/node.h" #include "options/bv_options.h" #include "theory/bv/theory_bv_utils.h" -#include - using namespace CVC4; using namespace CVC4::theory; @@ -41,55 +38,142 @@ namespace passes { namespace { -void storeFunction( - TNode func, - TNode term, - FunctionToArgsMap& fun_to_args, - SubstitutionMap& fun_to_skolem) +void addLemmaForPair(TNode args1, + TNode args2, + const TNode func, + AssertionPipeline* assertionsToPreprocess, + NodeManager* nm) { - if (fun_to_args.find(func) == fun_to_args.end()) + Node args_eq; + + if (args1.getKind() == kind::APPLY_UF) { - fun_to_args.insert(make_pair(func, NodeSet())); + Assert(args1.getOperator() == func); + Assert(args2.getKind() == kind::APPLY_UF && args2.getOperator() == func); + Assert(args1.getNumChildren() == args2.getNumChildren()); + + std::vector eqs(args1.getNumChildren()); + + for (unsigned i = 0, n = args1.getNumChildren(); i < n; ++i) + { + eqs[i] = nm->mkNode(kind::EQUAL, args1[i], args2[i]); + } + args_eq = bv::utils::mkAnd(eqs); } - NodeSet& set = fun_to_args[func]; - if (set.find(term) == set.end()) + else { - set.insert(term); - TypeNode tn = term.getType(); - Node skolem = NodeManager::currentNM()->mkSkolem( - "BVSKOLEM$$", - tn, - "is a variable created by the ackermannization " - "preprocessing pass for theory BV"); - fun_to_skolem.addSubstitution(term, skolem); + Assert(args1.getKind() == kind::SELECT && args1[0] == func); + Assert(args2.getKind() == kind::SELECT && args2[0] == func); + Assert(args1.getNumChildren() == 2); + Assert(args2.getNumChildren() == 2); + args_eq = nm->mkNode(kind::EQUAL, args1[1], args2[1]); } + Node func_eq = nm->mkNode(kind::EQUAL, args1, args2); + Node lemma = nm->mkNode(kind::IMPLIES, args_eq, func_eq); + assertionsToPreprocess->push_back(lemma); } -void collectFunctionSymbols( - TNode term, - FunctionToArgsMap& fun_to_args, - SubstitutionMap& fun_to_skolem, - std::unordered_set& seen) +void storeFunctionAndAddLemmas(TNode func, + TNode term, + FunctionToArgsMap& fun_to_args, + SubstitutionMap& fun_to_skolem, + AssertionPipeline* assertions, + NodeManager* nm, + std::vector* vec) { - if (seen.find(term) != seen.end()) return; - if (term.getKind() == kind::APPLY_UF) - { - storeFunction(term.getOperator(), term, fun_to_args, fun_to_skolem); - } - else if (term.getKind() == kind::SELECT) + if (fun_to_args.find(func) == fun_to_args.end()) { - storeFunction(term[0], term, fun_to_args, fun_to_skolem); + fun_to_args.insert(make_pair(func, TNodeSet())); } - else + TNodeSet& set = fun_to_args[func]; + if (set.find(term) == set.end()) { - AlwaysAssert(term.getKind() != kind::STORE, - "Cannot use eager bitblasting on QF_ABV formula with stores"); + TypeNode tn = term.getType(); + Node skolem = nm->mkSkolem("BVSKOLEM$$", + tn, + "is a variable created by the ackermannization " + "preprocessing pass for theory BV"); + for (const auto& t : set) + { + addLemmaForPair(t, term, func, assertions, nm); + } + fun_to_skolem.addSubstitution(term, skolem); + set.insert(term); + /* Add the arguments of term (newest element in set) to the vector, so that + * collectFunctionsAndLemmas will process them as well. + * This is only needed if the set has at least two elements + * (otherwise, no lemma is generated). + * Therefore, we defer this for term in case it is the first element in the + * set*/ + if (set.size() == 2) + { + for (TNode elem : set) + { + vec->insert(vec->end(), elem.begin(), elem.end()); + } + } + else if (set.size() > 2) + { + vec->insert(vec->end(), term.begin(), term.end()); + } } - for (const TNode& n : term) +} + +/* We only add top-level applications of functions. + * For example: when we see "f(g(x))", we do not add g as a function and x as a + * parameter. + * Instead, we only include f as a function and g(x) as a parameter. + * However, if we see g(x) later on as a top-level application, we will add it + * as well. + * Another example: for the formula f(g(x))=f(g(y)), + * we first only add f as a function and g(x),g(y) as arguments. + * storeFunctionAndAddLemmas will then add the constraint g(x)=g(y) -> + * f(g(x))=f(g(y)). + * Now that we see g(x) and g(y), we explicitly add them as well. */ +void collectFunctionsAndLemmas(FunctionToArgsMap& fun_to_args, + SubstitutionMap& fun_to_skolem, + std::vector* vec, + AssertionPipeline* assertions) +{ + TNodeSet seen; + NodeManager* nm = NodeManager::currentNM(); + TNode term; + while (!vec->empty()) { - collectFunctionSymbols(n, fun_to_args, fun_to_skolem, seen); + term = vec->back(); + vec->pop_back(); + if (seen.find(term) == seen.end()) + { + TNode func; + if (term.getKind() == kind::APPLY_UF) + { + storeFunctionAndAddLemmas(term.getOperator(), + term, + fun_to_args, + fun_to_skolem, + assertions, + nm, + vec); + } + else if (term.getKind() == kind::SELECT) + { + storeFunctionAndAddLemmas( + term[0], term, fun_to_args, fun_to_skolem, assertions, nm, vec); + } + else + { + AlwaysAssert( + term.getKind() != kind::STORE, + "Cannot use eager bitblasting on QF_ABV formula with stores"); + /* add children to the vector, so that they are processed later */ + for (TNode n : term) + { + vec->push_back(n); + } + } + seen.insert(term); + } } - seen.insert(term); } } // namespace @@ -108,57 +192,15 @@ PreprocessingPassResult BVAckermann::applyInternal( Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER); AlwaysAssert(!options::incrementalSolving()); - std::unordered_set seen; - + /* collect all function applications and generate consistency lemmas + * accordingly */ + std::vector to_process; for (const Node& a : assertionsToPreprocess->ref()) { - collectFunctionSymbols(a, d_funcToArgs, d_funcToSkolem, seen); - } - - NodeManager* nm = NodeManager::currentNM(); - for (const auto& p : d_funcToArgs) - { - TNode func = p.first; - const NodeSet& args = p.second; - NodeSet::const_iterator it1 = args.begin(); - for (; it1 != args.end(); ++it1) - { - 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()); - - std::vector eqs(args1.getNumChildren()); - - for (unsigned i = 0, n = args1.getNumChildren(); i < n; ++i) - { - eqs[i] = nm->mkNode(kind::EQUAL, args1[i], args2[i]); - } - args_eq = bv::utils::mkAnd(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 func_eq = nm->mkNode(kind::EQUAL, args1, args2); - Node lemma = nm->mkNode(kind::IMPLIES, args_eq, func_eq); - assertionsToPreprocess->push_back(lemma); - } - } + to_process.push_back(a); } + collectFunctionsAndLemmas( + d_funcToArgs, d_funcToSkolem, &to_process, assertionsToPreprocess); /* replace applications of UF by skolems */ // FIXME for model building, github issue #1901 diff --git a/src/preprocessing/passes/bv_ackermann.h b/src/preprocessing/passes/bv_ackermann.h index 197e92178..5f799ffe4 100644 --- a/src/preprocessing/passes/bv_ackermann.h +++ b/src/preprocessing/passes/bv_ackermann.h @@ -26,16 +26,18 @@ #ifndef __CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H #define __CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H +#include +#include "expr/node.h" #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" -#include - namespace CVC4 { namespace preprocessing { namespace passes { -typedef std::unordered_map FunctionToArgsMap; +using TNodeSet = std::unordered_set; +using FunctionToArgsMap = + std::unordered_map; class BVAckermann : public PreprocessingPass { diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index a4d318067..9f547eb86 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -155,6 +155,8 @@ REG0_TESTS = \ regress0/bug605.cvc \ regress0/bug639.smt2 \ regress0/buggy-ite.smt2 \ + regress0/bv/ackermann1.smt2 \ + regress0/bv/ackermann2.smt2 \ regress0/bv/bool-to-bv.smt2 \ regress0/bv/bug260a.smt \ regress0/bv/bug260b.smt \ diff --git a/test/regress/regress0/bv/ackermann1.smt2 b/test/regress/regress0/bv/ackermann1.smt2 new file mode 100644 index 000000000..9b96b38c4 --- /dev/null +++ b/test/regress/regress0/bv/ackermann1.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-proofs --no-check-unsat-cores +; EXPECT: sat +(set-logic QF_UFBV) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun v0 () (_ BitVec 4)) +(declare-fun f ((_ BitVec 4)) (_ BitVec 4)) +(declare-fun g ((_ BitVec 4)) (_ BitVec 4)) + +(assert (= (f (f v0)) (g (f v0)))) + + +(check-sat) +(exit) diff --git a/test/regress/regress0/bv/ackermann2.smt2 b/test/regress/regress0/bv/ackermann2.smt2 new file mode 100644 index 000000000..eeca505fe --- /dev/null +++ b/test/regress/regress0/bv/ackermann2.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-proofs --no-check-unsat-cores +; EXPECT: unsat +(set-logic QF_UFBV) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun v0 () (_ BitVec 4)) +(declare-fun v1 () (_ BitVec 4)) +(declare-fun f ((_ BitVec 4)) (_ BitVec 4)) +(declare-fun g ((_ BitVec 4)) (_ BitVec 4)) +(declare-fun h ((_ BitVec 4)) (_ BitVec 4)) + +(assert (not (= (f (g (h v0))) (f (g (h v1)))))) +(assert (= v0 v1)) + + +(check-sat) +(exit)