Cleanup deprecated quantifiers attribute features (#4215)

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 6e4fcb63a6db9e48bbb47411d831198265030efb..b5e137b4d91f428165a85ececec6873023007804 100644 (file)
--- 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 af4011bd9de7109dd55ac83fe4ec0def61bf2a8f..065c2ecd3d55965a31ba52a8694fad763ad2c5c5 100644 (file)
--- 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 fc0f859560d215ffc4676ebbbecb9cae7a510e7e..4d9e433a751894e51e39c3ac894229ea41761b18 100644 (file)
--- 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 5253638a73ac369909d2a8e9130fd7aed7ccc813..6407e0d6d50332c89109d526ebbd7599a5aefedc 100644 (file)
--- 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 );
 }