Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/ematching/inst_match_generator_simple.cpp	Lines:	79	90	87.8 %
Date:	2021-09-29	Branches:	184	422	43.6 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Mathias Preiner, 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.
 * ****************************************************************************
 *
 * Simple inst match generator class.
 */
#include "theory/quantifiers/ematching/inst_match_generator_simple.h"

#include "options/quantifiers_options.h"
#include "theory/quantifiers/ematching/trigger_term_info.h"
#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/quantifiers_state.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_registry.h"
#include "theory/quantifiers/term_util.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace quantifiers {
namespace inst {

InstMatchGeneratorSimple::InstMatchGeneratorSimple(Trigger* tparent,
                                                   Node q,
                                                   Node pat)
    : IMGenerator(tparent), d_quant(q), d_match_pattern(pat)
{
  if (d_match_pattern.getKind() == NOT)
  {
    d_match_pattern = d_match_pattern[0];
    d_pol = false;
  }
  else
  {
    d_pol = true;
  }
  if (d_match_pattern.getKind() == EQUAL)
  {
    d_eqc = d_match_pattern[1];
    d_match_pattern = d_match_pattern[0];
    Assert(!TermUtil::hasInstConstAttr(d_eqc));
  }
  Assert(TriggerTermInfo::isSimpleTrigger(d_match_pattern));
  for (size_t i = 0, nchild = d_match_pattern.getNumChildren(); i < nchild; i++)
  {
    if (d_match_pattern[i].getKind() == INST_CONSTANT)
    {
      if (!options::cegqi()
          || TermUtil::getInstConstAttr(d_match_pattern[i]) == q)
      {
        d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute());
      }
      else
      {
        d_var_num[i] = -1;
      }
    }
    d_match_pattern_arg_types.push_back(d_match_pattern[i].getType());
  }
  TermDb* tdb = d_treg.getTermDatabase();
  d_op = tdb->getMatchOperator(d_match_pattern);
}

void InstMatchGeneratorSimple::resetInstantiationRound() {}
uint64_t InstMatchGeneratorSimple::addInstantiations(Node q)
{
  uint64_t addedLemmas = 0;
  TNodeTrie* tat;
  TermDb* tdb = d_treg.getTermDatabase();
  if (d_eqc.isNull())
  {
    tat = tdb->getTermArgTrie(d_op);
  }
  else
  {
    if (d_pol)
    {
      tat = tdb->getTermArgTrie(d_eqc, d_op);
    }
    else
    {
      // iterate over all classes except r
      tat = tdb->getTermArgTrie(Node::null(), d_op);
      if (tat && !d_qstate.isInConflict())
      {
        Node r = d_qstate.getRepresentative(d_eqc);
        for (std::pair<const TNode, TNodeTrie>& t : tat->d_data)
        {
          if (t.first != r)
          {
            InstMatch m(q);
            addInstantiations(m, addedLemmas, 0, &(t.second));
            if (d_qstate.isInConflict())
            {
              break;
            }
          }
        }
      }
      tat = nullptr;
    }
  }
  Debug("simple-trigger-debug")
      << "Adding instantiations based on " << tat << " from " << d_op << " "
      << d_eqc << std::endl;
  if (tat && !d_qstate.isInConflict())
  {
    InstMatch m(q);
    addInstantiations(m, addedLemmas, 0, tat);
  }
  return addedLemmas;
}

void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
                                                 uint64_t& addedLemmas,
                                                 size_t argIndex,
                                                 TNodeTrie* tat)
{
  Debug("simple-trigger-debug")
      << "Add inst " << argIndex << " " << d_match_pattern << std::endl;
  if (argIndex == d_match_pattern.getNumChildren())
  {
    Assert(!tat->d_data.empty());
    TNode t = tat->getData();
    Debug("simple-trigger") << "Actual term is " << t << std::endl;
    // convert to actual used terms
    for (const auto& v : d_var_num)
    {
      if (v.second >= 0)
      {
        Assert(v.first < t.getNumChildren());
        Debug("simple-trigger")
            << "...set " << v.second << " " << t[v.first] << std::endl;
        m.setValue(v.second, t[v.first]);
      }
    }
    // we do not need the trigger parent for simple triggers (no post-processing
    // required)
    if (sendInstantiation(m, InferenceId::QUANTIFIERS_INST_E_MATCHING_SIMPLE))
    {
      addedLemmas++;
      Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl;
    }
    return;
  }
  if (d_match_pattern[argIndex].getKind() == INST_CONSTANT)
  {
    int v = d_var_num[argIndex];
    if (v != -1)
    {
      for (std::pair<const TNode, TNodeTrie>& tt : tat->d_data)
      {
        Node t = tt.first;
        Node prev = m.get(v);
        // using representatives, just check if equal
        Assert(t.getType().isComparableTo(d_match_pattern_arg_types[argIndex]));
        if (prev.isNull() || prev == t)
        {
          m.setValue(v, t);
          addInstantiations(m, addedLemmas, argIndex + 1, &(tt.second));
          m.setValue(v, prev);
          if (d_qstate.isInConflict())
          {
            break;
          }
        }
      }
      return;
    }
    // inst constant from another quantified formula, treat as ground term?
  }
  Node r = d_qstate.getRepresentative(d_match_pattern[argIndex]);
  std::map<TNode, TNodeTrie>::iterator it = tat->d_data.find(r);
  if (it != tat->d_data.end())
  {
    addInstantiations(m, addedLemmas, argIndex + 1, &(it->second));
  }
}

