#include "preprocessing/passes/bv_ackermann.h"
-#include "expr/node.h"
#include "options/bv_options.h"
#include "theory/bv/theory_bv_utils.h"
-#include <unordered_set>
-
using namespace CVC4;
using namespace CVC4::theory;
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<Node> 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<TNode, TNodeHashFunction>& seen)
+void storeFunctionAndAddLemmas(TNode func,
+ TNode term,
+ FunctionToArgsMap& fun_to_args,
+ SubstitutionMap& fun_to_skolem,
+ AssertionPipeline* assertions,
+ NodeManager* nm,
+ std::vector<TNode>* 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<TNode>* 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
Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER);
AlwaysAssert(!options::incrementalSolving());
- std::unordered_set<TNode, TNodeHashFunction> seen;
-
+ /* collect all function applications and generate consistency lemmas
+ * accordingly */
+ std::vector<TNode> 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<Node> 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
projects / cvc5.git / commitdiff