Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/quantifiers_attributes.cpp	Lines:	170	229	74.2 %
Date:	2021-09-30	Branches:	395	920	42.9 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Paul Meng, Morgan Deters
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Implementation of QuantifiersAttributes class.
 */

#include "theory/quantifiers/quantifiers_attributes.h"

#include "options/quantifiers_options.h"
#include "theory/arith/arith_msum.h"
#include "theory/quantifiers/sygus/synth_engine.h"
#include "theory/quantifiers/term_util.h"
#include "util/rational.h"
#include "util/string.h"

using namespace std;
using namespace cvc5::kind;
using namespace cvc5::context;

namespace cvc5 {
namespace theory {
namespace quantifiers {

bool QAttributes::isStandard() const
{
  return !d_sygus && !d_quant_elim && !isFunDef() && !d_isInternal;
}

QuantAttributes::QuantAttributes() {}

void QuantAttributes::setUserAttribute(const std::string& attr,
                                       TNode n,
                                       const std::vector<Node>& nodeValues)
{
  Trace("quant-attr-debug") << "Set " << attr << " " << n << std::endl;
  if (attr == "fun-def")
  {
    Trace("quant-attr-debug") << "Set function definition " << n << std::endl;
    FunDefAttribute fda;
    n.setAttribute( fda, true );
  }
  else if (attr == "qid")
  {
    // using z3 syntax "qid"
    Trace("quant-attr-debug") << "Set quant-name " << n << std::endl;
    QuantNameAttribute qna;
    n.setAttribute(qna, true);
  }else if( attr=="quant-inst-max-level" ){
    Assert(nodeValues.size() == 1);
    uint64_t lvl = nodeValues[0].getConst<Rational>().getNumerator().getLong();
    Trace("quant-attr-debug") << "Set instantiation level " << n << " to " << lvl << std::endl;
    QuantInstLevelAttribute qila;
    n.setAttribute( qila, lvl );
  }else if( attr=="quant-elim" ){
    Trace("quant-attr-debug") << "Set quantifier elimination " << n << std::endl;
    QuantElimAttribute qea;
    n.setAttribute( qea, true );
  }else if( attr=="quant-elim-partial" ){
    Trace("quant-attr-debug") << "Set partial quantifier elimination " << n << std::endl;
    QuantElimPartialAttribute qepa;
    n.setAttribute( qepa, true );
  }
}

bool QuantAttributes::checkFunDef( Node q ) {
  return !getFunDefHead( q ).isNull();
}

bool QuantAttributes::checkFunDefAnnotation( Node ipl ) {
  if( !ipl.isNull() ){
    for( unsigned i=0; i<ipl.getNumChildren(); i++ ){
      if( ipl[i].getKind()==INST_ATTRIBUTE ){
        if( ipl[i][0].getAttribute(FunDefAttribute()) ){
          return true;
        }
      }
    }
  }
  return false;
}

Node QuantAttributes::getFunDefHead( Node q ) {
  //&& q[1].getKind()==EQUAL && q[1][0].getKind()==APPLY_UF &&
  if( q.getKind()==FORALL && q.getNumChildren()==3 ){
    Node ipl = q[2];
    for (unsigned i = 0; i < ipl.getNumChildren(); i++)
    {
      if (ipl[i].getKind() == INST_ATTRIBUTE
          && ipl[i][0].getAttribute(FunDefAttribute()))
      {
        return ipl[i][0];
      }
    }
  }
  return Node::null();
}
Node QuantAttributes::getFunDefBody( Node q ) {
  Node h = getFunDefHead( q );
  if( !h.isNull() ){
    if( q[1].getKind()==EQUAL ){
      if( q[1][0]==h ){
        return q[1][1];
      }else if( q[1][1]==h ){
        return q[1][0];
      }
      else if (q[1][0].getType().isReal())
      {
        // solve for h in the equality
        std::map<Node, Node> msum;
        if (ArithMSum::getMonomialSumLit(q[1], msum))
        {
          Node veq;
          int res = ArithMSum::isolate(h, msum, veq, EQUAL);
          if (res != 0)
          {
            Assert(veq.getKind() == EQUAL);
            return res == 1 ? veq[1] : veq[0];
          }
        }
      }
    }else{
      Node atom = q[1].getKind()==NOT ? q[1][0] : q[1];
      bool pol = q[1].getKind()!=NOT;
      if( atom==h ){
        return NodeManager::currentNM()->mkConst( pol );
      }
    }
  }
  return Node::null();
}

bool QuantAttributes::checkSygusConjecture( Node q ) {
  return ( q.getKind()==FORALL && q.getNumChildren()==3 ) ? checkSygusConjectureAnnotation( q[2] ) : false;
}

bool QuantAttributes::checkSygusConjectureAnnotation( Node ipl ){
  if( !ipl.isNull() ){
    for( unsigned i=0; i<ipl.getNumChildren(); i++ ){
      if( ipl[i].getKind()==INST_ATTRIBUTE ){
        Node avar = ipl[i][0];
        if( avar.getAttribute(SygusAttribute()) ){
          return true;
        }
      }
    }
  }
  return false;
}

bool QuantAttributes::checkQuantElimAnnotation( Node ipl ) {
  if( !ipl.isNull() ){
    for( unsigned i=0; i<ipl.getNumChildren(); i++ ){
      if( ipl[i].getKind()==INST_ATTRIBUTE ){
        Node avar = ipl[i][0];
        if( avar.getAttribute(QuantElimAttribute()) ){
          return true;
        }
      }
    }
  }
  return false;
}

bool QuantAttributes::hasPattern(Node q)
{
  Assert(q.getKind() == FORALL);
  if (q.getNumChildren() != 3)
  {
    return false;
  }
  for (const Node& qc : q[2])
  {
    if (qc.getKind() == INST_PATTERN || qc.getKind() == INST_NO_PATTERN)
    {
      return true;
    }
  }
  return false;
}

void QuantAttributes::computeAttributes( Node q ) {
  computeQuantAttributes( q, d_qattr[q] );
  QAttributes& qa = d_qattr[q];
  if (qa.isFunDef())
  {
    Node f = qa.d_fundef_f;
    if( d_fun_defs.find( f )!=d_fun_defs.end() ){
      CVC5Message() << "Cannot define function " << f << " more than once."
                    << std::endl;
      AlwaysAssert(false);
    }
    d_fun_defs[f] = true;
  }
}

void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){
  Trace("quant-attr-debug") << "Compute attributes for " << q << std::endl;
  if( q.getNumChildren()==3 ){
    NodeManager* nm = NodeManager::currentNM();
    qa.d_ipl = q[2];
    for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
      Kind k = q[2][i].getKind();
      Trace("quant-attr-debug")
          << "Check : " << q[2][i] << " " << k << std::endl;
      if (k == INST_PATTERN || k == INST_NO_PATTERN)
      {
        qa.d_hasPattern = true;
      }
      else if (k == INST_POOL || k == INST_ADD_TO_POOL
               || k == SKOLEM_ADD_TO_POOL)
      {
        qa.d_hasPool = true;
      }
      else if (k == INST_ATTRIBUTE)
      {
        Node avar;
        // We support two use cases of INST_ATTRIBUTE:
        // (1) where the user constructs a term of the form
        // (INST_ATTRIBUTE "keyword" [nodeValues])
        // (2) where we internally generate nodes of the form
        // (INST_ATTRIBUTE v) where v has an internal attribute set on it.
        // We distinguish these two cases by checking the kind of the first
        // child.
        if (q[2][i][0].getKind() == CONST_STRING)
        {
          // make a dummy variable to be used below
          avar = nm->mkBoundVar(nm->booleanType());
          std::vector<Node> nodeValues(q[2][i].begin() + 1, q[2][i].end());
          // set user attribute on the dummy variable
          setUserAttribute(
              q[2][i][0].getConst<String>().toString(), avar, nodeValues);
        }
        else
        {
          // assume the dummy variable has already had its attributes set
          avar = q[2][i][0];
        }
        if( avar.getAttribute(FunDefAttribute()) ){
          Trace("quant-attr") << "Attribute : function definition : " << q << std::endl;
          //get operator directly from pattern
          qa.d_fundef_f = q[2][i][0].getOperator();
        }
        if( avar.getAttribute(SygusAttribute()) ){
          //not necessarily nested existential
          //Assert( q[1].getKind()==NOT );
          //Assert( q[1][0].getKind()==FORALL );
          Trace("quant-attr") << "Attribute : sygus : " << q << std::endl;
          qa.d_sygus = true;
        }
        if (avar.hasAttribute(SygusSideConditionAttribute()))
        {
          qa.d_sygusSideCondition =
              avar.getAttribute(SygusSideConditionAttribute());
          Trace("quant-attr")
              << "Attribute : sygus side condition : "
              << qa.d_sygusSideCondition << " : " << q << std::endl;
        }
        if (avar.getAttribute(QuantNameAttribute()))
        {
          // only set the name if there is a value
          if (q[2][i].getNumChildren() > 1)
          {
            Trace("quant-attr") << "Attribute : quantifier name : "
                                << q[2][i][1].getConst<String>().toString()
                                << " for " << q << std::endl;
            // assign the name to a variable with the given name (to avoid
            // enclosing the name in quotes)
            qa.d_name = nm->mkBoundVar(q[2][i][1].getConst<String>().toString(),
                                       nm->booleanType());
          }
          else
          {
            Warning() << "Missing name for qid attribute";
          }
        }
        if( avar.hasAttribute(QuantInstLevelAttribute()) ){
          qa.d_qinstLevel = avar.getAttribute(QuantInstLevelAttribute());
          Trace("quant-attr") << "Attribute : quant inst level " << qa.d_qinstLevel << " : " << q << std::endl;
        }
        if( avar.getAttribute(QuantElimAttribute()) ){
          Trace("quant-attr") << "Attribute : quantifier elimination : " << q << std::endl;
          qa.d_quant_elim = true;
          //don't set owner, should happen naturally
        }
        if( avar.getAttribute(QuantElimPartialAttribute()) ){
          Trace("quant-attr") << "Attribute : quantifier elimination partial : " << q << std::endl;
          qa.d_quant_elim = true;
          qa.d_quant_elim_partial = true;
          //don't set owner, should happen naturally
        }
        if (avar.getAttribute(InternalQuantAttribute()))
        {
          Trace("quant-attr") << "Attribute : internal : " << q << std::endl;
          qa.d_isInternal = true;
        }
        if( avar.hasAttribute(QuantIdNumAttribute()) ){
          qa.d_qid_num = avar;
          Trace("quant-attr") << "Attribute : id number " << qa.d_qid_num.getAttribute(QuantIdNumAttribute()) << " : " << q << std::endl;
        }
      }
    }
  }
}

bool QuantAttributes::isFunDef( Node q ) {
  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
  if( it==d_qattr.end() ){
    return false;
  }else{
    return it->second.isFunDef();
  }
}

bool QuantAttributes::isSygus( Node q ) {
  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
  if( it==d_qattr.end() ){
    return false;
  }else{
    return it->second.d_sygus;
  }
}

int64_t QuantAttributes::getQuantInstLevel(Node q)
{
  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
  if( it==d_qattr.end() ){
    return -1;
  }else{
    return it->second.d_qinstLevel;
  }
}

bool QuantAttributes::isQuantElim( Node q ) {
  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
  if( it==d_qattr.end() ){
    return false;
  }else{
    return it->second.d_quant_elim;
  }
}

bool QuantAttributes::isQuantElimPartial( Node q ) {
  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
  if( it==d_qattr.end() ){
    return false;
  }else{
    return it->second.d_quant_elim_partial;
  }
}

bool QuantAttributes::isInternal(Node q) const
{
  std::map<Node, QAttributes>::const_iterator it = d_qattr.find(q);
  if (it != d_qattr.end())
  {
    return it->second.d_isInternal;
  }
  return false;
}

Node QuantAttributes::getQuantName(Node q) const
{
  std::map<Node, QAttributes>::const_iterator it = d_qattr.find(q);
  if (it != d_qattr.end())
  {
    return it->second.d_name;
  }
  return Node::null();
}

std::string QuantAttributes::quantToString(Node q) const
{
  std::stringstream ss;
  Node name = getQuantName(q);
  ss << (name.isNull() ? q : name);
  return ss.str();
}

int QuantAttributes::getQuantIdNum( Node q ) {
  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
  if( it!=d_qattr.end() ){
    if( !it->second.d_qid_num.isNull() ){
      return it->second.d_qid_num.getAttribute(QuantIdNumAttribute());
    }
  }
  return -1;
}

Node QuantAttributes::getQuantIdNumNode( Node q ) {
  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
  if( it==d_qattr.end() ){
    return Node::null();
  }else{
    return it->second.d_qid_num;
  }
}

void QuantAttributes::setInstantiationLevelAttr(Node n, Node qn, uint64_t level)
{
  Trace("inst-level-debug2") << "IL : " << n << " " << qn << " " << level
                             << std::endl;
  // if not from the vector of terms we instantiatied
  if (qn.getKind() != BOUND_VARIABLE && n != qn)
  {
    // if this is a new term, without an instantiation level
    if (!n.hasAttribute(InstLevelAttribute()))
    {
      InstLevelAttribute ila;
      n.setAttribute(ila, level);
      Trace("inst-level-debug") << "Set instantiation level " << n << " to "
                                << level << std::endl;
      Assert(n.getNumChildren() == qn.getNumChildren());
      for (unsigned i = 0; i < n.getNumChildren(); i++)
      {
        setInstantiationLevelAttr(n[i], qn[i], level);
      }
    }
  }
}

void QuantAttributes::setInstantiationLevelAttr(Node n, uint64_t level)
{
  if (!n.hasAttribute(InstLevelAttribute()))
  {
    InstLevelAttribute ila;
    n.setAttribute(ila, level);
    Trace("inst-level-debug") << "Set instantiation level " << n << " to "
                              << level << std::endl;
    for (unsigned i = 0; i < n.getNumChildren(); i++)
    {
      setInstantiationLevelAttr(n[i], level);
    }
  }
}

}  // namespace quantifiers
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Paul Meng, Morgan Deters
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Implementation of QuantifiersAttributes class.
14		*/
15
16		#include "theory/quantifiers/quantifiers_attributes.h"
17
18		#include "options/quantifiers_options.h"
19		#include "theory/arith/arith_msum.h"
20		#include "theory/quantifiers/sygus/synth_engine.h"
21		#include "theory/quantifiers/term_util.h"
22		#include "util/rational.h"
23		#include "util/string.h"
24
25		using namespace std;
26		using namespace cvc5::kind;
27		using namespace cvc5::context;
28
29		namespace cvc5 {
30		namespace theory {
31		namespace quantifiers {
32
33	451662	bool QAttributes::isStandard() const
34		{
35	451662	return !d_sygus && !d_quant_elim && !isFunDef() && !d_isInternal;
36		}
37
38	6278	QuantAttributes::QuantAttributes() {}
39
40	1093	void QuantAttributes::setUserAttribute(const std::string& attr,
41		TNode n,
42		const std::vector<Node>& nodeValues)
43		{
44	1093	Trace("quant-attr-debug") << "Set " << attr << " " << n << std::endl;
45	1093	if (attr == "fun-def")
46		{
47		Trace("quant-attr-debug") << "Set function definition " << n << std::endl;
48		FunDefAttribute fda;
49		n.setAttribute( fda, true );
50		}
51	1093	else if (attr == "qid")
52		{
53		// using z3 syntax "qid"
54	987	Trace("quant-attr-debug") << "Set quant-name " << n << std::endl;
55		QuantNameAttribute qna;
56	987	n.setAttribute(qna, true);
57	106	}else if( attr=="quant-inst-max-level" ){
58		Assert(nodeValues.size() == 1);
59		uint64_t lvl = nodeValues[0].getConst<Rational>().getNumerator().getLong();
60		Trace("quant-attr-debug") << "Set instantiation level " << n << " to " << lvl << std::endl;
61		QuantInstLevelAttribute qila;
62		n.setAttribute( qila, lvl );
63	106	}else if( attr=="quant-elim" ){
64	88	Trace("quant-attr-debug") << "Set quantifier elimination " << n << std::endl;
65		QuantElimAttribute qea;
66	88	n.setAttribute( qea, true );
67	18	}else if( attr=="quant-elim-partial" ){
68	17	Trace("quant-attr-debug") << "Set partial quantifier elimination " << n << std::endl;
69		QuantElimPartialAttribute qepa;
70	17	n.setAttribute( qepa, true );
71		}
72	1093	}
73
74		bool QuantAttributes::checkFunDef( Node q ) {
75		return !getFunDefHead( q ).isNull();
76		}
77
78		bool QuantAttributes::checkFunDefAnnotation( Node ipl ) {
79		if( !ipl.isNull() ){
80		for( unsigned i=0; i<ipl.getNumChildren(); i++ ){
81		if( ipl[i].getKind()==INST_ATTRIBUTE ){
82		if( ipl[i][0].getAttribute(FunDefAttribute()) ){
83		return true;
84		}
85		}
86		}
87		}
88		return false;
89		}
90
91	422	Node QuantAttributes::getFunDefHead( Node q ) {
92		//&& q[1].getKind()==EQUAL && q[1][0].getKind()==APPLY_UF &&
93	422	if( q.getKind()==FORALL && q.getNumChildren()==3 ){
94	186	Node ipl = q[2];
95	186	for (unsigned i = 0; i < ipl.getNumChildren(); i++)
96		{
97	552	if (ipl[i].getKind() == INST_ATTRIBUTE
98	552	&& ipl[i][0].getAttribute(FunDefAttribute()))
99		{
100	182	return ipl[i][0];
101		}
102		}
103		}
104	240	return Node::null();
105		}
106	91	Node QuantAttributes::getFunDefBody( Node q ) {
107	182	Node h = getFunDefHead( q );
108	91	if( !h.isNull() ){
109	91	if( q[1].getKind()==EQUAL ){
110	86	if( q[1][0]==h ){
111	41	return q[1][1];
112	45	}else if( q[1][1]==h ){
113	44	return q[1][0];
114		}
115	1	else if (q[1][0].getType().isReal())
116		{
117		// solve for h in the equality
118	1	std::map<Node, Node> msum;
119	1	if (ArithMSum::getMonomialSumLit(q[1], msum))
120		{
121	1	Node veq;
122	1	int res = ArithMSum::isolate(h, msum, veq, EQUAL);
123	1	if (res != 0)
124		{
125	1	Assert(veq.getKind() == EQUAL);
126	1	return res == 1 ? veq[1] : veq[0];
127		}
128		}
129		}
130		}else{
131	5	Node atom = q[1].getKind()==NOT ? q[1][0] : q[1];
132	5	bool pol = q[1].getKind()!=NOT;
133	5	if( atom==h ){
134	5	return NodeManager::currentNM()->mkConst( pol );
135		}
136		}
137		}
138		return Node::null();
139		}
140
141	2519	bool QuantAttributes::checkSygusConjecture( Node q ) {
142	2519	return ( q.getKind()==FORALL && q.getNumChildren()==3 ) ? checkSygusConjectureAnnotation( q[2] ) : false;
143		}
144
145	420	bool QuantAttributes::checkSygusConjectureAnnotation( Node ipl ){
146	420	if( !ipl.isNull() ){
147	510	for( unsigned i=0; i<ipl.getNumChildren(); i++ ){
148	420	if( ipl[i].getKind()==INST_ATTRIBUTE ){
149	510	Node avar = ipl[i][0];
150	420	if( avar.getAttribute(SygusAttribute()) ){
151	330	return true;
152		}
153		}
154		}
155		}
156	90	return false;
157		}
158
159		bool QuantAttributes::checkQuantElimAnnotation( Node ipl ) {
160		if( !ipl.isNull() ){
161		for( unsigned i=0; i<ipl.getNumChildren(); i++ ){
162		if( ipl[i].getKind()==INST_ATTRIBUTE ){
163		Node avar = ipl[i][0];
164		if( avar.getAttribute(QuantElimAttribute()) ){
165		return true;
166		}
167		}
168		}
169		}
170		return false;
171		}
172
173	1057	bool QuantAttributes::hasPattern(Node q)
174		{
175	1057	Assert(q.getKind() == FORALL);
176	1057	if (q.getNumChildren() != 3)
177		{
178	989	return false;
179		}
180	79	for (const Node& qc : q[2])
181		{
182	71	if (qc.getKind() == INST_PATTERN \|\| qc.getKind() == INST_NO_PATTERN)
183		{
184	60	return true;
185		}
186		}
187	8	return false;
188		}
189
190	10540	void QuantAttributes::computeAttributes( Node q ) {
191	10540	computeQuantAttributes( q, d_qattr[q] );
192	10540	QAttributes& qa = d_qattr[q];
193	10540	if (qa.isFunDef())
194		{
195	192	Node f = qa.d_fundef_f;
196	96	if( d_fun_defs.find( f )!=d_fun_defs.end() ){
197		CVC5Message() << "Cannot define function " << f << " more than once."
198		<< std::endl;
199		AlwaysAssert(false);
200		}
201	96	d_fun_defs[f] = true;
202		}
203	10540	}
204
205	86960	void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){
206	86960	Trace("quant-attr-debug") << "Compute attributes for " << q << std::endl;
207	86960	if( q.getNumChildren()==3 ){
208	14860	NodeManager* nm = NodeManager::currentNM();
209	14860	qa.d_ipl = q[2];
210	30992	for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
211	16132	Kind k = q[2][i].getKind();
212	32264	Trace("quant-attr-debug")
213	16132	<< "Check : " << q[2][i] << " " << k << std::endl;
214	16132	if (k == INST_PATTERN \|\| k == INST_NO_PATTERN)
215		{
216	9026	qa.d_hasPattern = true;
217		}
218	7106	else if (k == INST_POOL \|\| k == INST_ADD_TO_POOL
219	7092	\|\| k == SKOLEM_ADD_TO_POOL)
220		{
221	28	qa.d_hasPool = true;
222		}
223	7078	else if (k == INST_ATTRIBUTE)
224		{
225	14156	Node avar;
226		// We support two use cases of INST_ATTRIBUTE:
227		// (1) where the user constructs a term of the form
228		// (INST_ATTRIBUTE "keyword" [nodeValues])
229		// (2) where we internally generate nodes of the form
230		// (INST_ATTRIBUTE v) where v has an internal attribute set on it.
231		// We distinguish these two cases by checking the kind of the first
232		// child.
233	7078	if (q[2][i][0].getKind() == CONST_STRING)
234		{
235		// make a dummy variable to be used below
236	1093	avar = nm->mkBoundVar(nm->booleanType());
237	2186	std::vector<Node> nodeValues(q[2][i].begin() + 1, q[2][i].end());
238		// set user attribute on the dummy variable
239	3279	setUserAttribute(
240	2186	q[2][i][0].getConst<String>().toString(), avar, nodeValues);
241		}
242		else
243		{
244		// assume the dummy variable has already had its attributes set
245	5985	avar = q[2][i][0];
246		}
247	7078	if( avar.getAttribute(FunDefAttribute()) ){
248	732	Trace("quant-attr") << "Attribute : function definition : " << q << std::endl;
249		//get operator directly from pattern
250	732	qa.d_fundef_f = q[2][i][0].getOperator();
251		}
252	7078	if( avar.getAttribute(SygusAttribute()) ){
253		//not necessarily nested existential
254		//Assert( q[1].getKind()==NOT );
255		//Assert( q[1][0].getKind()==FORALL );
256	2385	Trace("quant-attr") << "Attribute : sygus : " << q << std::endl;
257	2385	qa.d_sygus = true;
258		}
259	7078	if (avar.hasAttribute(SygusSideConditionAttribute()))
260		{
261	140	qa.d_sygusSideCondition =
262	280	avar.getAttribute(SygusSideConditionAttribute());
263	280	Trace("quant-attr")
264	140	<< "Attribute : sygus side condition : "
265	140	<< qa.d_sygusSideCondition << " : " << q << std::endl;
266		}
267	7078	if (avar.getAttribute(QuantNameAttribute()))
268		{
269		// only set the name if there is a value
270	987	if (q[2][i].getNumChildren() > 1)
271		{
272	1974	Trace("quant-attr") << "Attribute : quantifier name : "
273	1974	<< q[2][i][1].getConst<String>().toString()
274	987	<< " for " << q << std::endl;
275		// assign the name to a variable with the given name (to avoid
276		// enclosing the name in quotes)
277	1974	qa.d_name = nm->mkBoundVar(q[2][i][1].getConst<String>().toString(),
278	2961	nm->booleanType());
279		}
280		else
281		{
282		Warning() << "Missing name for qid attribute";
283		}
284		}
285	7078	if( avar.hasAttribute(QuantInstLevelAttribute()) ){
286		qa.d_qinstLevel = avar.getAttribute(QuantInstLevelAttribute());
287		Trace("quant-attr") << "Attribute : quant inst level " << qa.d_qinstLevel << " : " << q << std::endl;
288		}
289	7078	if( avar.getAttribute(QuantElimAttribute()) ){
290	344	Trace("quant-attr") << "Attribute : quantifier elimination : " << q << std::endl;
291	344	qa.d_quant_elim = true;
292		//don't set owner, should happen naturally
293		}
294	7078	if( avar.getAttribute(QuantElimPartialAttribute()) ){
295	17	Trace("quant-attr") << "Attribute : quantifier elimination partial : " << q << std::endl;
296	17	qa.d_quant_elim = true;
297	17	qa.d_quant_elim_partial = true;
298		//don't set owner, should happen naturally
299		}
300	7078	if (avar.getAttribute(InternalQuantAttribute()))
301		{
302	2197	Trace("quant-attr") << "Attribute : internal : " << q << std::endl;
303	2197	qa.d_isInternal = true;
304		}
305	7078	if( avar.hasAttribute(QuantIdNumAttribute()) ){
306		qa.d_qid_num = avar;
307		Trace("quant-attr") << "Attribute : id number " << qa.d_qid_num.getAttribute(QuantIdNumAttribute()) << " : " << q << std::endl;
308		}
309		}
310		}
311		}
312	86960	}
313
314	777	bool QuantAttributes::isFunDef( Node q ) {
315	777	std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
316	777	if( it==d_qattr.end() ){
317		return false;
318		}else{
319	777	return it->second.isFunDef();
320		}
321		}
322
323	1070	bool QuantAttributes::isSygus( Node q ) {
324	1070	std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
325	1070	if( it==d_qattr.end() ){
326		return false;
327		}else{
328	1070	return it->second.d_sygus;
329		}
330		}
331
332	260	int64_t QuantAttributes::getQuantInstLevel(Node q)
333		{
334	260	std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
335	260	if( it==d_qattr.end() ){
336		return -1;
337		}else{
338	260	return it->second.d_qinstLevel;
339		}
340		}
341
342		bool QuantAttributes::isQuantElim( Node q ) {
343		std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
344		if( it==d_qattr.end() ){
345		return false;
346		}else{
347		return it->second.d_quant_elim;
348		}
349		}
350
351	5628	bool QuantAttributes::isQuantElimPartial( Node q ) {
352	5628	std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
353	5628	if( it==d_qattr.end() ){
354		return false;
355		}else{
356	5628	return it->second.d_quant_elim_partial;
357		}
358		}
359
360	27009	bool QuantAttributes::isInternal(Node q) const
361		{
362	27009	std::map<Node, QAttributes>::const_iterator it = d_qattr.find(q);
363	27009	if (it != d_qattr.end())
364		{
365	27009	return it->second.d_isInternal;
366		}
367		return false;
368		}
369
370	12	Node QuantAttributes::getQuantName(Node q) const
371		{
372	12	std::map<Node, QAttributes>::const_iterator it = d_qattr.find(q);
373	12	if (it != d_qattr.end())
374		{
375	12	return it->second.d_name;
376		}
377		return Node::null();
378		}
379
380		std::string QuantAttributes::quantToString(Node q) const
381		{
382		std::stringstream ss;
383		Node name = getQuantName(q);
384		ss << (name.isNull() ? q : name);
385		return ss.str();
386		}
387
388		int QuantAttributes::getQuantIdNum( Node q ) {
389		std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
390		if( it!=d_qattr.end() ){
391		if( !it->second.d_qid_num.isNull() ){
392		return it->second.d_qid_num.getAttribute(QuantIdNumAttribute());
393		}
394		}
395		return -1;
396		}
397
398		Node QuantAttributes::getQuantIdNumNode( Node q ) {
399		std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
400		if( it==d_qattr.end() ){
401		return Node::null();
402		}else{
403		return it->second.d_qid_num;
404		}
405		}
406
407	893	void QuantAttributes::setInstantiationLevelAttr(Node n, Node qn, uint64_t level)
408		{
409	1786	Trace("inst-level-debug2") << "IL : " << n << " " << qn << " " << level
410	893	<< std::endl;
411		// if not from the vector of terms we instantiatied
412	893	if (qn.getKind() != BOUND_VARIABLE && n != qn)
413		{
414		// if this is a new term, without an instantiation level
415	650	if (!n.hasAttribute(InstLevelAttribute()))
416		{
417		InstLevelAttribute ila;
418	383	n.setAttribute(ila, level);
419	766	Trace("inst-level-debug") << "Set instantiation level " << n << " to "
420	383	<< level << std::endl;
421	383	Assert(n.getNumChildren() == qn.getNumChildren());
422	1183	for (unsigned i = 0; i < n.getNumChildren(); i++)
423		{
424	800	setInstantiationLevelAttr(n[i], qn[i], level);
425		}
426		}
427		}
428	893	}
429
430	688	void QuantAttributes::setInstantiationLevelAttr(Node n, uint64_t level)
431		{
432	688	if (!n.hasAttribute(InstLevelAttribute()))
433		{
434		InstLevelAttribute ila;
435	368	n.setAttribute(ila, level);
436	736	Trace("inst-level-debug") << "Set instantiation level " << n << " to "
437	368	<< level << std::endl;
438	991	for (unsigned i = 0; i < n.getNumChildren(); i++)
439		{
440	623	setInstantiationLevelAttr(n[i], level);
441		}
442		}
443	688	}
444
445		} // namespace quantifiers
446		} // namespace theory
447	22755	} // namespace cvc5