Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/relevant_domain.cpp	Lines:	226	234	96.6 %
Date:	2021-11-07	Branches:	452	894	50.6 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Mathias Preiner, Aina Niemetz
 *
 * 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 relevant domain class.
 */

#include "theory/quantifiers/relevant_domain.h"

#include "expr/term_context.h"
#include "expr/term_context_stack.h"
#include "theory/arith/arith_msum.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/quantifiers_registry.h"
#include "theory/quantifiers/quantifiers_state.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_registry.h"
#include "theory/quantifiers/term_util.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace quantifiers {

void RelevantDomain::RDomain::merge( RDomain * r ) {
  Assert(!d_parent);
  Assert(!r->d_parent);
  d_parent = r;
  for( unsigned i=0; i<d_terms.size(); i++ ){
    r->addTerm( d_terms[i] );
  }
  d_terms.clear();
}

void RelevantDomain::RDomain::addTerm( Node t ) {
  if( std::find( d_terms.begin(), d_terms.end(), t )==d_terms.end() ){
    d_terms.push_back( t );
  }
}

RelevantDomain::RDomain * RelevantDomain::RDomain::getParent() {
  if( !d_parent ){
    return this;
  }else{
    RDomain * p = d_parent->getParent();
    d_parent = p;
    return p;
  }
}

void RelevantDomain::RDomain::removeRedundantTerms(QuantifiersState& qs)
{
  std::map< Node, Node > rterms;
  for( unsigned i=0; i<d_terms.size(); i++ ){
    Node r = d_terms[i];
    if( !TermUtil::hasInstConstAttr( d_terms[i] ) ){
      r = qs.getRepresentative(d_terms[i]);
    }
    if( rterms.find( r )==rterms.end() ){
      rterms[r] = d_terms[i];
    }
  }
  d_terms.clear();
  for( std::map< Node, Node >::iterator it = rterms.begin(); it != rterms.end(); ++it ){
    d_terms.push_back( it->second );
  }
}

RelevantDomain::RelevantDomain(Env& env,
                               QuantifiersState& qs,
                               QuantifiersRegistry& qr,
                               TermRegistry& tr)
    : QuantifiersUtil(env), d_qs(qs), d_qreg(qr), d_treg(tr)
{
  d_is_computed = false;
}

RelevantDomain::~RelevantDomain() {
  for (auto& r : d_rel_doms)
  {
    for (auto& rr : r.second)
    {
      RDomain* current = rr.second;
      Assert(current != NULL);
      delete current;
    }
  }
}

RelevantDomain::RDomain* RelevantDomain::getRDomain(Node n,
                                                    size_t i,
                                                    bool getParent)
{
  if( d_rel_doms.find( n )==d_rel_doms.end() || d_rel_doms[n].find( i )==d_rel_doms[n].end() ){
    d_rel_doms[n][i] = new RDomain;
  }
  return getParent ? d_rel_doms[n][i]->getParent() : d_rel_doms[n][i];
}

bool RelevantDomain::reset( Theory::Effort e ) {
  d_is_computed = false;
  return true;
}

