summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/inst_match.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2018-08-22 17:40:22 -0500
committerGitHub <noreply@github.com>2018-08-22 17:40:22 -0500
commit9c02423e90cf9cb8509d4ca6565acba06e6f9b2d (patch)
tree8030c67f89b083b695900ade8d8a5d413b569f0f /src/theory/quantifiers/inst_match.h
parent810bd1f79ca8416a24d21f72a18b29689d6b57f6 (diff)
More unused code elimination (#2358)
Diffstat (limited to 'src/theory/quantifiers/inst_match.h')
-rw-r--r--src/theory/quantifiers/inst_match.h2
1 files changed, 0 insertions, 2 deletions
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index 86138feb3..5695d1294 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -80,8 +80,6 @@ public:
}
/** get the i^th term in the instantiation */
Node get(int i) const;
- /** append the terms of this instantiation to inst */
- void getInst(std::vector<Node>& inst) const;
/** set/overwrites the i^th field in the instantiation with n */
void setValue( int i, TNode n );
/** set the i^th term in the instantiation to n
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback