summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/CMakeLists.txt4
-rw-r--r--src/options/smt_options.toml8
-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.cpp4
-rw-r--r--src/smt/smt_engine.cpp51
6 files changed, 84 insertions, 30 deletions
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
@@ -23,6 +23,14 @@ header = "options/smt_options.h"
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"
category = "regular"
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>);
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())
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback