Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/relevant_domain.cpp	Lines:	215	222	96.8 %
Date:	2021-09-14	Branches:	492	952	51.7 %


/******************************************************************************
 * 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( std::map< Node, std::map< int, RDomain * > >::iterator itr = d_rel_doms.begin(); itr != d_rel_doms.end(); ++itr ){
    for( std::map< int, RDomain * >::iterator itr2 = itr->second.begin(); itr2 != itr->second.end(); ++itr2 ){
      RDomain * current = (*itr2).second;
      Assert(current != NULL);
      delete current;
    }
  }
}

RelevantDomain::RDomain * RelevantDomain::getRDomain( Node n, int 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;
    d_rn_map[d_rel_doms[n][i]] = n;
    d_ri_map[d_rel_doms[n][i]] = i;
  }
  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( std::map< Node, std::map< int, RDomain * > >::iterator it = d_rel_doms.begin(); it != d_rel_doms.end(); ++it ){
      for( std::map< int, RDomain * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
        it2->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::map< Node, std::map< int, RDomain * > >::iterator it = d_rel_doms.begin(); it != d_rel_doms.end(); ++it ){
      Trace("rel-dom") << "Relevant domain for " << it->first << " : " << std::endl;
      for( std::map< int, RDomain * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
        Trace("rel-dom") << "   " << it2->first << " : ";
        RDomain * r = it2->second;
        RDomain * rp = r->getParent();
        if( r==rp ){
          r->removeRedundantTerms(d_qs);
          for( unsigned i=0; i<r->d_terms.size(); i++ ){
            Trace("rel-dom") << r->d_terms[i] << " ";
          }
        }else{
          Trace("rel-dom") << "Dom( " << d_rn_map[rp] << ", " << d_ri_map[rp] << " ) ";
        }
        Trace("rel-dom") << std::endl;
      }
    }
  }
}

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);
  if (!op.isNull())
  {
    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 );
    if( d_rel_dom_lit[hasPol][pol][n].d_merge ){
      Assert(d_rel_dom_lit[hasPol][pol][n].d_rd[0] != NULL
             && d_rel_dom_lit[hasPol][pol][n].d_rd[1] != NULL);
      RDomain * rd1 = d_rel_dom_lit[hasPol][pol][n].d_rd[0]->getParent();
      RDomain * rd2 = d_rel_dom_lit[hasPol][pol][n].d_rd[1]->getParent();
      if( rd1!=rd2 ){
        rd1->merge( rd2 );
      }
    }else{
      if( d_rel_dom_lit[hasPol][pol][n].d_rd[0]!=NULL ){
        RDomain * rd = d_rel_dom_lit[hasPol][pol][n].d_rd[0]->getParent();
        for( unsigned i=0; i<d_rel_dom_lit[hasPol][pol][n].d_val.size(); i++ ){
          rd->addTerm( d_rel_dom_lit[hasPol][pol][n].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
    unsigned 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() ){
    d_rel_dom_lit[hasPol][pol][n].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());
        d_rel_dom_lit[hasPol][pol][n].d_rd[i] = getRDomain(qi, id, false);
        varCount++;
        varCh = i;
      }else{
        d_rel_dom_lit[hasPol][pol][n].d_rd[i] = NULL;
      }
    }

    Node r_add;
    bool varLhs = true;
    if( varCount==2 ){
      d_rel_dom_lit[hasPol][pol][n].d_merge = true;
    }else{
      if( varCount==1 ){
        r_add = n[1-varCh];
        varLhs = (varCh==0);
        d_rel_dom_lit[hasPol][pol][n].d_rd[0] = d_rel_dom_lit[hasPol][pol][n].d_rd[varCh];
        d_rel_dom_lit[hasPol][pol][n].d_rd[1] = NULL;
      }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;
              }
            }
            if( !var.isNull() ){
              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);
                    d_rel_dom_lit[hasPol][pol][n].d_rd[0] = getRDomain( q, var.getAttribute(InstVarNumAttribute()), false );
                    d_rel_dom_lit[hasPol][pol][n].d_rd[1] = NULL;
                  }
                }
              }else if( !hasNonVar ){
                //merge the domains
                d_rel_dom_lit[hasPol][pol][n].d_rd[0] = getRDomain( q, var.getAttribute(InstVarNumAttribute()), false );
                d_rel_dom_lit[hasPol][pol][n].d_rd[1] = getRDomain( q, var2.getAttribute(InstVarNumAttribute()), false );
                d_rel_dom_lit[hasPol][pol][n].d_merge = true;
              }
            }
          }
        }
      }
    }
    if( d_rel_dom_lit[hasPol][pol][n].d_merge ){
      //do not merge if constant negative polarity
      if( hasPol && !pol ){
        d_rel_dom_lit[hasPol][pol][n].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 ){
        d_rel_dom_lit[hasPol][pol][n].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++ ){
            d_rel_dom_lit[hasPol][pol][n].d_val.push_back(
                ArithMSum::offset(r_add, i == 0 ? 1 : -1));
          }
        }else if( n.getKind()==GEQ ){
          d_rel_dom_lit[hasPol][pol][n].d_val.push_back(
              ArithMSum::offset(r_add, varLhs ? 1 : -1));
        }
      }
    }else{
      d_rel_dom_lit[hasPol][pol][n].d_rd[0] = NULL;
      d_rel_dom_lit[hasPol][pol][n].d_rd[1] = NULL;
    }
  }
}

}  // 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	13348	void RelevantDomain::RDomain::merge( RDomain * r ) {
35	13348	Assert(!d_parent);
36	13348	Assert(!r->d_parent);
37	13348	d_parent = r;
38	13977	for( unsigned i=0; i<d_terms.size(); i++ ){
39	629	r->addTerm( d_terms[i] );
40		}
41	13348	d_terms.clear();
42	13348	}
43
44	12683	void RelevantDomain::RDomain::addTerm( Node t ) {
45	12683	if( std::find( d_terms.begin(), d_terms.end(), t )==d_terms.end() ){
46	2020	d_terms.push_back( t );
47		}
48	12683	}
49
50	419911	RelevantDomain::RDomain * RelevantDomain::RDomain::getParent() {
51	419911	if( !d_parent ){
52	208300	return this;
53		}else{
54	211611	RDomain * p = d_parent->getParent();
55	211611	d_parent = p;
56	211611	return p;
57		}
58		}
59
60	764	void RelevantDomain::RDomain::removeRedundantTerms(QuantifiersState& qs)
61		{
62	1528	std::map< Node, Node > rterms;
63	2155	for( unsigned i=0; i<d_terms.size(); i++ ){
64	2782	Node r = d_terms[i];
65	1391	if( !TermUtil::hasInstConstAttr( d_terms[i] ) ){
66	1391	r = qs.getRepresentative(d_terms[i]);
67		}
68	1391	if( rterms.find( r )==rterms.end() ){
69	1274	rterms[r] = d_terms[i];
70		}
71		}
72	764	d_terms.clear();
73	2038	for( std::map< Node, Node >::iterator it = rterms.begin(); it != rterms.end(); ++it ){
74	1274	d_terms.push_back( it->second );
75		}
76	764	}
77
78	98	RelevantDomain::RelevantDomain(Env& env,
79		QuantifiersState& qs,
80		QuantifiersRegistry& qr,
81	98	TermRegistry& tr)
82	98	: QuantifiersUtil(env), d_qs(qs), d_qreg(qr), d_treg(tr)
83		{
84	98	d_is_computed = false;
85	98	}
86
87	294	RelevantDomain::~RelevantDomain() {
88	829	for( std::map< Node, std::map< int, RDomain * > >::iterator itr = d_rel_doms.begin(); itr != d_rel_doms.end(); ++itr ){
89	5892	for( std::map< int, RDomain * >::iterator itr2 = itr->second.begin(); itr2 != itr->second.end(); ++itr2 ){
90	5161	RDomain * current = (*itr2).second;
91	5161	Assert(current != NULL);
92	5161	delete current;
93		}
94		}
95	196	}
96
97	193961	RelevantDomain::RDomain * RelevantDomain::getRDomain( Node n, int i, bool getParent ) {
98	193961	if( d_rel_doms.find( n )==d_rel_doms.end() \|\| d_rel_doms[n].find( i )==d_rel_doms[n].end() ){
99	5161	d_rel_doms[n][i] = new RDomain;
100	5161	d_rn_map[d_rel_doms[n][i]] = n;
101	5161	d_ri_map[d_rel_doms[n][i]] = i;
102		}
103	193961	return getParent ? d_rel_doms[n][i]->getParent() : d_rel_doms[n][i];
104		}
105
106	1185	bool RelevantDomain::reset( Theory::Effort e ) {
107	1185	d_is_computed = false;
108	1185	return true;
109		}
110
111	3732	void RelevantDomain::registerQuantifier(Node q) {}
112	112	void RelevantDomain::compute(){
113	112	if( !d_is_computed ){
114	112	d_is_computed = true;
115	1155	for( std::map< Node, std::map< int, RDomain * > >::iterator it = d_rel_doms.begin(); it != d_rel_doms.end(); ++it ){
116	10037	for( std::map< int, RDomain * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
117	8994	it2->second->reset();
118		}
119		}
120	112	FirstOrderModel* fm = d_treg.getModel();
121	1191	for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
122	2158	Node q = fm->getAssertedQuantifier( i );
123	2158	Node icf = d_qreg.getInstConstantBody(q);
124	1079	Trace("rel-dom-debug") << "compute relevant domain for " << icf << std::endl;
125	1079	computeRelevantDomain(q);
126		}
127
128	112	Trace("rel-dom-debug") << "account for ground terms" << std::endl;
129	112	TermDb* db = d_treg.getTermDatabase();
130	763	for (unsigned k = 0; k < db->getNumOperators(); k++)
131		{
132	1302	Node op = db->getOperator(k);
133	651	unsigned sz = db->getNumGroundTerms( op );
134	3297	for( unsigned i=0; i<sz; i++ ){
135	5292	Node n = db->getGroundTerm(op, i);
136		//if it is a non-redundant term
137	2646	if( db->isTermActive( n ) ){
138	13122	for( unsigned j=0; j<n.getNumChildren(); j++ ){
139	11137	RDomain * rf = getRDomain( op, j );
140	11137	rf->addTerm( n[j] );
141	11137	Trace("rel-dom-debug") << "...add ground term " << n[j] << " to rel dom " << op << "[" << j << "]" << std::endl;
142		}
143		}
144		}
145		}
146		//print debug
147	1867	for( std::map< Node, std::map< int, RDomain * > >::iterator it = d_rel_doms.begin(); it != d_rel_doms.end(); ++it ){
148	1755	Trace("rel-dom") << "Relevant domain for " << it->first << " : " << std::endl;
149	15867	for( std::map< int, RDomain * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
150	14112	Trace("rel-dom") << " " << it2->first << " : ";
151	14112	RDomain * r = it2->second;
152	14112	RDomain * rp = r->getParent();
153	14112	if( r==rp ){
154	764	r->removeRedundantTerms(d_qs);
155	2038	for( unsigned i=0; i<r->d_terms.size(); i++ ){
156	1274	Trace("rel-dom") << r->d_terms[i] << " ";
157		}
158		}else{
159	13348	Trace("rel-dom") << "Dom( " << d_rn_map[rp] << ", " << d_ri_map[rp] << " ) ";
160		}
161	14112	Trace("rel-dom") << std::endl;
162		}
163		}
164		}
165	112	}
166
167	1079	void RelevantDomain::computeRelevantDomain(Node q)
168		{
169	1079	Assert(q.getKind() == FORALL);
170	2158	Node n = d_qreg.getInstConstantBody(q);
171		// we care about polarity in the traversal, so we use a polarity term context
172	2158	PolarityTermContext tc;
173	2158	TCtxStack ctx(&tc);
174	1079	ctx.pushInitial(n);
175		std::unordered_set<std::pair<Node, uint32_t>,
176		PairHashFunction<Node, uint32_t, std::hash<Node> > >
177	2158	visited;
178	2158	std::pair<Node, uint32_t> curr;
179	2158	Node node;
180		uint32_t nodeVal;
181		std::unordered_set<
182		std::pair<Node, uint32_t>,
183	1079	PairHashFunction<Node, uint32_t, std::hash<Node> > >::const_iterator itc;
184		bool hasPol, pol;
185	202293	while (!ctx.empty())
186		{
187	100607	curr = ctx.getCurrent();
188	100607	itc = visited.find(curr);
189	100607	ctx.pop();
190	100607	if (itc == visited.end())
191		{
192	31278	visited.insert(curr);
193	31278	node = curr.first;
194		// if not a quantified formula
195	31278	if (!node.isClosure())
196		{
197	31179	nodeVal = curr.second;
198		// get the polarity of the current term and process it
199	31179	PolarityTermContext::getFlags(nodeVal, hasPol, pol);
200	31179	computeRelevantDomainNode(q, node, hasPol, pol);
201		// traverse the children
202	31179	ctx.pushChildren(node, nodeVal);
203		}
204		}
205		}
206	1079	}
207
208	31179	void RelevantDomain::computeRelevantDomainNode(Node q,
209		Node n,
210		bool hasPol,
211		bool pol)
212		{
213	31179	Trace("rel-dom-debug") << "Compute relevant domain " << n << "..." << std::endl;
214	62358	Node op = d_treg.getTermDatabase()->getMatchOperator(n);
215	31179	if (!op.isNull())
216		{
217	89077	for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
218		{
219	78683	RDomain * rf = getRDomain( op, i );
220	78683	if( n[i].getKind()==ITE ){
221		for( unsigned j=1; j<=2; j++ ){
222		computeRelevantDomainOpCh( rf, n[i][j] );
223		}
224		}else{
225	78683	computeRelevantDomainOpCh( rf, n[i] );
226		}
227		}
228		}
229
230	31179	if( ( ( n.getKind()==EQUAL && !n[0].getType().isBoolean() ) \|\| n.getKind()==GEQ ) && TermUtil::hasInstConstAttr( n ) ){
231		//compute the information for what this literal does
232	676	computeRelevantDomainLit( q, hasPol, pol, n );
233	676	if( d_rel_dom_lit[hasPol][pol][n].d_merge ){
234	112	Assert(d_rel_dom_lit[hasPol][pol][n].d_rd[0] != NULL
235		&& d_rel_dom_lit[hasPol][pol][n].d_rd[1] != NULL);
236	112	RDomain * rd1 = d_rel_dom_lit[hasPol][pol][n].d_rd[0]->getParent();
237	112	RDomain * rd2 = d_rel_dom_lit[hasPol][pol][n].d_rd[1]->getParent();
238	112	if( rd1!=rd2 ){
239	73	rd1->merge( rd2 );
240		}
241		}else{
242	564	if( d_rel_dom_lit[hasPol][pol][n].d_rd[0]!=NULL ){
243	234	RDomain * rd = d_rel_dom_lit[hasPol][pol][n].d_rd[0]->getParent();
244	610	for( unsigned i=0; i<d_rel_dom_lit[hasPol][pol][n].d_val.size(); i++ ){
245	376	rd->addTerm( d_rel_dom_lit[hasPol][pol][n].d_val[i] );
246		}
247		}
248		}
249		}
250	31179	Trace("rel-dom-debug") << "...finished Compute relevant domain " << n << std::endl;
251	31179	}
252
253	78683	void RelevantDomain::computeRelevantDomainOpCh( RDomain * rf, Node n ) {
254	78683	if( n.getKind()==INST_CONSTANT ){
255	155584	Node q = TermUtil::getInstConstAttr(n);
256		//merge the RDomains
257	77792	unsigned id = n.getAttribute(InstVarNumAttribute());
258	77792	Assert(q[0][id].getType() == n.getType());
259	77792	Trace("rel-dom-debug") << n << " is variable # " << id << " for " << q;
260	155584	Trace("rel-dom-debug") << " with body : " << d_qreg.getInstConstantBody(q)
261	77792	<< std::endl;
262	77792	RDomain * rq = getRDomain( q, id );
263	77792	if( rf!=rq ){
264	13275	rq->merge( rf );
265		}
266	891	}else if( !TermUtil::hasInstConstAttr( n ) ){
267	541	Trace("rel-dom-debug") << "...add ground term to rel dom " << n << std::endl;
268		//term to add
269	541	rf->addTerm( n );
270		}
271	78683	}
272
273	676	void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, Node n ) {
274	676	if( d_rel_dom_lit[hasPol][pol].find( n )==d_rel_dom_lit[hasPol][pol].end() ){
275	359	d_rel_dom_lit[hasPol][pol][n].d_merge = false;
276	359	int varCount = 0;
277	359	int varCh = -1;
278	1077	for( unsigned i=0; i<n.getNumChildren(); i++ ){
279	718	if( n[i].getKind()==INST_CONSTANT ){
280		// must get the quantified formula this belongs to, which may be
281		// different from q
282	420	Node qi = TermUtil::getInstConstAttr(n[i]);
283	210	unsigned id = n[i].getAttribute(InstVarNumAttribute());
284	210	d_rel_dom_lit[hasPol][pol][n].d_rd[i] = getRDomain(qi, id, false);
285	210	varCount++;
286	210	varCh = i;
287		}else{
288	508	d_rel_dom_lit[hasPol][pol][n].d_rd[i] = NULL;
289		}
290		}
291
292	718	Node r_add;
293	359	bool varLhs = true;
294	359	if( varCount==2 ){
295	15	d_rel_dom_lit[hasPol][pol][n].d_merge = true;
296		}else{
297	344	if( varCount==1 ){
298	180	r_add = n[1-varCh];
299	180	varLhs = (varCh==0);
300	180	d_rel_dom_lit[hasPol][pol][n].d_rd[0] = d_rel_dom_lit[hasPol][pol][n].d_rd[varCh];
301	180	d_rel_dom_lit[hasPol][pol][n].d_rd[1] = NULL;
302		}else{
303		//solve the inequality for one/two variables, if possible
304	164	if( n[0].getType().isReal() ){
305	262	std::map< Node, Node > msum;
306	131	if (ArithMSum::getMonomialSumLit(n, msum))
307		{
308	262	Node var;
309	262	Node var2;
310	131	bool hasNonVar = false;
311	392	for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
312	762	if (!it->first.isNull() && it->first.getKind() == INST_CONSTANT
313	577	&& TermUtil::getInstConstAttr(it->first) == q)
314		{
315	55	if( var.isNull() ){
316	33	var = it->first;
317	22	}else if( var2.isNull() ){
318	22	var2 = it->first;
319		}else{
320		hasNonVar = true;
321		}
322		}else{
323	206	hasNonVar = true;
324		}
325		}
326	131	if( !var.isNull() ){
327	33	if( var2.isNull() ){
328		//single variable solve
329	22	Node veq_c;
330	22	Node val;
331		int ires =
332	11	ArithMSum::isolate(var, msum, veq_c, val, n.getKind());
333	11	if( ires!=0 ){
334	11	if( veq_c.isNull() ){
335	3	r_add = val;
336	3	varLhs = (ires==1);
337	3	d_rel_dom_lit[hasPol][pol][n].d_rd[0] = getRDomain( q, var.getAttribute(InstVarNumAttribute()), false );
338	3	d_rel_dom_lit[hasPol][pol][n].d_rd[1] = NULL;
339		}
340		}
341	22	}else if( !hasNonVar ){
342		//merge the domains
343	9	d_rel_dom_lit[hasPol][pol][n].d_rd[0] = getRDomain( q, var.getAttribute(InstVarNumAttribute()), false );
344	9	d_rel_dom_lit[hasPol][pol][n].d_rd[1] = getRDomain( q, var2.getAttribute(InstVarNumAttribute()), false );
345	9	d_rel_dom_lit[hasPol][pol][n].d_merge = true;
346		}
347		}
348		}
349		}
350		}
351		}
352	359	if( d_rel_dom_lit[hasPol][pol][n].d_merge ){
353		//do not merge if constant negative polarity
354	24	if( hasPol && !pol ){
355		d_rel_dom_lit[hasPol][pol][n].d_merge = false;
356		}
357	335	}else if( !r_add.isNull() && !TermUtil::hasInstConstAttr( r_add ) ){
358	164	Trace("rel-dom-debug") << "...add term " << r_add << ", pol = " << pol << ", kind = " << n.getKind() << std::endl;
359		//the negative occurrence adds the term to the domain
360	164	if( !hasPol \|\| !pol ){
361	164	d_rel_dom_lit[hasPol][pol][n].d_val.push_back( r_add );
362		}
363		//the positive occurence adds other terms
364	164	if( ( !hasPol \|\| pol ) && n[0].getType().isInteger() ){
365	138	if( n.getKind()==EQUAL ){
366		for( unsigned i=0; i<2; i++ ){
367		d_rel_dom_lit[hasPol][pol][n].d_val.push_back(
368		ArithMSum::offset(r_add, i == 0 ? 1 : -1));
369		}
370	138	}else if( n.getKind()==GEQ ){
371	276	d_rel_dom_lit[hasPol][pol][n].d_val.push_back(
372	276	ArithMSum::offset(r_add, varLhs ? 1 : -1));
373		}
374		}
375		}else{
376	171	d_rel_dom_lit[hasPol][pol][n].d_rd[0] = NULL;
377	171	d_rel_dom_lit[hasPol][pol][n].d_rd[1] = NULL;
378		}
379		}
380	676	}
381
382		} // namespace quantifiers
383		} // namespace theory
384	29517	} // namespace cvc5