Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/equality_query.cpp	Lines:	68	89	76.4 %
Date:	2021-11-07	Branches:	163	418	39.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.
 * ****************************************************************************
 *
 * Utilities used for querying about equality information.
 */

#include "theory/quantifiers/equality_query.h"

#include "options/quantifiers_options.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/quantifiers_state.h"
#include "theory/quantifiers/term_util.h"

using namespace std;
using namespace cvc5::kind;
using namespace cvc5::context;

namespace cvc5 {
namespace theory {
namespace quantifiers {

EqualityQuery::EqualityQuery(Env& env, QuantifiersState& qs, FirstOrderModel* m)
    : QuantifiersUtil(env),
      d_qstate(qs),
      d_model(m),
      d_eqi_counter(context()),
      d_reset_count(0)
{
}

EqualityQuery::~EqualityQuery() {}

bool EqualityQuery::reset(Theory::Effort e)
{
  d_int_rep.clear();
  d_reset_count++;
  return true;
}

Node EqualityQuery::getInternalRepresentative(Node a, Node q, size_t index)
{
  Assert(q.isNull() || q.getKind() == FORALL);
  Node r = d_qstate.getRepresentative(a);
  if (options().quantifiers.finiteModelFind)
  {
    if( r.isConst() && quantifiers::TermUtil::containsUninterpretedConstant( r ) ){
      //map back from values assigned by model, if any
      if (d_model != nullptr)
      {
        Node tr = d_model->getRepSet()->getTermForRepresentative(r);
        if (!tr.isNull())
        {
          r = tr;
          r = d_qstate.getRepresentative(r);
        }else{
          if( r.getType().isSort() ){
            Trace("internal-rep-warn") << "No representative for UF constant." << std::endl;
            //should never happen : UF constants should never escape model
            Assert(false);
          }
        }
      }
    }
  }
  TypeNode v_tn = q.isNull() ? a.getType() : q[0][index].getType();
  if (options().quantifiers.quantRepMode == options::QuantRepMode::EE)
  {
    int32_t score = getRepScore(r, q, index, v_tn);
    if (score >= 0)
    {
      return r;
    }
    // if we are not a valid representative, try to select one below
  }
  std::map<Node, Node>& v_int_rep = d_int_rep[v_tn];
  std::map<Node, Node>::const_iterator itir = v_int_rep.find(r);
  if (itir != v_int_rep.end())
  {
    return itir->second;
  }
  // find best selection for representative
  Node r_best;
  std::vector<Node> eqc;
  d_qstate.getEquivalenceClass(r, eqc);
  Trace("internal-rep-select")
      << "Choose representative for equivalence class : " << eqc
      << ", type = " << v_tn << std::endl;
  int32_t r_best_score = -1;
  for (const Node& n : eqc)
  {
    int32_t score = getRepScore(n, q, index, v_tn);
    if (score != -2)
    {
      if (r_best.isNull()
          || (score >= 0 && (r_best_score < 0 || score < r_best_score)))
      {
        r_best = n;
        r_best_score = score;
      }
    }
  }
  if (r_best.isNull())
  {
    Trace("internal-rep-warn")
        << "No valid choice for representative in eqc class " << eqc
        << std::endl;
    return Node::null();
  }
  // now, make sure that no other member of the class is an instance
  std::unordered_map<TNode, Node> cache;
  r_best = getInstance(r_best, eqc, cache);
  // store that this representative was chosen at this point
  if (d_rep_score.find(r_best) == d_rep_score.end())
  {
    d_rep_score[r_best] = d_reset_count;
  }
  Trace("internal-rep-select")
      << "...Choose " << r_best << " with score " << r_best_score
      << " and type " << r_best.getType() << std::endl;
  Assert(r_best.getType().isSubtypeOf(v_tn));
  v_int_rep[r] = r_best;
  if (Trace.isOn("internal-rep-debug"))
  {
    if (r_best != a)
    {
      Trace("internal-rep-debug")
          << "rep( " << a << " ) = " << r << ", " << std::endl;
      Trace("internal-rep-debug")
          << "int_rep( " << a << " ) = " << r_best << ", " << std::endl;
    }
  }
  return r_best;
}

//helper functions

Node EqualityQuery::getInstance(Node n,
                                const std::vector<Node>& eqc,
                                std::unordered_map<TNode, Node>& cache)
{
  if(cache.find(n) != cache.end()) {
    return cache[n];
  }
  for( size_t i=0; i<n.getNumChildren(); i++ ){
    Node nn = getInstance( n[i], eqc, cache );
    if( !nn.isNull() ){
      return cache[n] = nn;
    }
  }
  if( std::find( eqc.begin(), eqc.end(), n )!=eqc.end() ){
    return cache[n] = n;
  }else{
    return cache[n] = Node::null();
  }
}

//-2 : invalid, -1 : undesired, otherwise : smaller the score, the better
int32_t EqualityQuery::getRepScore(Node n, Node q, size_t index, TypeNode v_tn)
{
  if (options().quantifiers.cegqi && quantifiers::TermUtil::hasInstConstAttr(n))
  {  // reject
    return -2;
  }
  else if (!n.getType().isSubtypeOf(v_tn))
  {  // reject if incorrect type
    return -2;
  }
  else if (options().quantifiers.instMaxLevel != -1)
  {
    //score prefer lowest instantiation level
    if( n.hasAttribute(InstLevelAttribute()) ){
      return n.getAttribute(InstLevelAttribute());
    }
    return options().quantifiers.instLevelInputOnly ? -1 : 0;
  }
  else if (options().quantifiers.quantRepMode == options::QuantRepMode::FIRST)
  {
    // score prefers earliest use of this term as a representative
    return d_rep_score.find(n) == d_rep_score.end() ? -1 : d_rep_score[n];
  }
  Assert(options().quantifiers.quantRepMode == options::QuantRepMode::DEPTH);
  return quantifiers::TermUtil::getTermDepth(n);
}

}  // 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		* Utilities used for querying about equality information.
14		*/
15
16		#include "theory/quantifiers/equality_query.h"
17
18		#include "options/quantifiers_options.h"
19		#include "theory/quantifiers/first_order_model.h"
20		#include "theory/quantifiers/quantifiers_attributes.h"
21		#include "theory/quantifiers/quantifiers_state.h"
22		#include "theory/quantifiers/term_util.h"
23
24		using namespace std;
25		using namespace cvc5::kind;
26		using namespace cvc5::context;
27
28		namespace cvc5 {
29		namespace theory {
30		namespace quantifiers {
31
32	15273	EqualityQuery::EqualityQuery(Env& env, QuantifiersState& qs, FirstOrderModel* m)
33		: QuantifiersUtil(env),
34		d_qstate(qs),
35		d_model(m),
36		d_eqi_counter(context()),
37	15273	d_reset_count(0)
38		{
39	15273	}
40
41	15268	EqualityQuery::~EqualityQuery() {}
42
43	34975	bool EqualityQuery::reset(Theory::Effort e)
44		{
45	34975	d_int_rep.clear();
46	34975	d_reset_count++;
47	34975	return true;
48		}
49
50	76584	Node EqualityQuery::getInternalRepresentative(Node a, Node q, size_t index)
51		{
52	76584	Assert(q.isNull() \|\| q.getKind() == FORALL);
53	153168	Node r = d_qstate.getRepresentative(a);
54	76584	if (options().quantifiers.finiteModelFind)
55		{
56	66114	if( r.isConst() && quantifiers::TermUtil::containsUninterpretedConstant( r ) ){
57		//map back from values assigned by model, if any
58	5445	if (d_model != nullptr)
59		{
60	10890	Node tr = d_model->getRepSet()->getTermForRepresentative(r);
61	5445	if (!tr.isNull())
62		{
63	5445	r = tr;
64	5445	r = d_qstate.getRepresentative(r);
65		}else{
66		if( r.getType().isSort() ){
67		Trace("internal-rep-warn") << "No representative for UF constant." << std::endl;
68		//should never happen : UF constants should never escape model
69		Assert(false);
70		}
71		}
72		}
73		}
74		}
75	153168	TypeNode v_tn = q.isNull() ? a.getType() : q[0][index].getType();
76	76584	if (options().quantifiers.quantRepMode == options::QuantRepMode::EE)
77		{
78		int32_t score = getRepScore(r, q, index, v_tn);
79		if (score >= 0)
80		{
81		return r;
82		}
83		// if we are not a valid representative, try to select one below
84		}
85	76584	std::map<Node, Node>& v_int_rep = d_int_rep[v_tn];
86	76584	std::map<Node, Node>::const_iterator itir = v_int_rep.find(r);
87	76584	if (itir != v_int_rep.end())
88		{
89	68207	return itir->second;
90		}
91		// find best selection for representative
92	16754	Node r_best;
93	16754	std::vector<Node> eqc;
94	8377	d_qstate.getEquivalenceClass(r, eqc);
95	16754	Trace("internal-rep-select")
96	8377	<< "Choose representative for equivalence class : " << eqc
97	8377	<< ", type = " << v_tn << std::endl;
98	8377	int32_t r_best_score = -1;
99	65106	for (const Node& n : eqc)
100		{
101	56729	int32_t score = getRepScore(n, q, index, v_tn);
102	56729	if (score != -2)
103		{
104	104966	if (r_best.isNull()
105	52483	\|\| (score >= 0 && (r_best_score < 0 \|\| score < r_best_score)))
106		{
107	8601	r_best = n;
108	8601	r_best_score = score;
109		}
110		}
111		}
112	8377	if (r_best.isNull())
113		{
114		Trace("internal-rep-warn")
115		<< "No valid choice for representative in eqc class " << eqc
116		<< std::endl;
117		return Node::null();
118		}
119		// now, make sure that no other member of the class is an instance
120	16754	std::unordered_map<TNode, Node> cache;
121	8377	r_best = getInstance(r_best, eqc, cache);
122		// store that this representative was chosen at this point
123	8377	if (d_rep_score.find(r_best) == d_rep_score.end())
124		{
125	1766	d_rep_score[r_best] = d_reset_count;
126		}
127	16754	Trace("internal-rep-select")
128	8377	<< "...Choose " << r_best << " with score " << r_best_score
129	8377	<< " and type " << r_best.getType() << std::endl;
130	8377	Assert(r_best.getType().isSubtypeOf(v_tn));
131	8377	v_int_rep[r] = r_best;
132	8377	if (Trace.isOn("internal-rep-debug"))
133		{
134		if (r_best != a)
135		{
136		Trace("internal-rep-debug")
137		<< "rep( " << a << " ) = " << r << ", " << std::endl;
138		Trace("internal-rep-debug")
139		<< "int_rep( " << a << " ) = " << r_best << ", " << std::endl;
140		}
141		}
142	8377	return r_best;
143		}
144
145		//helper functions
146
147	12785	Node EqualityQuery::getInstance(Node n,
148		const std::vector<Node>& eqc,
149		std::unordered_map<TNode, Node>& cache)
150		{
151	12785	if(cache.find(n) != cache.end()) {
152	499	return cache[n];
153		}
154	16682	for( size_t i=0; i<n.getNumChildren(); i++ ){
155	8804	Node nn = getInstance( n[i], eqc, cache );
156	4408	if( !nn.isNull() ){
157	12	return cache[n] = nn;
158		}
159		}
160	12274	if( std::find( eqc.begin(), eqc.end(), n )!=eqc.end() ){
161	8377	return cache[n] = n;
162		}else{
163	3897	return cache[n] = Node::null();
164		}
165		}
166
167		//-2 : invalid, -1 : undesired, otherwise : smaller the score, the better
168	56729	int32_t EqualityQuery::getRepScore(Node n, Node q, size_t index, TypeNode v_tn)
169		{
170	56729	if (options().quantifiers.cegqi && quantifiers::TermUtil::hasInstConstAttr(n))
171		{ // reject
172		return -2;
173		}
174	56729	else if (!n.getType().isSubtypeOf(v_tn))
175		{ // reject if incorrect type
176	4246	return -2;
177		}
178	52483	else if (options().quantifiers.instMaxLevel != -1)
179		{
180		//score prefer lowest instantiation level
181		if( n.hasAttribute(InstLevelAttribute()) ){
182		return n.getAttribute(InstLevelAttribute());
183		}
184		return options().quantifiers.instLevelInputOnly ? -1 : 0;
185		}
186	52483	else if (options().quantifiers.quantRepMode == options::QuantRepMode::FIRST)
187		{
188		// score prefers earliest use of this term as a representative
189	52483	return d_rep_score.find(n) == d_rep_score.end() ? -1 : d_rep_score[n];
190		}
191		Assert(options().quantifiers.quantRepMode == options::QuantRepMode::DEPTH);
192		return quantifiers::TermUtil::getTermDepth(n);
193		}
194
195		} // namespace quantifiers
196		} // namespace theory
197	31137	} // namespace cvc5