diff options
author | Ying Sheng <sqy1415@gmail.com> | 2019-10-08 08:18:21 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-10-08 08:18:21 -0700 |
commit | 00ccc01140bcdeaadedf8ae1b9f224ccdc812bc0 (patch) | |
tree | bc4981945d06c25d57854fbf2651431061e9ae42 /src/preprocessing/passes | |
parent | 94feff6c3b03325115e2c1c91121b83945dba4b0 (diff) |
Make ackermannization generally applicable rather than just BV (#3315)
The ackermannization process is currently already support general theories rather than specifically for BV. In this pull request, an option has been added to turn on ackermannization independently.
Diffstat (limited to 'src/preprocessing/passes')
-rw-r--r-- | src/preprocessing/passes/ackermann.cpp (renamed from src/preprocessing/passes/bv_ackermann.cpp) | 32 | ||||
-rw-r--r-- | src/preprocessing/passes/ackermann.h (renamed from src/preprocessing/passes/bv_ackermann.h) | 15 |
2 files changed, 28 insertions, 19 deletions
diff --git a/src/preprocessing/passes/bv_ackermann.cpp b/src/preprocessing/passes/ackermann.cpp index c8cefcb17..7ba689d0a 100644 --- a/src/preprocessing/passes/bv_ackermann.cpp +++ b/src/preprocessing/passes/ackermann.cpp @@ -1,8 +1,8 @@ /********************* */ -/*! \file bv_ackermann.cpp +/*! \file ackermann.cpp ** \verbatim ** Top contributors (to current version): - ** Yoni Zohar, Aina Niemetz, Clark Barrett + ** Yoni Zohar, Aina Niemetz, Clark Barrett, Ying Sheng ** This file is part of the CVC4 project. ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -21,10 +21,9 @@ ** https://cs.nyu.edu/media/publications/hadarean_liana.pdf **/ -#include "preprocessing/passes/bv_ackermann.h" +#include "preprocessing/passes/ackermann.h" -#include "options/bv_options.h" -#include "theory/bv/theory_bv_utils.h" +#include "options/options.h" using namespace CVC4; using namespace CVC4::theory; @@ -51,6 +50,7 @@ void addLemmaForPair(TNode args1, Assert(args1.getOperator() == func); Assert(args2.getKind() == kind::APPLY_UF && args2.getOperator() == func); Assert(args1.getNumChildren() == args2.getNumChildren()); + Assert(args1.getNumChildren() >= 1); std::vector<Node> eqs(args1.getNumChildren()); @@ -58,7 +58,14 @@ void addLemmaForPair(TNode args1, { eqs[i] = nm->mkNode(kind::EQUAL, args1[i], args2[i]); } - args_eq = bv::utils::mkAnd(eqs); + if (eqs.size() >= 2) + { + args_eq = nm->mkNode(kind::AND, eqs); + } + else + { + args_eq = eqs[0]; + } } else { @@ -89,10 +96,10 @@ void storeFunctionAndAddLemmas(TNode func, if (set.find(term) == set.end()) { TypeNode tn = term.getType(); - Node skolem = nm->mkSkolem("BVSKOLEM$$", + Node skolem = nm->mkSkolem("SKOLEM$$", tn, "is a variable created by the ackermannization " - "preprocessing pass for theory BV"); + "preprocessing pass"); for (const auto& t : set) { addLemmaForPair(t, term, func, assertions, nm); @@ -164,7 +171,7 @@ void collectFunctionsAndLemmas(FunctionToArgsMap& fun_to_args, { AlwaysAssert( term.getKind() != kind::STORE, - "Cannot use eager bitblasting on QF_ABV formula with stores"); + "Cannot use Ackermannization on formula with stores to arrays"); /* add children to the vector, so that they are processed later */ for (TNode n : term) { @@ -180,16 +187,15 @@ void collectFunctionsAndLemmas(FunctionToArgsMap& fun_to_args, /* -------------------------------------------------------------------------- */ -BVAckermann::BVAckermann(PreprocessingPassContext* preprocContext) - : PreprocessingPass(preprocContext, "bv-ackermann"), +Ackermann::Ackermann(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "ackermann"), d_funcToSkolem(preprocContext->getUserContext()) { } -PreprocessingPassResult BVAckermann::applyInternal( +PreprocessingPassResult Ackermann::applyInternal( AssertionPipeline* assertionsToPreprocess) { - Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER); AlwaysAssert(!options::incrementalSolving()); /* collect all function applications and generate consistency lemmas diff --git a/src/preprocessing/passes/bv_ackermann.h b/src/preprocessing/passes/ackermann.h index 98d1080bd..8f27cab25 100644 --- a/src/preprocessing/passes/bv_ackermann.h +++ b/src/preprocessing/passes/ackermann.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file bv_ackermann.h +/*! \file ackermann.h ** \verbatim ** Top contributors (to current version): ** Aina Niemetz, Yoni Zohar @@ -23,8 +23,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H -#define CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H +#ifndef CVC4__PREPROCESSING__PASSES__ACKERMANN_H +#define CVC4__PREPROCESSING__PASSES__ACKERMANN_H #include <unordered_map> #include "expr/node.h" @@ -39,10 +39,10 @@ using TNodeSet = std::unordered_set<TNode, TNodeHashFunction>; using FunctionToArgsMap = std::unordered_map<TNode, TNodeSet, TNodeHashFunction>; -class BVAckermann : public PreprocessingPass +class Ackermann : public PreprocessingPass { public: - BVAckermann(PreprocessingPassContext* preprocContext); + Ackermann(PreprocessingPassContext* preprocContext); protected: /** @@ -59,7 +59,10 @@ class BVAckermann : public PreprocessingPass AssertionPipeline* assertionsToPreprocess) override; 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 + * ackermannization */ theory::SubstitutionMap d_funcToSkolem; }; @@ -67,4 +70,4 @@ class BVAckermann : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif +#endif /* CVC4__PREPROCESSING__PASSES__ACKERMANN_H */ |