Simplify how user-provided quantifier attributes are handled (#6963)

This makes INST_ATTRIBUTE (optionally) take multiple children, giving a way for the user to set attributes on quantified formulas, which does not require a new API command.

This is a special case of term annotations that occur as the body of a quantified formula.

If we need to extend our API to support further user-provided attributes, we should use a similar approach, e.g. a new kind ANNOTATE.

1 files changed, 0 insertions, 6 deletions

diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp
index ee07dcd57..218175ee9 100644
--- a/src/theory/engine_output_channel.cpp
+++ b/src/theory/engine_output_channel.cpp
@@ -116,12 +116,6 @@ void EngineOutputChannel::spendResource(Resource r)
   d_engine->spendResource(r);
 }
 
-void EngineOutputChannel::handleUserAttribute(const char* attr,
-                                              theory::Theory* t)
-{
-  d_engine->handleUserAttribute(attr, t);
-}
-
 void EngineOutputChannel::trustedConflict(TrustNode pconf)
 {
   Assert(pconf.getKind() == TrustNodeKind::CONFLICT);