From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 7 Apr 2020 03:48:13 +0000 (-0500)
Subject: Cleanup deprecated quantifiers attribute features (#4215)
X-Git-Tag: cvc5-1.0.0~3398
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=82f5610afdf5a45404e6acecfc117bb29f98963f;p=cvc5.git

Cleanup deprecated quantifiers attribute features (#4215)
---

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 );
 }