Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/fmf/model_engine.cpp	Lines:	140	198	70.7 %
Date:	2021-11-05	Branches:	233	677	34.4 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Morgan Deters, Kshitij Bansal
 *
 * 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 class.
 */

#include "theory/quantifiers/fmf/model_engine.h"

#include "options/quantifiers_options.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/fmf/full_model_check.h"
#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/quant_rep_bound_ext.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/term_database.h"

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

namespace cvc5 {
namespace theory {
namespace quantifiers {

//Model Engine constructor
ModelEngine::ModelEngine(Env& env,
                         QuantifiersState& qs,
                         QuantifiersInferenceManager& qim,
                         QuantifiersRegistry& qr,
                         TermRegistry& tr,
                         QModelBuilder* builder)
    : QuantifiersModule(env, qs, qim, qr, tr),
      d_incomplete_check(true),
      d_addedLemmas(0),
      d_triedLemmas(0),
      d_totalLemmas(0),
      d_builder(builder)
{

}

ModelEngine::~ModelEngine() {

}

bool ModelEngine::needsCheck( Theory::Effort e ) {
  return e==Theory::EFFORT_LAST_CALL;
}

QuantifiersModule::QEffort ModelEngine::needsModel(Theory::Effort e)
{
  if (options().quantifiers.mbqiInterleave)
  {
    return QEFFORT_STANDARD;
  }
  else
  {
    return QEFFORT_MODEL;
  }
}

void ModelEngine::reset_round( Theory::Effort e ) {
  d_incomplete_check = true;
}
void ModelEngine::check(Theory::Effort e, QEffort quant_e)
{
  bool doCheck = false;
  if (options().quantifiers.mbqiInterleave)
  {
    doCheck = quant_e == QEFFORT_STANDARD && d_qim.hasPendingLemma();
  }
  if( !doCheck ){
    doCheck = quant_e == QEFFORT_MODEL;
  }
  if( doCheck ){
    Assert(!d_qstate.isInConflict());
    int addedLemmas = 0;

    //the following will test that the model satisfies all asserted universal quantifiers by
    // (model-based) exhaustive instantiation.
    double clSet = 0;
    if( Trace.isOn("model-engine") ){
      Trace("model-engine") << "---Model Engine Round---" << std::endl;
      clSet = double(clock())/double(CLOCKS_PER_SEC);
    }
    Trace("model-engine-debug") << "Check model..." << std::endl;
    d_incomplete_check = false;
    // print debug
    if (Trace.isOn("fmf-model-complete"))
    {
      Trace("fmf-model-complete") << std::endl;
      debugPrint("fmf-model-complete");
    }
    // successfully built an acceptable model, now check it
    addedLemmas += checkModel();

    if( Trace.isOn("model-engine") ){
      double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
      Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
    }

    if( addedLemmas==0 ){
      Trace("model-engine-debug")
          << "No lemmas added, incomplete = "
          << (d_incomplete_check || !d_incompleteQuants.empty()) << std::endl;
      // cvc5 will answer SAT or unknown
      if( Trace.isOn("fmf-consistent") ){
        Trace("fmf-consistent") << std::endl;
        debugPrint("fmf-consistent");
      }
    }
  }
}

bool ModelEngine::checkComplete(IncompleteId& incId)
{
  if (d_incomplete_check)
  {
    incId = IncompleteId::QUANTIFIERS_FMF;
    return false;
  }
  return true;
}

bool ModelEngine::checkCompleteFor( Node q ) {
  return d_incompleteQuants.find(q) == d_incompleteQuants.end();
}

void ModelEngine::registerQuantifier( Node f ){
  if( Trace.isOn("fmf-warn") ){
    bool canHandle = true;
    for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
      TypeNode tn = f[0][i].getType();
      if( !tn.isSort() ){
        if (!d_env.isFiniteType(tn))
        {
          if( tn.isInteger() ){
            if (!options().quantifiers.fmfBound)
            {
              canHandle = false;
            }
          }else{
            canHandle = false;
          }
        }
      }
    }
    if( !canHandle ){
      Trace("fmf-warn") << "Warning : Model Engine : may not be able to answer SAT because of formula : " << f << std::endl;
    }
  }
}

int ModelEngine::checkModel(){
  FirstOrderModel* fm = d_treg.getModel();

  //for debugging, setup
  for (std::map<TypeNode, std::vector<Node> >::iterator it =
           fm->getRepSetPtr()->d_type_reps.begin();
       it != fm->getRepSetPtr()->d_type_reps.end();
       ++it)
  {
    if( it->first.isSort() ){
      Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
      Trace("model-engine-debug") << "        Reps : ";
      for( size_t i=0; i<it->second.size(); i++ ){
        Trace("model-engine-debug") << it->second[i] << "  ";
      }
      Trace("model-engine-debug") << std::endl;
      Trace("model-engine-debug") << "   Term reps : ";
      for( size_t i=0; i<it->second.size(); i++ ){
        Node r = fm->getInternalRepresentative(it->second[i], Node::null(), 0);
        if (r.isNull())
        {
          // there was an invalid equivalence class
          d_incomplete_check = true;
        }
        Trace("model-engine-debug") << r << " ";
      }
      Trace("model-engine-debug") << std::endl;
      Node mbt = fm->getModelBasisTerm(it->first);
      Trace("model-engine-debug") << "  Basis term : " << mbt << std::endl;
    }
  }

  d_triedLemmas = 0;
  d_addedLemmas = 0;
  d_totalLemmas = 0;
  //for statistics
  if( Trace.isOn("model-engine") ){
    for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
      Node f = fm->getAssertedQuantifier( i );
      if (fm->isQuantifierActive(f) && shouldProcess(f))
      {
        int totalInst = 1;
        for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
          TypeNode tn = f[0][j].getType();
          if (fm->getRepSet()->hasType(tn))
          {
            totalInst =
                totalInst * (int)fm->getRepSet()->getNumRepresentatives(tn);
          }
        }
        d_totalLemmas += totalInst;
      }
    }
  }

  Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
  // FMC uses two sub-effort levels
  int e_max =
      options().quantifiers.mbqiMode == options::MbqiMode::FMC
          ? 2
          : (options().quantifiers.mbqiMode == options::MbqiMode::TRUST ? 0
                                                                        : 1);
  for( int e=0; e<e_max; e++) {
    d_incompleteQuants.clear();
    for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
      Node q = fm->getAssertedQuantifier( i, true );
      Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << q << ", effort = " << e << "..." << std::endl;
      //determine if we should check this quantifier
      if (!fm->isQuantifierActive(q))
      {
        Trace("fmf-exh-inst") << "-> Inactive : " << q << std::endl;
        continue;
      }
      if (!shouldProcess(q))
      {
        Trace("fmf-exh-inst") << "-> Not processed : " << q << std::endl;
        d_incompleteQuants.insert(q);
        continue;
      }
      exhaustiveInstantiate(q, e);
      if (d_qstate.isInConflict())
      {
        break;
      }
    }
    if( d_addedLemmas>0 ){
      break;
    }else{
      Assert(!d_qstate.isInConflict());
    }
  }

  //print debug information
  if (d_qstate.isInConflict())
  {
    Trace("model-engine") << "Conflict, added lemmas = ";
  }else{
    Trace("model-engine") << "Added Lemmas = ";
  }
  Trace("model-engine") << d_addedLemmas << " / " << d_triedLemmas << " / ";
  Trace("model-engine") << d_totalLemmas << std::endl;
  return d_addedLemmas;
}



