Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/quantifiers_state.cpp	Lines:	45	85	52.9 %
Date:	2021-11-07	Branches:	52	220	23.6 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Mathias Preiner, Morgan Deters
 *
 * 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.
 * ****************************************************************************
 *
 * Utility for quantifiers state.
 */

#include "theory/quantifiers/quantifiers_state.h"

#include "options/quantifiers_options.h"
#include "theory/uf/equality_engine_iterator.h"

namespace cvc5 {
namespace theory {
namespace quantifiers {

QuantifiersState::QuantifiersState(Env& env,
                                   Valuation val,
                                   const LogicInfo& logicInfo)
    : TheoryState(env, val),
      d_ierCounterc(env.getContext()),
      d_logicInfo(logicInfo)
{
  // allow theory combination to go first, once initially
  d_ierCounter = options().quantifiers.instWhenTcFirst ? 0 : 1;
  d_ierCounterc = d_ierCounter;
  d_ierCounterLc = 0;
  d_ierCounterLastLc = 0;
  d_instWhenPhase = 1
                    + (options().quantifiers.instWhenPhase < 1
                           ? 1
                           : options().quantifiers.instWhenPhase);
}

void QuantifiersState::incrementInstRoundCounters(Theory::Effort e)
{
  if (e == Theory::EFFORT_FULL)
  {
    // increment if a last call happened, we are not strictly enforcing
    // interleaving, or already were in phase
    if (d_ierCounterLastLc != d_ierCounterLc
        || !options().quantifiers.instWhenStrictInterleave
        || d_ierCounter % d_instWhenPhase != 0)
    {
      d_ierCounter = d_ierCounter + 1;
      d_ierCounterLastLc = d_ierCounterLc;
      d_ierCounterc = d_ierCounterc.get() + 1;
    }
  }
  else if (e == Theory::EFFORT_LAST_CALL)
  {
    d_ierCounterLc = d_ierCounterLc + 1;
  }
}

bool QuantifiersState::getInstWhenNeedsCheck(Theory::Effort e) const
{
  Trace("qstate-debug") << "Get inst when needs check, counts=" << d_ierCounter
                        << ", " << d_ierCounterLc << std::endl;
  // determine if we should perform check, based on instWhenMode
  bool performCheck = false;
  if (options().quantifiers.instWhenMode == options::InstWhenMode::FULL)
  {
    performCheck = (e >= Theory::EFFORT_FULL);
  }
  else if (options().quantifiers.instWhenMode
           == options::InstWhenMode::FULL_DELAY)
  {
    performCheck = (e >= Theory::EFFORT_FULL) && !d_valuation.needCheck();
  }
  else if (options().quantifiers.instWhenMode
           == options::InstWhenMode::FULL_LAST_CALL)
  {
    performCheck =
        ((e == Theory::EFFORT_FULL && d_ierCounter % d_instWhenPhase != 0)
         || e == Theory::EFFORT_LAST_CALL);
  }
  else if (options().quantifiers.instWhenMode
           == options::InstWhenMode::FULL_DELAY_LAST_CALL)
  {
    performCheck = ((e == Theory::EFFORT_FULL && !d_valuation.needCheck()
                     && d_ierCounter % d_instWhenPhase != 0)
                    || e == Theory::EFFORT_LAST_CALL);
  }
  else if (options().quantifiers.instWhenMode
           == options::InstWhenMode::LAST_CALL)
  {
    performCheck = (e >= Theory::EFFORT_LAST_CALL);
  }
  else
  {
    performCheck = true;
  }
  Trace("qstate-debug") << "...returned " << performCheck << std::endl;
  return performCheck;
}

uint64_t QuantifiersState::getInstRoundDepth() const
{
  return d_ierCounterc.get();
}

uint64_t QuantifiersState::getInstRounds() const { return d_ierCounter; }

void QuantifiersState::debugPrintEqualityEngine(const char* c) const
{
  bool traceEnabled = Trace.isOn(c);
  if (!traceEnabled)
  {
    return;
  }
  eq::EqualityEngine* ee = getEqualityEngine();
  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
  std::map<TypeNode, uint64_t> tnum;
  while (!eqcs_i.isFinished())
  {
    TNode r = (*eqcs_i);
    TypeNode tr = r.getType();
    if (tnum.find(tr) == tnum.end())
    {
      tnum[tr] = 0;
    }
    tnum[tr]++;
    bool firstTime = true;
    Trace(c) << "  " << r;
    Trace(c) << " : { ";
    eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee);
    while (!eqc_i.isFinished())
    {
      TNode n = (*eqc_i);
      if (r != n)
      {
        if (firstTime)
        {
          Trace(c) << std::endl;
          firstTime = false;
        }
        Trace(c) << "    " << n << std::endl;
      }
      ++eqc_i;
    }
    if (!firstTime)
    {
      Trace(c) << "  ";
    }
    Trace(c) << "}" << std::endl;
    ++eqcs_i;
  }
  Trace(c) << std::endl;
  for (const std::pair<const TypeNode, uint64_t>& t : tnum)
  {
    Trace(c) << "# eqc for " << t.first << " : " << t.second << std::endl;
  }
}

const LogicInfo& QuantifiersState::getLogicInfo() const { return d_logicInfo; }

QuantifiersStatistics& QuantifiersState::getStats() { return d_statistics; }

}  // 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, Morgan Deters
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		* Utility for quantifiers state.
14		*/
15
16		#include "theory/quantifiers/quantifiers_state.h"
17
18		#include "options/quantifiers_options.h"
19		#include "theory/uf/equality_engine_iterator.h"
20
21		namespace cvc5 {
22		namespace theory {
23		namespace quantifiers {
24
25	15273	QuantifiersState::QuantifiersState(Env& env,
26		Valuation val,
27	15273	const LogicInfo& logicInfo)
28		: TheoryState(env, val),
29		d_ierCounterc(env.getContext()),
30	15273	d_logicInfo(logicInfo)
31		{
32		// allow theory combination to go first, once initially
33	15273	d_ierCounter = options().quantifiers.instWhenTcFirst ? 0 : 1;
34	15273	d_ierCounterc = d_ierCounter;
35	15273	d_ierCounterLc = 0;
36	15273	d_ierCounterLastLc = 0;
37	15273	d_instWhenPhase = 1
38	30546	+ (options().quantifiers.instWhenPhase < 1
39		? 1
40	15273	: options().quantifiers.instWhenPhase);
41	15273	}
42
43	33448	void QuantifiersState::incrementInstRoundCounters(Theory::Effort e)
44		{
45	33448	if (e == Theory::EFFORT_FULL)
46		{
47		// increment if a last call happened, we are not strictly enforcing
48		// interleaving, or already were in phase
49	31348	if (d_ierCounterLastLc != d_ierCounterLc
50	12553	\|\| !options().quantifiers.instWhenStrictInterleave
51	28227	\|\| d_ierCounter % d_instWhenPhase != 0)
52		{
53	4990	d_ierCounter = d_ierCounter + 1;
54	4990	d_ierCounterLastLc = d_ierCounterLc;
55	4990	d_ierCounterc = d_ierCounterc.get() + 1;
56		}
57		}
58	17774	else if (e == Theory::EFFORT_LAST_CALL)
59		{
60	17774	d_ierCounterLc = d_ierCounterLc + 1;
61		}
62	33448	}
63
64	176419	bool QuantifiersState::getInstWhenNeedsCheck(Theory::Effort e) const
65		{
66	352838	Trace("qstate-debug") << "Get inst when needs check, counts=" << d_ierCounter
67	176419	<< ", " << d_ierCounterLc << std::endl;
68		// determine if we should perform check, based on instWhenMode
69	176419	bool performCheck = false;
70	176419	if (options().quantifiers.instWhenMode == options::InstWhenMode::FULL)
71		{
72	36	performCheck = (e >= Theory::EFFORT_FULL);
73		}
74	352766	else if (options().quantifiers.instWhenMode
75	176383	== options::InstWhenMode::FULL_DELAY)
76		{
77		performCheck = (e >= Theory::EFFORT_FULL) && !d_valuation.needCheck();
78		}
79	352766	else if (options().quantifiers.instWhenMode
80	176383	== options::InstWhenMode::FULL_LAST_CALL)
81		{
82	164491	performCheck =
83	56848	((e == Theory::EFFORT_FULL && d_ierCounter % d_instWhenPhase != 0)
84	323079	\|\| e == Theory::EFFORT_LAST_CALL);
85		}
86	23784	else if (options().quantifiers.instWhenMode
87	11892	== options::InstWhenMode::FULL_DELAY_LAST_CALL)
88		{
89		performCheck = ((e == Theory::EFFORT_FULL && !d_valuation.needCheck()
90		&& d_ierCounter % d_instWhenPhase != 0)
91		\|\| e == Theory::EFFORT_LAST_CALL);
92		}
93	23784	else if (options().quantifiers.instWhenMode
94	11892	== options::InstWhenMode::LAST_CALL)
95		{
96	11892	performCheck = (e >= Theory::EFFORT_LAST_CALL);
97		}
98		else
99		{
100		performCheck = true;
101		}
102	176419	Trace("qstate-debug") << "...returned " << performCheck << std::endl;
103	176419	return performCheck;
104		}
105
106		uint64_t QuantifiersState::getInstRoundDepth() const
107		{
108		return d_ierCounterc.get();
109		}
110
111		uint64_t QuantifiersState::getInstRounds() const { return d_ierCounter; }
112
113		void QuantifiersState::debugPrintEqualityEngine(const char* c) const
114		{
115		bool traceEnabled = Trace.isOn(c);
116		if (!traceEnabled)
117		{
118		return;
119		}
120		eq::EqualityEngine* ee = getEqualityEngine();
121		eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
122		std::map<TypeNode, uint64_t> tnum;
123		while (!eqcs_i.isFinished())
124		{
125		TNode r = (*eqcs_i);
126		TypeNode tr = r.getType();
127		if (tnum.find(tr) == tnum.end())
128		{
129		tnum[tr] = 0;
130		}
131		tnum[tr]++;
132		bool firstTime = true;
133		Trace(c) << " " << r;
134		Trace(c) << " : { ";
135		eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee);
136		while (!eqc_i.isFinished())
137		{
138		TNode n = (*eqc_i);
139		if (r != n)
140		{
141		if (firstTime)
142		{
143		Trace(c) << std::endl;
144		firstTime = false;
145		}
146		Trace(c) << " " << n << std::endl;
147		}
148		++eqc_i;
149		}
150		if (!firstTime)
151		{
152		Trace(c) << " ";
153		}
154		Trace(c) << "}" << std::endl;
155		++eqcs_i;
156		}
157		Trace(c) << std::endl;
158		for (const std::pair<const TypeNode, uint64_t>& t : tnum)
159		{
160		Trace(c) << "# eqc for " << t.first << " : " << t.second << std::endl;
161		}
162		}
163
164	4760	const LogicInfo& QuantifiersState::getLogicInfo() const { return d_logicInfo; }
165
166	290726	QuantifiersStatistics& QuantifiersState::getStats() { return d_statistics; }
167
168		} // namespace quantifiers
169		} // namespace theory
170	31137	} // namespace cvc5