diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-20 18:40:40 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-08-20 18:40:40 -0500 |
| commit | bf863b1f3cee791585e2c04e5f40afcadcdf113c (patch) | |
| tree | 28d4912780a9396733542bbbdf97bd5eb62c40fc /src/theory/quantifiers/quantifiers_attributes.h | |
| parent | a0c5a51f6fae81ffeb1752ee4d75db7a51c23680 (diff) | |
Remove support for prototype (non-sygus) synthesis (#2338)
Diffstat (limited to 'src/theory/quantifiers/quantifiers_attributes.h')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.h | 21 |
1 files changed, 11 insertions, 10 deletions
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 */ |