Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/ematching/instantiation_engine.cpp	Lines:	115	133	86.5 %
Date:	2021-08-19	Branches:	176	382	46.1 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Morgan Deters, Tim King
 *
 * 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 instantiation engine class
 */

#include "theory/quantifiers/ematching/instantiation_engine.h"

#include "options/quantifiers_options.h"
#include "theory/quantifiers/ematching/inst_strategy_e_matching.h"
#include "theory/quantifiers/ematching/inst_strategy_e_matching_user.h"
#include "theory/quantifiers/ematching/trigger.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"

using namespace cvc5::kind;
using namespace cvc5::context;
using namespace cvc5::theory::quantifiers::inst;

namespace cvc5 {
namespace theory {
namespace quantifiers {

InstantiationEngine::InstantiationEngine(QuantifiersState& qs,
                                         QuantifiersInferenceManager& qim,
                                         QuantifiersRegistry& qr,
                                         TermRegistry& tr)
    : QuantifiersModule(qs, qim, qr, tr),
      d_instStrategies(),
      d_isup(),
      d_i_ag(),
      d_quants(),
      d_trdb(qs, qim, qr, tr),
      d_quant_rel(nullptr)
{
  if (options::relevantTriggers())
  {
    d_quant_rel.reset(new quantifiers::QuantRelevance);
  }
  if (options::eMatching()) {
    // these are the instantiation strategies for E-matching
    // user-provided patterns
    if (options::userPatternsQuant() != options::UserPatMode::IGNORE)
    {
      d_isup.reset(new InstStrategyUserPatterns(d_trdb, qs, qim, qr, tr));
      d_instStrategies.push_back(d_isup.get());
    }

    // auto-generated patterns
    d_i_ag.reset(new InstStrategyAutoGenTriggers(
        d_trdb, qs, qim, qr, tr, d_quant_rel.get()));
    d_instStrategies.push_back(d_i_ag.get());
  }
}

InstantiationEngine::~InstantiationEngine() {}

void InstantiationEngine::presolve() {
  for( unsigned i=0; i<d_instStrategies.size(); ++i ){
    d_instStrategies[i]->presolve();
  }
}

void InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
  size_t lastWaiting = d_qim.numPendingLemmas();
  //iterate over an internal effort level e
  int e = 0;
  int eLimit = effort==Theory::EFFORT_LAST_CALL ? 10 : 2;
  bool finished = false;
  //while unfinished, try effort level=0,1,2....
  while( !finished && e<=eLimit ){
    Debug("inst-engine") << "IE: Prepare instantiation (" << e << ")." << std::endl;
    finished = true;
    //instantiate each quantifier
    for( unsigned i=0; i<d_quants.size(); i++ ){
      Node q = d_quants[i];
      Debug("inst-engine-debug") << "IE: Instantiate " << q << "..." << std::endl;
      //int e_use = d_quantEngine->getRelevance( q )==-1 ? e - 1 : e;
      int e_use = e;
      if( e_use>=0 ){
        Trace("inst-engine-debug") << "inst-engine : " << q << std::endl;
        //check each instantiation strategy
        for( unsigned j=0; j<d_instStrategies.size(); j++ ){
          InstStrategy* is = d_instStrategies[j];
          Trace("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl;
          InstStrategyStatus quantStatus = is->process(q, effort, e_use);
          Trace("inst-engine-debug")
              << " -> unfinished= "
              << (quantStatus == InstStrategyStatus::STATUS_UNFINISHED)
              << ", conflict=" << d_qstate.isInConflict() << std::endl;
          if (d_qstate.isInConflict())
          {
            return;
          }
          else if (quantStatus == InstStrategyStatus::STATUS_UNFINISHED)
          {
            finished = false;
          }
        }
      }
    }
    //do not consider another level if already added lemma at this level
    if (d_qim.numPendingLemmas() > lastWaiting)
    {
      finished = true;
    }
    e++;
  }
}

bool InstantiationEngine::needsCheck( Theory::Effort e ){
  return d_qstate.getInstWhenNeedsCheck(e);
}

void InstantiationEngine::reset_round( Theory::Effort e ){
  //if not, proceed to instantiation round
  //reset the instantiation strategies
  for( unsigned i=0; i<d_instStrategies.size(); ++i ){
    InstStrategy* is = d_instStrategies[i];
    is->processResetInstantiationRound( e );
  }
}

void InstantiationEngine::check(Theory::Effort e, QEffort quant_e)
{
  CodeTimer codeTimer(d_qstate.getStats().d_ematching_time);
  if (quant_e != QEFFORT_STANDARD)
  {
    return;
  }
  double clSet = 0;
  if (Trace.isOn("inst-engine"))
  {
    clSet = double(clock()) / double(CLOCKS_PER_SEC);
    Trace("inst-engine") << "---Instantiation Engine Round, effort = " << e
                         << "---" << std::endl;
  }
  // collect all active quantified formulas belonging to this
  bool quantActive = false;
  d_quants.clear();
  FirstOrderModel* m = d_treg.getModel();
  size_t nquant = m->getNumAssertedQuantifiers();
  for (size_t i = 0; i < nquant; i++)
  {
    Node q = m->getAssertedQuantifier(i, true);
    if (shouldProcess(q) && m->isQuantifierActive(q))
    {
      quantActive = true;
      d_quants.push_back(q);
    }
  }
  Trace("inst-engine-debug")
      << "InstEngine: check: # asserted quantifiers " << d_quants.size() << "/";
  Trace("inst-engine-debug") << nquant << " " << quantActive << std::endl;
  if (quantActive)
  {
    size_t lastWaiting = d_qim.numPendingLemmas();
    doInstantiationRound(e);
    if (d_qstate.isInConflict())
    {
      Assert(d_qim.numPendingLemmas() > lastWaiting);
      Trace("inst-engine") << "Conflict, added lemmas = "
                           << (d_qim.numPendingLemmas() - lastWaiting)
                           << std::endl;
    }
    else if (d_qim.hasPendingLemma())
    {
      Trace("inst-engine") << "Added lemmas = "
                           << (d_qim.numPendingLemmas() - lastWaiting)
                           << std::endl;
    }
  }
  else
  {
    d_quants.clear();
  }
  if (Trace.isOn("inst-engine"))
  {
    double clSet2 = double(clock()) / double(CLOCKS_PER_SEC);
    Trace("inst-engine") << "Finished instantiation engine, time = "
                         << (clSet2 - clSet) << std::endl;
  }
}

bool InstantiationEngine::checkCompleteFor( Node q ) {
  //TODO?
  return false;
}

void InstantiationEngine::checkOwnership(Node q)
{
  if (options::userPatternsQuant() == options::UserPatMode::STRICT
      && q.getNumChildren() == 3)
  {
    //if strict triggers, take ownership of this quantified formula
    bool hasPat = false;
    for (const Node& qc : q[2])
    {
      if (qc.getKind() == INST_PATTERN || qc.getKind() == INST_NO_PATTERN)
      {
        hasPat = true;
        break;
      }
    }
    if( hasPat ){
      d_qreg.setOwner(q, this, 1);
    }
  }
}

void InstantiationEngine::registerQuantifier(Node q)
{
  if (!shouldProcess(q))
  {
    return;
  }
  if (d_quant_rel)
  {
    d_quant_rel->registerQuantifier(q);
  }
  // take into account user patterns
  if (q.getNumChildren() == 3)
  {
    Node subsPat = d_qreg.substituteBoundVariablesToInstConstants(q[2], q);
    // add patterns
    for (const Node& p : subsPat)
    {
      if (p.getKind() == INST_PATTERN)
      {
        addUserPattern(q, p);
      }
      else if (p.getKind() == INST_NO_PATTERN)
      {
        addUserNoPattern(q, p);
      }
    }
  }
}

void InstantiationEngine::addUserPattern(Node q, Node pat) {
  if (d_isup) {
    d_isup->addUserPattern(q, pat);
  }
}

void InstantiationEngine::addUserNoPattern(Node q, Node pat) {
  if (d_i_ag) {
    d_i_ag->addUserNoPattern(q, pat);
  }
}

bool InstantiationEngine::shouldProcess(Node q)
{
  if (!d_qreg.hasOwnership(q, this))
  {
    return false;
  }
  // also ignore internal quantifiers
  QuantAttributes& qattr = d_qreg.getQuantAttributes();
  if (qattr.isInternal(q))
  {
    return false;
  }
  return true;
}

}  // 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, Tim King
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 instantiation engine class
14		*/
15
16		#include "theory/quantifiers/ematching/instantiation_engine.h"
17
18		#include "options/quantifiers_options.h"
19		#include "theory/quantifiers/ematching/inst_strategy_e_matching.h"
20		#include "theory/quantifiers/ematching/inst_strategy_e_matching_user.h"
21		#include "theory/quantifiers/ematching/trigger.h"
22		#include "theory/quantifiers/first_order_model.h"
23		#include "theory/quantifiers/quantifiers_attributes.h"
24		#include "theory/quantifiers/term_database.h"
25		#include "theory/quantifiers/term_util.h"
26
27		using namespace cvc5::kind;
28		using namespace cvc5::context;
29		using namespace cvc5::theory::quantifiers::inst;
30
31		namespace cvc5 {
32		namespace theory {
33		namespace quantifiers {
34
35	6506	InstantiationEngine::InstantiationEngine(QuantifiersState& qs,
36		QuantifiersInferenceManager& qim,
37		QuantifiersRegistry& qr,
38	6506	TermRegistry& tr)
39		: QuantifiersModule(qs, qim, qr, tr),
40		d_instStrategies(),
41		d_isup(),
42		d_i_ag(),
43		d_quants(),
44		d_trdb(qs, qim, qr, tr),
45	6506	d_quant_rel(nullptr)
46		{
47	6506	if (options::relevantTriggers())
48		{
49	4	d_quant_rel.reset(new quantifiers::QuantRelevance);
50		}
51	6506	if (options::eMatching()) {
52		// these are the instantiation strategies for E-matching
53		// user-provided patterns
54	6504	if (options::userPatternsQuant() != options::UserPatMode::IGNORE)
55		{
56	6504	d_isup.reset(new InstStrategyUserPatterns(d_trdb, qs, qim, qr, tr));
57	6504	d_instStrategies.push_back(d_isup.get());
58		}
59
60		// auto-generated patterns
61	13008	d_i_ag.reset(new InstStrategyAutoGenTriggers(
62	6504	d_trdb, qs, qim, qr, tr, d_quant_rel.get()));
63	6504	d_instStrategies.push_back(d_i_ag.get());
64		}
65	6506	}
66
67	13012	InstantiationEngine::~InstantiationEngine() {}
68
69	7857	void InstantiationEngine::presolve() {
70	23567	for( unsigned i=0; i<d_instStrategies.size(); ++i ){
71	15710	d_instStrategies[i]->presolve();
72		}
73	7857	}
74
75	2252	void InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
76	2252	size_t lastWaiting = d_qim.numPendingLemmas();
77		//iterate over an internal effort level e
78	2252	int e = 0;
79	2252	int eLimit = effort==Theory::EFFORT_LAST_CALL ? 10 : 2;
80	2252	bool finished = false;
81		//while unfinished, try effort level=0,1,2....
82	11260	while( !finished && e<=eLimit ){
83	4504	Debug("inst-engine") << "IE: Prepare instantiation (" << e << ")." << std::endl;
84	4504	finished = true;
85		//instantiate each quantifier
86	87690	for( unsigned i=0; i<d_quants.size(); i++ ){
87	166372	Node q = d_quants[i];
88	83186	Debug("inst-engine-debug") << "IE: Instantiate " << q << "..." << std::endl;
89		//int e_use = d_quantEngine->getRelevance( q )==-1 ? e - 1 : e;
90	83186	int e_use = e;
91	83186	if( e_use>=0 ){
92	83186	Trace("inst-engine-debug") << "inst-engine : " << q << std::endl;
93		//check each instantiation strategy
94	249558	for( unsigned j=0; j<d_instStrategies.size(); j++ ){
95	166372	InstStrategy* is = d_instStrategies[j];
96	166372	Trace("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl;
97	166372	InstStrategyStatus quantStatus = is->process(q, effort, e_use);
98	332744	Trace("inst-engine-debug")
99	166372	<< " -> unfinished= "
100	332744	<< (quantStatus == InstStrategyStatus::STATUS_UNFINISHED)
101	166372	<< ", conflict=" << d_qstate.isInConflict() << std::endl;
102	166372	if (d_qstate.isInConflict())
103		{
104		return;
105		}
106	166372	else if (quantStatus == InstStrategyStatus::STATUS_UNFINISHED)
107		{
108	69643	finished = false;
109		}
110		}
111		}
112		}
113		//do not consider another level if already added lemma at this level
114	4504	if (d_qim.numPendingLemmas() > lastWaiting)
115		{
116	1181	finished = true;
117		}
118	4504	e++;
119		}
120		}
121
122	66653	bool InstantiationEngine::needsCheck( Theory::Effort e ){
123	66653	return d_qstate.getInstWhenNeedsCheck(e);
124		}
125
126	24146	void InstantiationEngine::reset_round( Theory::Effort e ){
127		//if not, proceed to instantiation round
128		//reset the instantiation strategies
129	72432	for( unsigned i=0; i<d_instStrategies.size(); ++i ){
130	48286	InstStrategy* is = d_instStrategies[i];
131	48286	is->processResetInstantiationRound( e );
132		}
133	24146	}
134
135	38225	void InstantiationEngine::check(Theory::Effort e, QEffort quant_e)
136		{
137	51278	CodeTimer codeTimer(d_qstate.getStats().d_ematching_time);
138	38225	if (quant_e != QEFFORT_STANDARD)
139		{
140	25172	return;
141		}
142	13053	double clSet = 0;
143	13053	if (Trace.isOn("inst-engine"))
144		{
145		clSet = double(clock()) / double(CLOCKS_PER_SEC);
146		Trace("inst-engine") << "---Instantiation Engine Round, effort = " << e
147		<< "---" << std::endl;
148		}
149		// collect all active quantified formulas belonging to this
150	13053	bool quantActive = false;
151	13053	d_quants.clear();
152	13053	FirstOrderModel* m = d_treg.getModel();
153	13053	size_t nquant = m->getNumAssertedQuantifiers();
154	71124	for (size_t i = 0; i < nquant; i++)
155		{
156	116142	Node q = m->getAssertedQuantifier(i, true);
157	58071	if (shouldProcess(q) && m->isQuantifierActive(q))
158		{
159	41593	quantActive = true;
160	41593	d_quants.push_back(q);
161		}
162		}
163	26106	Trace("inst-engine-debug")
164	13053	<< "InstEngine: check: # asserted quantifiers " << d_quants.size() << "/";
165	13053	Trace("inst-engine-debug") << nquant << " " << quantActive << std::endl;
166	13053	if (quantActive)
167		{
168	2252	size_t lastWaiting = d_qim.numPendingLemmas();
169	2252	doInstantiationRound(e);
170	2252	if (d_qstate.isInConflict())
171		{
172		Assert(d_qim.numPendingLemmas() > lastWaiting);
173		Trace("inst-engine") << "Conflict, added lemmas = "
174		<< (d_qim.numPendingLemmas() - lastWaiting)
175		<< std::endl;
176		}
177	2252	else if (d_qim.hasPendingLemma())
178		{
179	2362	Trace("inst-engine") << "Added lemmas = "
180	2362	<< (d_qim.numPendingLemmas() - lastWaiting)
181	1181	<< std::endl;
182		}
183		}
184		else
185		{
186	10801	d_quants.clear();
187		}
188	13053	if (Trace.isOn("inst-engine"))
189		{
190		double clSet2 = double(clock()) / double(CLOCKS_PER_SEC);
191		Trace("inst-engine") << "Finished instantiation engine, time = "
192		<< (clSet2 - clSet) << std::endl;
193		}
194		}
195
196	544	bool InstantiationEngine::checkCompleteFor( Node q ) {
197		//TODO?
198	544	return false;
199		}
200
201	22787	void InstantiationEngine::checkOwnership(Node q)
202		{
203	45574	if (options::userPatternsQuant() == options::UserPatMode::STRICT
204	22787	&& q.getNumChildren() == 3)
205		{
206		//if strict triggers, take ownership of this quantified formula
207		bool hasPat = false;
208		for (const Node& qc : q[2])
209		{
210		if (qc.getKind() == INST_PATTERN \|\| qc.getKind() == INST_NO_PATTERN)
211		{
212		hasPat = true;
213		break;
214		}
215		}
216		if( hasPat ){
217		d_qreg.setOwner(q, this, 1);
218		}
219		}
220	22787	}
221
222	22787	void InstantiationEngine::registerQuantifier(Node q)
223		{
224	22787	if (!shouldProcess(q))
225		{
226	3373	return;
227		}
228	19414	if (d_quant_rel)
229		{
230	344	d_quant_rel->registerQuantifier(q);
231		}
232		// take into account user patterns
233	19414	if (q.getNumChildren() == 3)
234		{
235	7942	Node subsPat = d_qreg.substituteBoundVariablesToInstConstants(q[2], q);
236		// add patterns
237	8410	for (const Node& p : subsPat)
238		{
239	4439	if (p.getKind() == INST_PATTERN)
240		{
241	3902	addUserPattern(q, p);
242		}
243	537	else if (p.getKind() == INST_NO_PATTERN)
244		{
245	8	addUserNoPattern(q, p);
246		}
247		}
248		}
249		}
250
251	3902	void InstantiationEngine::addUserPattern(Node q, Node pat) {
252	3902	if (d_isup) {
253	3902	d_isup->addUserPattern(q, pat);
254		}
255	3902	}
256
257	8	void InstantiationEngine::addUserNoPattern(Node q, Node pat) {
258	8	if (d_i_ag) {
259	8	d_i_ag->addUserNoPattern(q, pat);
260		}
261	8	}
262
263	80858	bool InstantiationEngine::shouldProcess(Node q)
264		{
265	80858	if (!d_qreg.hasOwnership(q, this))
266		{
267	16966	return false;
268		}
269		// also ignore internal quantifiers
270	63892	QuantAttributes& qattr = d_qreg.getQuantAttributes();
271	63892	if (qattr.isInternal(q))
272		{
273	2843	return false;
274		}
275	61049	return true;
276		}
277
278		} // namespace quantifiers
279		} // namespace theory
280	29349	} // namespace cvc5