void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
  //first check if the builder can do the exhaustive instantiation
  unsigned prev_alem = d_builder->getNumAddedLemmas();
  unsigned prev_tlem = d_builder->getNumTriedLemmas();
  FirstOrderModel* fm = d_treg.getModel();
  int retEi = d_builder->doExhaustiveInstantiation(fm, f, effort);
  if( retEi!=0 ){
    if( retEi<0 ){
      Trace("fmf-exh-inst") << "-> Builder determined complete instantiation was impossible." << std::endl;
      d_incompleteQuants.insert(f);
    }else{
      Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl;
    }
    d_triedLemmas += d_builder->getNumTriedLemmas() - prev_tlem;
    d_addedLemmas += d_builder->getNumAddedLemmas() - prev_alem;
  }else{
    if( Trace.isOn("fmf-exh-inst-debug") ){
      Trace("fmf-exh-inst-debug") << "   Instantiation Constants: ";
      for( size_t i=0; i<f[0].getNumChildren(); i++ ){
        Trace("fmf-exh-inst-debug")
            << d_qreg.getInstantiationConstant(f, i) << " ";
      }
      Trace("fmf-exh-inst-debug") << std::endl;
    }
    QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference();
    //create a rep set iterator and iterate over the (relevant) domain of the quantifier
    QRepBoundExt qrbe(qbi, fm);
    RepSetIterator riter(fm->getRepSet(), &qrbe);
    if( riter.setQuantifier( f ) ){
      Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
      if( !riter.isIncomplete() ){
        int triedLemmas = 0;
        int addedLemmas = 0;
        Instantiate* inst = d_qim.getInstantiate();
        while (
            !riter.isFinished()
            && (addedLemmas == 0 || !options().quantifiers.fmfOneInstPerRound))
        {
          //instantiation was not shown to be true, construct the match
          InstMatch m( f );
          for (unsigned i = 0; i < riter.getNumTerms(); i++)
          {
            m.set(d_qstate, i, riter.getCurrentTerm(i));
          }
          Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
          triedLemmas++;
          //add as instantiation
          if (inst->addInstantiation(f,
                                     m.d_vals,
                                     InferenceId::QUANTIFIERS_INST_FMF_EXH,
                                     Node::null(),
                                     true))
          {
            addedLemmas++;
            if (d_qstate.isInConflict())
            {
              break;
            }
          }else{
            Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
          }
          riter.increment();
        }
        d_addedLemmas += addedLemmas;
        d_triedLemmas += triedLemmas;
      }
    }else{
      Trace("fmf-exh-inst") << "...exhaustive instantiation did set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
    }
    //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
    if( riter.isIncomplete() ){
      d_incompleteQuants.insert(f);
    }
  }
}

void ModelEngine::debugPrint( const char* c ){
  if (Trace.isOn(c))
  {
    Trace(c) << "Quantifiers: " << std::endl;
    FirstOrderModel* m = d_treg.getModel();
    for (size_t i = 0, nquant = m->getNumAssertedQuantifiers(); i < nquant; i++)
    {
      Node q = m->getAssertedQuantifier(i);
      if (d_qreg.hasOwnership(q, this))
      {
        Trace(c) << "   ";
        if (!m->isQuantifierActive(q))
        {
          Trace(c) << "*Inactive* ";
        }
        else
        {
          Trace(c) << "           ";
        }
        Trace(c) << q << std::endl;
      }
    }
  }
}

bool ModelEngine::shouldProcess(Node q)
{
  if (!d_qreg.hasOwnership(q, this))
  {
    // if we don't have ownership, another module has taken responsibility
    // for processing q.
    return false;
  }
  // if finite model finding or fmf bound is on, we process everything
  if (options().quantifiers.finiteModelFind || options().quantifiers.fmfBound)
  {
    return true;
  }
  // otherwise, we are only using model-based instantiation for internally
  // generated bounded quantified formulas
  QuantAttributes& qattr = d_qreg.getQuantAttributes();
  return qattr.isQuantBounded(q);
}

}  // 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, Morgan Deters, Kshitij Bansal
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 class.
14		*/
15
16		#include "theory/quantifiers/fmf/model_engine.h"
17
18		#include "options/quantifiers_options.h"
19		#include "theory/quantifiers/first_order_model.h"
20		#include "theory/quantifiers/fmf/full_model_check.h"
21		#include "theory/quantifiers/instantiate.h"
22		#include "theory/quantifiers/quant_rep_bound_ext.h"
23		#include "theory/quantifiers/quantifiers_attributes.h"
24		#include "theory/quantifiers/term_database.h"
25
26		using namespace cvc5::kind;
27		using namespace cvc5::context;
28
29		namespace cvc5 {
30		namespace theory {
31		namespace quantifiers {
32
33		//Model Engine constructor
34	1546	ModelEngine::ModelEngine(Env& env,
35		QuantifiersState& qs,
36		QuantifiersInferenceManager& qim,
37		QuantifiersRegistry& qr,
38		TermRegistry& tr,
39	1546	QModelBuilder* builder)
40		: QuantifiersModule(env, qs, qim, qr, tr),
41		d_incomplete_check(true),
42		d_addedLemmas(0),
43		d_triedLemmas(0),
44		d_totalLemmas(0),
45	1546	d_builder(builder)
46		{
47
48	1546	}
49
50	3092	ModelEngine::~ModelEngine() {
51
52	3092	}
53
54	24957	bool ModelEngine::needsCheck( Theory::Effort e ) {
55	24957	return e==Theory::EFFORT_LAST_CALL;
56		}
57
58	1868	QuantifiersModule::QEffort ModelEngine::needsModel(Theory::Effort e)
59		{
60	1868	if (options().quantifiers.mbqiInterleave)
61		{
62		return QEFFORT_STANDARD;
63		}
64		else
65		{
66	1868	return QEFFORT_MODEL;
67		}
68		}
69
70	13567	void ModelEngine::reset_round( Theory::Effort e ) {
71	13567	d_incomplete_check = true;
72	13567	}
73	5553	void ModelEngine::check(Theory::Effort e, QEffort quant_e)
74		{
75	5553	bool doCheck = false;
76	5553	if (options().quantifiers.mbqiInterleave)
77		{
78		doCheck = quant_e == QEFFORT_STANDARD && d_qim.hasPendingLemma();
79		}
80	5553	if( !doCheck ){
81	5553	doCheck = quant_e == QEFFORT_MODEL;
82		}
83	5553	if( doCheck ){
84	1756	Assert(!d_qstate.isInConflict());
85	1756	int addedLemmas = 0;
86
87		//the following will test that the model satisfies all asserted universal quantifiers by
88		// (model-based) exhaustive instantiation.
89	1756	double clSet = 0;
90	1756	if( Trace.isOn("model-engine") ){
91		Trace("model-engine") << "---Model Engine Round---" << std::endl;
92		clSet = double(clock())/double(CLOCKS_PER_SEC);
93		}
94	1756	Trace("model-engine-debug") << "Check model..." << std::endl;
95	1756	d_incomplete_check = false;
96		// print debug
97	1756	if (Trace.isOn("fmf-model-complete"))
98		{
99		Trace("fmf-model-complete") << std::endl;
100		debugPrint("fmf-model-complete");
101		}
102		// successfully built an acceptable model, now check it
103	1756	addedLemmas += checkModel();
104
105	1756	if( Trace.isOn("model-engine") ){
106		double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
107		Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
108		}
109
110	1756	if( addedLemmas==0 ){
111	1088	Trace("model-engine-debug")
112	544	<< "No lemmas added, incomplete = "
113	544	<< (d_incomplete_check \|\| !d_incompleteQuants.empty()) << std::endl;
114		// cvc5 will answer SAT or unknown
115	544	if( Trace.isOn("fmf-consistent") ){
116		Trace("fmf-consistent") << std::endl;
117		debugPrint("fmf-consistent");
118		}
119		}
120		}
121	5553	}
122
123	440	bool ModelEngine::checkComplete(IncompleteId& incId)
124		{
125	440	if (d_incomplete_check)
126		{
127		incId = IncompleteId::QUANTIFIERS_FMF;
128		return false;
129		}
130	440	return true;
131		}
132
133	1215	bool ModelEngine::checkCompleteFor( Node q ) {
134	1215	return d_incompleteQuants.find(q) == d_incompleteQuants.end();
135		}
136
137	3160	void ModelEngine::registerQuantifier( Node f ){
138	3160	if( Trace.isOn("fmf-warn") ){
139		bool canHandle = true;
140		for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
141		TypeNode tn = f[0][i].getType();
142		if( !tn.isSort() ){
143		if (!d_env.isFiniteType(tn))
144		{
145		if( tn.isInteger() ){
146		if (!options().quantifiers.fmfBound)
147		{
148		canHandle = false;
149		}
150		}else{
151		canHandle = false;
152		}
153		}
154		}
155		}
156		if( !canHandle ){
157		Trace("fmf-warn") << "Warning : Model Engine : may not be able to answer SAT because of formula : " << f << std::endl;
158		}
159		}
160	3160	}
161
162	1756	int ModelEngine::checkModel(){
163	1756	FirstOrderModel* fm = d_treg.getModel();
164
165		//for debugging, setup
166	7647	for (std::map<TypeNode, std::vector<Node> >::iterator it =
167	1756	fm->getRepSetPtr()->d_type_reps.begin();
168	9403	it != fm->getRepSetPtr()->d_type_reps.end();
169		++it)
170		{
171	7647	if( it->first.isSort() ){
172	1954	Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
173	1954	Trace("model-engine-debug") << " Reps : ";
174	5555	for( size_t i=0; i<it->second.size(); i++ ){
175	3601	Trace("model-engine-debug") << it->second[i] << " ";
176		}
177	1954	Trace("model-engine-debug") << std::endl;
178	1954	Trace("model-engine-debug") << " Term reps : ";
179	5555	for( size_t i=0; i<it->second.size(); i++ ){
180	7202	Node r = fm->getInternalRepresentative(it->second[i], Node::null(), 0);
181	3601	if (r.isNull())
182		{
183		// there was an invalid equivalence class
184		d_incomplete_check = true;
185		}
186	3601	Trace("model-engine-debug") << r << " ";
187		}
188	1954	Trace("model-engine-debug") << std::endl;
189	3908	Node mbt = fm->getModelBasisTerm(it->first);
190	1954	Trace("model-engine-debug") << " Basis term : " << mbt << std::endl;
191		}
192		}
193
194	1756	d_triedLemmas = 0;
195	1756	d_addedLemmas = 0;
196	1756	d_totalLemmas = 0;
197		//for statistics
198	1756	if( Trace.isOn("model-engine") ){
199		for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
200		Node f = fm->getAssertedQuantifier( i );
201		if (fm->isQuantifierActive(f) && shouldProcess(f))
202		{
203		int totalInst = 1;
204		for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
205		TypeNode tn = f[0][j].getType();
206		if (fm->getRepSet()->hasType(tn))
207		{
208		totalInst =
209		totalInst * (int)fm->getRepSet()->getNumRepresentatives(tn);
210		}
211		}
212		d_totalLemmas += totalInst;
213		}
214		}
215		}
216
217	1756	Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
218		// FMC uses two sub-effort levels
219		int e_max =
220	1756	options().quantifiers.mbqiMode == options::MbqiMode::FMC
221	2113	? 2
222	357	: (options().quantifiers.mbqiMode == options::MbqiMode::TRUST ? 0
223	1756	: 1);
224	3226	for( int e=0; e<e_max; e++) {
225	2682	d_incompleteQuants.clear();
226	14994	for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
227	24146	Node q = fm->getAssertedQuantifier( i, true );
228	12312	Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << q << ", effort = " << e << "..." << std::endl;
229		//determine if we should check this quantifier
230	12322	if (!fm->isQuantifierActive(q))
231		{
232	10	Trace("fmf-exh-inst") << "-> Inactive : " << q << std::endl;
233	10	continue;
234		}
235	12770	if (!shouldProcess(q))
236		{
237	468	Trace("fmf-exh-inst") << "-> Not processed : " << q << std::endl;
238	468	d_incompleteQuants.insert(q);
239	468	continue;
240		}
241	11834	exhaustiveInstantiate(q, e);
242	11834	if (d_qstate.isInConflict())
243		{
244		break;
245		}
246		}
247	2682	if( d_addedLemmas>0 ){
248	1212	break;
249		}else{
250	1470	Assert(!d_qstate.isInConflict());
251		}
252		}
253
254		//print debug information
255	1756	if (d_qstate.isInConflict())
256		{
257		Trace("model-engine") << "Conflict, added lemmas = ";
258		}else{
259	1756	Trace("model-engine") << "Added Lemmas = ";
260		}
261	1756	Trace("model-engine") << d_addedLemmas << " / " << d_triedLemmas << " / ";
262	1756	Trace("model-engine") << d_totalLemmas << std::endl;
263	1756	return d_addedLemmas;
264		}
265
266
267
268	11834	void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
269		//first check if the builder can do the exhaustive instantiation
270	11834	unsigned prev_alem = d_builder->getNumAddedLemmas();
271	11834	unsigned prev_tlem = d_builder->getNumTriedLemmas();
272	11834	FirstOrderModel* fm = d_treg.getModel();
273	11834	int retEi = d_builder->doExhaustiveInstantiation(fm, f, effort);
274	11834	if( retEi!=0 ){
275	11608	if( retEi<0 ){
276		Trace("fmf-exh-inst") << "-> Builder determined complete instantiation was impossible." << std::endl;
277		d_incompleteQuants.insert(f);
278		}else{
279	11608	Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl;
280		}
281	11608	d_triedLemmas += d_builder->getNumTriedLemmas() - prev_tlem;
282	11608	d_addedLemmas += d_builder->getNumAddedLemmas() - prev_alem;
283		}else{
284	226	if( Trace.isOn("fmf-exh-inst-debug") ){
285		Trace("fmf-exh-inst-debug") << " Instantiation Constants: ";
286		for( size_t i=0; i<f[0].getNumChildren(); i++ ){
287		Trace("fmf-exh-inst-debug")
288		<< d_qreg.getInstantiationConstant(f, i) << " ";
289		}
290		Trace("fmf-exh-inst-debug") << std::endl;
291		}
292	226	QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference();
293		//create a rep set iterator and iterate over the (relevant) domain of the quantifier
294	452	QRepBoundExt qrbe(qbi, fm);
295	452	RepSetIterator riter(fm->getRepSet(), &qrbe);
296	226	if( riter.setQuantifier( f ) ){
297	226	Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
298	226	if( !riter.isIncomplete() ){
299	210	int triedLemmas = 0;
300	210	int addedLemmas = 0;
301	210	Instantiate* inst = d_qim.getInstantiate();
302	663	while (
303	873	!riter.isFinished()
304	873	&& (addedLemmas == 0 \|\| !options().quantifiers.fmfOneInstPerRound))
305		{
306		//instantiation was not shown to be true, construct the match
307	1326	InstMatch m( f );
308	1983	for (unsigned i = 0; i < riter.getNumTerms(); i++)
309		{
310	1320	m.set(d_qstate, i, riter.getCurrentTerm(i));
311		}
312	663	Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
313	663	triedLemmas++;
314		//add as instantiation
315	1326	if (inst->addInstantiation(f,
316		m.d_vals,
317		InferenceId::QUANTIFIERS_INST_FMF_EXH,
318	1326	Node::null(),
319		true))
320		{
321	318	addedLemmas++;
322	318	if (d_qstate.isInConflict())
323		{
324		break;
325		}
326		}else{
327	345	Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
328		}
329	663	riter.increment();
330		}
331	210	d_addedLemmas += addedLemmas;
332	210	d_triedLemmas += triedLemmas;
333		}
334		}else{
335		Trace("fmf-exh-inst") << "...exhaustive instantiation did set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
336		}
337		//if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
338	226	if( riter.isIncomplete() ){
339	24	d_incompleteQuants.insert(f);
340		}
341		}
342	11834	}
343
344		void ModelEngine::debugPrint( const char* c ){
345		if (Trace.isOn(c))
346		{
347		Trace(c) << "Quantifiers: " << std::endl;
348		FirstOrderModel* m = d_treg.getModel();
349		for (size_t i = 0, nquant = m->getNumAssertedQuantifiers(); i < nquant; i++)
350		{
351		Node q = m->getAssertedQuantifier(i);
352		if (d_qreg.hasOwnership(q, this))
353		{
354		Trace(c) << " ";
355		if (!m->isQuantifierActive(q))
356		{
357		Trace(c) << "Inactive ";
358		}
359		else
360		{
361		Trace(c) << " ";
362		}
363		Trace(c) << q << std::endl;
364		}
365		}
366		}
367		}
368
369	12302	bool ModelEngine::shouldProcess(Node q)
370		{
371	12302	if (!d_qreg.hasOwnership(q, this))
372		{
373		// if we don't have ownership, another module has taken responsibility
374		// for processing q.
375	458	return false;
376		}
377		// if finite model finding or fmf bound is on, we process everything
378	11844	if (options().quantifiers.finiteModelFind \|\| options().quantifiers.fmfBound)
379		{
380	9668	return true;
381		}
382		// otherwise, we are only using model-based instantiation for internally
383		// generated bounded quantified formulas
384	2176	QuantAttributes& qattr = d_qreg.getQuantAttributes();
385	2176	return qattr.isQuantBounded(q);
386		}
387
388		} // namespace quantifiers
389		} // namespace theory
390	31125	} // namespace cvc5