Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp	Lines:	52	79	65.8 %
Date:	2021-09-29	Branches:	90	239	37.7 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Morgan Deters, 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 e-matching instantiation strategies.
 */

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

#include "theory/quantifiers/ematching/pattern_term_selector.h"
#include "theory/quantifiers/ematching/trigger_database.h"
#include "theory/quantifiers/quantifiers_state.h"

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

namespace cvc5 {
namespace theory {
namespace quantifiers {

InstStrategyUserPatterns::InstStrategyUserPatterns(
    Env& env,
    inst::TriggerDatabase& td,
    QuantifiersState& qs,
    QuantifiersInferenceManager& qim,
    QuantifiersRegistry& qr,
    TermRegistry& tr)
    : InstStrategy(env, td, qs, qim, qr, tr)
{
}
InstStrategyUserPatterns::~InstStrategyUserPatterns() {}

size_t InstStrategyUserPatterns::getNumUserGenerators(Node q) const
{
  std::map<Node, std::vector<Trigger*> >::const_iterator it =
      d_user_gen.find(q);
  if (it == d_user_gen.end())
  {
    return 0;
  }
  return it->second.size();
}

Trigger* InstStrategyUserPatterns::getUserGenerator(Node q, size_t i) const
{
  std::map<Node, std::vector<Trigger*> >::const_iterator it =
      d_user_gen.find(q);
  if (it == d_user_gen.end())
  {
    return nullptr;
  }
  Assert(i < it->second.size());
  return it->second[i];
}

std::string InstStrategyUserPatterns::identify() const
{
  return std::string("UserPatterns");
}

void InstStrategyUserPatterns::processResetInstantiationRound(
    Theory::Effort effort)
{
  Trace("inst-alg-debug") << "reset user triggers" << std::endl;
  // reset triggers
  for (std::pair<const Node, std::vector<Trigger*> >& u : d_user_gen)
  {
    for (Trigger* t : u.second)
    {
      t->resetInstantiationRound();
      t->reset(Node::null());
    }
  }
  Trace("inst-alg-debug") << "done reset user triggers" << std::endl;
}

InstStrategyStatus InstStrategyUserPatterns::process(Node q,
                                                     Theory::Effort effort,
                                                     int e)
{
  if (e == 0)
  {
    return InstStrategyStatus::STATUS_UNFINISHED;
  }
  options::UserPatMode upm = getInstUserPatMode();
  int peffort = upm == options::UserPatMode::RESORT ? 2 : 1;
  if (e < peffort)
  {
    return InstStrategyStatus::STATUS_UNFINISHED;
  }
  if (e != peffort)
  {
    return InstStrategyStatus::STATUS_UNKNOWN;
  }
  d_counter[q]++;

  Trace("inst-alg") << "-> User-provided instantiate " << q << "..."
                    << std::endl;
  if (upm == options::UserPatMode::RESORT)
  {
    std::vector<std::vector<Node> >& ugw = d_user_gen_wait[q];
    for (size_t i = 0, usize = ugw.size(); i < usize; i++)
    {
      Trigger* t =
          d_td.mkTrigger(q, ugw[i], true, TriggerDatabase::TR_RETURN_NULL);
      if (t)
      {
        d_user_gen[q].push_back(t);
      }
    }
    ugw.clear();
  }

  std::vector<Trigger*>& ug = d_user_gen[q];
  for (Trigger* t : ug)
  {
    if (Trace.isOn("process-trigger"))
    {
      Trace("process-trigger") << "  Process (user) ";
      t->debugPrint("process-trigger");
      Trace("process-trigger") << "..." << std::endl;
    }
    unsigned numInst = t->addInstantiations();
    Trace("process-trigger")
        << "  Done, numInst = " << numInst << "." << std::endl;
    if (d_qstate.isInConflict())
    {
      // we are already in conflict
      break;
    }
  }
  return InstStrategyStatus::STATUS_UNKNOWN;
}

void InstStrategyUserPatterns::addUserPattern(Node q, Node pat)
{
  Assert(pat.getKind() == INST_PATTERN);
  // add to generators
  std::vector<Node> nodes;
  for (const Node& p : pat)
  {
    if (std::find(nodes.begin(), nodes.end(), p) != nodes.end())
    {
      // skip duplicate pattern term
      continue;
    }
    Node pat_use = PatternTermSelector::getIsUsableTrigger(p, q);
    if (pat_use.isNull())
    {
      Trace("trigger-warn") << "User-provided trigger is not usable : " << pat
                            << " because of " << p << std::endl;
      return;
    }
    nodes.push_back(pat_use);
  }
  Trace("user-pat") << "Add user pattern: " << pat << " for " << q << std::endl;
  // check match option
  if (getInstUserPatMode() == options::UserPatMode::RESORT)
  {
    d_user_gen_wait[q].push_back(nodes);
    return;
  }
  Trigger* t = d_td.mkTrigger(q, nodes, true, TriggerDatabase::TR_MAKE_NEW);
  if (t)
  {
    d_user_gen[q].push_back(t);
  }
  else
  {
    Trace("trigger-warn") << "Failed to construct trigger : " << pat
                          << " due to variable mismatch" << 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, 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 e-matching instantiation strategies.
14		*/
15
16		#include "theory/quantifiers/ematching/inst_strategy_e_matching_user.h"
17
18		#include "theory/quantifiers/ematching/pattern_term_selector.h"
19		#include "theory/quantifiers/ematching/trigger_database.h"
20		#include "theory/quantifiers/quantifiers_state.h"
21
22		using namespace cvc5::kind;
23		using namespace cvc5::theory::quantifiers::inst;
24
25		namespace cvc5 {
26		namespace theory {
27		namespace quantifiers {
28
29	4578	InstStrategyUserPatterns::InstStrategyUserPatterns(
30		Env& env,
31		inst::TriggerDatabase& td,
32		QuantifiersState& qs,
33		QuantifiersInferenceManager& qim,
34		QuantifiersRegistry& qr,
35	4578	TermRegistry& tr)
36	4578	: InstStrategy(env, td, qs, qim, qr, tr)
37		{
38	4578	}
39	9150	InstStrategyUserPatterns::~InstStrategyUserPatterns() {}
40
41		size_t InstStrategyUserPatterns::getNumUserGenerators(Node q) const
42		{
43		std::map<Node, std::vector<Trigger*> >::const_iterator it =
44		d_user_gen.find(q);
45		if (it == d_user_gen.end())
46		{
47		return 0;
48		}
49		return it->second.size();
50		}
51
52		Trigger* InstStrategyUserPatterns::getUserGenerator(Node q, size_t i) const
53		{
54		std::map<Node, std::vector<Trigger*> >::const_iterator it =
55		d_user_gen.find(q);
56		if (it == d_user_gen.end())
57		{
58		return nullptr;
59		}
60		Assert(i < it->second.size());
61		return it->second[i];
62		}
63
64	29452	std::string InstStrategyUserPatterns::identify() const
65		{
66	29452	return std::string("UserPatterns");
67		}
68
69	16304	void InstStrategyUserPatterns::processResetInstantiationRound(
70		Theory::Effort effort)
71		{
72	16304	Trace("inst-alg-debug") << "reset user triggers" << std::endl;
73		// reset triggers
74	53581	for (std::pair<const Node, std::vector<Trigger*> >& u : d_user_gen)
75		{
76	54239	for (Trigger* t : u.second)
77		{
78	16962	t->resetInstantiationRound();
79	16962	t->reset(Node::null());
80		}
81		}
82	16304	Trace("inst-alg-debug") << "done reset user triggers" << std::endl;
83	16304	}
84
85	29452	InstStrategyStatus InstStrategyUserPatterns::process(Node q,
86		Theory::Effort effort,
87		int e)
88		{
89	29452	if (e == 0)
90		{
91	14726	return InstStrategyStatus::STATUS_UNFINISHED;
92		}
93	14726	options::UserPatMode upm = getInstUserPatMode();
94	14726	int peffort = upm == options::UserPatMode::RESORT ? 2 : 1;
95	14726	if (e < peffort)
96		{
97		return InstStrategyStatus::STATUS_UNFINISHED;
98		}
99	14726	if (e != peffort)
100		{
101		return InstStrategyStatus::STATUS_UNKNOWN;
102		}
103	14726	d_counter[q]++;
104
105	29452	Trace("inst-alg") << "-> User-provided instantiate " << q << "..."
106	14726	<< std::endl;
107	14726	if (upm == options::UserPatMode::RESORT)
108		{
109		std::vector<std::vector<Node> >& ugw = d_user_gen_wait[q];
110		for (size_t i = 0, usize = ugw.size(); i < usize; i++)
111		{
112		Trigger* t =
113		d_td.mkTrigger(q, ugw[i], true, TriggerDatabase::TR_RETURN_NULL);
114		if (t)
115		{
116		d_user_gen[q].push_back(t);
117		}
118		}
119		ugw.clear();
120		}
121
122	14726	std::vector<Trigger*>& ug = d_user_gen[q];
123	18451	for (Trigger* t : ug)
124		{
125	3725	if (Trace.isOn("process-trigger"))
126		{
127		Trace("process-trigger") << " Process (user) ";
128		t->debugPrint("process-trigger");
129		Trace("process-trigger") << "..." << std::endl;
130		}
131	3725	unsigned numInst = t->addInstantiations();
132	7450	Trace("process-trigger")
133	3725	<< " Done, numInst = " << numInst << "." << std::endl;
134	3725	if (d_qstate.isInConflict())
135		{
136		// we are already in conflict
137		break;
138		}
139		}
140	14726	return InstStrategyStatus::STATUS_UNKNOWN;
141		}
142
143	1224	void InstStrategyUserPatterns::addUserPattern(Node q, Node pat)
144		{
145	1224	Assert(pat.getKind() == INST_PATTERN);
146		// add to generators
147	2441	std::vector<Node> nodes;
148	2521	for (const Node& p : pat)
149		{
150	1305	if (std::find(nodes.begin(), nodes.end(), p) != nodes.end())
151		{
152		// skip duplicate pattern term
153	1	continue;
154		}
155	2601	Node pat_use = PatternTermSelector::getIsUsableTrigger(p, q);
156	1304	if (pat_use.isNull())
157		{
158	14	Trace("trigger-warn") << "User-provided trigger is not usable : " << pat
159	7	<< " because of " << p << std::endl;
160	7	return;
161		}
162	1297	nodes.push_back(pat_use);
163		}
164	1217	Trace("user-pat") << "Add user pattern: " << pat << " for " << q << std::endl;
165		// check match option
166	1217	if (getInstUserPatMode() == options::UserPatMode::RESORT)
167		{
168		d_user_gen_wait[q].push_back(nodes);
169		return;
170		}
171	1217	Trigger* t = d_td.mkTrigger(q, nodes, true, TriggerDatabase::TR_MAKE_NEW);
172	1217	if (t)
173		{
174	1217	d_user_gen[q].push_back(t);
175		}
176		else
177		{
178		Trace("trigger-warn") << "Failed to construct trigger : " << pat
179		<< " due to variable mismatch" << std::endl;
180		}
181		}
182
183		} // namespace quantifiers
184		} // namespace theory
185	22746	} // namespace cvc5