From 00ccc01140bcdeaadedf8ae1b9f224ccdc812bc0 Mon Sep 17 00:00:00 2001 From: Ying Sheng Date: Tue, 8 Oct 2019 08:18:21 -0700 Subject: 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. --- src/CMakeLists.txt | 4 +- src/options/smt_options.toml | 8 + src/preprocessing/passes/ackermann.cpp | 227 +++++++++++++++++++++ src/preprocessing/passes/ackermann.h | 73 +++++++ src/preprocessing/passes/bv_ackermann.cpp | 221 -------------------- src/preprocessing/passes/bv_ackermann.h | 70 ------- src/preprocessing/preprocessing_pass_registry.cpp | 4 +- src/smt/smt_engine.cpp | 51 ++++- test/regress/CMakeLists.txt | 7 + test/regress/regress0/arith/ackermann.real.smt2 | 19 ++ .../regress0/arith/integers/ackermann1.smt2 | 19 ++ .../regress0/arith/integers/ackermann2.smt2 | 15 ++ .../regress0/arith/integers/ackermann3.smt2 | 15 ++ .../regress0/arith/integers/ackermann4.smt2 | 22 ++ .../regress0/arith/integers/ackermann5.smt2 | 15 ++ .../regress0/arith/integers/ackermann6.smt2 | 15 ++ 16 files changed, 483 insertions(+), 302 deletions(-) create mode 100644 src/preprocessing/passes/ackermann.cpp create mode 100644 src/preprocessing/passes/ackermann.h delete mode 100644 src/preprocessing/passes/bv_ackermann.cpp delete mode 100644 src/preprocessing/passes/bv_ackermann.h create mode 100644 test/regress/regress0/arith/ackermann.real.smt2 create mode 100644 test/regress/regress0/arith/integers/ackermann1.smt2 create mode 100644 test/regress/regress0/arith/integers/ackermann2.smt2 create mode 100644 test/regress/regress0/arith/integers/ackermann3.smt2 create mode 100644 test/regress/regress0/arith/integers/ackermann4.smt2 create mode 100644 test/regress/regress0/arith/integers/ackermann5.smt2 create mode 100644 test/regress/regress0/arith/integers/ackermann6.smt2 diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 7289f650b..0a6dec216 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -38,6 +38,8 @@ libcvc4_add_sources( lib/strtok_r.h preprocessing/assertion_pipeline.cpp preprocessing/assertion_pipeline.h + preprocessing/passes/ackermann.cpp + preprocessing/passes/ackermann.h preprocessing/passes/apply_substs.cpp preprocessing/passes/apply_substs.h preprocessing/passes/apply_to_const.cpp @@ -46,8 +48,6 @@ libcvc4_add_sources( preprocessing/passes/bool_to_bv.h preprocessing/passes/bv_abstraction.cpp preprocessing/passes/bv_abstraction.h - preprocessing/passes/bv_ackermann.cpp - preprocessing/passes/bv_ackermann.h preprocessing/passes/bv_eager_atoms.cpp preprocessing/passes/bv_eager_atoms.h preprocessing/passes/bv_gauss.cpp diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 394875fae..571094618 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -22,6 +22,14 @@ header = "options/smt_options.h" read_only = true help = "all dumping goes to FILE (instead of stdout)" +[[option]] + name = "ackermann" + category = "regular" + long = "ackermann" + type = "bool" + default = "false" + help = "eliminate functions by ackermannization" + [[option]] name = "simplificationMode" smt_name = "simplification-mode" diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp new file mode 100644 index 000000000..7ba689d0a --- /dev/null +++ b/src/preprocessing/passes/ackermann.cpp @@ -0,0 +1,227 @@ +/********************* */ +/*! \file ackermann.cpp + ** \verbatim + ** Top contributors (to current version): + ** 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. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Ackermannization preprocessing pass. + ** + ** This implements the Ackermannization preprocessing pass, which enables + ** very limited theory combination support for eager bit-blasting via + ** Ackermannization. It reduces constraints over the combination of the + ** theories of fixed-size bit-vectors and uninterpreted functions as + ** described in + ** Liana Hadarean, An Efficient and Trustworthy Theory Solver for + ** Bit-vectors in Satisfiability Modulo Theories. +** https://cs.nyu.edu/media/publications/hadarean_liana.pdf + **/ + +#include "preprocessing/passes/ackermann.h" + +#include "options/options.h" + +using namespace CVC4; +using namespace CVC4::theory; + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +/* -------------------------------------------------------------------------- */ + +namespace +{ + +void addLemmaForPair(TNode args1, + TNode args2, + const TNode func, + AssertionPipeline* assertionsToPreprocess, + NodeManager* nm) +{ + Node args_eq; + + if (args1.getKind() == kind::APPLY_UF) + { + Assert(args1.getOperator() == func); + Assert(args2.getKind() == kind::APPLY_UF && args2.getOperator() == func); + Assert(args1.getNumChildren() == args2.getNumChildren()); + Assert(args1.getNumChildren() >= 1); + + std::vector eqs(args1.getNumChildren()); + + for (unsigned i = 0, n = args1.getNumChildren(); i < n; ++i) + { + eqs[i] = nm->mkNode(kind::EQUAL, args1[i], args2[i]); + } + if (eqs.size() >= 2) + { + args_eq = nm->mkNode(kind::AND, eqs); + } + else + { + args_eq = eqs[0]; + } + } + else + { + 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 storeFunctionAndAddLemmas(TNode func, + TNode term, + FunctionToArgsMap& fun_to_args, + SubstitutionMap& fun_to_skolem, + AssertionPipeline* assertions, + NodeManager* nm, + std::vector* vec) +{ + if (fun_to_args.find(func) == fun_to_args.end()) + { + fun_to_args.insert(make_pair(func, TNodeSet())); + } + TNodeSet& set = fun_to_args[func]; + if (set.find(term) == set.end()) + { + TypeNode tn = term.getType(); + Node skolem = nm->mkSkolem("SKOLEM$$", + tn, + "is a variable created by the ackermannization " + "preprocessing pass"); + 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()); + } + } +} + +/* 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* vec, + AssertionPipeline* assertions) +{ + TNodeSet seen; + NodeManager* nm = NodeManager::currentNM(); + TNode term; + while (!vec->empty()) + { + 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 Ackermannization on formula with stores to arrays"); + /* add children to the vector, so that they are processed later */ + for (TNode n : term) + { + vec->push_back(n); + } + } + seen.insert(term); + } + } +} + +} // namespace + +/* -------------------------------------------------------------------------- */ + +Ackermann::Ackermann(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "ackermann"), + d_funcToSkolem(preprocContext->getUserContext()) +{ +} + +PreprocessingPassResult Ackermann::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + AlwaysAssert(!options::incrementalSolving()); + + /* collect all function applications and generate consistency lemmas + * accordingly */ + std::vector to_process; + for (const Node& a : assertionsToPreprocess->ref()) + { + 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 + for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i) + { + assertionsToPreprocess->replace( + i, d_funcToSkolem.apply((*assertionsToPreprocess)[i])); + } + + return PreprocessingPassResult::NO_CONFLICT; +} + + +/* -------------------------------------------------------------------------- */ + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/ackermann.h b/src/preprocessing/passes/ackermann.h new file mode 100644 index 000000000..8f27cab25 --- /dev/null +++ b/src/preprocessing/passes/ackermann.h @@ -0,0 +1,73 @@ +/********************* */ +/*! \file ackermann.h + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Yoni Zohar + ** 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. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Ackermannization preprocessing pass. + ** + ** This implements the Ackermannization preprocessing pass, which enables + ** very limited theory combination support for eager bit-blasting via + ** Ackermannization. It reduces constraints over the combination of the + ** theories of fixed-size bit-vectors and uninterpreted functions as + ** described in + ** Liana Hadarean, An Efficient and Trustworthy Theory Solver for + ** Bit-vectors in Satisfiability Modulo Theories. +** https://cs.nyu.edu/media/publications/hadarean_liana.pdf + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__PREPROCESSING__PASSES__ACKERMANN_H +#define CVC4__PREPROCESSING__PASSES__ACKERMANN_H + +#include +#include "expr/node.h" +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +using TNodeSet = std::unordered_set; +using FunctionToArgsMap = + std::unordered_map; + +class Ackermann : public PreprocessingPass +{ + public: + Ackermann(PreprocessingPassContext* preprocContext); + + protected: + /** + * Apply Ackermannization as follows: + * + * - For each application f(X) where X = (x1, . . . , xn), introduce a fresh + * variable f_X and use it to replace all occurrences of f(X). + * + * - 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 + */ + PreprocessingPassResult applyInternal( + 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; +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif /* CVC4__PREPROCESSING__PASSES__ACKERMANN_H */ diff --git a/src/preprocessing/passes/bv_ackermann.cpp b/src/preprocessing/passes/bv_ackermann.cpp deleted file mode 100644 index c8cefcb17..000000000 --- a/src/preprocessing/passes/bv_ackermann.cpp +++ /dev/null @@ -1,221 +0,0 @@ -/********************* */ -/*! \file bv_ackermann.cpp - ** \verbatim - ** Top contributors (to current version): - ** Yoni Zohar, Aina Niemetz, Clark Barrett - ** 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. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Ackermannization preprocessing pass. - ** - ** This implements the Ackermannization preprocessing pass, which enables - ** very limited theory combination support for eager bit-blasting via - ** Ackermannization. It reduces constraints over the combination of the - ** theories of fixed-size bit-vectors and uninterpreted functions as - ** described in - ** Liana Hadarean, An Efficient and Trustworthy Theory Solver for - ** Bit-vectors in Satisfiability Modulo Theories. -** https://cs.nyu.edu/media/publications/hadarean_liana.pdf - **/ - -#include "preprocessing/passes/bv_ackermann.h" - -#include "options/bv_options.h" -#include "theory/bv/theory_bv_utils.h" - -using namespace CVC4; -using namespace CVC4::theory; - -namespace CVC4 { -namespace preprocessing { -namespace passes { - -/* -------------------------------------------------------------------------- */ - -namespace -{ - -void addLemmaForPair(TNode args1, - TNode args2, - const TNode func, - AssertionPipeline* assertionsToPreprocess, - NodeManager* nm) -{ - Node args_eq; - - if (args1.getKind() == kind::APPLY_UF) - { - Assert(args1.getOperator() == func); - Assert(args2.getKind() == kind::APPLY_UF && args2.getOperator() == func); - Assert(args1.getNumChildren() == args2.getNumChildren()); - - std::vector 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 - { - 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 storeFunctionAndAddLemmas(TNode func, - TNode term, - FunctionToArgsMap& fun_to_args, - SubstitutionMap& fun_to_skolem, - AssertionPipeline* assertions, - NodeManager* nm, - std::vector* vec) -{ - if (fun_to_args.find(func) == fun_to_args.end()) - { - fun_to_args.insert(make_pair(func, TNodeSet())); - } - TNodeSet& set = fun_to_args[func]; - if (set.find(term) == set.end()) - { - 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()); - } - } -} - -/* 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* vec, - AssertionPipeline* assertions) -{ - TNodeSet seen; - NodeManager* nm = NodeManager::currentNM(); - TNode term; - while (!vec->empty()) - { - 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); - } - } -} - -} // namespace - -/* -------------------------------------------------------------------------- */ - -BVAckermann::BVAckermann(PreprocessingPassContext* preprocContext) - : PreprocessingPass(preprocContext, "bv-ackermann"), - d_funcToSkolem(preprocContext->getUserContext()) -{ -} - -PreprocessingPassResult BVAckermann::applyInternal( - AssertionPipeline* assertionsToPreprocess) -{ - Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER); - AlwaysAssert(!options::incrementalSolving()); - - /* collect all function applications and generate consistency lemmas - * accordingly */ - std::vector to_process; - for (const Node& a : assertionsToPreprocess->ref()) - { - 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 - for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i) - { - assertionsToPreprocess->replace( - i, d_funcToSkolem.apply((*assertionsToPreprocess)[i])); - } - - return PreprocessingPassResult::NO_CONFLICT; -} - - -/* -------------------------------------------------------------------------- */ - -} // namespace passes -} // namespace preprocessing -} // namespace CVC4 diff --git a/src/preprocessing/passes/bv_ackermann.h b/src/preprocessing/passes/bv_ackermann.h deleted file mode 100644 index 98d1080bd..000000000 --- a/src/preprocessing/passes/bv_ackermann.h +++ /dev/null @@ -1,70 +0,0 @@ -/********************* */ -/*! \file bv_ackermann.h - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Yoni Zohar - ** 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. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Ackermannization preprocessing pass. - ** - ** This implements the Ackermannization preprocessing pass, which enables - ** very limited theory combination support for eager bit-blasting via - ** Ackermannization. It reduces constraints over the combination of the - ** theories of fixed-size bit-vectors and uninterpreted functions as - ** described in - ** Liana Hadarean, An Efficient and Trustworthy Theory Solver for - ** Bit-vectors in Satisfiability Modulo Theories. -** https://cs.nyu.edu/media/publications/hadarean_liana.pdf - **/ - -#include "cvc4_private.h" - -#ifndef CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H -#define CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H - -#include -#include "expr/node.h" -#include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" - -namespace CVC4 { -namespace preprocessing { -namespace passes { - -using TNodeSet = std::unordered_set; -using FunctionToArgsMap = - std::unordered_map; - -class BVAckermann : public PreprocessingPass -{ - public: - BVAckermann(PreprocessingPassContext* preprocContext); - - protected: - /** - * Apply Ackermannization as follows: - * - * - For each application f(X) where X = (x1, . . . , xn), introduce a fresh - * variable f_X and use it to replace all occurrences of f(X). - * - * - 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 - */ - PreprocessingPassResult applyInternal( - AssertionPipeline* assertionsToPreprocess) override; - - private: - FunctionToArgsMap d_funcToArgs; - theory::SubstitutionMap d_funcToSkolem; -}; - -} // namespace passes -} // namespace preprocessing -} // namespace CVC4 - -#endif 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); registerPassInfo("miplib-trick", callCtor); registerPassInfo("non-clausal-simp", callCtor); - registerPassInfo("bv-ackermann", callCtor); + registerPassInfo("ackermann", callCtor); registerPassInfo("sym-break", callCtor); registerPassInfo("ext-rew-pre", callCtor); registerPassInfo("theory-preprocess", callCtor); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 918539f4f..8705bfb9b 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1185,6 +1185,10 @@ void SmtEngine::setDefaults() { << "generation" << endl; setOption("bitblastMode", SExpr("lazy")); } + else if (!options::incrementalSolving()) + { + options::ackermann.set(true); + } if (options::incrementalSolving() && !d_logic.isPure(THEORY_BV)) { @@ -1208,11 +1212,45 @@ void SmtEngine::setDefaults() { { d_logic = LogicInfo("QF_NIA"); } - else if ((d_logic.getLogicString() == "QF_UFBV" - || d_logic.getLogicString() == "QF_ABV") - && options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) + + // set options about ackermannization + if (options::produceModels()) { - d_logic = LogicInfo("QF_BV"); + if (options::ackermann() + && (d_logic.isTheoryEnabled(THEORY_ARRAYS) + || d_logic.isTheoryEnabled(THEORY_UF))) + { + if (options::produceModels.wasSetByUser()) + { + throw OptionException(std::string( + "Ackermannization currently does not support model generation.")); + } + Notice() << "SmtEngine: turn off ackermannization to support model" + << "generation" << endl; + options::ackermann.set(false); + } + } + + if (options::ackermann()) + { + if (options::incrementalSolving()) + { + throw OptionException( + "Incremental Ackermannization is currently not supported."); + } + + if (d_logic.isTheoryEnabled(THEORY_UF)) + { + d_logic = d_logic.getUnlockedCopy(); + d_logic.disableTheory(THEORY_UF); + d_logic.lock(); + } + if (d_logic.isTheoryEnabled(THEORY_ARRAYS)) + { + d_logic = d_logic.getUnlockedCopy(); + d_logic.disableTheory(THEORY_ARRAYS); + d_logic.lock(); + } } // set default options associated with strings-exp @@ -3241,10 +3279,9 @@ void SmtEnginePrivate::processAssertions() { "Try --bv-div-zero-const to interpret division by zero as a constant."); } - if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER - && !options::incrementalSolving()) + if (options::ackermann()) { - d_passes["bv-ackermann"]->apply(&d_assertions); + d_passes["ackermann"]->apply(&d_assertions); } if (options::bvAbstraction() && !options::incrementalSolving()) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 3045ea35e..d3f463afd 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2,6 +2,7 @@ # Regression level 0 tests set(regress_0_tests + regress0/arith/ackermann.real.smt2 regress0/arith/arith.01.cvc regress0/arith/arith.02.cvc regress0/arith/arith.03.cvc @@ -16,6 +17,12 @@ set(regress_0_tests regress0/arith/div.05.smt2 regress0/arith/div.07.smt2 regress0/arith/fuzz_3-eq.smtv1.smt2 + regress0/arith/integers/ackermann1.smt2 + regress0/arith/integers/ackermann2.smt2 + regress0/arith/integers/ackermann3.smt2 + regress0/arith/integers/ackermann4.smt2 + regress0/arith/integers/ackermann5.smt2 + regress0/arith/integers/ackermann6.smt2 regress0/arith/integers/arith-int-042.cvc regress0/arith/integers/arith-int-042.min.cvc regress0/arith/leq.01.smtv1.smt2 diff --git a/test/regress/regress0/arith/ackermann.real.smt2 b/test/regress/regress0/arith/ackermann.real.smt2 new file mode 100644 index 000000000..00dd79ebe --- /dev/null +++ b/test/regress/regress0/arith/ackermann.real.smt2 @@ -0,0 +1,19 @@ +; COMMAND-LINE: --ackermann --no-check-models --no-check-unsat-cores +; EXPECT: unsat +(set-logic QF_UFNRA) + +(declare-fun a () Real) +(declare-fun b () Real) + +(declare-fun f (Real) Real) +(declare-fun g (Real) Real) + +(assert (= (f (g (f (f a)))) (f (g (f a))))) +(assert (= (f a) b)) +(assert (= (f b) a)) +(assert (not (= a b))) +(assert (= (g a) (f a))) +(assert (= (g b) (f b))) + +(check-sat) +(exit) \ No newline at end of file diff --git a/test/regress/regress0/arith/integers/ackermann1.smt2 b/test/regress/regress0/arith/integers/ackermann1.smt2 new file mode 100644 index 000000000..b04210f36 --- /dev/null +++ b/test/regress/regress0/arith/integers/ackermann1.smt2 @@ -0,0 +1,19 @@ +; COMMAND-LINE: --ackermann --no-check-models --no-check-unsat-cores +; EXPECT: unsat +(set-logic QF_UFLIA) + +(declare-fun a () Int) +(declare-fun b () Int) + +(declare-fun f (Int) Int) +(declare-fun g (Int) Int) + +(assert (= (f (g (f (f a)))) (f (g (f a))))) +(assert (= (f a) b)) +(assert (= (f b) a)) +(assert (not (= a b))) +(assert (= (g a) (f a))) +(assert (= (g b) (f b))) + +(check-sat) +(exit) \ No newline at end of file diff --git a/test/regress/regress0/arith/integers/ackermann2.smt2 b/test/regress/regress0/arith/integers/ackermann2.smt2 new file mode 100644 index 000000000..f20fd99bf --- /dev/null +++ b/test/regress/regress0/arith/integers/ackermann2.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --ackermann --no-check-models --no-check-unsat-cores +; EXPECT: unsat +(set-logic QF_UFLIA) + +(declare-fun a () Int) +(declare-fun b () Int) + +(declare-fun f (Int) Int) +(declare-fun g (Int) Int) + +(assert (not (= (f (g (f (f a)))) (f (g (f (f b))))))) +(assert (= a b)) + +(check-sat) +(exit) diff --git a/test/regress/regress0/arith/integers/ackermann3.smt2 b/test/regress/regress0/arith/integers/ackermann3.smt2 new file mode 100644 index 000000000..4b4137cb9 --- /dev/null +++ b/test/regress/regress0/arith/integers/ackermann3.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --ackermann --no-check-models --no-check-unsat-cores +; EXPECT: sat +(set-logic QF_UFLIA) + +(declare-fun a () Int) +(declare-fun b () Int) + +(declare-fun f (Int) Int) +(declare-fun g (Int) Int) + +(assert (= (f (g (f (f a)))) (f (g (f (f b)))))) +(assert (not (= a b))) + +(check-sat) +(exit) diff --git a/test/regress/regress0/arith/integers/ackermann4.smt2 b/test/regress/regress0/arith/integers/ackermann4.smt2 new file mode 100644 index 000000000..1b76e1075 --- /dev/null +++ b/test/regress/regress0/arith/integers/ackermann4.smt2 @@ -0,0 +1,22 @@ +; COMMAND-LINE: --ackermann --no-check-models --no-check-proofs --no-check-unsat-cores +; EXPECT: unsat +(set-logic QF_ALIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) + +(define-sort bv () Int) +(define-sort abv () (Array bv bv)) + +(declare-fun v0 () Int) +(declare-fun v1 () Int) +(declare-fun a () abv) +(declare-fun b () abv) +(declare-fun c () abv) + +(assert (not (= (select a (select b (select c v0))) (select a (select b (select c v1)))))) + +(assert (= v0 v1)) + +(check-sat) +(exit) \ No newline at end of file diff --git a/test/regress/regress0/arith/integers/ackermann5.smt2 b/test/regress/regress0/arith/integers/ackermann5.smt2 new file mode 100644 index 000000000..8b93a3c35 --- /dev/null +++ b/test/regress/regress0/arith/integers/ackermann5.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --ackermann --no-check-models --no-check-proofs --no-check-unsat-cores +; EXPECT: sat +(set-logic QF_UFLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(declare-fun v0 () Int) +(declare-fun f (Int) Int) +(declare-fun g (Int) Int) + +(assert (= (f v0) (g (f v0)))) +(assert (= (f (f v0)) (g (f v0)))) +(assert (= (f (f (f v0))) (g (f v0)))) + +(check-sat) +(exit) diff --git a/test/regress/regress0/arith/integers/ackermann6.smt2 b/test/regress/regress0/arith/integers/ackermann6.smt2 new file mode 100644 index 000000000..62f2f1276 --- /dev/null +++ b/test/regress/regress0/arith/integers/ackermann6.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --ackermann --no-check-models --no-check-proofs --no-check-unsat-cores +; EXPECT: unsat +(set-logic QF_UFLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(declare-fun v0 () Int) +(declare-fun f (Int) Int) +(declare-fun g (Int) Int) + +(assert (= (f v0) (g (f v0)))) +(assert (= (f (f v0)) (g (f v0)))) +(assert (not (= (f (f (f v0))) (g (f v0))))) + +(check-sat) +(exit) -- cgit v1.2.3