Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/theory_state.cpp	Lines:	73	73	100.0 %
Date:	2021-05-21	Branches:	80	192	41.7 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Mathias Preiner
 *
 * 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.
 * ****************************************************************************
 *
 * A theory state for Theory.
 */

#include "theory/theory_state.h"

#include "theory/uf/equality_engine.h"

namespace cvc5 {
namespace theory {

TheoryState::TheoryState(context::Context* c,
                         context::UserContext* u,
                         Valuation val)
    : d_context(c),
      d_ucontext(u),
      d_valuation(val),
      d_ee(nullptr),
      d_conflict(c, false)
{
}

void TheoryState::setEqualityEngine(eq::EqualityEngine* ee) { d_ee = ee; }

context::Context* TheoryState::getSatContext() const { return d_context; }

context::UserContext* TheoryState::getUserContext() const { return d_ucontext; }

bool TheoryState::hasTerm(TNode a) const
{
  Assert(d_ee != nullptr);
  return d_ee->hasTerm(a);
}

TNode TheoryState::getRepresentative(TNode t) const
{
  Assert(d_ee != nullptr);
  if (d_ee->hasTerm(t))
  {
    return d_ee->getRepresentative(t);
  }
  return t;
}

bool TheoryState::areEqual(TNode a, TNode b) const
{
  Assert(d_ee != nullptr);
  if (a == b)
  {
    return true;
  }
  else if (hasTerm(a) && hasTerm(b))
  {
    return d_ee->areEqual(a, b);
  }
  return false;
}

bool TheoryState::areDisequal(TNode a, TNode b) const
{
  Assert(d_ee != nullptr);
  if (a == b)
  {
    return false;
  }

  bool isConst = true;
  bool hasTerms = true;
  if (hasTerm(a))
  {
    a = d_ee->getRepresentative(a);
    isConst = a.isConst();
  }
  else if (!a.isConst())
  {
    // if not constant and not a term in the ee, it cannot be disequal
    return false;
  }
  else
  {
    hasTerms = false;
  }

  if (hasTerm(b))
  {
    b = d_ee->getRepresentative(b);
    isConst = isConst && b.isConst();
  }
  else if (!b.isConst())
  {
    // same as above, it cannot be disequal
    return false;
  }
  else
  {
    hasTerms = false;
  }

  if (isConst)
  {
    // distinct constants are disequal
    return a != b;
  }
  else if (!hasTerms)
  {
    return false;
  }
  // otherwise there may be an explicit disequality in the equality engine
  return d_ee->areDisequal(a, b, false);
}

void TheoryState::getEquivalenceClass(Node a, std::vector<Node>& eqc) const
{
  if (d_ee->hasTerm(a))
  {
    Node rep = d_ee->getRepresentative(a);
    eq::EqClassIterator eqc_iter(rep, d_ee);
    while (!eqc_iter.isFinished())
    {
      eqc.push_back(*eqc_iter);
      eqc_iter++;
    }
  }
  else
  {
    eqc.push_back(a);
  }
  // a should be in its equivalence class
  Assert(std::find(eqc.begin(), eqc.end(), a) != eqc.end());
}

eq::EqualityEngine* TheoryState::getEqualityEngine() const { return d_ee; }

void TheoryState::notifyInConflict() { d_conflict = true; }

bool TheoryState::isInConflict() const { return d_conflict; }

bool TheoryState::isSatLiteral(TNode lit) const
{
  return d_valuation.isSatLiteral(lit);
}

TheoryModel* TheoryState::getModel() { return d_valuation.getModel(); }

SortInference* TheoryState::getSortInference()
{
  return d_valuation.getSortInference();
}

bool TheoryState::hasSatValue(TNode n, bool& value) const
{
  return d_valuation.hasSatValue(n, value);
}

context::CDList<Assertion>::const_iterator TheoryState::factsBegin(TheoryId tid)
{
  return d_valuation.factsBegin(tid);
}
context::CDList<Assertion>::const_iterator TheoryState::factsEnd(TheoryId tid)
{
  return d_valuation.factsEnd(tid);
}

bool TheoryState::isFiniteType(TypeNode tn) const
{
  return d_valuation.isFiniteType(tn);
}

Valuation& TheoryState::getValuation() { return d_valuation; }

}  // 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
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		* A theory state for Theory.
14		*/
15
16		#include "theory/theory_state.h"
17
18		#include "theory/uf/equality_engine.h"
19
20		namespace cvc5 {
21		namespace theory {
22
23	98536	TheoryState::TheoryState(context::Context* c,
24		context::UserContext* u,
25	98536	Valuation val)
26		: d_context(c),
27		d_ucontext(u),
28		d_valuation(val),
29		d_ee(nullptr),
30	98536	d_conflict(c, false)
31		{
32	98536	}
33
34	98494	void TheoryState::setEqualityEngine(eq::EqualityEngine* ee) { d_ee = ee; }
35
36	159179	context::Context* TheoryState::getSatContext() const { return d_context; }
37
38	242738	context::UserContext* TheoryState::getUserContext() const { return d_ucontext; }
39
40	27247694	bool TheoryState::hasTerm(TNode a) const
41		{
42	27247694	Assert(d_ee != nullptr);
43	27247694	return d_ee->hasTerm(a);
44		}
45
46	12248523	TNode TheoryState::getRepresentative(TNode t) const
47		{
48	12248523	Assert(d_ee != nullptr);
49	12248523	if (d_ee->hasTerm(t))
50		{
51	12082427	return d_ee->getRepresentative(t);
52		}
53	166096	return t;
54		}
55
56	7743244	bool TheoryState::areEqual(TNode a, TNode b) const
57		{
58	7743244	Assert(d_ee != nullptr);
59	7743244	if (a == b)
60		{
61	2402620	return true;
62		}
63	5340624	else if (hasTerm(a) && hasTerm(b))
64		{
65	5314622	return d_ee->areEqual(a, b);
66		}
67	26002	return false;
68		}
69
70	571213	bool TheoryState::areDisequal(TNode a, TNode b) const
71		{
72	571213	Assert(d_ee != nullptr);
73	571213	if (a == b)
74		{
75	294382	return false;
76		}
77
78	276831	bool isConst = true;
79	276831	bool hasTerms = true;
80	276831	if (hasTerm(a))
81		{
82	276364	a = d_ee->getRepresentative(a);
83	276364	isConst = a.isConst();
84		}
85	467	else if (!a.isConst())
86		{
87		// if not constant and not a term in the ee, it cannot be disequal
88	297	return false;
89		}
90		else
91		{
92	170	hasTerms = false;
93		}
94
95	276534	if (hasTerm(b))
96		{
97	276122	b = d_ee->getRepresentative(b);
98	276122	isConst = isConst && b.isConst();
99		}
100	412	else if (!b.isConst())
101		{
102		// same as above, it cannot be disequal
103	77	return false;
104		}
105		else
106		{
107	335	hasTerms = false;
108		}
109
110	276457	if (isConst)
111		{
112		// distinct constants are disequal
113	47736	return a != b;
114		}
115	228721	else if (!hasTerms)
116		{
117	261	return false;
118		}
119		// otherwise there may be an explicit disequality in the equality engine
120	228460	return d_ee->areDisequal(a, b, false);
121		}
122
123	8627	void TheoryState::getEquivalenceClass(Node a, std::vector<Node>& eqc) const
124		{
125	8627	if (d_ee->hasTerm(a))
126		{
127	15918	Node rep = d_ee->getRepresentative(a);
128	7959	eq::EqClassIterator eqc_iter(rep, d_ee);
129	105673	while (!eqc_iter.isFinished())
130		{
131	48857	eqc.push_back(*eqc_iter);
132	48857	eqc_iter++;
133		}
134		}
135		else
136		{
137	668	eqc.push_back(a);
138		}
139		// a should be in its equivalence class
140	8627	Assert(std::find(eqc.begin(), eqc.end(), a) != eqc.end());
141	8627	}
142
143	6220375	eq::EqualityEngine* TheoryState::getEqualityEngine() const { return d_ee; }
144
145	157940	void TheoryState::notifyInConflict() { d_conflict = true; }
146
147	35569493	bool TheoryState::isInConflict() const { return d_conflict; }
148
149	567453	bool TheoryState::isSatLiteral(TNode lit) const
150		{
151	567453	return d_valuation.isSatLiteral(lit);
152		}
153
154	1706	TheoryModel* TheoryState::getModel() { return d_valuation.getModel(); }
155
156	5148	SortInference* TheoryState::getSortInference()
157		{
158	5148	return d_valuation.getSortInference();
159		}
160
161	108	bool TheoryState::hasSatValue(TNode n, bool& value) const
162		{
163	108	return d_valuation.hasSatValue(n, value);
164		}
165
166	6448	context::CDList<Assertion>::const_iterator TheoryState::factsBegin(TheoryId tid)
167		{
168	6448	return d_valuation.factsBegin(tid);
169		}
170	6448	context::CDList<Assertion>::const_iterator TheoryState::factsEnd(TheoryId tid)
171		{
172	6448	return d_valuation.factsEnd(tid);
173		}
174
175	10974	bool TheoryState::isFiniteType(TypeNode tn) const
176		{
177	10974	return d_valuation.isFiniteType(tn);
178		}
179
180	132454	Valuation& TheoryState::getValuation() { return d_valuation; }
181
182		} // namespace theory
183	27735	} // namespace cvc5