summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.h
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2018-05-10 11:25:19 -0700
committerGitHub <noreply@github.com>2018-05-10 11:25:19 -0700
commit31a2135f4650a63fa772f001fcf191f2f7093a8d (patch)
tree1d01c094b7df9b010f748905aeaace44f17d904a /src/theory/theory_engine.h
parentaef0e5ed90b1b8913b5c8c743cbcd012d5916ba7 (diff)
Refactored BVAckermann preprocessing pass. (#1889)
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r--src/theory/theory_engine.h1
1 files changed, 0 insertions, 1 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 3ae0a9ea9..fb33b45de 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -852,7 +852,6 @@ private:
/** For preprocessing pass lifting bit-vectors of size 1 to booleans */
public:
void staticInitializeBVOptions(const std::vector<Node>& assertions);
- void mkAckermanizationAssertions(std::vector<Node>& assertions);
Node ppSimpITE(TNode assertion);
/** Returns false if an assertion simplified to false. */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback