Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/sets/solver_state.cpp	Lines:	275	292	94.2 %
Date:	2021-11-07	Branches:	579	1216	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(Env& env, Valuation val, SkolemCache& skc)
    : TheoryState(env, val), d_skCache(skc), d_members(env.getContext())
{
  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().sets.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	15273	SolverState::SolverState(Env& env, Valuation val, SkolemCache& skc)
30	15273	: TheoryState(env, val), d_skCache(skc), d_members(env.getContext())
31		{
32	15273	d_true = NodeManager::currentNM()->mkConst(true);
33	15273	d_false = NodeManager::currentNM()->mkConst(false);
34	15273	}
35
36	44661	void SolverState::reset()
37		{
38	44661	d_set_eqc.clear();
39	44661	d_eqc_emptyset.clear();
40	44661	d_eqc_univset.clear();
41	44661	d_eqc_singleton.clear();
42	44661	d_congruent.clear();
43	44661	d_nvar_sets.clear();
44	44661	d_var_set.clear();
45	44661	d_compSets.clear();
46	44661	d_pol_mems[0].clear();
47	44661	d_pol_mems[1].clear();
48	44661	d_members_index.clear();
49	44661	d_singleton_index.clear();
50	44661	d_bop_index.clear();
51	44661	d_op_list.clear();
52	44661	d_allCompSets.clear();
53	44661	}
54
55	257203	void SolverState::registerEqc(TypeNode tn, Node r)
56		{
57	257203	if (tn.isSet())
58		{
59	87206	d_set_eqc.push_back(r);
60		}
61	257203	}
62
63	1324957	void SolverState::registerTerm(Node r, TypeNode tnn, Node n)
64		{
65	1324957	Kind nk = n.getKind();
66	1324957	if (nk == MEMBER)
67		{
68	477341	if (r.isConst())
69		{
70	887334	Node s = d_ee->getRepresentative(n[1]);
71	887334	Node x = d_ee->getRepresentative(n[0]);
72	443667	int pindex = r == d_true ? 0 : (r == d_false ? 1 : -1);
73	443667	if (pindex != -1)
74		{
75	443667	if (d_pol_mems[pindex][s].find(x) == d_pol_mems[pindex][s].end())
76		{
77	179248	d_pol_mems[pindex][s][x] = n;
78	358496	Trace("sets-debug2") << "Membership[" << x << "][" << s << "] : " << n
79	179248	<< ", pindex = " << pindex << std::endl;
80		}
81	443667	if (d_members_index[s].find(x) == d_members_index[s].end())
82		{
83	179248	d_members_index[s][x] = n;
84	179248	d_op_list[MEMBER].push_back(n);
85		}
86		}
87		else
88		{
89		Assert(false);
90		}
91		}
92		}
93	847616	else if (nk == SINGLETON \|\| nk == UNION \|\| nk == INTERSECTION
94	778509	\|\| nk == SETMINUS \|\| nk == EMPTYSET \|\| nk == UNIVERSE_SET)
95		{
96	123082	if (nk == SINGLETON)
97		{
98	46032	Node re = d_ee->getRepresentative(n[0]);
99	23016	if (d_singleton_index.find(re) == d_singleton_index.end())
100		{
101	20691	d_singleton_index[re] = n;
102	20691	d_eqc_singleton[r] = n;
103	20691	d_op_list[SINGLETON].push_back(n);
104		}
105		else
106		{
107	2325	d_congruent[n] = d_singleton_index[re];
108		}
109		}
110	100066	else if (nk == EMPTYSET)
111		{
112	4962	d_eqc_emptyset[tnn] = r;
113		}
114	95104	else if (nk == UNIVERSE_SET)
115		{
116	2517	Assert(options().sets.setsExt);
117	2517	d_eqc_univset[tnn] = r;
118		}
119		else
120		{
121	185174	Node r1 = d_ee->getRepresentative(n[0]);
122	185174	Node r2 = d_ee->getRepresentative(n[1]);
123	92587	std::map<Node, Node>& binr1 = d_bop_index[nk][r1];
124	92587	std::map<Node, Node>::iterator itb = binr1.find(r2);
125	92587	if (itb == binr1.end())
126		{
127	83003	binr1[r2] = n;
128	83003	d_op_list[nk].push_back(n);
129		}
130		else
131		{
132	9584	d_congruent[n] = itb->second;
133		}
134		}
135	123082	d_nvar_sets[r].push_back(n);
136	123082	Trace("sets-debug2") << "Non-var-set[" << r << "] : " << n << std::endl;
137		}
138	724534	else if (nk == COMPREHENSION)
139		{
140	140	d_compSets[r].push_back(n);
141	140	d_allCompSets.push_back(n);
142	140	Trace("sets-debug2") << "Comp-set[" << r << "] : " << n << std::endl;
143		}
144	724394	else if (n.isVar() && !d_skCache.isSkolem(n))
145		{
146		// it is important that we check it is a variable, but not an internally
147		// introduced skolem, due to the semantics of the universe set.
148	38232	if (tnn.isSet())
149		{
150	26337	if (d_var_set.find(r) == d_var_set.end())
151		{
152	23473	d_var_set[r] = n;
153	23473	Trace("sets-debug2") << "var-set[" << r << "] : " << n << std::endl;
154		}
155		}
156		}
157		else
158		{
159	686162	Trace("sets-debug2") << "Unknown-set[" << r << "] : " << n << std::endl;
160		}
161	1324957	}
162
163	158595	void SolverState::addEqualityToExp(Node a, Node b, std::vector<Node>& exp) const
164		{
165	158595	if (a != b)
166		{
167	61534	Assert(areEqual(a, b));
168	61534	exp.push_back(a.eqNode(b));
169		}
170	158595	}
171
172	40336	Node SolverState::getEmptySetEqClass(TypeNode tn) const
173		{
174	40336	std::map<TypeNode, Node>::const_iterator it = d_eqc_emptyset.find(tn);
175	40336	if (it != d_eqc_emptyset.end())
176		{
177	38914	return it->second;
178		}
179	1422	return Node::null();
180		}
181
182	5208	Node SolverState::getUnivSetEqClass(TypeNode tn) const
183		{
184	5208	std::map<TypeNode, Node>::const_iterator it = d_eqc_univset.find(tn);
185	5208	if (it != d_eqc_univset.end())
186		{
187	4218	return it->second;
188		}
189	990	return Node::null();
190		}
191
192	12920	Node SolverState::getSingletonEqClass(Node r) const
193		{
194	12920	std::map<Node, Node>::const_iterator it = d_eqc_singleton.find(r);
195	12920	if (it != d_eqc_singleton.end())
196		{
197	8	return it->second;
198		}
199	12912	return Node::null();
200		}
201
202	305	Node SolverState::getBinaryOpTerm(Kind k, Node r1, Node r2) const
203		{
204		std::map<Kind, std::map<Node, std::map<Node, Node> > >::const_iterator itk =
205	305	d_bop_index.find(k);
206	305	if (itk == d_bop_index.end())
207		{
208		return Node::null();
209		}
210		std::map<Node, std::map<Node, Node> >::const_iterator it1 =
211	305	itk->second.find(r1);
212	305	if (it1 == itk->second.end())
213		{
214	172	return Node::null();
215		}
216	133	std::map<Node, Node>::const_iterator it2 = it1->second.find(r2);
217	133	if (it2 == it1->second.end())
218		{
219	88	return Node::null();
220		}
221	45	return it2->second;
222		}
223
224	443753	bool SolverState::isEntailed(Node n, bool polarity) const
225		{
226	443753	if (n.getKind() == NOT)
227		{
228	47732	return isEntailed(n[0], !polarity);
229		}
230	396021	else if (n.getKind() == EQUAL)
231		{
232	11033	if (polarity)
233		{
234	10191	return areEqual(n[0], n[1]);
235		}
236	842	return areDisequal(n[0], n[1]);
237		}
238	384988	else if (n.getKind() == MEMBER)
239		{
240	224785	if (areEqual(n, polarity ? d_true : d_false))
241		{
242	173704	return true;
243		}
244		// check members cache
245	51081	if (polarity && d_ee->hasTerm(n[1]))
246		{
247	74649	Node r = d_ee->getRepresentative(n[1]);
248	50049	if (isMember(n[0], r))
249		{
250	25449	return true;
251		}
252		}
253		}
254	160203	else if (n.getKind() == AND \|\| n.getKind() == OR)
255		{
256	115714	bool conj = (n.getKind() == AND) == polarity;
257	287053	for (const Node& nc : n)
258		{
259	212452	bool isEnt = isEntailed(nc, polarity);
260	212452	if (isEnt != conj)
261		{
262	41113	return !conj;
263		}
264		}
265	74601	return conj;
266		}
267	44489	else if (n.isConst())
268		{
269	27042	return (polarity && n == d_true) \|\| (!polarity && n == d_false);
270		}
271	43079	return false;
272		}
273
274	28056	bool SolverState::isSetDisequalityEntailed(Node r1, Node r2) const
275		{
276	28056	Assert(d_ee->hasTerm(r1) && d_ee->getRepresentative(r1) == r1);
277	28056	Assert(d_ee->hasTerm(r2) && d_ee->getRepresentative(r2) == r2);
278	56112	TypeNode tn = r1.getType();
279	56112	Node re = getEmptySetEqClass(tn);
280	34849	for (unsigned e = 0; e < 2; e++)
281		{
282	40154	Node a = e == 0 ? r1 : r2;
283	40154	Node b = e == 0 ? r2 : r1;
284	33361	if (isSetDisequalityEntailedInternal(a, b, re))
285		{
286	26568	return true;
287		}
288		}
289	1488	return false;
290		}
291
292	33361	bool SolverState::isSetDisequalityEntailedInternal(Node a,
293		Node b,
294		Node re) const
295		{
296		// if there are members in a
297		std::map<Node, std::map<Node, Node> >::const_iterator itpma =
298	33361	d_pol_mems[0].find(a);
299	33361	if (itpma == d_pol_mems[0].end())
300		{
301		// no positive members, continue
302	3653	return false;
303		}
304		// if b is empty
305	29708	if (b == re)
306		{
307	5655	if (!itpma->second.empty())
308		{
309	11310	Trace("sets-deq") << "Disequality is satisfied because members are in "
310	5655	<< a << " and " << b << " is empty" << std::endl;
311	5655	return true;
312		}
313		else
314		{
315		// a should not be singleton
316		Assert(d_eqc_singleton.find(a) == d_eqc_singleton.end());
317		}
318		return false;
319		}
320	24053	std::map<Node, Node>::const_iterator itsb = d_eqc_singleton.find(b);
321		std::map<Node, std::map<Node, Node> >::const_iterator itpmb =
322	24053	d_pol_mems[1].find(b);
323	48106	std::vector<Node> prev;
324	36984	for (const std::pair<const Node, Node>& itm : itpma->second)
325		{
326		// if b is a singleton
327	33844	if (itsb != d_eqc_singleton.end())
328		{
329	18429	if (areDisequal(itm.first, itsb->second[0]))
330		{
331	34478	Trace("sets-deq") << "Disequality is satisfied because of "
332	34478	<< itm.second << ", singleton eq " << itsb->second[0]
333	17239	<< std::endl;
334	38152	return true;
335		}
336		// or disequal with another member
337	1283	for (const Node& p : prev)
338		{
339	104	if (areDisequal(itm.first, p))
340		{
341	22	Trace("sets-deq")
342	11	<< "Disequality is satisfied because of disequal members "
343	11	<< itm.first << " " << p << ", singleton eq " << std::endl;
344	11	return true;
345		}
346		}
347		// if a has positive member that is negative member in b
348		}
349	15415	else if (itpmb != d_pol_mems[1].end())
350		{
351	33276	for (const std::pair<const Node, Node>& itnm : itpmb->second)
352		{
353	24997	if (areEqual(itm.first, itnm.first))
354		{
355	7326	Trace("sets-deq") << "Disequality is satisfied because of "
356	3663	<< itm.second << " " << itnm.second << std::endl;
357	3663	return true;
358		}
359		}
360		}
361	12931	prev.push_back(itm.first);
362		}
363	3140	return false;
364		}
365
366		Node SolverState::getCongruent(Node n) const
367		{
368		Assert(d_ee->hasTerm(n));
369		std::map<Node, Node>::const_iterator it = d_congruent.find(n);
370		if (it == d_congruent.end())
371		{
372		return n;
373		}
374		return it->second;
375		}
376	159636	bool SolverState::isCongruent(Node n) const
377		{
378	159636	return d_congruent.find(n) != d_congruent.end();
379		}
380	118269	const std::vector<Node>& SolverState::getNonVariableSets(Node r) const
381		{
382	118269	std::map<Node, std::vector<Node> >::const_iterator it = d_nvar_sets.find(r);
383	118269	if (it == d_nvar_sets.end())
384		{
385	19223	return d_emptyVec;
386		}
387	99046	return it->second;
388		}
389
390	38445	Node SolverState::getVariableSet(Node r) const
391		{
392	38445	std::map<Node, Node>::const_iterator it = d_var_set.find(r);
393	38445	if (it != d_var_set.end())
394		{
395	8374	return it->second;
396		}
397	30071	return Node::null();
398		}
399
400		const std::vector<Node>& SolverState::getComprehensionSets(Node r) const
401		{
402		std::map<Node, std::vector<Node> >::const_iterator it = d_compSets.find(r);
403		if (it == d_compSets.end())
404		{
405		return d_emptyVec;
406		}
407		return it->second;
408		}
409
410	197208	const std::map<Node, Node>& SolverState::getMembers(Node r) const
411		{
412	197208	return getMembersInternal(r, 0);
413		}
414	57011	const std::map<Node, Node>& SolverState::getNegativeMembers(Node r) const
415		{
416	57011	return getMembersInternal(r, 1);
417		}
418	254219	const std::map<Node, Node>& SolverState::getMembersInternal(Node r,
419		unsigned i) const
420		{
421		std::map<Node, std::map<Node, Node> >::const_iterator itp =
422	254219	d_pol_mems[i].find(r);
423	254219	if (itp == d_pol_mems[i].end())
424		{
425	57856	return d_emptyMap;
426		}
427	196363	return itp->second;
428		}
429
430	1354	bool SolverState::hasMembers(Node r) const
431		{
432		std::map<Node, std::map<Node, Node> >::const_iterator it =
433	1354	d_pol_mems[0].find(r);
434	1354	if (it == d_pol_mems[0].end())
435		{
436	460	return false;
437		}
438	894	return !it->second.empty();
439		}
440		const std::map<Kind, std::map<Node, std::map<Node, Node> > >&
441	22763	SolverState::getBinaryOpIndex() const
442		{
443	22763	return d_bop_index;
444		}
445
446		const std::map<Node, std::map<Node, Node>>& SolverState::getBinaryOpIndex(
447		Kind k)
448		{
449		return d_bop_index[k];
450		}
451
452	8788	const std::map<Kind, std::vector<Node> >& SolverState::getOperatorList() const
453		{
454	8788	return d_op_list;
455		}
456
457	20743	const std::vector<Node>& SolverState::getComprehensionSets() const
458		{
459	20743	return d_allCompSets;
460		}
461
462	1263	const vector<Node> SolverState::getSetsEqClasses(const TypeNode& t) const
463		{
464	1263	vector<Node> representatives;
465	16436	for (const Node& eqc : getSetsEqClasses())
466		{
467	15173	if (eqc.getType().getSetElementType() == t)
468		{
469	15173	representatives.push_back(eqc);
470		}
471		}
472	1263	return representatives;
473		}
474
475	148619	bool SolverState::isMember(TNode x, TNode s) const
476		{
477	148619	Assert(hasTerm(s) && getRepresentative(s) == s);
478	148619	NodeIntMap::const_iterator mem_i = d_members.find(s);
479	148619	if (mem_i != d_members.end())
480		{
481		std::map<Node, std::vector<Node> >::const_iterator itd =
482	139649	d_members_data.find(s);
483	139649	Assert(itd != d_members_data.end());
484	139649	const std::vector<Node>& members = itd->second;
485	139649	Assert((*mem_i).second <= members.size());
486	803084	for (size_t i = 0, nmem = (*mem_i).second; i < nmem; i++)
487		{
488	783567	if (areEqual(members[i][0], x))
489		{
490	120132	return true;
491		}
492		}
493		}
494	28487	return false;
495		}
496
497	188565	void SolverState::addMember(TNode r, TNode atom)
498		{
499	188565	NodeIntMap::iterator mem_i = d_members.find(r);
500	188565	size_t n_members = 0;
501	188565	if (mem_i != d_members.end())
502		{
503	162215	n_members = (*mem_i).second;
504		}
505	188565	d_members[r] = n_members + 1;
506	188565	if (n_members < d_members_data[r].size())
507		{
508	176606	d_members_data[r][n_members] = atom;
509		}
510		else
511		{
512	11959	d_members_data[r].push_back(atom);
513		}
514	188565	}
515
516	51713	bool SolverState::merge(TNode t1,
517		TNode t2,
518		std::vector<Node>& facts,
519		TNode cset)
520		{
521	51713	NodeIntMap::iterator mem_i2 = d_members.find(t2);
522	51713	if (mem_i2 == d_members.end())
523		{
524		// no members in t2, we are done
525	27637	return true;
526		}
527	24076	NodeIntMap::iterator mem_i1 = d_members.find(t1);
528	24076	size_t n_members = 0;
529	24076	if (mem_i1 != d_members.end())
530		{
531	23288	n_members = (*mem_i1).second;
532		}
533	63136	for (size_t i = 0, nmem2 = (*mem_i2).second; i < nmem2; i++)
534		{
535	39273	Assert(i < d_members_data[t2].size()
536		&& d_members_data[t2][i].getKind() == MEMBER);
537	78333	Node m2 = d_members_data[t2][i];
538		// check if redundant
539	39273	bool add = true;
540	67339	for (size_t j = 0; j < n_members; j++)
541		{
542	63281	Assert(j < d_members_data[t1].size()
543		&& d_members_data[t1][j].getKind() == MEMBER);
544	63281	if (areEqual(m2[0], d_members_data[t1][j][0]))
545		{
546	35215	add = false;
547	35215	break;
548		}
549		}
550	39273	if (add)
551		{
552		// if there is a concrete set in t1, propagate new facts or conflicts
553	4058	if (!cset.isNull())
554		{
555	1147	NodeManager* nm = NodeManager::currentNM();
556	1147	Assert(areEqual(m2[1], cset));
557	2081	Node exp = nm->mkNode(AND, m2[1].eqNode(cset), m2);
558	1147	if (cset.getKind() == SINGLETON)
559		{
560	934	if (cset[0] != m2[0])
561		{
562	1868	Node eq = cset[0].eqNode(m2[0]);
563	1868	Trace("sets-prop") << "Propagate eq-mem eq inference : " << exp
564	934	<< " => " << eq << std::endl;
565	1868	Node fact = nm->mkNode(IMPLIES, exp, eq);
566	934	facts.push_back(fact);
567		}
568		}
569		else
570		{
571		// conflict
572	213	Assert(facts.empty());
573	426	Trace("sets-prop")
574	213	<< "Propagate eq-mem conflict : " << exp << std::endl;
575	213	facts.push_back(exp);
576	213	return false;
577		}
578		}
579	3845	if (n_members < d_members_data[t1].size())
580		{
581	3392	d_members_data[t1][n_members] = m2;
582		}
583		else
584		{
585	453	d_members_data[t1].push_back(m2);
586		}
587	3845	n_members++;
588		}
589		}
590	23863	d_members[t1] = n_members;
591	23863	return true;
592		}
593
594		} // namespace sets
595		} // namespace theory
596	31137	} // namespace cvc5