void RelevantDomain::registerQuantifier(Node q) {}
void RelevantDomain::compute(){
  if( !d_is_computed ){
    d_is_computed = true;
    for (auto& r : d_rel_doms)
    {
      for (auto& rr : r.second)
      {
        rr.second->reset();
      }
    }
    FirstOrderModel* fm = d_treg.getModel();
    for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
      Node q = fm->getAssertedQuantifier( i );
      Node icf = d_qreg.getInstConstantBody(q);
      Trace("rel-dom-debug") << "compute relevant domain for " << icf << std::endl;
      computeRelevantDomain(q);
    }

    Trace("rel-dom-debug") << "account for ground terms" << std::endl;
    TermDb* db = d_treg.getTermDatabase();
    for (unsigned k = 0; k < db->getNumOperators(); k++)
    {
      Node op = db->getOperator(k);
      unsigned sz = db->getNumGroundTerms( op );
      for( unsigned i=0; i<sz; i++ ){
        Node n = db->getGroundTerm(op, i);
        //if it is a non-redundant term
        if( db->isTermActive( n ) ){
          for( unsigned j=0; j<n.getNumChildren(); j++ ){
            RDomain * rf = getRDomain( op, j );
            rf->addTerm( n[j] );
            Trace("rel-dom-debug") << "...add ground term " << n[j] << " to rel dom " << op << "[" << j << "]" << std::endl;
          }
        }
      }
    }
    //print debug
    for (std::pair<const Node, std::map<size_t, RDomain*> >& d : d_rel_doms)
    {
      Trace("rel-dom") << "Relevant domain for " << d.first << " : "
                       << std::endl;
      for (std::pair<const size_t, RDomain*>& dd : d.second)
      {
        Trace("rel-dom") << "   " << dd.first << " : ";
        RDomain* r = dd.second;
        RDomain * rp = r->getParent();
        if( r==rp ){
          r->removeRedundantTerms(d_qs);
          Trace("rel-dom") << r->d_terms;
        }else{
          Trace("rel-dom") << "Dom( " << d.first << ", " << dd.first << " ) ";
        }
        Trace("rel-dom") << std::endl;
        if (Configuration::isAssertionBuild())
        {
          if (d.first.getKind() == FORALL)
          {
            TypeNode expectedType = d.first[0][dd.first].getType();
            for (const Node& t : r->d_terms)
            {
              if (!t.getType().isComparableTo(expectedType))
              {
                Unhandled() << "Relevant domain: bad type " << t.getType()
                            << ", expected " << expectedType;
              }
            }
          }
        }
      }
    }
  }
}

void RelevantDomain::computeRelevantDomain(Node q)
{
  Assert(q.getKind() == FORALL);
  Node n = d_qreg.getInstConstantBody(q);
  // we care about polarity in the traversal, so we use a polarity term context
  PolarityTermContext tc;
  TCtxStack ctx(&tc);
  ctx.pushInitial(n);
  std::unordered_set<std::pair<Node, uint32_t>,
                     PairHashFunction<Node, uint32_t, std::hash<Node> > >
      visited;
  std::pair<Node, uint32_t> curr;
  Node node;
  uint32_t nodeVal;
  std::unordered_set<
      std::pair<Node, uint32_t>,
      PairHashFunction<Node, uint32_t, std::hash<Node> > >::const_iterator itc;
  bool hasPol, pol;
  while (!ctx.empty())
  {
    curr = ctx.getCurrent();
    itc = visited.find(curr);
    ctx.pop();
    if (itc == visited.end())
    {
      visited.insert(curr);
      node = curr.first;
      // if not a quantified formula
      if (!node.isClosure())
      {
        nodeVal = curr.second;
        // get the polarity of the current term and process it
        PolarityTermContext::getFlags(nodeVal, hasPol, pol);
        computeRelevantDomainNode(q, node, hasPol, pol);
        // traverse the children
        ctx.pushChildren(node, nodeVal);
      }
    }
  }
}

