From bf863b1f3cee791585e2c04e5f40afcadcdf113c Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 20 Aug 2018 18:40:40 -0500
Subject:  Remove support for prototype (non-sygus) synthesis (#2338)

---
 src/theory/quantifiers/quantifiers_attributes.h | 21 +++++++++++----------
 1 file changed, 11 insertions(+), 10 deletions(-)

(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 16de5fd2e..918269bbe 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -57,10 +57,6 @@ struct QuantNameAttributeId
 };
 typedef expr::Attribute<QuantNameAttributeId, bool> QuantNameAttribute;
 
-/** Attribute true for quantifiers that are synthesis conjectures */
-struct SynthesisAttributeId {};
-typedef expr::Attribute< SynthesisAttributeId, bool > SynthesisAttribute;
-
 struct InstLevelAttributeId
 {
 };
@@ -87,8 +83,17 @@ namespace quantifiers {
 struct QAttributes
 {
  public:
-  QAttributes() : d_hasPattern(false), d_conjecture(false), d_axiom(false), d_sygus(false),
-                  d_synthesis(false), d_rr_priority(-1), d_qinstLevel(-1), d_quant_elim(false), d_quant_elim_partial(false){}
+  QAttributes()
+      : d_hasPattern(false),
+        d_conjecture(false),
+        d_axiom(false),
+        d_sygus(false),
+        d_rr_priority(-1),
+        d_qinstLevel(-1),
+        d_quant_elim(false),
+        d_quant_elim_partial(false)
+  {
+  }
   ~QAttributes(){}
   /** does the quantified formula have a pattern? */
   bool d_hasPattern;
@@ -104,8 +109,6 @@ struct QAttributes
   Node d_fundef_f;
   /** is this formula marked as a sygus conjecture? */
   bool d_sygus;
-  /** is this formula marked as a synthesis (non-sygus) conjecture? */
-  bool d_synthesis;
   /** if a rewrite rule, then this is the priority value for the rewrite rule */
   int d_rr_priority;
   /** stores the maximum instantiation level allowed for this quantified formula
@@ -192,8 +195,6 @@ public:
   bool isFunDef( Node q );
   /** is sygus conjecture */
   bool isSygus( Node q );
-  /** is synthesis conjecture */
-  bool isSynthesis( Node q );
   /** get instantiation level */
   int getQuantInstLevel( Node q );
   /** get rewrite rule priority */
-- 
cgit v1.2.3