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