From 72281a35622ae4656d3a2e4cd29e42cb96eba205 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 13 Aug 2019 15:08:00 -0500
Subject:  Track sygus variable to term relationship via attribute (#3182)

---
 src/theory/quantifiers/quantifiers_attributes.h | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'src/theory/quantifiers/quantifiers_attributes.h')

diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index 329f9d08a..827c5e7f4 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -84,6 +84,18 @@ struct SygusSideConditionAttributeId
 typedef expr::Attribute<SygusSideConditionAttributeId, Node>
     SygusSideConditionAttribute;
 
+/** Attribute for indicating that a sygus variable encodes a term
+ *
+ * This is used, e.g., for abduction where the formal argument list of the
+ * abduct-to-synthesize corresponds to the free variables of the sygus
+ * problem.
+ */
+struct SygusVarToTermAttributeId
+{
+};
+typedef expr::Attribute<SygusVarToTermAttributeId, Node>
+    SygusVarToTermAttribute;
+
 namespace quantifiers {
 
 /** Attribute priority for rewrite rules */
-- 
cgit v1.2.3