Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/first_order_model.cpp	Lines:	161	180	89.4 %
Date:	2021-09-17	Branches:	247	536	46.1 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Aina Niemetz
 *
 * 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 model engine model class.
 */

#include "theory/quantifiers/first_order_model.h"
#include "options/base_options.h"
#include "options/quantifiers_options.h"
#include "theory/quantifiers/fmf/bounded_integers.h"
#include "theory/quantifiers/fmf/model_engine.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_enumeration.h"
#include "theory/quantifiers/term_registry.h"
#include "theory/quantifiers/term_util.h"

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

namespace cvc5 {
namespace theory {
namespace quantifiers {

struct ModelBasisAttributeId
{
};
using ModelBasisAttribute = expr::Attribute<ModelBasisAttributeId, bool>;
// for APPLY_UF terms, 1 : term has direct child with model basis attribute,
//                     0 : term has no direct child with model basis attribute.
struct ModelBasisArgAttributeId
{
};
using ModelBasisArgAttribute = expr::Attribute<ModelBasisArgAttributeId, uint64_t>;

FirstOrderModel::FirstOrderModel(Env& env,
                                 QuantifiersState& qs,
                                 QuantifiersRegistry& qr,
                                 TermRegistry& tr)
    : EnvObj(env),
      d_model(nullptr),
      d_qreg(qr),
      d_treg(tr),
      d_eq_query(env, qs, this),
      d_forall_asserts(context()),
      d_forallRlvComputed(false)
{
}

void FirstOrderModel::finishInit(TheoryModel* m) { d_model = m; }

Node FirstOrderModel::getValue(TNode n) const { return d_model->getValue(n); }
bool FirstOrderModel::hasTerm(TNode a) { return d_model->hasTerm(a); }
Node FirstOrderModel::getRepresentative(TNode a)
{
  return d_model->getRepresentative(a);
}
bool FirstOrderModel::areEqual(TNode a, TNode b)
{
  return d_model->areEqual(a, b);
}
bool FirstOrderModel::areDisequal(TNode a, TNode b)
{
  return d_model->areDisequal(a, b);
}
eq::EqualityEngine* FirstOrderModel::getEqualityEngine()
{
  return d_model->getEqualityEngine();
}
const RepSet* FirstOrderModel::getRepSet() const
{
  return d_model->getRepSet();
}
RepSet* FirstOrderModel::getRepSetPtr() { return d_model->getRepSetPtr(); }
TheoryModel* FirstOrderModel::getTheoryModel() { return d_model; }

Node FirstOrderModel::getInternalRepresentative(Node a, Node q, size_t index)
{
  return d_eq_query.getInternalRepresentative(a, q, index);
}

void FirstOrderModel::assertQuantifier( Node n ){
  if( n.getKind()==FORALL ){
    d_forall_asserts.push_back( n );
  }else if( n.getKind()==NOT ){
    Assert(n[0].getKind() == FORALL);
  }
}

size_t FirstOrderModel::getNumAssertedQuantifiers() const
{
  return d_forall_asserts.size();
}

Node FirstOrderModel::getAssertedQuantifier( unsigned i, bool ordered ) {
  if( !ordered || !d_forallRlvComputed ){
    return d_forall_asserts[i];
  }
  // If we computed the relevant forall assertion vector, in reset_round,
  // then it should have the same size as the default assertion vector.
  Assert(d_forall_rlv_assert.size() == d_forall_asserts.size());
  return d_forall_rlv_assert[i];
}

void FirstOrderModel::initialize() {
  processInitialize( true );
  //this is called after representatives have been chosen and the equality engine has been built
  //for each quantifier, collect all operators we care about
  for( unsigned i=0; i<getNumAssertedQuantifiers(); i++ ){
    Node f = getAssertedQuantifier( i );
    if( d_quant_var_id.find( f )==d_quant_var_id.end() ){
      for(unsigned j=0; j<f[0].getNumChildren(); j++){
        d_quant_var_id[f][f[0][j]] = j;
      }
    }
    processInitializeQuantifier( f );
    //initialize relevant models within bodies of all quantifiers
    std::map< Node, bool > visited;
    initializeModelForTerm( f[1], visited );
  }
  processInitialize( false );
}

void FirstOrderModel::initializeModelForTerm( Node n, std::map< Node, bool >& visited ){
  if( visited.find( n )==visited.end() ){
    visited[n] = true;
    processInitializeModelForTerm( n );
    for( int i=0; i<(int)n.getNumChildren(); i++ ){
      initializeModelForTerm( n[i], visited );
    }
  }
}

Node FirstOrderModel::getSomeDomainElement(TypeNode tn){
  //check if there is even any domain elements at all
  RepSet* rs = d_model->getRepSetPtr();
  if (!rs->hasType(tn) || rs->getNumRepresentatives(tn) == 0)
  {
    Trace("fm-debug") << "Must create domain element for " << tn << "..."
                      << std::endl;
    Node mbt = getModelBasisTerm(tn);
    Trace("fm-debug") << "Add to representative set..." << std::endl;
    rs->add(tn, mbt);
  }
  return rs->getRepresentative(tn, 0);
}

bool FirstOrderModel::initializeRepresentativesForType(TypeNode tn)
{
  RepSet* rs = d_model->getRepSetPtr();
  if (tn.isSort())
  {
    // must ensure uninterpreted type is non-empty.
    if (!rs->hasType(tn))
    {
      // terms in rep_set are now constants which mapped to terms through
      // TheoryModel. Thus, should introduce a constant and a term.
      // For now, we just add an arbitrary term.
      Node var = getSomeDomainElement(tn);
      Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn
                     << std::endl;
      rs->add(tn, var);
    }
    return true;
  }
  else
  {
    // can we complete it?
    if (d_qreg.getQuantifiersBoundInference().mayComplete(tn))
    {
      Trace("fm-debug") << "  do complete, since cardinality is small ("
                        << tn.getCardinality() << ")..." << std::endl;
      rs->complete(tn);
      // must have succeeded
      Assert(rs->hasType(tn));
      return true;
    }
    Trace("fm-debug") << "  variable cannot be bounded." << std::endl;
    return false;
  }
}

bool FirstOrderModel::isModelBasis(TNode n)
{
  return n.getAttribute(ModelBasisAttribute());
}

EqualityQuery* FirstOrderModel::getEqualityQuery() { return &d_eq_query; }

/** needs check */
bool FirstOrderModel::checkNeeded() {
  return d_forall_asserts.size()>0;
}

void FirstOrderModel::reset_round() {
  d_quant_active.clear();

  // compute which quantified formulas are asserted if necessary
  std::map<Node, bool> qassert;
  if (!d_forall_rlv_vec.empty())
  {
    Trace("fm-relevant-debug")
        << "Mark asserted quantified formulas..." << std::endl;
    for (const Node& q : d_forall_asserts)
    {
      qassert[q] = true;
    }
  }
  //order the quantified formulas
  d_forall_rlv_assert.clear();
  d_forallRlvComputed = false;
  if( !d_forall_rlv_vec.empty() ){
    d_forallRlvComputed = true;
    Trace("fm-relevant") << "Build sorted relevant list..." << std::endl;
    Trace("fm-relevant-debug") << "Add relevant asserted formulas..." << std::endl;
    std::map<Node, bool>::iterator ita;
    for( int i=(int)(d_forall_rlv_vec.size()-1); i>=0; i-- ){
      Node q = d_forall_rlv_vec[i];
      ita = qassert.find(q);
      if (ita != qassert.end())
      {
        Trace("fm-relevant") << "   " << q << std::endl;
        d_forall_rlv_assert.push_back( q );
        qassert.erase(ita);
      }
    }
    Trace("fm-relevant-debug") << "Add remaining asserted formulas..." << std::endl;
    for (const Node& q : d_forall_asserts)
    {
      // if we didn't include it above
      if (qassert.find(q) != qassert.end())
      {
        d_forall_rlv_assert.push_back( q );
      }else{
        Trace("fm-relevant-debug") << "...already included " << q << std::endl;
      }
    }
    Trace("fm-relevant-debug") << "Sizes : " << d_forall_rlv_assert.size() << " " << d_forall_asserts.size() << std::endl;
    Assert(d_forall_rlv_assert.size() == d_forall_asserts.size());
  }
}

void FirstOrderModel::markRelevant( Node q ) {
  // Put q on the back of the vector d_forall_rlv_vec.
  // If we were the last quantifier marked relevant, this is a no-op, return.
  if( q!=d_last_forall_rlv ){
    Trace("fm-relevant") << "Mark relevant : " << q << std::endl;
    std::vector<Node>::iterator itr =
        std::find(d_forall_rlv_vec.begin(), d_forall_rlv_vec.end(), q);
    if (itr != d_forall_rlv_vec.end())
    {
      d_forall_rlv_vec.erase(itr, itr + 1);
    }
    d_forall_rlv_vec.push_back(q);
    d_last_forall_rlv = q;
  }
}

void FirstOrderModel::setQuantifierActive( TNode q, bool active ) {
  d_quant_active[q] = active;
}

bool FirstOrderModel::isQuantifierActive(TNode q) const
{
  std::map<TNode, bool>::const_iterator it = d_quant_active.find(q);
  if( it==d_quant_active.end() ){
    return true;
  }
  return it->second;
}

bool FirstOrderModel::isQuantifierAsserted(TNode q) const
{
  return std::find( d_forall_asserts.begin(), d_forall_asserts.end(), q )!=d_forall_asserts.end();
}

Node FirstOrderModel::getModelBasisTerm(TypeNode tn)
{
  if (d_model_basis_term.find(tn) == d_model_basis_term.end())
  {
    Node mbt;
    if (tn.isClosedEnumerable())
    {
      mbt = d_treg.getTermEnumeration()->getEnumerateTerm(tn, 0);
    }
    else
    {
      if (options::fmfFreshDistConst())
      {
        mbt = d_treg.getTermDatabase()->getOrMakeTypeFreshVariable(tn);
      }
      else
      {
        // The model basis term cannot be an interpreted function, or else we
        // may produce an inconsistent model by choosing an arbitrary
        // equivalence class for it. Hence, we require that it be an existing or
        // fresh variable.
        mbt = d_treg.getTermDatabase()->getOrMakeTypeGroundTerm(tn, true);
      }
    }
    ModelBasisAttribute mba;
    mbt.setAttribute(mba, true);
    d_model_basis_term[tn] = mbt;
    Trace("model-basis-term") << "Choose " << mbt << " as model basis term for "
                              << tn << std::endl;
  }
  return d_model_basis_term[tn];
}

bool FirstOrderModel::isModelBasisTerm(Node n)
{
  return n == getModelBasisTerm(n.getType());
}

Node FirstOrderModel::getModelBasisOpTerm(Node op)
{
  if (d_model_basis_op_term.find(op) == d_model_basis_op_term.end())
  {
    TypeNode t = op.getType();
    std::vector<Node> children;
    children.push_back(op);
    for (int i = 0; i < (int)(t.getNumChildren() - 1); i++)
    {
      children.push_back(getModelBasisTerm(t[i]));
    }
    if (children.size() == 1)
    {
      d_model_basis_op_term[op] = op;
    }
    else
    {
      d_model_basis_op_term[op] =
          NodeManager::currentNM()->mkNode(APPLY_UF, children);
    }
  }
  return d_model_basis_op_term[op];
}

Node FirstOrderModel::getModelBasis(Node q, Node n)
{
  // make model basis
  if (d_model_basis_terms.find(q) == d_model_basis_terms.end())
  {
    for (unsigned j = 0; j < q[0].getNumChildren(); j++)
    {
      d_model_basis_terms[q].push_back(getModelBasisTerm(q[0][j].getType()));
    }
  }
  Node gn = d_qreg.substituteInstConstants(n, q, d_model_basis_terms[q]);
  return gn;
}

void FirstOrderModel::computeModelBasisArgAttribute(Node n)
{
  if (!n.hasAttribute(ModelBasisArgAttribute()))
  {
    // ensure that the model basis terms have been defined
    if (n.getKind() == APPLY_UF)
    {
      getModelBasisOpTerm(n.getOperator());
    }
    uint64_t val = 0;
    // determine if it has model basis attribute
    for (unsigned j = 0, nchild = n.getNumChildren(); j < nchild; j++)
    {
      if (n[j].getAttribute(ModelBasisAttribute()))
      {
        val++;
      }
    }
    ModelBasisArgAttribute mbaa;
    n.setAttribute(mbaa, val);
  }
}

unsigned FirstOrderModel::getModelBasisArg(Node n)
{
  computeModelBasisArgAttribute(n);
  return n.getAttribute(ModelBasisArgAttribute());
}

}  // 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, Aina Niemetz
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 model engine model class.
14		*/
15
16		#include "theory/quantifiers/first_order_model.h"
17		#include "options/base_options.h"
18		#include "options/quantifiers_options.h"
19		#include "theory/quantifiers/fmf/bounded_integers.h"
20		#include "theory/quantifiers/fmf/model_engine.h"
21		#include "theory/quantifiers/quantifiers_attributes.h"
22		#include "theory/quantifiers/term_database.h"
23		#include "theory/quantifiers/term_enumeration.h"
24		#include "theory/quantifiers/term_registry.h"
25		#include "theory/quantifiers/term_util.h"
26
27		using namespace cvc5::kind;
28		using namespace cvc5::context;
29
30		namespace cvc5 {
31		namespace theory {
32		namespace quantifiers {
33
34		struct ModelBasisAttributeId
35		{
36		};
37		using ModelBasisAttribute = expr::Attribute<ModelBasisAttributeId, bool>;
38		// for APPLY_UF terms, 1 : term has direct child with model basis attribute,
39		// 0 : term has no direct child with model basis attribute.
40		struct ModelBasisArgAttributeId
41		{
42		};
43		using ModelBasisArgAttribute = expr::Attribute<ModelBasisArgAttributeId, uint64_t>;
44
45	9942	FirstOrderModel::FirstOrderModel(Env& env,
46		QuantifiersState& qs,
47		QuantifiersRegistry& qr,
48	9942	TermRegistry& tr)
49		: EnvObj(env),
50		d_model(nullptr),
51		d_qreg(qr),
52		d_treg(tr),
53		d_eq_query(env, qs, this),
54		d_forall_asserts(context()),
55	9942	d_forallRlvComputed(false)
56		{
57	9942	}
58
59	6839	void FirstOrderModel::finishInit(TheoryModel* m) { d_model = m; }
60
61	129358	Node FirstOrderModel::getValue(TNode n) const { return d_model->getValue(n); }
62	8512	bool FirstOrderModel::hasTerm(TNode a) { return d_model->hasTerm(a); }
63	237486	Node FirstOrderModel::getRepresentative(TNode a)
64		{
65	237486	return d_model->getRepresentative(a);
66		}
67		bool FirstOrderModel::areEqual(TNode a, TNode b)
68		{
69		return d_model->areEqual(a, b);
70		}
71		bool FirstOrderModel::areDisequal(TNode a, TNode b)
72		{
73		return d_model->areDisequal(a, b);
74		}
75		eq::EqualityEngine* FirstOrderModel::getEqualityEngine()
76		{
77		return d_model->getEqualityEngine();
78		}
79	168061	const RepSet* FirstOrderModel::getRepSet() const
80		{
81	168061	return d_model->getRepSet();
82		}
83	11193	RepSet* FirstOrderModel::getRepSetPtr() { return d_model->getRepSetPtr(); }
84		TheoryModel* FirstOrderModel::getTheoryModel() { return d_model; }
85
86	76405	Node FirstOrderModel::getInternalRepresentative(Node a, Node q, size_t index)
87		{
88	76405	return d_eq_query.getInternalRepresentative(a, q, index);
89		}
90
91	68192	void FirstOrderModel::assertQuantifier( Node n ){
92	68192	if( n.getKind()==FORALL ){
93	68192	d_forall_asserts.push_back( n );
94		}else if( n.getKind()==NOT ){
95		Assert(n[0].getKind() == FORALL);
96		}
97	68192	}
98
99	101541	size_t FirstOrderModel::getNumAssertedQuantifiers() const
100		{
101	101541	return d_forall_asserts.size();
102		}
103
104	695416	Node FirstOrderModel::getAssertedQuantifier( unsigned i, bool ordered ) {
105	695416	if( !ordered \|\| !d_forallRlvComputed ){
106	462095	return d_forall_asserts[i];
107		}
108		// If we computed the relevant forall assertion vector, in reset_round,
109		// then it should have the same size as the default assertion vector.
110	233321	Assert(d_forall_rlv_assert.size() == d_forall_asserts.size());
111	233321	return d_forall_rlv_assert[i];
112		}
113
114	2038	void FirstOrderModel::initialize() {
115	2038	processInitialize( true );
116		//this is called after representatives have been chosen and the equality engine has been built
117		//for each quantifier, collect all operators we care about
118	11159	for( unsigned i=0; i<getNumAssertedQuantifiers(); i++ ){
119	18242	Node f = getAssertedQuantifier( i );
120	9121	if( d_quant_var_id.find( f )==d_quant_var_id.end() ){
121	3677	for(unsigned j=0; j<f[0].getNumChildren(); j++){
122	2191	d_quant_var_id[f][f[0][j]] = j;
123		}
124		}
125	9121	processInitializeQuantifier( f );
126		//initialize relevant models within bodies of all quantifiers
127	18242	std::map< Node, bool > visited;
128	9121	initializeModelForTerm( f[1], visited );
129		}
130	2038	processInitialize( false );
131	2038	}
132
133	219613	void FirstOrderModel::initializeModelForTerm( Node n, std::map< Node, bool >& visited ){
134	219613	if( visited.find( n )==visited.end() ){
135	158755	visited[n] = true;
136	158755	processInitializeModelForTerm( n );
137	369247	for( int i=0; i<(int)n.getNumChildren(); i++ ){
138	210492	initializeModelForTerm( n[i], visited );
139		}
140		}
141	219613	}
142
143	3562	Node FirstOrderModel::getSomeDomainElement(TypeNode tn){
144		//check if there is even any domain elements at all
145	3562	RepSet* rs = d_model->getRepSetPtr();
146	3562	if (!rs->hasType(tn) \|\| rs->getNumRepresentatives(tn) == 0)
147		{
148	246	Trace("fm-debug") << "Must create domain element for " << tn << "..."
149	123	<< std::endl;
150	246	Node mbt = getModelBasisTerm(tn);
151	123	Trace("fm-debug") << "Add to representative set..." << std::endl;
152	123	rs->add(tn, mbt);
153		}
154	3562	return rs->getRepresentative(tn, 0);
155		}
156
157	7490	bool FirstOrderModel::initializeRepresentativesForType(TypeNode tn)
158		{
159	7490	RepSet* rs = d_model->getRepSetPtr();
160	7490	if (tn.isSort())
161		{
162		// must ensure uninterpreted type is non-empty.
163	1812	if (!rs->hasType(tn))
164		{
165		// terms in rep_set are now constants which mapped to terms through
166		// TheoryModel. Thus, should introduce a constant and a term.
167		// For now, we just add an arbitrary term.
168	14	Node var = getSomeDomainElement(tn);
169	14	Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn
170	7	<< std::endl;
171	7	rs->add(tn, var);
172		}
173	1812	return true;
174		}
175		else
176		{
177		// can we complete it?
178	5678	if (d_qreg.getQuantifiersBoundInference().mayComplete(tn))
179		{
180	4264	Trace("fm-debug") << " do complete, since cardinality is small ("
181	2132	<< tn.getCardinality() << ")..." << std::endl;
182	2132	rs->complete(tn);
183		// must have succeeded
184	2132	Assert(rs->hasType(tn));
185	2132	return true;
186		}
187	3546	Trace("fm-debug") << " variable cannot be bounded." << std::endl;
188	3546	return false;
189		}
190		}
191
192		bool FirstOrderModel::isModelBasis(TNode n)
193		{
194		return n.getAttribute(ModelBasisAttribute());
195		}
196
197	9942	EqualityQuery* FirstOrderModel::getEqualityQuery() { return &d_eq_query; }
198
199		/** needs check */
200	101720	bool FirstOrderModel::checkNeeded() {
201	101720	return d_forall_asserts.size()>0;
202		}
203
204	28107	void FirstOrderModel::reset_round() {
205	28107	d_quant_active.clear();
206
207		// compute which quantified formulas are asserted if necessary
208	56214	std::map<Node, bool> qassert;
209	28107	if (!d_forall_rlv_vec.empty())
210		{
211	6528	Trace("fm-relevant-debug")
212	3264	<< "Mark asserted quantified formulas..." << std::endl;
213	151474	for (const Node& q : d_forall_asserts)
214		{
215	148210	qassert[q] = true;
216		}
217		}
218		//order the quantified formulas
219	28107	d_forall_rlv_assert.clear();
220	28107	d_forallRlvComputed = false;
221	28107	if( !d_forall_rlv_vec.empty() ){
222	3264	d_forallRlvComputed = true;
223	3264	Trace("fm-relevant") << "Build sorted relevant list..." << std::endl;
224	3264	Trace("fm-relevant-debug") << "Add relevant asserted formulas..." << std::endl;
225	3264	std::map<Node, bool>::iterator ita;
226	11495	for( int i=(int)(d_forall_rlv_vec.size()-1); i>=0; i-- ){
227	16462	Node q = d_forall_rlv_vec[i];
228	8231	ita = qassert.find(q);
229	8231	if (ita != qassert.end())
230		{
231	7643	Trace("fm-relevant") << " " << q << std::endl;
232	7643	d_forall_rlv_assert.push_back( q );
233	7643	qassert.erase(ita);
234		}
235		}
236	3264	Trace("fm-relevant-debug") << "Add remaining asserted formulas..." << std::endl;
237	151474	for (const Node& q : d_forall_asserts)
238		{
239		// if we didn't include it above
240	148210	if (qassert.find(q) != qassert.end())
241		{
242	140567	d_forall_rlv_assert.push_back( q );
243		}else{
244	7643	Trace("fm-relevant-debug") << "...already included " << q << std::endl;
245		}
246		}
247	3264	Trace("fm-relevant-debug") << "Sizes : " << d_forall_rlv_assert.size() << " " << d_forall_asserts.size() << std::endl;
248	3264	Assert(d_forall_rlv_assert.size() == d_forall_asserts.size());
249		}
250	28107	}
251
252	2403	void FirstOrderModel::markRelevant( Node q ) {
253		// Put q on the back of the vector d_forall_rlv_vec.
254		// If we were the last quantifier marked relevant, this is a no-op, return.
255	2403	if( q!=d_last_forall_rlv ){
256	1147	Trace("fm-relevant") << "Mark relevant : " << q << std::endl;
257		std::vector<Node>::iterator itr =
258	1147	std::find(d_forall_rlv_vec.begin(), d_forall_rlv_vec.end(), q);
259	1147	if (itr != d_forall_rlv_vec.end())
260		{
261	147	d_forall_rlv_vec.erase(itr, itr + 1);
262		}
263	1147	d_forall_rlv_vec.push_back(q);
264	1147	d_last_forall_rlv = q;
265		}
266	2403	}
267
268	1549	void FirstOrderModel::setQuantifierActive( TNode q, bool active ) {
269	1549	d_quant_active[q] = active;
270	1549	}
271
272	318459	bool FirstOrderModel::isQuantifierActive(TNode q) const
273		{
274	318459	std::map<TNode, bool>::const_iterator it = d_quant_active.find(q);
275	318459	if( it==d_quant_active.end() ){
276	318298	return true;
277		}
278	161	return it->second;
279		}
280
281	27385	bool FirstOrderModel::isQuantifierAsserted(TNode q) const
282		{
283	27385	return std::find( d_forall_asserts.begin(), d_forall_asserts.end(), q )!=d_forall_asserts.end();
284		}
285
286	87630	Node FirstOrderModel::getModelBasisTerm(TypeNode tn)
287		{
288	87630	if (d_model_basis_term.find(tn) == d_model_basis_term.end())
289		{
290	2144	Node mbt;
291	1072	if (tn.isClosedEnumerable())
292		{
293	562	mbt = d_treg.getTermEnumeration()->getEnumerateTerm(tn, 0);
294		}
295		else
296		{
297	510	if (options::fmfFreshDistConst())
298		{
299		mbt = d_treg.getTermDatabase()->getOrMakeTypeFreshVariable(tn);
300		}
301		else
302		{
303		// The model basis term cannot be an interpreted function, or else we
304		// may produce an inconsistent model by choosing an arbitrary
305		// equivalence class for it. Hence, we require that it be an existing or
306		// fresh variable.
307	510	mbt = d_treg.getTermDatabase()->getOrMakeTypeGroundTerm(tn, true);
308		}
309		}
310		ModelBasisAttribute mba;
311	1072	mbt.setAttribute(mba, true);
312	1072	d_model_basis_term[tn] = mbt;
313	2144	Trace("model-basis-term") << "Choose " << mbt << " as model basis term for "
314	1072	<< tn << std::endl;
315		}
316	87630	return d_model_basis_term[tn];
317		}
318
319	74784	bool FirstOrderModel::isModelBasisTerm(Node n)
320		{
321	74784	return n == getModelBasisTerm(n.getType());
322		}
323
324	11211	Node FirstOrderModel::getModelBasisOpTerm(Node op)
325		{
326	11211	if (d_model_basis_op_term.find(op) == d_model_basis_op_term.end())
327		{
328	2140	TypeNode t = op.getType();
329	2140	std::vector<Node> children;
330	1070	children.push_back(op);
331	2655	for (int i = 0; i < (int)(t.getNumChildren() - 1); i++)
332		{
333	1585	children.push_back(getModelBasisTerm(t[i]));
334		}
335	1070	if (children.size() == 1)
336		{
337		d_model_basis_op_term[op] = op;
338		}
339		else
340		{
341	1070	d_model_basis_op_term[op] =
342	2140	NodeManager::currentNM()->mkNode(APPLY_UF, children);
343		}
344		}
345	11211	return d_model_basis_op_term[op];
346		}
347
348		Node FirstOrderModel::getModelBasis(Node q, Node n)
349		{
350		// make model basis
351		if (d_model_basis_terms.find(q) == d_model_basis_terms.end())
352		{
353		for (unsigned j = 0; j < q[0].getNumChildren(); j++)
354		{
355		d_model_basis_terms[q].push_back(getModelBasisTerm(q[0][j].getType()));
356		}
357		}
358		Node gn = d_qreg.substituteInstConstants(n, q, d_model_basis_terms[q]);
359		return gn;
360		}
361
362	24387	void FirstOrderModel::computeModelBasisArgAttribute(Node n)
363		{
364	24387	if (!n.hasAttribute(ModelBasisArgAttribute()))
365		{
366		// ensure that the model basis terms have been defined
367	4004	if (n.getKind() == APPLY_UF)
368		{
369	4004	getModelBasisOpTerm(n.getOperator());
370		}
371	4004	uint64_t val = 0;
372		// determine if it has model basis attribute
373	11080	for (unsigned j = 0, nchild = n.getNumChildren(); j < nchild; j++)
374		{
375	7076	if (n[j].getAttribute(ModelBasisAttribute()))
376		{
377	908	val++;
378		}
379		}
380		ModelBasisArgAttribute mbaa;
381	4004	n.setAttribute(mbaa, val);
382		}
383	24387	}
384
385	24387	unsigned FirstOrderModel::getModelBasisArg(Node n)
386		{
387	24387	computeModelBasisArgAttribute(n);
388	24387	return n.getAttribute(ModelBasisArgAttribute());
389		}
390
391		} // namespace quantifiers
392		} // namespace theory
393	29577	} // namespace cvc5