void RelevantDomain::computeRelevantDomainNode(Node q,
                                               Node n,
                                               bool hasPol,
                                               bool pol)
{
  Trace("rel-dom-debug") << "Compute relevant domain " << n << "..." << std::endl;
  Node op = d_treg.getTermDatabase()->getMatchOperator(n);
  // Relevant domain only makes sense for non-parametric operators, thus we
  // check op==n.getOperator() here. This otherwise would lead to bad types
  // for terms in the relevant domain.
  if (!op.isNull() && op == n.getOperator())
  {
    for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
    {
      RDomain * rf = getRDomain( op, i );
      if( n[i].getKind()==ITE ){
        for( unsigned j=1; j<=2; j++ ){
          computeRelevantDomainOpCh( rf, n[i][j] );
        }
      }else{
        computeRelevantDomainOpCh( rf, n[i] );
      }
    }
  }

  if( ( ( n.getKind()==EQUAL && !n[0].getType().isBoolean() ) || n.getKind()==GEQ ) && TermUtil::hasInstConstAttr( n ) ){
    //compute the information for what this literal does
    computeRelevantDomainLit( q, hasPol, pol, n );
    RDomainLit& rdl = d_rel_dom_lit[hasPol][pol][n];
    if (rdl.d_merge)
    {
      Assert(rdl.d_rd[0] != nullptr && rdl.d_rd[1] != nullptr);
      RDomain* rd1 = rdl.d_rd[0]->getParent();
      RDomain* rd2 = rdl.d_rd[1]->getParent();
      if( rd1!=rd2 ){
        rd1->merge( rd2 );
      }
    }
    else
    {
      if (rdl.d_rd[0] != nullptr)
      {
        RDomain* rd = rdl.d_rd[0]->getParent();
        for (unsigned i = 0; i < rdl.d_val.size(); i++)
        {
          rd->addTerm(rdl.d_val[i]);
        }
      }
    }
  }
  Trace("rel-dom-debug") << "...finished Compute relevant domain " << n << std::endl;
}

void RelevantDomain::computeRelevantDomainOpCh( RDomain * rf, Node n ) {
  if( n.getKind()==INST_CONSTANT ){
    Node q = TermUtil::getInstConstAttr(n);
    //merge the RDomains
    size_t id = n.getAttribute(InstVarNumAttribute());
    Assert(q[0][id].getType() == n.getType());
    Trace("rel-dom-debug") << n << " is variable # " << id << " for " << q;
    Trace("rel-dom-debug") << " with body : " << d_qreg.getInstConstantBody(q)
                           << std::endl;
    RDomain * rq = getRDomain( q, id );
    if( rf!=rq ){
      rq->merge( rf );
    }
  }else if( !TermUtil::hasInstConstAttr( n ) ){
    Trace("rel-dom-debug") << "...add ground term to rel dom " << n << std::endl;
    //term to add
    rf->addTerm( n );
  }
}

