Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/entailment_check.cpp	Lines:	181	184	98.4 %
Date:	2021-11-07	Branches:	450	796	56.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds
 *
 * 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.
 * ****************************************************************************
 *
 * Implementation of entailment check class.
 */

#include "theory/quantifiers/entailment_check.h"

#include "theory/quantifiers/quantifiers_state.h"
#include "theory/quantifiers/term_database.h"

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

namespace cvc5 {
namespace theory {
namespace quantifiers {

EntailmentCheck::EntailmentCheck(Env& env, QuantifiersState& qs, TermDb& tdb)
    : EnvObj(env), d_qstate(qs), d_tdb(tdb)
{
  d_true = NodeManager::currentNM()->mkConst(true);
  d_false = NodeManager::currentNM()->mkConst(false);
}

EntailmentCheck::~EntailmentCheck() {}

Node EntailmentCheck::evaluateTerm2(TNode n,
                                    std::map<TNode, Node>& visited,
                                    std::map<TNode, TNode>& subs,
                                    bool subsRep,
                                    bool useEntailmentTests,
                                    bool reqHasTerm)
{
  std::map<TNode, Node>::iterator itv = visited.find(n);
  if (itv != visited.end())
  {
    return itv->second;
  }
  Trace("term-db-eval") << "evaluate term : " << n << std::endl;
  Node ret = n;
  Kind k = n.getKind();
  if (k == FORALL)
  {
    // do nothing
  }
  else if (k == BOUND_VARIABLE)
  {
    std::map<TNode, TNode>::iterator it = subs.find(n);
    if (it != subs.end())
    {
      if (!subsRep)
      {
        ret = d_qstate.getRepresentative(it->second);
      }
      else
      {
        ret = it->second;
      }
    }
  }
  else if (d_qstate.hasTerm(n))
  {
    Trace("term-db-eval") << "...exists in ee, return rep" << std::endl;
    ret = d_qstate.getRepresentative(n);
    reqHasTerm = false;
  }
  else if (n.hasOperator())
  {
    std::vector<TNode> args;
    bool ret_set = false;
    for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++)
    {
      TNode c = evaluateTerm2(
          n[i], visited, subs, subsRep, useEntailmentTests, reqHasTerm);
      if (c.isNull())
      {
        ret = Node::null();
        ret_set = true;
        break;
      }
      else if (c == d_true || c == d_false)
      {
        // short-circuiting
        if ((k == AND && c == d_false) || (k == OR && c == d_true))
        {
          ret = c;
          ret_set = true;
          reqHasTerm = false;
          break;
        }
        else if (k == ITE && i == 0)
        {
          ret = evaluateTerm2(n[c == d_true ? 1 : 2],
                              visited,
                              subs,
                              subsRep,
                              useEntailmentTests,
                              reqHasTerm);
          ret_set = true;
          reqHasTerm = false;
          break;
        }
      }
      Trace("term-db-eval") << "  child " << i << " : " << c << std::endl;
      args.push_back(c);
    }
    if (!ret_set)
    {
      // get the (indexed) operator of n, if it exists
      TNode f = d_tdb.getMatchOperator(n);
      // if it is an indexed term, return the congruent term
      if (!f.isNull())
      {
        // if f is congruent to a term indexed by this class
        TNode nn = d_tdb.getCongruentTerm(f, args);
        Trace("term-db-eval") << "  got congruent term " << nn
                              << " from DB for " << n << std::endl;
        if (!nn.isNull())
        {
          ret = d_qstate.getRepresentative(nn);
          Trace("term-db-eval") << "return rep" << std::endl;
          ret_set = true;
          reqHasTerm = false;
          Assert(!ret.isNull());
        }
      }
      if (!ret_set)
      {
        Trace("term-db-eval") << "return rewrite" << std::endl;
        // a theory symbol or a new UF term
        if (n.getMetaKind() == metakind::PARAMETERIZED)
        {
          args.insert(args.begin(), n.getOperator());
        }
        ret = NodeManager::currentNM()->mkNode(n.getKind(), args);
        ret = rewrite(ret);
        if (ret.getKind() == EQUAL)
        {
          if (d_qstate.areDisequal(ret[0], ret[1]))
          {
            ret = d_false;
          }
        }
        if (useEntailmentTests)
        {
          if (ret.getKind() == EQUAL || ret.getKind() == GEQ)
          {
            Valuation& val = d_qstate.getValuation();
            for (unsigned j = 0; j < 2; j++)
            {
              std::pair<bool, Node> et = val.entailmentCheck(
                  options::TheoryOfMode::THEORY_OF_TYPE_BASED,
                  j == 0 ? ret : ret.negate());
              if (et.first)
              {
                ret = j == 0 ? d_true : d_false;
                break;
              }
            }
          }
        }
      }
    }
  }
  // must have the term
  if (reqHasTerm && !ret.isNull())
  {
    Kind rk = ret.getKind();
    if (rk != OR && rk != AND && rk != EQUAL && rk != ITE && rk != NOT
        && rk != FORALL)
    {
      if (!d_qstate.hasTerm(ret))
      {
        ret = Node::null();
      }
    }
  }
  Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret
                        << ", reqHasTerm = " << reqHasTerm << std::endl;
  visited[n] = ret;
  return ret;
}

TNode EntailmentCheck::getEntailedTerm2(TNode n,
                                        std::map<TNode, TNode>& subs,
                                        bool subsRep)
{
  Trace("term-db-entail") << "get entailed term : " << n << std::endl;
  if (d_qstate.hasTerm(n))
  {
    Trace("term-db-entail") << "...exists in ee, return rep " << std::endl;
    return n;
  }
  else if (n.getKind() == BOUND_VARIABLE)
  {
    std::map<TNode, TNode>::iterator it = subs.find(n);
    if (it != subs.end())
    {
      Trace("term-db-entail")
          << "...substitution is : " << it->second << std::endl;
      if (subsRep)
      {
        Assert(d_qstate.hasTerm(it->second));
        Assert(d_qstate.getRepresentative(it->second) == it->second);
        return it->second;
      }
      return getEntailedTerm2(it->second, subs, subsRep);
    }
  }
  else if (n.getKind() == ITE)
  {
    for (uint32_t i = 0; i < 2; i++)
    {
      if (isEntailed2(n[0], subs, subsRep, i == 0))
      {
        return getEntailedTerm2(n[i == 0 ? 1 : 2], subs, subsRep);
      }
    }
  }
  else
  {
    if (n.hasOperator())
    {
      TNode f = d_tdb.getMatchOperator(n);
      if (!f.isNull())
      {
        std::vector<TNode> args;
        for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
        {
          TNode c = getEntailedTerm2(n[i], subs, subsRep);
          if (c.isNull())
          {
            return TNode::null();
          }
          c = d_qstate.getRepresentative(c);
          Trace("term-db-entail") << "  child " << i << " : " << c << std::endl;
          args.push_back(c);
        }
        TNode nn = d_tdb.getCongruentTerm(f, args);
        Trace("term-db-entail")
            << "  got congruent term " << nn << " for " << n << std::endl;
        return nn;
      }
    }
  }
  return TNode::null();
}

Node EntailmentCheck::evaluateTerm(TNode n,
                                   std::map<TNode, TNode>& subs,
                                   bool subsRep,
                                   bool useEntailmentTests,
                                   bool reqHasTerm)
{
  std::map<TNode, Node> visited;
  return evaluateTerm2(
      n, visited, subs, subsRep, useEntailmentTests, reqHasTerm);
}

Node EntailmentCheck::evaluateTerm(TNode n,
                                   bool useEntailmentTests,
                                   bool reqHasTerm)
{
  std::map<TNode, Node> visited;
  std::map<TNode, TNode> subs;
  return evaluateTerm2(n, visited, subs, false, useEntailmentTests, reqHasTerm);
}

TNode EntailmentCheck::getEntailedTerm(TNode n,
                                       std::map<TNode, TNode>& subs,
                                       bool subsRep)
{
  return getEntailedTerm2(n, subs, subsRep);
}

TNode EntailmentCheck::getEntailedTerm(TNode n)
{
  std::map<TNode, TNode> subs;
  return getEntailedTerm2(n, subs, false);
}

bool EntailmentCheck::isEntailed2(TNode n,
                                  std::map<TNode, TNode>& subs,
                                  bool subsRep,
                                  bool pol)
{
  Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol
                          << std::endl;
  Assert(n.getType().isBoolean());
  if (n.getKind() == EQUAL && !n[0].getType().isBoolean())
  {
    TNode n1 = getEntailedTerm2(n[0], subs, subsRep);
    if (!n1.isNull())
    {
      TNode n2 = getEntailedTerm2(n[1], subs, subsRep);
      if (!n2.isNull())
      {
        if (n1 == n2)
        {
          return pol;
        }
        else
        {
          Assert(d_qstate.hasTerm(n1));
          Assert(d_qstate.hasTerm(n2));
          if (pol)
          {
            return d_qstate.areEqual(n1, n2);
          }
          else
          {
            return d_qstate.areDisequal(n1, n2);
          }
        }
      }
    }
  }
  else if (n.getKind() == NOT)
  {
    return isEntailed2(n[0], subs, subsRep, !pol);
  }
  else if (n.getKind() == OR || n.getKind() == AND)
  {
    bool simPol = (pol && n.getKind() == OR) || (!pol && n.getKind() == AND);
    for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
    {
      if (isEntailed2(n[i], subs, subsRep, pol))
      {
        if (simPol)
        {
          return true;
        }
      }
      else
      {
        if (!simPol)
        {
          return false;
        }
      }
    }
    return !simPol;
    // Boolean equality here
  }
  else if (n.getKind() == EQUAL || n.getKind() == ITE)
  {
    for (size_t i = 0; i < 2; i++)
    {
      if (isEntailed2(n[0], subs, subsRep, i == 0))
      {
        size_t ch = (n.getKind() == EQUAL || i == 0) ? 1 : 2;
        bool reqPol = (n.getKind() == ITE || i == 0) ? pol : !pol;
        return isEntailed2(n[ch], subs, subsRep, reqPol);
      }
    }
  }
  else if (n.getKind() == APPLY_UF)
  {
    TNode n1 = getEntailedTerm2(n, subs, subsRep);
    if (!n1.isNull())
    {
      Assert(d_qstate.hasTerm(n1));
      if (n1 == d_true)
      {
        return pol;
      }
      else if (n1 == d_false)
      {
        return !pol;
      }
      else
      {
        return d_qstate.getRepresentative(n1) == (pol ? d_true : d_false);
      }
    }
  }
  else if (n.getKind() == FORALL && !pol)
  {
    return isEntailed2(n[1], subs, subsRep, pol);
  }
  return false;
}

bool EntailmentCheck::isEntailed(TNode n, bool pol)
{
  std::map<TNode, TNode> subs;
  return isEntailed2(n, subs, false, pol);
}

bool EntailmentCheck::isEntailed(TNode n,
                                 std::map<TNode, TNode>& subs,
                                 bool subsRep,
                                 bool pol)
{
  return isEntailed2(n, subs, subsRep, pol);
}

}  // 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
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		* Implementation of entailment check class.
14		*/
15
16		#include "theory/quantifiers/entailment_check.h"
17
18		#include "theory/quantifiers/quantifiers_state.h"
19		#include "theory/quantifiers/term_database.h"
20
21		using namespace cvc5::kind;
22		using namespace cvc5::context;
23
24		namespace cvc5 {
25		namespace theory {
26		namespace quantifiers {
27
28	15273	EntailmentCheck::EntailmentCheck(Env& env, QuantifiersState& qs, TermDb& tdb)
29	15273	: EnvObj(env), d_qstate(qs), d_tdb(tdb)
30		{
31	15273	d_true = NodeManager::currentNM()->mkConst(true);
32	15273	d_false = NodeManager::currentNM()->mkConst(false);
33	15273	}
34
35	30536	EntailmentCheck::~EntailmentCheck() {}
36
37	1517519	Node EntailmentCheck::evaluateTerm2(TNode n,
38		std::map<TNode, Node>& visited,
39		std::map<TNode, TNode>& subs,
40		bool subsRep,
41		bool useEntailmentTests,
42		bool reqHasTerm)
43		{
44	1517519	std::map<TNode, Node>::iterator itv = visited.find(n);
45	1517519	if (itv != visited.end())
46		{
47	307645	return itv->second;
48		}
49	1209874	Trace("term-db-eval") << "evaluate term : " << n << std::endl;
50	2419748	Node ret = n;
51	1209874	Kind k = n.getKind();
52	1209874	if (k == FORALL)
53		{
54		// do nothing
55		}
56	1209749	else if (k == BOUND_VARIABLE)
57		{
58	303649	std::map<TNode, TNode>::iterator it = subs.find(n);
59	303649	if (it != subs.end())
60		{
61	301288	if (!subsRep)
62		{
63	301288	ret = d_qstate.getRepresentative(it->second);
64		}
65		else
66		{
67		ret = it->second;
68		}
69		}
70		}
71	906100	else if (d_qstate.hasTerm(n))
72		{
73	112915	Trace("term-db-eval") << "...exists in ee, return rep" << std::endl;
74	112915	ret = d_qstate.getRepresentative(n);
75	112915	reqHasTerm = false;
76		}
77	793185	else if (n.hasOperator())
78		{
79	1585190	std::vector<TNode> args;
80	792595	bool ret_set = false;
81	1955905	for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++)
82		{
83	2763616	TNode c = evaluateTerm2(
84	2545118	n[i], visited, subs, subsRep, useEntailmentTests, reqHasTerm);
85	1381808	if (c.isNull())
86		{
87	177292	ret = Node::null();
88	177292	ret_set = true;
89	177292	break;
90		}
91	1204516	else if (c == d_true \|\| c == d_false)
92		{
93		// short-circuiting
94	223423	if ((k == AND && c == d_false) \|\| (k == OR && c == d_true))
95		{
96	35954	ret = c;
97	35954	ret_set = true;
98	35954	reqHasTerm = false;
99	35954	break;
100		}
101	187469	else if (k == ITE && i == 0)
102		{
103	5252	ret = evaluateTerm2(n[c == d_true ? 1 : 2],
104		visited,
105		subs,
106		subsRep,
107		useEntailmentTests,
108		reqHasTerm);
109	5252	ret_set = true;
110	5252	reqHasTerm = false;
111	5252	break;
112		}
113		}
114	1163310	Trace("term-db-eval") << " child " << i << " : " << c << std::endl;
115	1163310	args.push_back(c);
116		}
117	792595	if (!ret_set)
118		{
119		// get the (indexed) operator of n, if it exists
120	1148194	TNode f = d_tdb.getMatchOperator(n);
121		// if it is an indexed term, return the congruent term
122	574097	if (!f.isNull())
123		{
124		// if f is congruent to a term indexed by this class
125	737068	TNode nn = d_tdb.getCongruentTerm(f, args);
126	737068	Trace("term-db-eval") << " got congruent term " << nn
127	368534	<< " from DB for " << n << std::endl;
128	368534	if (!nn.isNull())
129		{
130	295261	ret = d_qstate.getRepresentative(nn);
131	295261	Trace("term-db-eval") << "return rep" << std::endl;
132	295261	ret_set = true;
133	295261	reqHasTerm = false;
134	295261	Assert(!ret.isNull());
135		}
136		}
137	574097	if (!ret_set)
138		{
139	278836	Trace("term-db-eval") << "return rewrite" << std::endl;
140		// a theory symbol or a new UF term
141	278836	if (n.getMetaKind() == metakind::PARAMETERIZED)
142		{
143	73140	args.insert(args.begin(), n.getOperator());
144		}
145	278836	ret = NodeManager::currentNM()->mkNode(n.getKind(), args);
146	278836	ret = rewrite(ret);
147	278836	if (ret.getKind() == EQUAL)
148		{
149	32201	if (d_qstate.areDisequal(ret[0], ret[1]))
150		{
151	15925	ret = d_false;
152		}
153		}
154	278836	if (useEntailmentTests)
155		{
156	822	if (ret.getKind() == EQUAL \|\| ret.getKind() == GEQ)
157		{
158	22	Valuation& val = d_qstate.getValuation();
159	62	for (unsigned j = 0; j < 2; j++)
160		{
161		std::pair<bool, Node> et = val.entailmentCheck(
162		options::TheoryOfMode::THEORY_OF_TYPE_BASED,
163	84	j == 0 ? ret : ret.negate());
164	44	if (et.first)
165		{
166	4	ret = j == 0 ? d_true : d_false;
167	4	break;
168		}
169		}
170		}
171		}
172		}
173		}
174		}
175		// must have the term
176	1209874	if (reqHasTerm && !ret.isNull())
177		{
178	578384	Kind rk = ret.getKind();
179	578384	if (rk != OR && rk != AND && rk != EQUAL && rk != ITE && rk != NOT
180	559324	&& rk != FORALL)
181		{
182	559091	if (!d_qstate.hasTerm(ret))
183		{
184	71197	ret = Node::null();
185		}
186		}
187		}
188	2419748	Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret
189	1209874	<< ", reqHasTerm = " << reqHasTerm << std::endl;
190	1209874	visited[n] = ret;
191	1209874	return ret;
192		}
193
194	9793465	TNode EntailmentCheck::getEntailedTerm2(TNode n,
195		std::map<TNode, TNode>& subs,
196		bool subsRep)
197		{
198	9793465	Trace("term-db-entail") << "get entailed term : " << n << std::endl;
199	9793465	if (d_qstate.hasTerm(n))
200		{
201	3162031	Trace("term-db-entail") << "...exists in ee, return rep " << std::endl;
202	3162031	return n;
203		}
204	6631434	else if (n.getKind() == BOUND_VARIABLE)
205		{
206	3868767	std::map<TNode, TNode>::iterator it = subs.find(n);
207	3868767	if (it != subs.end())
208		{
209	5886850	Trace("term-db-entail")
210	2943425	<< "...substitution is : " << it->second << std::endl;
211	2943425	if (subsRep)
212		{
213	348105	Assert(d_qstate.hasTerm(it->second));
214	348105	Assert(d_qstate.getRepresentative(it->second) == it->second);
215	3291530	return it->second;
216		}
217	2595320	return getEntailedTerm2(it->second, subs, subsRep);
218		}
219		}
220	2762667	else if (n.getKind() == ITE)
221		{
222	41500	for (uint32_t i = 0; i < 2; i++)
223		{
224	36142	if (isEntailed2(n[0], subs, subsRep, i == 0))
225		{
226	14635	return getEntailedTerm2(n[i == 0 ? 1 : 2], subs, subsRep);
227		}
228		}
229		}
230		else
231		{
232	2742674	if (n.hasOperator())
233		{
234	2748173	TNode f = d_tdb.getMatchOperator(n);
235	2735155	if (!f.isNull())
236		{
237	5444274	std::vector<TNode> args;
238	6204221	for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
239		{
240	8527844	TNode c = getEntailedTerm2(n[i], subs, subsRep);
241	5045760	if (c.isNull())
242		{
243	1563676	return TNode::null();
244		}
245	3482084	c = d_qstate.getRepresentative(c);
246	3482084	Trace("term-db-entail") << " child " << i << " : " << c << std::endl;
247	3482084	args.push_back(c);
248		}
249	2316922	TNode nn = d_tdb.getCongruentTerm(f, args);
250	2316922	Trace("term-db-entail")
251	1158461	<< " got congruent term " << nn << " for " << n << std::endl;
252	1158461	return nn;
253		}
254		}
255		}
256	951237	return TNode::null();
257		}
258
259	128841	Node EntailmentCheck::evaluateTerm(TNode n,
260		std::map<TNode, TNode>& subs,
261		bool subsRep,
262		bool useEntailmentTests,
263		bool reqHasTerm)
264		{
265	257682	std::map<TNode, Node> visited;
266		return evaluateTerm2(
267	257682	n, visited, subs, subsRep, useEntailmentTests, reqHasTerm);
268		}
269
270	1618	Node EntailmentCheck::evaluateTerm(TNode n,
271		bool useEntailmentTests,
272		bool reqHasTerm)
273		{
274	3236	std::map<TNode, Node> visited;
275	3236	std::map<TNode, TNode> subs;
276	3236	return evaluateTerm2(n, visited, subs, false, useEntailmentTests, reqHasTerm);
277		}
278
279	860201	TNode EntailmentCheck::getEntailedTerm(TNode n,
280		std::map<TNode, TNode>& subs,
281		bool subsRep)
282		{
283	860201	return getEntailedTerm2(n, subs, subsRep);
284		}
285
286	86651	TNode EntailmentCheck::getEntailedTerm(TNode n)
287		{
288	173302	std::map<TNode, TNode> subs;
289	173302	return getEntailedTerm2(n, subs, false);
290		}
291
292	1859179	bool EntailmentCheck::isEntailed2(TNode n,
293		std::map<TNode, TNode>& subs,
294		bool subsRep,
295		bool pol)
296		{
297	3718358	Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol
298	1859179	<< std::endl;
299	1859179	Assert(n.getType().isBoolean());
300	1859179	if (n.getKind() == EQUAL && !n[0].getType().isBoolean())
301		{
302	461465	TNode n1 = getEntailedTerm2(n[0], subs, subsRep);
303	385854	if (!n1.isNull())
304		{
305	383967	TNode n2 = getEntailedTerm2(n[1], subs, subsRep);
306	347105	if (!n2.isNull())
307		{
308	310243	if (n1 == n2)
309		{
310	29417	return pol;
311		}
312		else
313		{
314	280826	Assert(d_qstate.hasTerm(n1));
315	280826	Assert(d_qstate.hasTerm(n2));
316	280826	if (pol)
317		{
318	142940	return d_qstate.areEqual(n1, n2);
319		}
320		else
321		{
322	137886	return d_qstate.areDisequal(n1, n2);
323		}
324		}
325		}
326		}
327		}
328	1473325	else if (n.getKind() == NOT)
329		{
330	492818	return isEntailed2(n[0], subs, subsRep, !pol);
331		}
332	980507	else if (n.getKind() == OR \|\| n.getKind() == AND)
333		{
334	239366	bool simPol = (pol && n.getKind() == OR) \|\| (!pol && n.getKind() == AND);
335	829402	for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
336		{
337	745093	if (isEntailed2(n[i], subs, subsRep, pol))
338		{
339	187632	if (simPol)
340		{
341	71569	return true;
342		}
343		}
344		else
345		{
346	557461	if (!simPol)
347		{
348	83488	return false;
349		}
350		}
351		}
352	84309	return !simPol;
353		// Boolean equality here
354		}
355	741141	else if (n.getKind() == EQUAL \|\| n.getKind() == ITE)
356		{
357	247957	for (size_t i = 0; i < 2; i++)
358		{
359	186054	if (isEntailed2(n[0], subs, subsRep, i == 0))
360		{
361	41423	size_t ch = (n.getKind() == EQUAL \|\| i == 0) ? 1 : 2;
362	41423	bool reqPol = (n.getKind() == ITE \|\| i == 0) ? pol : !pol;
363	41423	return isEntailed2(n[ch], subs, subsRep, reqPol);
364		}
365		}
366		}
367	637815	else if (n.getKind() == APPLY_UF)
368		{
369	670253	TNode n1 = getEntailedTerm2(n, subs, subsRep);
370	457939	if (!n1.isNull())
371		{
372	245625	Assert(d_qstate.hasTerm(n1));
373	245625	if (n1 == d_true)
374		{
375		return pol;
376		}
377	245625	else if (n1 == d_false)
378		{
379		return !pol;
380		}
381		else
382		{
383	245625	return d_qstate.getRepresentative(n1) == (pol ? d_true : d_false);
384		}
385		}
386		}
387	179876	else if (n.getKind() == FORALL && !pol)
388		{
389	6282	return isEntailed2(n[1], subs, subsRep, pol);
390		}
391	523422	return false;
392		}
393
394	2232	bool EntailmentCheck::isEntailed(TNode n, bool pol)
395		{
396	4464	std::map<TNode, TNode> subs;
397	4464	return isEntailed2(n, subs, false, pol);
398		}
399
400	349135	bool EntailmentCheck::isEntailed(TNode n,
401		std::map<TNode, TNode>& subs,
402		bool subsRep,
403		bool pol)
404		{
405	349135	return isEntailed2(n, subs, subsRep, pol);
406		}
407
408		} // namespace quantifiers
409		} // namespace theory
410	31137	} // namespace cvc5