From 00ccc01140bcdeaadedf8ae1b9f224ccdc812bc0 Mon Sep 17 00:00:00 2001 From: Ying Sheng Date: Tue, 8 Oct 2019 08:18:21 -0700 Subject: [PATCH] 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 +++ .../{bv_ackermann.cpp => ackermann.cpp} | 32 +++++++----- .../passes/{bv_ackermann.h => ackermann.h} | 15 +++--- .../preprocessing_pass_registry.cpp | 4 +- src/smt/smt_engine.cpp | 51 ++++++++++++++++--- test/regress/CMakeLists.txt | 7 +++ .../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 ++++++ 14 files changed, 211 insertions(+), 30 deletions(-) rename src/preprocessing/passes/{bv_ackermann.cpp => ackermann.cpp} (91%) rename src/preprocessing/passes/{bv_ackermann.h => ackermann.h} (83%) 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/bv_ackermann.cpp b/src/preprocessing/passes/ackermann.cpp similarity index 91% rename from src/preprocessing/passes/bv_ackermann.cpp rename to 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 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 similarity index 83% rename from src/preprocessing/passes/bv_ackermann.h rename to 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 #include "expr/node.h" @@ -39,10 +39,10 @@ using TNodeSet = std::unordered_set; using FunctionToArgsMap = std::unordered_map; -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); 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) -- 2.30.2