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-07	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	7721	InstMatchGeneratorSimple::InstMatchGeneratorSimple(Trigger* tparent,
33		Node q,
34	7721	Node pat)
35	7721	: IMGenerator(tparent), d_quant(q), d_match_pattern(pat)
36		{
37	7721	if (d_match_pattern.getKind() == NOT)
38		{
39	1289	d_match_pattern = d_match_pattern[0];
40	1289	d_pol = false;
41		}
42		else
43		{
44	6432	d_pol = true;
45		}
46	7721	if (d_match_pattern.getKind() == EQUAL)
47		{
48	1289	d_eqc = d_match_pattern[1];
49	1289	d_match_pattern = d_match_pattern[0];
50	1289	Assert(!TermUtil::hasInstConstAttr(d_eqc));
51		}
52	7721	Assert(TriggerTermInfo::isSimpleTrigger(d_match_pattern));
53	24899	for (size_t i = 0, nchild = d_match_pattern.getNumChildren(); i < nchild; i++)
54		{
55	17178	if (d_match_pattern[i].getKind() == INST_CONSTANT)
56		{
57	27148	if (!options::cegqi()
58	27148	\|\| TermUtil::getInstConstAttr(d_match_pattern[i]) == q)
59		{
60	13574	d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute());
61		}
62		else
63		{
64		d_var_num[i] = -1;
65		}
66		}
67	17178	d_match_pattern_arg_types.push_back(d_match_pattern[i].getType());
68		}
69	7721	TermDb* tdb = d_treg.getTermDatabase();
70	7721	d_op = tdb->getMatchOperator(d_match_pattern);
71	7721	}
72
73	74137	void InstMatchGeneratorSimple::resetInstantiationRound() {}
74	25592	uint64_t InstMatchGeneratorSimple::addInstantiations(Node q)
75		{
76	25592	uint64_t addedLemmas = 0;
77		TNodeTrie* tat;
78	25592	TermDb* tdb = d_treg.getTermDatabase();
79	25592	if (d_eqc.isNull())
80		{
81	20558	tat = tdb->getTermArgTrie(d_op);
82		}
83		else
84		{
85	5034	if (d_pol)
86		{
87		tat = tdb->getTermArgTrie(d_eqc, d_op);
88		}
89		else
90		{
91		// iterate over all classes except r
92	5034	tat = tdb->getTermArgTrie(Node::null(), d_op);
93	5034	if (tat && !d_qstate.isInConflict())
94		{
95	10068	Node r = d_qstate.getRepresentative(d_eqc);
96	16456	for (std::pair<const TNode, TNodeTrie>& t : tat->d_data)
97		{
98	11422	if (t.first != r)
99		{
100	16496	InstMatch m(q);
101	8248	addInstantiations(m, addedLemmas, 0, &(t.second));
102	8248	if (d_qstate.isInConflict())
103		{
104		break;
105		}
106		}
107		}
108		}
109	5034	tat = nullptr;
110		}
111		}
112	51184	Debug("simple-trigger-debug")
113	25592	<< "Adding instantiations based on " << tat << " from " << d_op << " "
114	25592	<< d_eqc << std::endl;
115	25592	if (tat && !d_qstate.isInConflict())
116		{
117	24272	InstMatch m(q);
118	12136	addInstantiations(m, addedLemmas, 0, tat);
119		}
120	25592	return addedLemmas;
121		}
122
123	201238	void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
124		uint64_t& addedLemmas,
125		size_t argIndex,
126		TNodeTrie* tat)
127		{
128	402476	Debug("simple-trigger-debug")
129	201238	<< "Add inst " << argIndex << " " << d_match_pattern << std::endl;
130	201238	if (argIndex == d_match_pattern.getNumChildren())
131		{
132	50028	Assert(!tat->d_data.empty());
133	100056	TNode t = tat->getData();
134	50028	Debug("simple-trigger") << "Actual term is " << t << std::endl;
135		// convert to actual used terms
136	170412	for (const auto& v : d_var_num)
137		{
138	120384	if (v.second >= 0)
139		{
140	120384	Assert(v.first < t.getNumChildren());
141	240768	Debug("simple-trigger")
142	120384	<< "...set " << v.second << " " << t[v.first] << std::endl;
143	120384	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	50028	if (sendInstantiation(m, InferenceId::QUANTIFIERS_INST_E_MATCHING_SIMPLE))
149		{
150	13826	addedLemmas++;
151	13826	Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl;
152		}
153	50028	return;
154		}
155	151210	if (d_match_pattern[argIndex].getKind() == INST_CONSTANT)
156		{
157	80206	int v = d_var_num[argIndex];
158	80206	if (v != -1)
159		{
160	254782	for (std::pair<const TNode, TNodeTrie>& tt : tat->d_data)
161		{
162	349152	Node t = tt.first;
163	349152	Node prev = m.get(v);
164		// using representatives, just check if equal
165	174576	Assert(t.getType().isComparableTo(d_match_pattern_arg_types[argIndex]));
166	174576	if (prev.isNull() \|\| prev == t)
167		{
168	170332	m.setValue(v, t);
169	170332	addInstantiations(m, addedLemmas, argIndex + 1, &(tt.second));
170	170332	m.setValue(v, prev);
171	170332	if (d_qstate.isInConflict())
172		{
173		break;
174		}
175		}
176		}
177	80206	return;
178		}
179		// inst constant from another quantified formula, treat as ground term?
180		}
181	142008	Node r = d_qstate.getRepresentative(d_match_pattern[argIndex]);
182	71004	std::map<TNode, TNodeTrie>::iterator it = tat->d_data.find(r);
183	71004	if (it != tat->d_data.end())
184		{
185	10522	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	29502	} // namespace cvc5