diff options
Diffstat (limited to 'src/preprocessing/passes/ackermann.h')
| -rw-r--r-- | src/preprocessing/passes/ackermann.h | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/src/preprocessing/passes/ackermann.h b/src/preprocessing/passes/ackermann.h index 410dde8b9..4aa26da85 100644 --- a/src/preprocessing/passes/ackermann.h +++ b/src/preprocessing/passes/ackermann.h @@ -38,6 +38,8 @@ namespace passes { using TNodeSet = std::unordered_set<TNode, TNodeHashFunction>; using FunctionToArgsMap = std::unordered_map<TNode, TNodeSet, TNodeHashFunction>; +using USortToBVSizeMap = + std::unordered_map<TypeNode, size_t, TypeNode::HashFunction>; class Ackermann : public PreprocessingPass { @@ -54,6 +56,10 @@ class Ackermann : public PreprocessingPass * - For each f(X) and f(Y) with X = (x1, . . . , xn) and Y = (y1, . . . , yn) * occurring in the input formula, add the following lemma: * (x_1 = y_1 /\ ... /\ x_n = y_n) => f_X = f_Y + * + * - For each uninterpreted sort S, suppose k is the number of variables with + * sort S, then for each such variable X, introduce a fresh variable BV_X + * with BV with size log_2(k)+1 and use it to replace all occurrences of X. */ PreprocessingPassResult applyInternal( AssertionPipeline* assertionsToPreprocess) override; @@ -61,9 +67,15 @@ class Ackermann : public PreprocessingPass private: /* Map each function to a set of terms associated with it */ FunctionToArgsMap d_funcToArgs; - /* Map each function term to the new Skolem variable created by + /* Map each function-application term to the new Skolem variable created by * ackermannization */ theory::SubstitutionMap d_funcToSkolem; + /* Map each variable with uninterpreted sort to the new Skolem BV variable + * created by ackermannization */ + theory::SubstitutionMap d_usVarsToBVVars; + /* Map each uninterpreted sort to the number of variables in this sort. */ + USortToBVSizeMap d_usortCardinality; + LogicInfo d_logic; }; } // namespace passes |