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-05-22	Branches:	185	430	43.0 %


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