summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/inst_match.h
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2015-09-25 17:58:56 +0200
committerajreynol <andrew.j.reynolds@gmail.com>2015-09-25 17:58:56 +0200
commit773963f4342bb860fe4deb1d3c65d801b6acd72f (patch)
treec5cf5b0685df6311226f7f823f61c7bb3ff14241 /src/theory/quantifiers/inst_match.h
parent30920046fd6992b6e2c12c33ba888df5c1caf8de (diff)
Clear term caches for quantifiers + incremental, fixes bug 674. Refactoring of term database, other refactoring. Bug fixes for cbqi+datatypes.
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 21220491f..6424b67d3 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -53,8 +53,6 @@ public:
void debugPrint( const char* c );
/** is complete? */
bool isComplete();
- /** make complete */
- void makeComplete( Node f, QuantifiersEngine* qe );
/** make representative */
void makeRepresentative( QuantifiersEngine* qe );
/** empty */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback