diff options
Diffstat (limited to 'src/preprocessing')
-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 | ||||
-rw-r--r-- | src/preprocessing/preprocessing_pass_registry.cpp | 4 |
3 files changed, 30 insertions, 21 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 */ diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp index 36b3c6392..82132774b 100644 --- a/src/preprocessing/preprocessing_pass_registry.cpp +++ b/src/preprocessing/preprocessing_pass_registry.cpp @@ -23,11 +23,11 @@ #include "base/cvc4_assert.h" #include "base/map_util.h" #include "base/output.h" +#include "preprocessing/passes/ackermann.h" #include "preprocessing/passes/apply_substs.h" #include "preprocessing/passes/apply_to_const.h" #include "preprocessing/passes/bool_to_bv.h" #include "preprocessing/passes/bv_abstraction.h" -#include "preprocessing/passes/bv_ackermann.h" #include "preprocessing/passes/bv_eager_atoms.h" #include "preprocessing/passes/bv_gauss.h" #include "preprocessing/passes/bv_intro_pow2.h" @@ -142,7 +142,7 @@ PreprocessingPassRegistry::PreprocessingPassRegistry() registerPassInfo("ite-removal", callCtor<IteRemoval>); registerPassInfo("miplib-trick", callCtor<MipLibTrick>); registerPassInfo("non-clausal-simp", callCtor<NonClausalSimp>); - registerPassInfo("bv-ackermann", callCtor<BVAckermann>); + registerPassInfo("ackermann", callCtor<Ackermann>); registerPassInfo("sym-break", callCtor<SymBreakerPass>); registerPassInfo("ext-rew-pre", callCtor<ExtRewPre>); registerPassInfo("theory-preprocess", callCtor<TheoryPreprocess>); |