diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-06 22:48:13 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-06 22:48:13 -0500 |
commit | 82f5610afdf5a45404e6acecfc117bb29f98963f (patch) | |
tree | 32a5aa23a9a471f45017f11f451d559c68cf4bf4 /src/theory/quantifiers/theory_quantifiers.cpp | |
parent | 5ce47c94e28028493ab648eabac4b21302b41129 (diff) |
Cleanup deprecated quantifiers attribute features (#4215)
Diffstat (limited to 'src/theory/quantifiers/theory_quantifiers.cpp')
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 5253638a7..6407e0d6d 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -38,15 +38,12 @@ using namespace CVC4::theory::quantifiers; TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo) { - out.handleUserAttribute( "axiom", this ); - out.handleUserAttribute( "conjecture", this ); out.handleUserAttribute( "fun-def", this ); out.handleUserAttribute( "sygus", this ); out.handleUserAttribute("quant-name", this); out.handleUserAttribute("sygus-synth-grammar", this); out.handleUserAttribute( "sygus-synth-fun-var-list", this ); out.handleUserAttribute( "quant-inst-max-level", this ); - out.handleUserAttribute( "rr-priority", this ); out.handleUserAttribute( "quant-elim", this ); out.handleUserAttribute( "quant-elim-partial", this ); } |