summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.h
diff options
context:
space:
mode:
authorMathias Preiner <mathias.preiner@gmail.com>2018-05-08 15:18:15 -0700
committerGitHub <noreply@github.com>2018-05-08 15:18:15 -0700
commit08ddea9c91fc5c481642c4911d4af562ac2a88e1 (patch)
tree4c6f039f1a7d65d13526d7b1f3de59d32b8df2a9 /src/theory/theory_engine.h
parentcfaa03f3db71dc2805b695f98b073431d0430e43 (diff)
Refactor bv-abstraction preprocessing pass. (#1860)
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 80853bb6f..3ae0a9ea9 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);
- bool ppBvAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
void mkAckermanizationAssertions(std::vector<Node>& assertions);
Node ppSimpITE(TNode assertion);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback