Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/fmf/model_engine.cpp	Lines:	124	182	68.1 %
Date:	2021-05-22	Branches:	222	676	32.8 %


/******************************************************************************
 * 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(QuantifiersState& qs,
                         QuantifiersInferenceManager& qim,
                         QuantifiersRegistry& qr,
                         TermRegistry& tr,
                         QModelBuilder* builder)
    : QuantifiersModule(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::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::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_incomplete_quants.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 std::find( d_incomplete_quants.begin(), d_incomplete_quants.end(), q )==d_incomplete_quants.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_qstate.isFiniteType(tn))
        {
          if( tn.isInteger() ){
            if( !options::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;
    }
  }
}

void ModelEngine::assertNode( Node f ){

}

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) && d_qreg.hasOwnership(f, this))
      {
        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::mbqiMode() == options::MbqiMode::FMC
                  ? 2
                  : (options::mbqiMode() == options::MbqiMode::TRUST ? 0 : 1);
  for( int e=0; e<e_max; e++) {
    d_incomplete_quants.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) && d_qreg.hasOwnership(q, this))
      {
        exhaustiveInstantiate( q, e );
        if (d_qstate.isInConflict())
        {
          break;
        }
      }else{
        Trace("fmf-exh-inst") << "-> Inactive : " << q << std::endl;
      }
    }
    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_incomplete_quants.push_back( 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::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, 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_incomplete_quants.push_back( 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;
      }
    }
  }
}

}  // 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	1338	ModelEngine::ModelEngine(QuantifiersState& qs,
35		QuantifiersInferenceManager& qim,
36		QuantifiersRegistry& qr,
37		TermRegistry& tr,
38	1338	QModelBuilder* builder)
39		: QuantifiersModule(qs, qim, qr, tr),
40		d_incomplete_check(true),
41		d_addedLemmas(0),
42		d_triedLemmas(0),
43		d_totalLemmas(0),
44	1338	d_builder(builder)
45		{
46
47	1338	}
48
49	2676	ModelEngine::~ModelEngine() {
50
51	2676	}
52
53	36431	bool ModelEngine::needsCheck( Theory::Effort e ) {
54	36431	return e==Theory::EFFORT_LAST_CALL;
55		}
56
57	1710	QuantifiersModule::QEffort ModelEngine::needsModel(Theory::Effort e)
58		{
59	8516	if( options::mbqiInterleave() ){
60		return QEFFORT_STANDARD;
61		}else{
62	1710	return QEFFORT_MODEL;
63		}
64		}
65
66	10540	void ModelEngine::reset_round( Theory::Effort e ) {
67	10540	d_incomplete_check = true;
68	10540	}
69	5096	void ModelEngine::check(Theory::Effort e, QEffort quant_e)
70		{
71	5096	bool doCheck = false;
72	5096	if( options::mbqiInterleave() ){
73		doCheck = quant_e == QEFFORT_STANDARD && d_qim.hasPendingLemma();
74		}
75	5096	if( !doCheck ){
76	5096	doCheck = quant_e == QEFFORT_MODEL;
77		}
78	5096	if( doCheck ){
79	1603	Assert(!d_qstate.isInConflict());
80	1603	int addedLemmas = 0;
81
82		//the following will test that the model satisfies all asserted universal quantifiers by
83		// (model-based) exhaustive instantiation.
84	1603	double clSet = 0;
85	1603	if( Trace.isOn("model-engine") ){
86		Trace("model-engine") << "---Model Engine Round---" << std::endl;
87		clSet = double(clock())/double(CLOCKS_PER_SEC);
88		}
89	1603	Trace("model-engine-debug") << "Check model..." << std::endl;
90	1603	d_incomplete_check = false;
91		// print debug
92	1603	if (Trace.isOn("fmf-model-complete"))
93		{
94		Trace("fmf-model-complete") << std::endl;
95		debugPrint("fmf-model-complete");
96		}
97		// successfully built an acceptable model, now check it
98	1603	addedLemmas += checkModel();
99
100	1603	if( Trace.isOn("model-engine") ){
101		double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
102		Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
103		}
104
105	1603	if( addedLemmas==0 ){
106	467	Trace("model-engine-debug") << "No lemmas added, incomplete = " << ( d_incomplete_check \|\| !d_incomplete_quants.empty() ) << std::endl;
107		// cvc5 will answer SAT or unknown
108	467	if( Trace.isOn("fmf-consistent") ){
109		Trace("fmf-consistent") << std::endl;
110		debugPrint("fmf-consistent");
111		}
112		}
113		}
114	5096	}
115
116	406	bool ModelEngine::checkComplete(IncompleteId& incId)
117		{
118	406	if (d_incomplete_check)
119		{
120		incId = IncompleteId::QUANTIFIERS_FMF;
121		return false;
122		}
123	406	return true;
124		}
125
126	1099	bool ModelEngine::checkCompleteFor( Node q ) {
127	1099	return std::find( d_incomplete_quants.begin(), d_incomplete_quants.end(), q )==d_incomplete_quants.end();
128		}
129
130	2874	void ModelEngine::registerQuantifier( Node f ){
131	2874	if( Trace.isOn("fmf-warn") ){
132		bool canHandle = true;
133		for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
134		TypeNode tn = f[0][i].getType();
135		if( !tn.isSort() ){
136		if (!d_qstate.isFiniteType(tn))
137		{
138		if( tn.isInteger() ){
139		if( !options::fmfBound() ){
140		canHandle = false;
141		}
142		}else{
143		canHandle = false;
144		}
145		}
146		}
147		}
148		if( !canHandle ){
149		Trace("fmf-warn") << "Warning : Model Engine : may not be able to answer SAT because of formula : " << f << std::endl;
150		}
151		}
152	2874	}
153
154	16451	void ModelEngine::assertNode( Node f ){
155
156	16451	}
157
158	1603	int ModelEngine::checkModel(){
159	1603	FirstOrderModel* fm = d_treg.getModel();
160
161		//for debugging, setup
162	8115	for (std::map<TypeNode, std::vector<Node> >::iterator it =
163	1603	fm->getRepSetPtr()->d_type_reps.begin();
164	9718	it != fm->getRepSetPtr()->d_type_reps.end();
165		++it)
166		{
167	8115	if( it->first.isSort() ){
168	2326	Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
169	2326	Trace("model-engine-debug") << " Reps : ";
170	6751	for( size_t i=0; i<it->second.size(); i++ ){
171	4425	Trace("model-engine-debug") << it->second[i] << " ";
172		}
173	2326	Trace("model-engine-debug") << std::endl;
174	2326	Trace("model-engine-debug") << " Term reps : ";
175	6751	for( size_t i=0; i<it->second.size(); i++ ){
176	8850	Node r = fm->getInternalRepresentative(it->second[i], Node::null(), 0);
177	4425	if (r.isNull())
178		{
179		// there was an invalid equivalence class
180		d_incomplete_check = true;
181		}
182	4425	Trace("model-engine-debug") << r << " ";
183		}
184	2326	Trace("model-engine-debug") << std::endl;
185	4652	Node mbt = fm->getModelBasisTerm(it->first);
186	2326	Trace("model-engine-debug") << " Basis term : " << mbt << std::endl;
187		}
188		}
189
190	1603	d_triedLemmas = 0;
191	1603	d_addedLemmas = 0;
192	1603	d_totalLemmas = 0;
193		//for statistics
194	1603	if( Trace.isOn("model-engine") ){
195		for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
196		Node f = fm->getAssertedQuantifier( i );
197		if (fm->isQuantifierActive(f) && d_qreg.hasOwnership(f, this))
198		{
199		int totalInst = 1;
200		for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
201		TypeNode tn = f[0][j].getType();
202		if (fm->getRepSet()->hasType(tn))
203		{
204		totalInst =
205		totalInst * (int)fm->getRepSet()->getNumRepresentatives(tn);
206		}
207		}
208		d_totalLemmas += totalInst;
209		}
210		}
211		}
212
213	1603	Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
214		// FMC uses two sub-effort levels
215	1603	int e_max = options::mbqiMode() == options::MbqiMode::FMC
216	2510	? 2
217	2510	: (options::mbqiMode() == options::MbqiMode::TRUST ? 0 : 1);
218	2438	for( int e=0; e<e_max; e++) {
219	1971	d_incomplete_quants.clear();
220	14427	for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
221	24912	Node q = fm->getAssertedQuantifier( i, true );
222	12456	Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << q << ", effort = " << e << "..." << std::endl;
223		//determine if we should check this quantifier
224	12456	if (fm->isQuantifierActive(q) && d_qreg.hasOwnership(q, this))
225		{
226	12163	exhaustiveInstantiate( q, e );
227	12163	if (d_qstate.isInConflict())
228		{
229		break;
230		}
231		}else{
232	293	Trace("fmf-exh-inst") << "-> Inactive : " << q << std::endl;
233		}
234		}
235	1971	if( d_addedLemmas>0 ){
236	1136	break;
237		}else{
238	835	Assert(!d_qstate.isInConflict());
239		}
240		}
241
242		//print debug information
243	1603	if (d_qstate.isInConflict())
244		{
245		Trace("model-engine") << "Conflict, added lemmas = ";
246		}else{
247	1603	Trace("model-engine") << "Added Lemmas = ";
248		}
249	1603	Trace("model-engine") << d_addedLemmas << " / " << d_triedLemmas << " / ";
250	1603	Trace("model-engine") << d_totalLemmas << std::endl;
251	1603	return d_addedLemmas;
252		}
253
254
255
256	12163	void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
257		//first check if the builder can do the exhaustive instantiation
258	12163	unsigned prev_alem = d_builder->getNumAddedLemmas();
259	12163	unsigned prev_tlem = d_builder->getNumTriedLemmas();
260	12163	FirstOrderModel* fm = d_treg.getModel();
261	12163	int retEi = d_builder->doExhaustiveInstantiation(fm, f, effort);
262	12163	if( retEi!=0 ){
263	11965	if( retEi<0 ){
264		Trace("fmf-exh-inst") << "-> Builder determined complete instantiation was impossible." << std::endl;
265		d_incomplete_quants.push_back( f );
266		}else{
267	11965	Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl;
268		}
269	11965	d_triedLemmas += d_builder->getNumTriedLemmas() - prev_tlem;
270	11965	d_addedLemmas += d_builder->getNumAddedLemmas() - prev_alem;
271		}else{
272	198	if( Trace.isOn("fmf-exh-inst-debug") ){
273		Trace("fmf-exh-inst-debug") << " Instantiation Constants: ";
274		for( size_t i=0; i<f[0].getNumChildren(); i++ ){
275		Trace("fmf-exh-inst-debug")
276		<< d_qreg.getInstantiationConstant(f, i) << " ";
277		}
278		Trace("fmf-exh-inst-debug") << std::endl;
279		}
280	198	QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference();
281		//create a rep set iterator and iterate over the (relevant) domain of the quantifier
282	396	QRepBoundExt qrbe(qbi, fm);
283	396	RepSetIterator riter(fm->getRepSet(), &qrbe);
284	198	if( riter.setQuantifier( f ) ){
285	198	Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
286	198	if( !riter.isIncomplete() ){
287	182	int triedLemmas = 0;
288	182	int addedLemmas = 0;
289	182	Instantiate* inst = d_qim.getInstantiate();
290	1402	while( !riter.isFinished() && ( addedLemmas==0 \|\| !options::fmfOneInstPerRound() ) ){
291		//instantiation was not shown to be true, construct the match
292	1220	InstMatch m( f );
293	1815	for (unsigned i = 0; i < riter.getNumTerms(); i++)
294		{
295	1205	m.set(d_qstate, i, riter.getCurrentTerm(i));
296		}
297	610	Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
298	610	triedLemmas++;
299		//add as instantiation
300	610	if (inst->addInstantiation(
301		f, m.d_vals, InferenceId::QUANTIFIERS_INST_FMF_EXH, true))
302		{
303	265	addedLemmas++;
304	265	if (d_qstate.isInConflict())
305		{
306		break;
307		}
308		}else{
309	345	Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
310		}
311	610	riter.increment();
312		}
313	182	d_addedLemmas += addedLemmas;
314	182	d_triedLemmas += triedLemmas;
315		}
316		}else{
317		Trace("fmf-exh-inst") << "...exhaustive instantiation did set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
318		}
319		//if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
320	198	if( riter.isIncomplete() ){
321	22	d_incomplete_quants.push_back( f );
322		}
323		}
324	12163	}
325
326		void ModelEngine::debugPrint( const char* c ){
327		if (Trace.isOn(c))
328		{
329		Trace(c) << "Quantifiers: " << std::endl;
330		FirstOrderModel* m = d_treg.getModel();
331		for (size_t i = 0, nquant = m->getNumAssertedQuantifiers(); i < nquant; i++)
332		{
333		Node q = m->getAssertedQuantifier(i);
334		if (d_qreg.hasOwnership(q, this))
335		{
336		Trace(c) << " ";
337		if (!m->isQuantifierActive(q))
338		{
339		Trace(c) << "Inactive ";
340		}
341		else
342		{
343		Trace(c) << " ";
344		}
345		Trace(c) << q << std::endl;
346		}
347		}
348		}
349		}
350
351		} // namespace quantifiers
352		} // namespace theory
353	35000	} // namespace cvc5