void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, Node n ) {
  if( d_rel_dom_lit[hasPol][pol].find( n )==d_rel_dom_lit[hasPol][pol].end() ){
    RDomainLit& rdl = d_rel_dom_lit[hasPol][pol][n];
    rdl.d_merge = false;
    int varCount = 0;
    int varCh = -1;
    for( unsigned i=0; i<n.getNumChildren(); i++ ){
      if( n[i].getKind()==INST_CONSTANT ){
        // must get the quantified formula this belongs to, which may be
        // different from q
        Node qi = TermUtil::getInstConstAttr(n[i]);
        unsigned id = n[i].getAttribute(InstVarNumAttribute());
        rdl.d_rd[i] = getRDomain(qi, id, false);
        varCount++;
        varCh = i;
      }else{
        rdl.d_rd[i] = nullptr;
      }
    }

    Node r_add;
    bool varLhs = true;
    if( varCount==2 ){
      rdl.d_merge = true;
    }else{
      if( varCount==1 ){
        r_add = n[1-varCh];
        varLhs = (varCh==0);
        rdl.d_rd[0] = rdl.d_rd[varCh];
        rdl.d_rd[1] = nullptr;
      }else{
        //solve the inequality for one/two variables, if possible
        if( n[0].getType().isReal() ){
          std::map< Node, Node > msum;
          if (ArithMSum::getMonomialSumLit(n, msum))
          {
            Node var;
            Node var2;
            bool hasNonVar = false;
            for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
              if (!it->first.isNull() && it->first.getKind() == INST_CONSTANT
                  && TermUtil::getInstConstAttr(it->first) == q)
              {
                if( var.isNull() ){
                  var = it->first;
                }else if( var2.isNull() ){
                  var2 = it->first;
                }else{
                  hasNonVar = true;
                }
              }else{
                hasNonVar = true;
              }
            }
            Trace("rel-dom") << "Process lit " << n << ", var/var2=" << var
                             << "/" << var2 << std::endl;
            if( !var.isNull() ){
              Assert(var.hasAttribute(InstVarNumAttribute()));
              if( var2.isNull() ){
                //single variable solve
                Node veq_c;
                Node val;
                int ires =
                    ArithMSum::isolate(var, msum, veq_c, val, n.getKind());
                if( ires!=0 ){
                  if( veq_c.isNull() ){
                    r_add = val;
                    varLhs = (ires==1);
                    rdl.d_rd[0] = getRDomain(
                        q, var.getAttribute(InstVarNumAttribute()), false);
                    rdl.d_rd[1] = nullptr;
                  }
                }
              }else if( !hasNonVar ){
                Assert(var2.hasAttribute(InstVarNumAttribute()));
                //merge the domains
                rdl.d_rd[0] = getRDomain(
                    q, var.getAttribute(InstVarNumAttribute()), false);
                rdl.d_rd[1] = getRDomain(
                    q, var2.getAttribute(InstVarNumAttribute()), false);
                rdl.d_merge = true;
              }
            }
          }
        }
      }
    }
    if (rdl.d_merge)
    {
      //do not merge if constant negative polarity
      if( hasPol && !pol ){
        rdl.d_merge = false;
      }
    }
    else if (!r_add.isNull() && !TermUtil::hasInstConstAttr(r_add))
    {
      Trace("rel-dom-debug") << "...add term " << r_add << ", pol = " << pol << ", kind = " << n.getKind() << std::endl;
      //the negative occurrence adds the term to the domain
      if( !hasPol || !pol ){
        rdl.d_val.push_back(r_add);
      }
      //the positive occurence adds other terms
      if( ( !hasPol || pol ) && n[0].getType().isInteger() ){
        if( n.getKind()==EQUAL ){
          for( unsigned i=0; i<2; i++ ){
            rdl.d_val.push_back(ArithMSum::offset(r_add, i == 0 ? 1 : -1));
          }
        }else if( n.getKind()==GEQ ){
          rdl.d_val.push_back(ArithMSum::offset(r_add, varLhs ? 1 : -1));
        }
      }
    }
    else
    {
      rdl.d_rd[0] = nullptr;
      rdl.d_rd[1] = nullptr;
    }
  }
}

}  // namespace quantifiers
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Mathias Preiner, Aina Niemetz
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 relevant domain class.
14		*/
15
16		#include "theory/quantifiers/relevant_domain.h"
17
18		#include "expr/term_context.h"
19		#include "expr/term_context_stack.h"
20		#include "theory/arith/arith_msum.h"
21		#include "theory/quantifiers/first_order_model.h"
22		#include "theory/quantifiers/quantifiers_registry.h"
23		#include "theory/quantifiers/quantifiers_state.h"
24		#include "theory/quantifiers/term_database.h"
25		#include "theory/quantifiers/term_registry.h"
26		#include "theory/quantifiers/term_util.h"
27
28		using namespace cvc5::kind;
29
30		namespace cvc5 {
31		namespace theory {
32		namespace quantifiers {
33
34	13575	void RelevantDomain::RDomain::merge( RDomain * r ) {
35	13575	Assert(!d_parent);
36	13575	Assert(!r->d_parent);
37	13575	d_parent = r;
38	14176	for( unsigned i=0; i<d_terms.size(); i++ ){
39	601	r->addTerm( d_terms[i] );
40		}
41	13575	d_terms.clear();
42	13575	}
43
44	16434	void RelevantDomain::RDomain::addTerm( Node t ) {
45	16434	if( std::find( d_terms.begin(), d_terms.end(), t )==d_terms.end() ){
46	2802	d_terms.push_back( t );
47		}
48	16434	}
49
50	428802	RelevantDomain::RDomain * RelevantDomain::RDomain::getParent() {
51	428802	if( !d_parent ){
52	214543	return this;
53		}else{
54	214259	RDomain * p = d_parent->getParent();
55	214259	d_parent = p;
56	214259	return p;
57		}
58		}
59
60	1090	void RelevantDomain::RDomain::removeRedundantTerms(QuantifiersState& qs)
61		{
62	2180	std::map< Node, Node > rterms;
63	3291	for( unsigned i=0; i<d_terms.size(); i++ ){
64	4402	Node r = d_terms[i];
65	2201	if( !TermUtil::hasInstConstAttr( d_terms[i] ) ){
66	2201	r = qs.getRepresentative(d_terms[i]);
67		}
68	2201	if( rterms.find( r )==rterms.end() ){
69	2002	rterms[r] = d_terms[i];
70		}
71		}
72	1090	d_terms.clear();
73	3092	for( std::map< Node, Node >::iterator it = rterms.begin(); it != rterms.end(); ++it ){
74	2002	d_terms.push_back( it->second );
75		}
76	1090	}
77
78	111	RelevantDomain::RelevantDomain(Env& env,
79		QuantifiersState& qs,
80		QuantifiersRegistry& qr,
81	111	TermRegistry& tr)
82	111	: QuantifiersUtil(env), d_qs(qs), d_qreg(qr), d_treg(tr)
83		{
84	111	d_is_computed = false;
85	111	}
86
87	333	RelevantDomain::~RelevantDomain() {
88	947	for (auto& r : d_rel_doms)
89		{
90	6159	for (auto& rr : r.second)
91		{
92	5323	RDomain* current = rr.second;
93	5323	Assert(current != NULL);
94	5323	delete current;
95		}
96		}
97	222	}
98
99	199504	RelevantDomain::RDomain* RelevantDomain::getRDomain(Node n,
100		size_t i,
101		bool getParent)
102		{
103	199504	if( d_rel_doms.find( n )==d_rel_doms.end() \|\| d_rel_doms[n].find( i )==d_rel_doms[n].end() ){
104	5323	d_rel_doms[n][i] = new RDomain;
105		}
106	199504	return getParent ? d_rel_doms[n][i]->getParent() : d_rel_doms[n][i];
107		}
108
109	1449	bool RelevantDomain::reset( Theory::Effort e ) {
110	1449	d_is_computed = false;
111	1449	return true;
112		}
113
114	3881	void RelevantDomain::registerQuantifier(Node q) {}
115	139	void RelevantDomain::compute(){
116	139	if( !d_is_computed ){
117	139	d_is_computed = true;
118	1440	for (auto& r : d_rel_doms)
119		{
120	10706	for (auto& rr : r.second)
121		{
122	9405	rr.second->reset();
123		}
124		}
125	139	FirstOrderModel* fm = d_treg.getModel();
126	1516	for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
127	2754	Node q = fm->getAssertedQuantifier( i );
128	2754	Node icf = d_qreg.getInstConstantBody(q);
129	1377	Trace("rel-dom-debug") << "compute relevant domain for " << icf << std::endl;
130	1377	computeRelevantDomain(q);
131		}
132
133	139	Trace("rel-dom-debug") << "account for ground terms" << std::endl;
134	139	TermDb* db = d_treg.getTermDatabase();
135	870	for (unsigned k = 0; k < db->getNumOperators(); k++)
136		{
137	1462	Node op = db->getOperator(k);
138	731	unsigned sz = db->getNumGroundTerms( op );
139	5878	for( unsigned i=0; i<sz; i++ ){
140	10294	Node n = db->getGroundTerm(op, i);
141		//if it is a non-redundant term
142	5147	if( db->isTermActive( n ) ){
143	17750	for( unsigned j=0; j<n.getNumChildren(); j++ ){
144	14207	RDomain * rf = getRDomain( op, j );
145	14207	rf->addTerm( n[j] );
146	14207	Trace("rel-dom-debug") << "...add ground term " << n[j] << " to rel dom " << op << "[" << j << "]" << std::endl;
147		}
148		}
149		}
150		}
151		//print debug
152	2245	for (std::pair<const Node, std::map<size_t, RDomain*> >& d : d_rel_doms)
153		{
154	4212	Trace("rel-dom") << "Relevant domain for " << d.first << " : "
155	2106	<< std::endl;
156	16771	for (std::pair<const size_t, RDomain*>& dd : d.second)
157		{
158	14665	Trace("rel-dom") << " " << dd.first << " : ";
159	14665	RDomain* r = dd.second;
160	14665	RDomain * rp = r->getParent();
161	14665	if( r==rp ){
162	1090	r->removeRedundantTerms(d_qs);
163	1090	Trace("rel-dom") << r->d_terms;
164		}else{
165	13575	Trace("rel-dom") << "Dom( " << d.first << ", " << dd.first << " ) ";
166		}
167	14665	Trace("rel-dom") << std::endl;
168	14665	if (Configuration::isAssertionBuild())
169		{
170	14665	if (d.first.getKind() == FORALL)
171		{
172	19622	TypeNode expectedType = d.first[0][dd.first].getType();
173	10106	for (const Node& t : r->d_terms)
174		{
175	295	if (!t.getType().isComparableTo(expectedType))
176		{
177		Unhandled() << "Relevant domain: bad type " << t.getType()
178		<< ", expected " << expectedType;
179		}
180		}
181		}
182		}
183		}
184		}
185		}
186	139	}
187
188	1377	void RelevantDomain::computeRelevantDomain(Node q)
189		{
190	1377	Assert(q.getKind() == FORALL);
191	2754	Node n = d_qreg.getInstConstantBody(q);
192		// we care about polarity in the traversal, so we use a polarity term context
193	2754	PolarityTermContext tc;
194	2754	TCtxStack ctx(&tc);
195	1377	ctx.pushInitial(n);
196		std::unordered_set<std::pair<Node, uint32_t>,
197		PairHashFunction<Node, uint32_t, std::hash<Node> > >
198	2754	visited;
199	2754	std::pair<Node, uint32_t> curr;
200	2754	Node node;
201		uint32_t nodeVal;
202		std::unordered_set<
203		std::pair<Node, uint32_t>,
204	1377	PairHashFunction<Node, uint32_t, std::hash<Node> > >::const_iterator itc;
205		bool hasPol, pol;
206	209069	while (!ctx.empty())
207		{
208	103846	curr = ctx.getCurrent();
209	103846	itc = visited.find(curr);
210	103846	ctx.pop();
211	103846	if (itc == visited.end())
212		{
213	33912	visited.insert(curr);
214	33912	node = curr.first;
215		// if not a quantified formula
216	33912	if (!node.isClosure())
217		{
218	33746	nodeVal = curr.second;
219		// get the polarity of the current term and process it
220	33746	PolarityTermContext::getFlags(nodeVal, hasPol, pol);
221	33746	computeRelevantDomainNode(q, node, hasPol, pol);
222		// traverse the children
223	33746	ctx.pushChildren(node, nodeVal);
224		}
225		}
226		}
227	1377	}
228
229	33746	void RelevantDomain::computeRelevantDomainNode(Node q,
230		Node n,
231		bool hasPol,
232		bool pol)
233		{
234	33746	Trace("rel-dom-debug") << "Compute relevant domain " << n << "..." << std::endl;
235	67492	Node op = d_treg.getTermDatabase()->getMatchOperator(n);
236		// Relevant domain only makes sense for non-parametric operators, thus we
237		// check op==n.getOperator() here. This otherwise would lead to bad types
238		// for terms in the relevant domain.
239	33746	if (!op.isNull() && op == n.getOperator())
240		{
241	90087	for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
242		{
243	79350	RDomain * rf = getRDomain( op, i );
244	79350	if( n[i].getKind()==ITE ){
245		for( unsigned j=1; j<=2; j++ ){
246		computeRelevantDomainOpCh( rf, n[i][j] );
247		}
248		}else{
249	79350	computeRelevantDomainOpCh( rf, n[i] );
250		}
251		}
252		}
253
254	33746	if( ( ( n.getKind()==EQUAL && !n[0].getType().isBoolean() ) \|\| n.getKind()==GEQ ) && TermUtil::hasInstConstAttr( n ) ){
255		//compute the information for what this literal does
256	991	computeRelevantDomainLit( q, hasPol, pol, n );
257	991	RDomainLit& rdl = d_rel_dom_lit[hasPol][pol][n];
258	991	if (rdl.d_merge)
259		{
260	148	Assert(rdl.d_rd[0] != nullptr && rdl.d_rd[1] != nullptr);
261	148	RDomain* rd1 = rdl.d_rd[0]->getParent();
262	148	RDomain* rd2 = rdl.d_rd[1]->getParent();
263	148	if( rd1!=rd2 ){
264	106	rd1->merge( rd2 );
265		}
266		}
267		else
268		{
269	843	if (rdl.d_rd[0] != nullptr)
270		{
271	373	RDomain* rd = rdl.d_rd[0]->getParent();
272	898	for (unsigned i = 0; i < rdl.d_val.size(); i++)
273		{
274	525	rd->addTerm(rdl.d_val[i]);
275		}
276		}
277		}
278		}
279	33746	Trace("rel-dom-debug") << "...finished Compute relevant domain " << n << std::endl;
280	33746	}
281
282	79350	void RelevantDomain::computeRelevantDomainOpCh( RDomain * rf, Node n ) {
283	79350	if( n.getKind()==INST_CONSTANT ){
284	155986	Node q = TermUtil::getInstConstAttr(n);
285		//merge the RDomains
286	77993	size_t id = n.getAttribute(InstVarNumAttribute());
287	77993	Assert(q[0][id].getType() == n.getType());
288	77993	Trace("rel-dom-debug") << n << " is variable # " << id << " for " << q;
289	155986	Trace("rel-dom-debug") << " with body : " << d_qreg.getInstConstantBody(q)
290	77993	<< std::endl;
291	77993	RDomain * rq = getRDomain( q, id );
292	77993	if( rf!=rq ){
293	13469	rq->merge( rf );
294		}
295	1357	}else if( !TermUtil::hasInstConstAttr( n ) ){
296	1101	Trace("rel-dom-debug") << "...add ground term to rel dom " << n << std::endl;
297		//term to add
298	1101	rf->addTerm( n );
299		}
300	79350	}
301
302	991	void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, Node n ) {
303	991	if( d_rel_dom_lit[hasPol][pol].find( n )==d_rel_dom_lit[hasPol][pol].end() ){
304	452	RDomainLit& rdl = d_rel_dom_lit[hasPol][pol][n];
305	452	rdl.d_merge = false;
306	452	int varCount = 0;
307	452	int varCh = -1;
308	1356	for( unsigned i=0; i<n.getNumChildren(); i++ ){
309	904	if( n[i].getKind()==INST_CONSTANT ){
310		// must get the quantified formula this belongs to, which may be
311		// different from q
312	534	Node qi = TermUtil::getInstConstAttr(n[i]);
313	267	unsigned id = n[i].getAttribute(InstVarNumAttribute());
314	267	rdl.d_rd[i] = getRDomain(qi, id, false);
315	267	varCount++;
316	267	varCh = i;
317		}else{
318	637	rdl.d_rd[i] = nullptr;
319		}
320		}
321
322	904	Node r_add;
323	452	bool varLhs = true;
324	452	if( varCount==2 ){
325	25	rdl.d_merge = true;
326		}else{
327	427	if( varCount==1 ){
328	217	r_add = n[1-varCh];
329	217	varLhs = (varCh==0);
330	217	rdl.d_rd[0] = rdl.d_rd[varCh];
331	217	rdl.d_rd[1] = nullptr;
332		}else{
333		//solve the inequality for one/two variables, if possible
334	210	if( n[0].getType().isReal() ){
335	302	std::map< Node, Node > msum;
336	151	if (ArithMSum::getMonomialSumLit(n, msum))
337		{
338	302	Node var;
339	302	Node var2;
340	151	bool hasNonVar = false;
341	460	for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
342	890	if (!it->first.isNull() && it->first.getKind() == INST_CONSTANT
343	681	&& TermUtil::getInstConstAttr(it->first) == q)
344		{
345	63	if( var.isNull() ){
346	41	var = it->first;
347	22	}else if( var2.isNull() ){
348	22	var2 = it->first;
349		}else{
350		hasNonVar = true;
351		}
352		}else{
353	246	hasNonVar = true;
354		}
355		}
356	302	Trace("rel-dom") << "Process lit " << n << ", var/var2=" << var
357	151	<< "/" << var2 << std::endl;
358	151	if( !var.isNull() ){
359	41	Assert(var.hasAttribute(InstVarNumAttribute()));
360	41	if( var2.isNull() ){
361		//single variable solve
362	38	Node veq_c;
363	38	Node val;
364		int ires =
365	19	ArithMSum::isolate(var, msum, veq_c, val, n.getKind());
366	19	if( ires!=0 ){
367	19	if( veq_c.isNull() ){
368	10	r_add = val;
369	10	varLhs = (ires==1);
370	10	rdl.d_rd[0] = getRDomain(
371	10	q, var.getAttribute(InstVarNumAttribute()), false);
372	10	rdl.d_rd[1] = nullptr;
373		}
374		}
375	22	}else if( !hasNonVar ){
376	9	Assert(var2.hasAttribute(InstVarNumAttribute()));
377		//merge the domains
378	9	rdl.d_rd[0] = getRDomain(
379	9	q, var.getAttribute(InstVarNumAttribute()), false);
380	9	rdl.d_rd[1] = getRDomain(
381	9	q, var2.getAttribute(InstVarNumAttribute()), false);
382	9	rdl.d_merge = true;
383		}
384		}
385		}
386		}
387		}
388		}
389	452	if (rdl.d_merge)
390		{
391		//do not merge if constant negative polarity
392	34	if( hasPol && !pol ){
393		rdl.d_merge = false;
394		}
395		}
396	418	else if (!r_add.isNull() && !TermUtil::hasInstConstAttr(r_add))
397		{
398	195	Trace("rel-dom-debug") << "...add term " << r_add << ", pol = " << pol << ", kind = " << n.getKind() << std::endl;
399		//the negative occurrence adds the term to the domain
400	195	if( !hasPol \|\| !pol ){
401	195	rdl.d_val.push_back(r_add);
402		}
403		//the positive occurence adds other terms
404	195	if( ( !hasPol \|\| pol ) && n[0].getType().isInteger() ){
405	143	if( n.getKind()==EQUAL ){
406		for( unsigned i=0; i<2; i++ ){
407		rdl.d_val.push_back(ArithMSum::offset(r_add, i == 0 ? 1 : -1));
408		}
409	143	}else if( n.getKind()==GEQ ){
410	143	rdl.d_val.push_back(ArithMSum::offset(r_add, varLhs ? 1 : -1));
411		}
412		}
413		}
414		else
415		{
416	223	rdl.d_rd[0] = nullptr;
417	223	rdl.d_rd[1] = nullptr;
418		}
419		}
420	991	}
421
422		} // namespace quantifiers
423		} // namespace theory
424	31137	} // namespace cvc5