From 82f5610afdf5a45404e6acecfc117bb29f98963f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 6 Apr 2020 22:48:13 -0500 Subject: [PATCH] Cleanup deprecated quantifiers attribute features (#4215) --- src/printer/smt2/smt2_printer.cpp | 9 +---- .../quantifiers/quantifiers_attributes.cpp | 37 +------------------ .../quantifiers/quantifiers_attributes.h | 18 --------- src/theory/quantifiers/theory_quantifiers.cpp | 3 -- 4 files changed, 3 insertions(+), 64 deletions(-) diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 6e4fcb63a..b5e137b4d 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -878,14 +878,7 @@ void Smt2Printer::toStream(std::ostream& out, { for (const Node& nc : n) { - if (nc.getKind() == kind::INST_ATTRIBUTE) - { - if (nc[0].getAttribute(theory::FunDefAttribute())) - { - out << ":fun-def"; - } - } - else if (nc.getKind() == kind::INST_PATTERN) + if (nc.getKind() == kind::INST_PATTERN) { out << ":pattern " << nc; } diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index af4011bd9..065c2ecd3 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -40,15 +40,8 @@ d_quantEngine(qe) { void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::vector< Node >& node_values, std::string str_value ){ Trace("quant-attr-debug") << "Set " << attr << " " << n << std::endl; - if( attr=="axiom" ){ - Trace("quant-attr-debug") << "Set axiom " << n << std::endl; - AxiomAttribute aa; - n.setAttribute( aa, true ); - }else if( attr=="conjecture" ){ - Trace("quant-attr-debug") << "Set conjecture " << n << std::endl; - ConjectureAttribute ca; - n.setAttribute( ca, true ); - }else if( attr=="fun-def" ){ + if (attr == "fun-def") + { Trace("quant-attr-debug") << "Set function definition " << n << std::endl; FunDefAttribute fda; n.setAttribute( fda, true ); @@ -215,14 +208,6 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){ qa.d_hasPattern = true; }else if( q[2][i].getKind()==INST_ATTRIBUTE ){ Node avar = q[2][i][0]; - if( avar.getAttribute(AxiomAttribute()) ){ - Trace("quant-attr") << "Attribute : axiom : " << q << std::endl; - qa.d_axiom = true; - } - if( avar.getAttribute(ConjectureAttribute()) ){ - Trace("quant-attr") << "Attribute : conjecture : " << q << std::endl; - qa.d_conjecture = true; - } if( avar.getAttribute(FunDefAttribute()) ){ Trace("quant-attr") << "Attribute : function definition : " << q << std::endl; //get operator directly from pattern @@ -273,24 +258,6 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){ } } -bool QuantAttributes::isConjecture( Node q ) { - std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); - if( it==d_qattr.end() ){ - return false; - }else{ - return it->second.d_conjecture; - } -} - -bool QuantAttributes::isAxiom( Node q ) { - std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); - if( it==d_qattr.end() ){ - return false; - }else{ - return it->second.d_axiom; - } -} - bool QuantAttributes::isFunDef( Node q ) { std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); if( it==d_qattr.end() ){ diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index fc0f85956..4d9e433a7 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -27,14 +27,6 @@ namespace theory { class QuantifiersEngine; -/** Attribute true for quantifiers that are axioms */ -struct AxiomAttributeId {}; -typedef expr::Attribute< AxiomAttributeId, bool > AxiomAttribute; - -/** Attribute true for quantifiers that are conjecture */ -struct ConjectureAttributeId {}; -typedef expr::Attribute< ConjectureAttributeId, bool > ConjectureAttribute; - /** Attribute true for function definition quantifiers */ struct FunDefAttributeId {}; typedef expr::Attribute< FunDefAttributeId, bool > FunDefAttribute; @@ -108,8 +100,6 @@ struct QAttributes public: QAttributes() : d_hasPattern(false), - d_conjecture(false), - d_axiom(false), d_sygus(false), d_qinstLevel(-1), d_quant_elim(false), @@ -119,10 +109,6 @@ struct QAttributes ~QAttributes(){} /** does the quantified formula have a pattern? */ bool d_hasPattern; - /** is this formula marked a conjecture? */ - bool d_conjecture; - /** is this formula marked an axiom? */ - bool d_axiom; /** if non-null, this quantified formula is a function definition for function * d_fundef_f */ Node d_fundef_f; @@ -200,10 +186,6 @@ public: /** is quant elim annotation */ static bool checkQuantElimAnnotation( Node ipl ); - /** is conjecture */ - bool isConjecture( Node q ); - /** is axiom */ - bool isAxiom( Node q ); /** is function definition */ bool isFunDef( Node q ); /** is sygus conjecture */ 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 ); } -- 2.30.2