diff options
author | Ying Sheng <sqy1415@gmail.com> | 2019-12-16 11:42:36 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-16 11:42:36 -0800 |
commit | 49f0f09c6ef1c04fcd5b088456cea9998cff3c91 (patch) | |
tree | 0d5746c90c1e7ca3e336a8cfc7417b05c0eecbe8 /src/preprocessing/passes/ackermann.cpp | |
parent | c101a6b42d1f14bc750fb2328ddd83261148d7ae (diff) |
Support ackermannization on uninterpreted sorts in BV (#3372)
Support ackermannization on uninterpreted sorts in BV. For uninterpreted sorts, we create a bit-vector sort to replace it. For an uninterpreted sort `S`, if the number of variables within sort `S` is `n`, the replacing bit-vector will have size (log n)+1.
Diffstat (limited to 'src/preprocessing/passes/ackermann.cpp')
-rw-r--r-- | src/preprocessing/passes/ackermann.cpp | 111 |
1 files changed, 109 insertions, 2 deletions
diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp index 87c7fa2ce..888456174 100644 --- a/src/preprocessing/passes/ackermann.cpp +++ b/src/preprocessing/passes/ackermann.cpp @@ -22,8 +22,9 @@ **/ #include "preprocessing/passes/ackermann.h" - +#include <cmath> #include "base/check.h" +#include "expr/node_algorithm.h" #include "options/options.h" using namespace CVC4; @@ -186,9 +187,111 @@ void collectFunctionsAndLemmas(FunctionToArgsMap& fun_to_args, /* -------------------------------------------------------------------------- */ +/* Given a minimum capacity for an uninterpreted sort, return the size of the + * new BV type */ +size_t getBVSkolemSize(size_t capacity) +{ + return static_cast<size_t>(log2(capacity)) + 1; +} + +/* Given the lowest capacity requirements for each uninterpreted sort, assign + * a sufficient bit-vector size. + * Populate usVarsToBVVars so that it maps variables with uninterpreted sort to + * the fresh skolem BV variables. variables */ +void collectUSortsToBV(const unordered_set<TNode, TNodeHashFunction>& vars, + const USortToBVSizeMap& usortCardinality, + SubstitutionMap& usVarsToBVVars) +{ + NodeManager* nm = NodeManager::currentNM(); + + for (TNode var : vars) + { + TypeNode type = var.getType(); + size_t size = getBVSkolemSize(usortCardinality.at(type)); + Node skolem = nm->mkSkolem( + "BVSKOLEM$$", + nm->mkBitVectorType(size), + "a variable created by the ackermannization " + "preprocessing pass, representing a variable with uninterpreted sort " + + type.toString() + "."); + usVarsToBVVars.addSubstitution(var, skolem); + } +} + +/* This function returns the list of terms with uninterpreted sort in the + * formula represented by assertions. */ +std::unordered_set<TNode, TNodeHashFunction> getVarsWithUSorts( + AssertionPipeline* assertions) +{ + std::unordered_set<TNode, TNodeHashFunction> res; + + for (const Node& assertion : assertions->ref()) + { + std::unordered_set<TNode, TNodeHashFunction> vars; + expr::getVariables(assertion, vars); + + for (const TNode& var : vars) + { + if (var.getType().isSort()) + { + res.insert(var); + } + } + } + + return res; +} + +/* This is the top level of converting uninterpreted sorts to bit-vectors. + * We count the number of different variables for each uninterpreted sort. + * Then for each sort, we will assign a new bit-vector type with a sufficient + * size. The size is calculated to have enough capacity, that can accommodate + * the variables occured in the original formula. At the end, all variables of + * uninterpreted sorts will be converted into Skolem variables of BV */ +void usortsToBitVectors(const LogicInfo& d_logic, + AssertionPipeline* assertions, + USortToBVSizeMap& usortCardinality, + SubstitutionMap& usVarsToBVVars) +{ + std::unordered_set<TNode, TNodeHashFunction> toProcess = + getVarsWithUSorts(assertions); + + if (toProcess.size() > 0) + { + /* the current version only supports BV for removing uninterpreted sorts */ + if (not d_logic.isTheoryEnabled(theory::THEORY_BV)) + { + return; + } + + for (TNode term : toProcess) + { + TypeNode type = term.getType(); + /* Update the counts for each uninterpreted sort. + * For non-existing keys, C++ will create a new element for it, which has + * a default 0 value, before incrementing by 1. */ + usortCardinality[type] = usortCardinality[type] + 1; + } + + collectUSortsToBV(toProcess, usortCardinality, usVarsToBVVars); + + for (size_t i = 0, size = assertions->size(); i < size; ++i) + { + Node old = (*assertions)[i]; + assertions->replace(i, usVarsToBVVars.apply((*assertions)[i])); + Trace("uninterpretedSorts-to-bv") + << " " << old << " => " << (*assertions)[i] << "\n"; + } + } +} + +/* -------------------------------------------------------------------------- */ + Ackermann::Ackermann(PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "ackermann"), - d_funcToSkolem(preprocContext->getUserContext()) + d_funcToSkolem(preprocContext->getUserContext()), + d_usVarsToBVVars(preprocContext->getUserContext()), + d_logic(preprocContext->getLogicInfo()) { } @@ -215,6 +318,10 @@ PreprocessingPassResult Ackermann::applyInternal( i, d_funcToSkolem.apply((*assertionsToPreprocess)[i])); } + /* replace uninterpreted sorts with bit-vectors */ + usortsToBitVectors( + d_logic, assertionsToPreprocess, d_usortCardinality, d_usVarsToBVVars); + return PreprocessingPassResult::NO_CONFLICT; } |