Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/sets/solver_state.cpp	Lines:	276	293	94.2 %
Date:	2021-08-16	Branches:	578	1214	47.6 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Mudathir Mohamed, Paul Meng
 *
 * 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 sets state object.
 */

#include "theory/sets/solver_state.h"

#include "expr/emptyset.h"
#include "options/sets_options.h"
#include "theory/sets/theory_sets_private.h"

using namespace std;
using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace sets {

SolverState::SolverState(context::Context* c,
                         context::UserContext* u,
                         Valuation val,
                         SkolemCache& skc)
    : TheoryState(c, u, val), d_skCache(skc), d_members(c)
{
  d_true = NodeManager::currentNM()->mkConst(true);
  d_false = NodeManager::currentNM()->mkConst(false);
}

void SolverState::reset()
{
  d_set_eqc.clear();
  d_eqc_emptyset.clear();
  d_eqc_univset.clear();
  d_eqc_singleton.clear();
  d_congruent.clear();
  d_nvar_sets.clear();
  d_var_set.clear();
  d_compSets.clear();
  d_pol_mems[0].clear();
  d_pol_mems[1].clear();
  d_members_index.clear();
  d_singleton_index.clear();
  d_bop_index.clear();
  d_op_list.clear();
  d_allCompSets.clear();
}

void SolverState::registerEqc(TypeNode tn, Node r)
{
  if (tn.isSet())
  {
    d_set_eqc.push_back(r);
  }
}

void SolverState::registerTerm(Node r, TypeNode tnn, Node n)
{
  Kind nk = n.getKind();
  if (nk == MEMBER)
  {
    if (r.isConst())
    {
      Node s = d_ee->getRepresentative(n[1]);
      Node x = d_ee->getRepresentative(n[0]);
      int pindex = r == d_true ? 0 : (r == d_false ? 1 : -1);
      if (pindex != -1)
      {
        if (d_pol_mems[pindex][s].find(x) == d_pol_mems[pindex][s].end())
        {
          d_pol_mems[pindex][s][x] = n;
          Trace("sets-debug2") << "Membership[" << x << "][" << s << "] : " << n
                               << ", pindex = " << pindex << std::endl;
        }
        if (d_members_index[s].find(x) == d_members_index[s].end())
        {
          d_members_index[s][x] = n;
          d_op_list[MEMBER].push_back(n);
        }
      }
      else
      {
        Assert(false);
      }
    }
  }
  else if (nk == SINGLETON || nk == UNION || nk == INTERSECTION
           || nk == SETMINUS || nk == EMPTYSET || nk == UNIVERSE_SET)
  {
    if (nk == SINGLETON)
    {
      Node re = d_ee->getRepresentative(n[0]);
      if (d_singleton_index.find(re) == d_singleton_index.end())
      {
        d_singleton_index[re] = n;
        d_eqc_singleton[r] = n;
        d_op_list[SINGLETON].push_back(n);
      }
      else
      {
        d_congruent[n] = d_singleton_index[re];
      }
    }
    else if (nk == EMPTYSET)
    {
      d_eqc_emptyset[tnn] = r;
    }
    else if (nk == UNIVERSE_SET)
    {
      Assert(options::setsExt());
      d_eqc_univset[tnn] = r;
    }
    else
    {
      Node r1 = d_ee->getRepresentative(n[0]);
      Node r2 = d_ee->getRepresentative(n[1]);
      std::map<Node, Node>& binr1 = d_bop_index[nk][r1];
      std::map<Node, Node>::iterator itb = binr1.find(r2);
      if (itb == binr1.end())
      {
        binr1[r2] = n;
        d_op_list[nk].push_back(n);
      }
      else
      {
        d_congruent[n] = itb->second;
      }
    }
    d_nvar_sets[r].push_back(n);
    Trace("sets-debug2") << "Non-var-set[" << r << "] : " << n << std::endl;
  }
  else if (nk == COMPREHENSION)
  {
    d_compSets[r].push_back(n);
    d_allCompSets.push_back(n);
    Trace("sets-debug2") << "Comp-set[" << r << "] : " << n << std::endl;
  }
  else if (n.isVar() && !d_skCache.isSkolem(n))
  {
    // it is important that we check it is a variable, but not an internally
    // introduced skolem, due to the semantics of the universe set.
    if (tnn.isSet())
    {
      if (d_var_set.find(r) == d_var_set.end())
      {
        d_var_set[r] = n;
        Trace("sets-debug2") << "var-set[" << r << "] : " << n << std::endl;
      }
    }
  }
  else
  {
    Trace("sets-debug2") << "Unknown-set[" << r << "] : " << n << std::endl;
  }
}

void SolverState::addEqualityToExp(Node a, Node b, std::vector<Node>& exp) const
{
  if (a != b)
  {
    Assert(areEqual(a, b));
    exp.push_back(a.eqNode(b));
  }
}

Node SolverState::getEmptySetEqClass(TypeNode tn) const
{
  std::map<TypeNode, Node>::const_iterator it = d_eqc_emptyset.find(tn);
  if (it != d_eqc_emptyset.end())
  {
    return it->second;
  }
  return Node::null();
}

Node SolverState::getUnivSetEqClass(TypeNode tn) const
{
  std::map<TypeNode, Node>::const_iterator it = d_eqc_univset.find(tn);
  if (it != d_eqc_univset.end())
  {
    return it->second;
  }
  return Node::null();
}

Node SolverState::getSingletonEqClass(Node r) const
{
  std::map<Node, Node>::const_iterator it = d_eqc_singleton.find(r);
  if (it != d_eqc_singleton.end())
  {
    return it->second;
  }
  return Node::null();
}

Node SolverState::getBinaryOpTerm(Kind k, Node r1, Node r2) const
{
  std::map<Kind, std::map<Node, std::map<Node, Node> > >::const_iterator itk =
      d_bop_index.find(k);
  if (itk == d_bop_index.end())
  {
    return Node::null();
  }
  std::map<Node, std::map<Node, Node> >::const_iterator it1 =
      itk->second.find(r1);
  if (it1 == itk->second.end())
  {
    return Node::null();
  }
  std::map<Node, Node>::const_iterator it2 = it1->second.find(r2);
  if (it2 == it1->second.end())
  {
    return Node::null();
  }
  return it2->second;
}

bool SolverState::isEntailed(Node n, bool polarity) const
{
  if (n.getKind() == NOT)
  {
    return isEntailed(n[0], !polarity);
  }
  else if (n.getKind() == EQUAL)
  {
    if (polarity)
    {
      return areEqual(n[0], n[1]);
    }
    return areDisequal(n[0], n[1]);
  }
  else if (n.getKind() == MEMBER)
  {
    if (areEqual(n, polarity ? d_true : d_false))
    {
      return true;
    }
    // check members cache
    if (polarity && d_ee->hasTerm(n[1]))
    {
      Node r = d_ee->getRepresentative(n[1]);
      if (isMember(n[0], r))
      {
        return true;
      }
    }
  }
  else if (n.getKind() == AND || n.getKind() == OR)
  {
    bool conj = (n.getKind() == AND) == polarity;
    for (const Node& nc : n)
    {
      bool isEnt = isEntailed(nc, polarity);
      if (isEnt != conj)
      {
        return !conj;
      }
    }
    return conj;
  }
  else if (n.isConst())
  {
    return (polarity && n == d_true) || (!polarity && n == d_false);
  }
  return false;
}

bool SolverState::isSetDisequalityEntailed(Node r1, Node r2) const
{
  Assert(d_ee->hasTerm(r1) && d_ee->getRepresentative(r1) == r1);
  Assert(d_ee->hasTerm(r2) && d_ee->getRepresentative(r2) == r2);
  TypeNode tn = r1.getType();
  Node re = getEmptySetEqClass(tn);
  for (unsigned e = 0; e < 2; e++)
  {
    Node a = e == 0 ? r1 : r2;
    Node b = e == 0 ? r2 : r1;
    if (isSetDisequalityEntailedInternal(a, b, re))
    {
      return true;
    }
  }
  return false;
}

bool SolverState::isSetDisequalityEntailedInternal(Node a,
                                                   Node b,
                                                   Node re) const
{
  // if there are members in a
  std::map<Node, std::map<Node, Node> >::const_iterator itpma =
      d_pol_mems[0].find(a);
  if (itpma == d_pol_mems[0].end())
  {
    // no positive members, continue
    return false;
  }
  // if b is empty
  if (b == re)
  {
    if (!itpma->second.empty())
    {
      Trace("sets-deq") << "Disequality is satisfied because members are in "
                        << a << " and " << b << " is empty" << std::endl;
      return true;
    }
    else
    {
      // a should not be singleton
      Assert(d_eqc_singleton.find(a) == d_eqc_singleton.end());
    }
    return false;
  }
  std::map<Node, Node>::const_iterator itsb = d_eqc_singleton.find(b);
  std::map<Node, std::map<Node, Node> >::const_iterator itpmb =
      d_pol_mems[1].find(b);
  std::vector<Node> prev;
  for (const std::pair<const Node, Node>& itm : itpma->second)
  {
    // if b is a singleton
    if (itsb != d_eqc_singleton.end())
    {
      if (areDisequal(itm.first, itsb->second[0]))
      {
        Trace("sets-deq") << "Disequality is satisfied because of "
                          << itm.second << ", singleton eq " << itsb->second[0]
                          << std::endl;
        return true;
      }
      // or disequal with another member
      for (const Node& p : prev)
      {
        if (areDisequal(itm.first, p))
        {
          Trace("sets-deq")
              << "Disequality is satisfied because of disequal members "
              << itm.first << " " << p << ", singleton eq " << std::endl;
          return true;
        }
      }
      // if a has positive member that is negative member in b
    }
    else if (itpmb != d_pol_mems[1].end())
    {
      for (const std::pair<const Node, Node>& itnm : itpmb->second)
      {
        if (areEqual(itm.first, itnm.first))
        {
          Trace("sets-deq") << "Disequality is satisfied because of "
                            << itm.second << " " << itnm.second << std::endl;
          return true;
        }
      }
    }
    prev.push_back(itm.first);
  }
  return false;
}

Node SolverState::getCongruent(Node n) const
{
  Assert(d_ee->hasTerm(n));
  std::map<Node, Node>::const_iterator it = d_congruent.find(n);
  if (it == d_congruent.end())
  {
    return n;
  }
  return it->second;
}
bool SolverState::isCongruent(Node n) const
{
  return d_congruent.find(n) != d_congruent.end();
}
const std::vector<Node>& SolverState::getNonVariableSets(Node r) const
{
  std::map<Node, std::vector<Node> >::const_iterator it = d_nvar_sets.find(r);
  if (it == d_nvar_sets.end())
  {
    return d_emptyVec;
  }
  return it->second;
}

Node SolverState::getVariableSet(Node r) const
{
  std::map<Node, Node>::const_iterator it = d_var_set.find(r);
  if (it != d_var_set.end())
  {
    return it->second;
  }
  return Node::null();
}

const std::vector<Node>& SolverState::getComprehensionSets(Node r) const
{
  std::map<Node, std::vector<Node> >::const_iterator it = d_compSets.find(r);
  if (it == d_compSets.end())
  {
    return d_emptyVec;
  }
  return it->second;
}

const std::map<Node, Node>& SolverState::getMembers(Node r) const
{
  return getMembersInternal(r, 0);
}
const std::map<Node, Node>& SolverState::getNegativeMembers(Node r) const
{
  return getMembersInternal(r, 1);
}
const std::map<Node, Node>& SolverState::getMembersInternal(Node r,
                                                            unsigned i) const
{
  std::map<Node, std::map<Node, Node> >::const_iterator itp =
      d_pol_mems[i].find(r);
  if (itp == d_pol_mems[i].end())
  {
    return d_emptyMap;
  }
  return itp->second;
}

bool SolverState::hasMembers(Node r) const
{
  std::map<Node, std::map<Node, Node> >::const_iterator it =
      d_pol_mems[0].find(r);
  if (it == d_pol_mems[0].end())
  {
    return false;
  }
  return !it->second.empty();
}
const std::map<Kind, std::map<Node, std::map<Node, Node> > >&
SolverState::getBinaryOpIndex() const
{
  return d_bop_index;
}

const std::map<Node, std::map<Node, Node>>& SolverState::getBinaryOpIndex(
    Kind k)
{
  return d_bop_index[k];
}

const std::map<Kind, std::vector<Node> >& SolverState::getOperatorList() const
{
  return d_op_list;
}

const std::vector<Node>& SolverState::getComprehensionSets() const
{
  return d_allCompSets;
}

const vector<Node> SolverState::getSetsEqClasses(const TypeNode& t) const
{
  vector<Node> representatives;
  for (const Node& eqc : getSetsEqClasses())
  {
    if (eqc.getType().getSetElementType() == t)
    {
      representatives.push_back(eqc);
    }
  }
  return representatives;
}

bool SolverState::isMember(TNode x, TNode s) const
{
  Assert(hasTerm(s) && getRepresentative(s) == s);
  NodeIntMap::const_iterator mem_i = d_members.find(s);
  if (mem_i != d_members.end())
  {
    std::map<Node, std::vector<Node> >::const_iterator itd =
        d_members_data.find(s);
    Assert(itd != d_members_data.end());
    const std::vector<Node>& members = itd->second;
    Assert((*mem_i).second <= members.size());
    for (size_t i = 0, nmem = (*mem_i).second; i < nmem; i++)
    {
      if (areEqual(members[i][0], x))
      {
        return true;
      }
    }
  }
  return false;
}

void SolverState::addMember(TNode r, TNode atom)
{
  NodeIntMap::iterator mem_i = d_members.find(r);
  size_t n_members = 0;
  if (mem_i != d_members.end())
  {
    n_members = (*mem_i).second;
  }
  d_members[r] = n_members + 1;
  if (n_members < d_members_data[r].size())
  {
    d_members_data[r][n_members] = atom;
  }
  else
  {
    d_members_data[r].push_back(atom);
  }
}

bool SolverState::merge(TNode t1,
                        TNode t2,
                        std::vector<Node>& facts,
                        TNode cset)
{
  NodeIntMap::iterator mem_i2 = d_members.find(t2);
  if (mem_i2 == d_members.end())
  {
    // no members in t2, we are done
    return true;
  }
  NodeIntMap::iterator mem_i1 = d_members.find(t1);
  size_t n_members = 0;
  if (mem_i1 != d_members.end())
  {
    n_members = (*mem_i1).second;
  }
  for (size_t i = 0, nmem2 = (*mem_i2).second; i < nmem2; i++)
  {
    Assert(i < d_members_data[t2].size()
           && d_members_data[t2][i].getKind() == MEMBER);
    Node m2 = d_members_data[t2][i];
    // check if redundant
    bool add = true;
    for (size_t j = 0; j < n_members; j++)
    {
      Assert(j < d_members_data[t1].size()
             && d_members_data[t1][j].getKind() == MEMBER);
      if (areEqual(m2[0], d_members_data[t1][j][0]))
      {
        add = false;
        break;
      }
    }
    if (add)
    {
      // if there is a concrete set in t1, propagate new facts or conflicts
      if (!cset.isNull())
      {
        NodeManager* nm = NodeManager::currentNM();
        Assert(areEqual(m2[1], cset));
        Node exp = nm->mkNode(AND, m2[1].eqNode(cset), m2);
        if (cset.getKind() == SINGLETON)
        {
          if (cset[0] != m2[0])
          {
            Node eq = cset[0].eqNode(m2[0]);
            Trace("sets-prop") << "Propagate eq-mem eq inference : " << exp
                               << " => " << eq << std::endl;
            Node fact = nm->mkNode(IMPLIES, exp, eq);
            facts.push_back(fact);
          }
        }
        else
        {
          // conflict
          Assert(facts.empty());
          Trace("sets-prop")
              << "Propagate eq-mem conflict : " << exp << std::endl;
          facts.push_back(exp);
          return false;
        }
      }
      if (n_members < d_members_data[t1].size())
      {
        d_members_data[t1][n_members] = m2;
      }
      else
      {
        d_members_data[t1].push_back(m2);
      }
      n_members++;
    }
  }
  d_members[t1] = n_members;
  return true;
}

}  // namespace sets
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Mudathir Mohamed, Paul Meng
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 sets state object.
14		*/
15
16		#include "theory/sets/solver_state.h"
17
18		#include "expr/emptyset.h"
19		#include "options/sets_options.h"
20		#include "theory/sets/theory_sets_private.h"
21
22		using namespace std;
23		using namespace cvc5::kind;
24
25		namespace cvc5 {
26		namespace theory {
27		namespace sets {
28
29	9853	SolverState::SolverState(context::Context* c,
30		context::UserContext* u,
31		Valuation val,
32	9853	SkolemCache& skc)
33	9853	: TheoryState(c, u, val), d_skCache(skc), d_members(c)
34		{
35	9853	d_true = NodeManager::currentNM()->mkConst(true);
36	9853	d_false = NodeManager::currentNM()->mkConst(false);
37	9853	}
38
39	35347	void SolverState::reset()
40		{
41	35347	d_set_eqc.clear();
42	35347	d_eqc_emptyset.clear();
43	35347	d_eqc_univset.clear();
44	35347	d_eqc_singleton.clear();
45	35347	d_congruent.clear();
46	35347	d_nvar_sets.clear();
47	35347	d_var_set.clear();
48	35347	d_compSets.clear();
49	35347	d_pol_mems[0].clear();
50	35347	d_pol_mems[1].clear();
51	35347	d_members_index.clear();
52	35347	d_singleton_index.clear();
53	35347	d_bop_index.clear();
54	35347	d_op_list.clear();
55	35347	d_allCompSets.clear();
56	35347	}
57
58	161189	void SolverState::registerEqc(TypeNode tn, Node r)
59		{
60	161189	if (tn.isSet())
61		{
62	54121	d_set_eqc.push_back(r);
63		}
64	161189	}
65
66	538041	void SolverState::registerTerm(Node r, TypeNode tnn, Node n)
67		{
68	538041	Kind nk = n.getKind();
69	538041	if (nk == MEMBER)
70		{
71	123638	if (r.isConst())
72		{
73	234780	Node s = d_ee->getRepresentative(n[1]);
74	234780	Node x = d_ee->getRepresentative(n[0]);
75	117390	int pindex = r == d_true ? 0 : (r == d_false ? 1 : -1);
76	117390	if (pindex != -1)
77		{
78	117390	if (d_pol_mems[pindex][s].find(x) == d_pol_mems[pindex][s].end())
79		{
80	84013	d_pol_mems[pindex][s][x] = n;
81	168026	Trace("sets-debug2") << "Membership[" << x << "][" << s << "] : " << n
82	84013	<< ", pindex = " << pindex << std::endl;
83		}
84	117390	if (d_members_index[s].find(x) == d_members_index[s].end())
85		{
86	84013	d_members_index[s][x] = n;
87	84013	d_op_list[MEMBER].push_back(n);
88		}
89		}
90		else
91		{
92		Assert(false);
93		}
94		}
95		}
96	414403	else if (nk == SINGLETON \|\| nk == UNION \|\| nk == INTERSECTION
97	377427	\|\| nk == SETMINUS \|\| nk == EMPTYSET \|\| nk == UNIVERSE_SET)
98		{
99	63862	if (nk == SINGLETON)
100		{
101	17696	Node re = d_ee->getRepresentative(n[0]);
102	8848	if (d_singleton_index.find(re) == d_singleton_index.end())
103		{
104	6707	d_singleton_index[re] = n;
105	6707	d_eqc_singleton[r] = n;
106	6707	d_op_list[SINGLETON].push_back(n);
107		}
108		else
109		{
110	2141	d_congruent[n] = d_singleton_index[re];
111		}
112		}
113	55014	else if (nk == EMPTYSET)
114		{
115	3753	d_eqc_emptyset[tnn] = r;
116		}
117	51261	else if (nk == UNIVERSE_SET)
118		{
119	1857	Assert(options::setsExt());
120	1857	d_eqc_univset[tnn] = r;
121		}
122		else
123		{
124	98808	Node r1 = d_ee->getRepresentative(n[0]);
125	98808	Node r2 = d_ee->getRepresentative(n[1]);
126	49404	std::map<Node, Node>& binr1 = d_bop_index[nk][r1];
127	49404	std::map<Node, Node>::iterator itb = binr1.find(r2);
128	49404	if (itb == binr1.end())
129		{
130	46439	binr1[r2] = n;
131	46439	d_op_list[nk].push_back(n);
132		}
133		else
134		{
135	2965	d_congruent[n] = itb->second;
136		}
137		}
138	63862	d_nvar_sets[r].push_back(n);
139	63862	Trace("sets-debug2") << "Non-var-set[" << r << "] : " << n << std::endl;
140		}
141	350541	else if (nk == COMPREHENSION)
142		{
143	124	d_compSets[r].push_back(n);
144	124	d_allCompSets.push_back(n);
145	124	Trace("sets-debug2") << "Comp-set[" << r << "] : " << n << std::endl;
146		}
147	350417	else if (n.isVar() && !d_skCache.isSkolem(n))
148		{
149		// it is important that we check it is a variable, but not an internally
150		// introduced skolem, due to the semantics of the universe set.
151	33233	if (tnn.isSet())
152		{
153	22485	if (d_var_set.find(r) == d_var_set.end())
154		{
155	20771	d_var_set[r] = n;
156	20771	Trace("sets-debug2") << "var-set[" << r << "] : " << n << std::endl;
157		}
158		}
159		}
160		else
161		{
162	317184	Trace("sets-debug2") << "Unknown-set[" << r << "] : " << n << std::endl;
163		}
164	538041	}
165
166	67233	void SolverState::addEqualityToExp(Node a, Node b, std::vector<Node>& exp) const
167		{
168	67233	if (a != b)
169		{
170	19850	Assert(areEqual(a, b));
171	19850	exp.push_back(a.eqNode(b));
172		}
173	67233	}
174
175	14513	Node SolverState::getEmptySetEqClass(TypeNode tn) const
176		{
177	14513	std::map<TypeNode, Node>::const_iterator it = d_eqc_emptyset.find(tn);
178	14513	if (it != d_eqc_emptyset.end())
179		{
180	13163	return it->second;
181		}
182	1350	return Node::null();
183		}
184
185	3660	Node SolverState::getUnivSetEqClass(TypeNode tn) const
186		{
187	3660	std::map<TypeNode, Node>::const_iterator it = d_eqc_univset.find(tn);
188	3660	if (it != d_eqc_univset.end())
189		{
190	2764	return it->second;
191		}
192	896	return Node::null();
193		}
194
195	8027	Node SolverState::getSingletonEqClass(Node r) const
196		{
197	8027	std::map<Node, Node>::const_iterator it = d_eqc_singleton.find(r);
198	8027	if (it != d_eqc_singleton.end())
199		{
200	4	return it->second;
201		}
202	8023	return Node::null();
203		}
204
205	234	Node SolverState::getBinaryOpTerm(Kind k, Node r1, Node r2) const
206		{
207		std::map<Kind, std::map<Node, std::map<Node, Node> > >::const_iterator itk =
208	234	d_bop_index.find(k);
209	234	if (itk == d_bop_index.end())
210		{
211		return Node::null();
212		}
213		std::map<Node, std::map<Node, Node> >::const_iterator it1 =
214	234	itk->second.find(r1);
215	234	if (it1 == itk->second.end())
216		{
217	136	return Node::null();
218		}
219	98	std::map<Node, Node>::const_iterator it2 = it1->second.find(r2);
220	98	if (it2 == it1->second.end())
221		{
222	62	return Node::null();
223		}
224	36	return it2->second;
225		}
226
227	167839	bool SolverState::isEntailed(Node n, bool polarity) const
228		{
229	167839	if (n.getKind() == NOT)
230		{
231	15524	return isEntailed(n[0], !polarity);
232		}
233	152315	else if (n.getKind() == EQUAL)
234		{
235	8117	if (polarity)
236		{
237	7333	return areEqual(n[0], n[1]);
238		}
239	784	return areDisequal(n[0], n[1]);
240		}
241	144198	else if (n.getKind() == MEMBER)
242		{
243	80068	if (areEqual(n, polarity ? d_true : d_false))
244		{
245	56551	return true;
246		}
247		// check members cache
248	23517	if (polarity && d_ee->hasTerm(n[1]))
249		{
250	33995	Node r = d_ee->getRepresentative(n[1]);
251	22703	if (isMember(n[0], r))
252		{
253	11411	return true;
254		}
255		}
256		}
257	64130	else if (n.getKind() == AND \|\| n.getKind() == OR)
258		{
259	39906	bool conj = (n.getKind() == AND) == polarity;
260	98015	for (const Node& nc : n)
261		{
262	73659	bool isEnt = isEntailed(nc, polarity);
263	73659	if (isEnt != conj)
264		{
265	15550	return !conj;
266		}
267		}
268	24356	return conj;
269		}
270	24224	else if (n.isConst())
271		{
272	12004	return (polarity && n == d_true) \|\| (!polarity && n == d_false);
273		}
274	24326	return false;
275		}
276
277	5393	bool SolverState::isSetDisequalityEntailed(Node r1, Node r2) const
278		{
279	5393	Assert(d_ee->hasTerm(r1) && d_ee->getRepresentative(r1) == r1);
280	5393	Assert(d_ee->hasTerm(r2) && d_ee->getRepresentative(r2) == r2);
281	10786	TypeNode tn = r1.getType();
282	10786	Node re = getEmptySetEqClass(tn);
283	7756	for (unsigned e = 0; e < 2; e++)
284		{
285	9387	Node a = e == 0 ? r1 : r2;
286	9387	Node b = e == 0 ? r2 : r1;
287	7024	if (isSetDisequalityEntailedInternal(a, b, re))
288		{
289	4661	return true;
290		}
291		}
292	732	return false;
293		}
294
295	7024	bool SolverState::isSetDisequalityEntailedInternal(Node a,
296		Node b,
297		Node re) const
298		{
299		// if there are members in a
300		std::map<Node, std::map<Node, Node> >::const_iterator itpma =
301	7024	d_pol_mems[0].find(a);
302	7024	if (itpma == d_pol_mems[0].end())
303		{
304		// no positive members, continue
305	1360	return false;
306		}
307		// if b is empty
308	5664	if (b == re)
309		{
310	2323	if (!itpma->second.empty())
311		{
312	4646	Trace("sets-deq") << "Disequality is satisfied because members are in "
313	2323	<< a << " and " << b << " is empty" << std::endl;
314	2323	return true;
315		}
316		else
317		{
318		// a should not be singleton
319		Assert(d_eqc_singleton.find(a) == d_eqc_singleton.end());
320		}
321		return false;
322		}
323	3341	std::map<Node, Node>::const_iterator itsb = d_eqc_singleton.find(b);
324		std::map<Node, std::map<Node, Node> >::const_iterator itpmb =
325	3341	d_pol_mems[1].find(b);
326	6682	std::vector<Node> prev;
327	5762	for (const std::pair<const Node, Node>& itm : itpma->second)
328		{
329		// if b is a singleton
330	4759	if (itsb != d_eqc_singleton.end())
331		{
332	1714	if (areDisequal(itm.first, itsb->second[0]))
333		{
334	2462	Trace("sets-deq") << "Disequality is satisfied because of "
335	2462	<< itm.second << ", singleton eq " << itsb->second[0]
336	1231	<< std::endl;
337	3569	return true;
338		}
339		// or disequal with another member
340	574	for (const Node& p : prev)
341		{
342	102	if (areDisequal(itm.first, p))
343		{
344	22	Trace("sets-deq")
345	11	<< "Disequality is satisfied because of disequal members "
346	11	<< itm.first << " " << p << ", singleton eq " << std::endl;
347	11	return true;
348		}
349		}
350		// if a has positive member that is negative member in b
351		}
352	3045	else if (itpmb != d_pol_mems[1].end())
353		{
354	4039	for (const std::pair<const Node, Node>& itnm : itpmb->second)
355		{
356	3075	if (areEqual(itm.first, itnm.first))
357		{
358	2192	Trace("sets-deq") << "Disequality is satisfied because of "
359	1096	<< itm.second << " " << itnm.second << std::endl;
360	1096	return true;
361		}
362		}
363		}
364	2421	prev.push_back(itm.first);
365		}
366	1003	return false;
367		}
368
369		Node SolverState::getCongruent(Node n) const
370		{
371		Assert(d_ee->hasTerm(n));
372		std::map<Node, Node>::const_iterator it = d_congruent.find(n);
373		if (it == d_congruent.end())
374		{
375		return n;
376		}
377		return it->second;
378		}
379	82692	bool SolverState::isCongruent(Node n) const
380		{
381	82692	return d_congruent.find(n) != d_congruent.end();
382		}
383	76522	const std::vector<Node>& SolverState::getNonVariableSets(Node r) const
384		{
385	76522	std::map<Node, std::vector<Node> >::const_iterator it = d_nvar_sets.find(r);
386	76522	if (it == d_nvar_sets.end())
387		{
388	18115	return d_emptyVec;
389		}
390	58407	return it->second;
391		}
392
393	21815	Node SolverState::getVariableSet(Node r) const
394		{
395	21815	std::map<Node, Node>::const_iterator it = d_var_set.find(r);
396	21815	if (it != d_var_set.end())
397		{
398	6197	return it->second;
399		}
400	15618	return Node::null();
401		}
402
403		const std::vector<Node>& SolverState::getComprehensionSets(Node r) const
404		{
405		std::map<Node, std::vector<Node> >::const_iterator it = d_compSets.find(r);
406		if (it == d_compSets.end())
407		{
408		return d_emptyVec;
409		}
410		return it->second;
411		}
412
413	113172	const std::map<Node, Node>& SolverState::getMembers(Node r) const
414		{
415	113172	return getMembersInternal(r, 0);
416		}
417	32049	const std::map<Node, Node>& SolverState::getNegativeMembers(Node r) const
418		{
419	32049	return getMembersInternal(r, 1);
420		}
421	145221	const std::map<Node, Node>& SolverState::getMembersInternal(Node r,
422		unsigned i) const
423		{
424		std::map<Node, std::map<Node, Node> >::const_iterator itp =
425	145221	d_pol_mems[i].find(r);
426	145221	if (itp == d_pol_mems[i].end())
427		{
428	46200	return d_emptyMap;
429		}
430	99021	return itp->second;
431		}
432
433	1137	bool SolverState::hasMembers(Node r) const
434		{
435		std::map<Node, std::map<Node, Node> >::const_iterator it =
436	1137	d_pol_mems[0].find(r);
437	1137	if (it == d_pol_mems[0].end())
438		{
439	387	return false;
440		}
441	750	return !it->second.empty();
442		}
443		const std::map<Kind, std::map<Node, std::map<Node, Node> > >&
444	19063	SolverState::getBinaryOpIndex() const
445		{
446	19063	return d_bop_index;
447		}
448
449		const std::map<Node, std::map<Node, Node>>& SolverState::getBinaryOpIndex(
450		Kind k)
451		{
452		return d_bop_index[k];
453		}
454
455	6672	const std::map<Kind, std::vector<Node> >& SolverState::getOperatorList() const
456		{
457	6672	return d_op_list;
458		}
459
460	17314	const std::vector<Node>& SolverState::getComprehensionSets() const
461		{
462	17314	return d_allCompSets;
463		}
464
465	986	const vector<Node> SolverState::getSetsEqClasses(const TypeNode& t) const
466		{
467	986	vector<Node> representatives;
468	9954	for (const Node& eqc : getSetsEqClasses())
469		{
470	8968	if (eqc.getType().getSetElementType() == t)
471		{
472	8968	representatives.push_back(eqc);
473		}
474		}
475	986	return representatives;
476		}
477
478	66235	bool SolverState::isMember(TNode x, TNode s) const
479		{
480	66235	Assert(hasTerm(s) && getRepresentative(s) == s);
481	66235	NodeIntMap::const_iterator mem_i = d_members.find(s);
482	66235	if (mem_i != d_members.end())
483		{
484		std::map<Node, std::vector<Node> >::const_iterator itd =
485	59218	d_members_data.find(s);
486	59218	Assert(itd != d_members_data.end());
487	59218	const std::vector<Node>& members = itd->second;
488	59218	Assert((*mem_i).second <= members.size());
489	128565	for (size_t i = 0, nmem = (*mem_i).second; i < nmem; i++)
490		{
491	121394	if (areEqual(members[i][0], x))
492		{
493	52047	return true;
494		}
495		}
496		}
497	14188	return false;
498		}
499
500	63814	void SolverState::addMember(TNode r, TNode atom)
501		{
502	63814	NodeIntMap::iterator mem_i = d_members.find(r);
503	63814	size_t n_members = 0;
504	63814	if (mem_i != d_members.end())
505		{
506	47428	n_members = (*mem_i).second;
507		}
508	63814	d_members[r] = n_members + 1;
509	63814	if (n_members < d_members_data[r].size())
510		{
511	53283	d_members_data[r][n_members] = atom;
512		}
513		else
514		{
515	10531	d_members_data[r].push_back(atom);
516		}
517	63814	}
518
519	27971	bool SolverState::merge(TNode t1,
520		TNode t2,
521		std::vector<Node>& facts,
522		TNode cset)
523		{
524	27971	NodeIntMap::iterator mem_i2 = d_members.find(t2);
525	27971	if (mem_i2 == d_members.end())
526		{
527		// no members in t2, we are done
528	12310	return true;
529		}
530	15661	NodeIntMap::iterator mem_i1 = d_members.find(t1);
531	15661	size_t n_members = 0;
532	15661	if (mem_i1 != d_members.end())
533		{
534	15264	n_members = (*mem_i1).second;
535		}
536	32593	for (size_t i = 0, nmem2 = (*mem_i2).second; i < nmem2; i++)
537		{
538	17037	Assert(i < d_members_data[t2].size()
539		&& d_members_data[t2][i].getKind() == MEMBER);
540	33969	Node m2 = d_members_data[t2][i];
541		// check if redundant
542	17037	bool add = true;
543	20239	for (size_t j = 0; j < n_members; j++)
544		{
545	19327	Assert(j < d_members_data[t1].size()
546		&& d_members_data[t1][j].getKind() == MEMBER);
547	19327	if (areEqual(m2[0], d_members_data[t1][j][0]))
548		{
549	16125	add = false;
550	16125	break;
551		}
552		}
553	17037	if (add)
554		{
555		// if there is a concrete set in t1, propagate new facts or conflicts
556	912	if (!cset.isNull())
557		{
558	234	NodeManager* nm = NodeManager::currentNM();
559	234	Assert(areEqual(m2[1], cset));
560	363	Node exp = nm->mkNode(AND, m2[1].eqNode(cset), m2);
561	234	if (cset.getKind() == SINGLETON)
562		{
563	129	if (cset[0] != m2[0])
564		{
565	258	Node eq = cset[0].eqNode(m2[0]);
566	258	Trace("sets-prop") << "Propagate eq-mem eq inference : " << exp
567	129	<< " => " << eq << std::endl;
568	258	Node fact = nm->mkNode(IMPLIES, exp, eq);
569	129	facts.push_back(fact);
570		}
571		}
572		else
573		{
574		// conflict
575	105	Assert(facts.empty());
576	210	Trace("sets-prop")
577	105	<< "Propagate eq-mem conflict : " << exp << std::endl;
578	105	facts.push_back(exp);
579	105	return false;
580		}
581		}
582	807	if (n_members < d_members_data[t1].size())
583		{
584	582	d_members_data[t1][n_members] = m2;
585		}
586		else
587		{
588	225	d_members_data[t1].push_back(m2);
589		}
590	807	n_members++;
591		}
592		}
593	15556	d_members[t1] = n_members;
594	15556	return true;
595		}
596
597		} // namespace sets
598		} // namespace theory
599	29340	} // namespace cvc5