int InstMatchGeneratorSimple::getActiveScore()
{
  TermDb* tdb = d_treg.getTermDatabase();
  Node f = tdb->getMatchOperator(d_match_pattern);
  size_t ngt = tdb->getNumGroundTerms(f);
  Trace("trigger-active-sel-debug") << "Number of ground terms for (simple) "
                                    << f << " is " << ngt << std::endl;
  return static_cast<int>(ngt);
}

}  // namespace inst
}  // 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, Mathias Preiner, 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		* Simple inst match generator class.
14		*/
15		#include "theory/quantifiers/ematching/inst_match_generator_simple.h"
16
17		#include "options/quantifiers_options.h"
18		#include "theory/quantifiers/ematching/trigger_term_info.h"
19		#include "theory/quantifiers/instantiate.h"
20		#include "theory/quantifiers/quantifiers_state.h"
21		#include "theory/quantifiers/term_database.h"
22		#include "theory/quantifiers/term_registry.h"
23		#include "theory/quantifiers/term_util.h"
24
25		using namespace cvc5::kind;
26
27		namespace cvc5 {
28		namespace theory {
29		namespace quantifiers {
30		namespace inst {
31
32	2619	InstMatchGeneratorSimple::InstMatchGeneratorSimple(Trigger* tparent,
33		Node q,
34	2619	Node pat)
35	2619	: IMGenerator(tparent), d_quant(q), d_match_pattern(pat)
36		{
37	2619	if (d_match_pattern.getKind() == NOT)
38		{
39	424	d_match_pattern = d_match_pattern[0];
40	424	d_pol = false;
41		}
42		else
43		{
44	2195	d_pol = true;
45		}
46	2619	if (d_match_pattern.getKind() == EQUAL)
47		{
48	424	d_eqc = d_match_pattern[1];
49	424	d_match_pattern = d_match_pattern[0];
50	424	Assert(!TermUtil::hasInstConstAttr(d_eqc));
51		}
52	2619	Assert(TriggerTermInfo::isSimpleTrigger(d_match_pattern));
53	8249	for (size_t i = 0, nchild = d_match_pattern.getNumChildren(); i < nchild; i++)
54		{
55	5630	if (d_match_pattern[i].getKind() == INST_CONSTANT)
56		{
57	8850	if (!options::cegqi()
58	8850	\|\| TermUtil::getInstConstAttr(d_match_pattern[i]) == q)
59		{
60	4425	d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute());
61		}
62		else
63		{
64		d_var_num[i] = -1;
65		}
66		}
67	5630	d_match_pattern_arg_types.push_back(d_match_pattern[i].getType());
68		}
69	2619	TermDb* tdb = d_treg.getTermDatabase();
70	2619	d_op = tdb->getMatchOperator(d_match_pattern);
71	2619	}
72
73	23195	void InstMatchGeneratorSimple::resetInstantiationRound() {}
74	8851	uint64_t InstMatchGeneratorSimple::addInstantiations(Node q)
75		{
76	8851	uint64_t addedLemmas = 0;
77		TNodeTrie* tat;
78	8851	TermDb* tdb = d_treg.getTermDatabase();
79	8851	if (d_eqc.isNull())
80		{
81	7185	tat = tdb->getTermArgTrie(d_op);
82		}
83		else
84		{
85	1666	if (d_pol)
86		{
87		tat = tdb->getTermArgTrie(d_eqc, d_op);
88		}
89		else
90		{
91		// iterate over all classes except r
92	1666	tat = tdb->getTermArgTrie(Node::null(), d_op);
93	1666	if (tat && !d_qstate.isInConflict())
94		{
95	3332	Node r = d_qstate.getRepresentative(d_eqc);
96	5215	for (std::pair<const TNode, TNodeTrie>& t : tat->d_data)
97		{
98	3549	if (t.first != r)
99		{
100	5000	InstMatch m(q);
101	2500	addInstantiations(m, addedLemmas, 0, &(t.second));
102	2500	if (d_qstate.isInConflict())
103		{
104		break;
105		}
106		}
107		}
108		}
109	1666	tat = nullptr;
110		}
111		}
112	17702	Debug("simple-trigger-debug")
113	8851	<< "Adding instantiations based on " << tat << " from " << d_op << " "
114	8851	<< d_eqc << std::endl;
115	8851	if (tat && !d_qstate.isInConflict())
116		{
117	8310	InstMatch m(q);
118	4155	addInstantiations(m, addedLemmas, 0, tat);
119		}
120	8851	return addedLemmas;
121		}
122
123	63451	void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
124		uint64_t& addedLemmas,
125		size_t argIndex,
126		TNodeTrie* tat)
127		{
128	126902	Debug("simple-trigger-debug")
129	63451	<< "Add inst " << argIndex << " " << d_match_pattern << std::endl;
130	63451	if (argIndex == d_match_pattern.getNumChildren())
131		{
132	16569	Assert(!tat->d_data.empty());
133	33138	TNode t = tat->getData();
134	16569	Debug("simple-trigger") << "Actual term is " << t << std::endl;
135		// convert to actual used terms
136	55682	for (const auto& v : d_var_num)
137		{
138	39113	if (v.second >= 0)
139		{
140	39113	Assert(v.first < t.getNumChildren());
141	78226	Debug("simple-trigger")
142	39113	<< "...set " << v.second << " " << t[v.first] << std::endl;
143	39113	m.setValue(v.second, t[v.first]);
144		}
145		}
146		// we do not need the trigger parent for simple triggers (no post-processing
147		// required)
148	16569	if (sendInstantiation(m, InferenceId::QUANTIFIERS_INST_E_MATCHING_SIMPLE))
149		{
150	4473	addedLemmas++;
151	4473	Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl;
152		}
153	16569	return;
154		}
155	46882	if (d_match_pattern[argIndex].getKind() == INST_CONSTANT)
156		{
157	26102	int v = d_var_num[argIndex];
158	26102	if (v != -1)
159		{
160	80953	for (std::pair<const TNode, TNodeTrie>& tt : tat->d_data)
161		{
162	109702	Node t = tt.first;
163	109702	Node prev = m.get(v);
164		// using representatives, just check if equal
165	54851	Assert(t.getType().isComparableTo(d_match_pattern_arg_types[argIndex]));
166	54851	if (prev.isNull() \|\| prev == t)
167		{
168	53595	m.setValue(v, t);
169	53595	addInstantiations(m, addedLemmas, argIndex + 1, &(tt.second));
170	53595	m.setValue(v, prev);
171	53595	if (d_qstate.isInConflict())
172		{
173		break;
174		}
175		}
176		}
177	26102	return;
178		}
179		// inst constant from another quantified formula, treat as ground term?
180		}
181	41560	Node r = d_qstate.getRepresentative(d_match_pattern[argIndex]);
182	20780	std::map<TNode, TNodeTrie>::iterator it = tat->d_data.find(r);
183	20780	if (it != tat->d_data.end())
184		{
185	3201	addInstantiations(m, addedLemmas, argIndex + 1, &(it->second));
186		}
187		}
188
189		int InstMatchGeneratorSimple::getActiveScore()
190		{
191		TermDb* tdb = d_treg.getTermDatabase();
192		Node f = tdb->getMatchOperator(d_match_pattern);
193		size_t ngt = tdb->getNumGroundTerms(f);
194		Trace("trigger-active-sel-debug") << "Number of ground terms for (simple) "
195		<< f << " is " << ngt << std::endl;
196		return static_cast<int>(ngt);
197		}
198
199		} // namespace inst
200		} // namespace quantifiers
201		} // namespace theory
202	22746	} // namespace cvc5