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.
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
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
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"
--- /dev/null
+/********************* */
+/*! \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<Node> 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<TNode>* 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<TNode>* 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<TNode> 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
--- /dev/null
+/********************* */
+/*! \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 <unordered_map>
+#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<TNode, TNodeHashFunction>;
+using FunctionToArgsMap =
+ std::unordered_map<TNode, TNodeSet, TNodeHashFunction>;
+
+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 */
+++ /dev/null
-/********************* */
-/*! \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<Node> 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<TNode>* 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<TNode>* 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<TNode> 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
+++ /dev/null
-/********************* */
-/*! \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 <unordered_map>
-#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<TNode, TNodeHashFunction>;
-using FunctionToArgsMap =
- std::unordered_map<TNode, TNodeSet, TNodeHashFunction>;
-
-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
#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"
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>);
<< "generation" << endl;
setOption("bitblastMode", SExpr("lazy"));
}
+ else if (!options::incrementalSolving())
+ {
+ options::ackermann.set(true);
+ }
if (options::incrementalSolving() && !d_logic.isPure(THEORY_BV))
{
{
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
"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())
# 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
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
--- /dev/null
+; 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
--- /dev/null
+; 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
--- /dev/null
+; 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)
--- /dev/null
+; 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)
--- /dev/null
+; 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
--- /dev/null
+; 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)
--- /dev/null
+; 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)
projects / cvc5.git / commitdiff