Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/relevant_domain.cpp	Lines:	199	202	98.5 %
Date:	2021-05-21	Branches:	490	906	54.1 %


/******************************************************************************
 * 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 "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(QuantifiersState& qs,
                               QuantifiersRegistry& qr,
                               TermRegistry& tr)
    : 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, icf, true, true );
    }

    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, Node n, bool hasPol, bool pol ) {
  Trace("rel-dom-debug") << "Compute relevant domain " << n << "..." << std::endl;
  Node op = d_treg.getTermDatabase()->getMatchOperator(n);
  for( unsigned i=0; i<n.getNumChildren(); i++ ){
    if( !op.isNull() ){
      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] );
      }
    }
    // do not recurse under nested closures
    if (!n[i].isClosure())
    {
      bool newHasPol;
      bool newPol;
      QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
      computeRelevantDomain( q, n[i], newHasPol, newPol );
    }
  }

  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 "theory/arith/arith_msum.h"
19		#include "theory/quantifiers/first_order_model.h"
20		#include "theory/quantifiers/quantifiers_registry.h"
21		#include "theory/quantifiers/quantifiers_state.h"
22		#include "theory/quantifiers/term_database.h"
23		#include "theory/quantifiers/term_registry.h"
24		#include "theory/quantifiers/term_util.h"
25
26		using namespace cvc5::kind;
27
28		namespace cvc5 {
29		namespace theory {
30		namespace quantifiers {
31
32	13833	void RelevantDomain::RDomain::merge( RDomain * r ) {
33	13833	Assert(!d_parent);
34	13833	Assert(!r->d_parent);
35	13833	d_parent = r;
36	15323	for( unsigned i=0; i<d_terms.size(); i++ ){
37	1490	r->addTerm( d_terms[i] );
38		}
39	13833	d_terms.clear();
40	13833	}
41
42	22337	void RelevantDomain::RDomain::addTerm( Node t ) {
43	22337	if( std::find( d_terms.begin(), d_terms.end(), t )==d_terms.end() ){
44	3780	d_terms.push_back( t );
45		}
46	22337	}
47
48	462189	RelevantDomain::RDomain * RelevantDomain::RDomain::getParent() {
49	462189	if( !d_parent ){
50	224082	return this;
51		}else{
52	238107	RDomain * p = d_parent->getParent();
53	238107	d_parent = p;
54	238107	return p;
55		}
56		}
57
58	946	void RelevantDomain::RDomain::removeRedundantTerms(QuantifiersState& qs)
59		{
60	1892	std::map< Node, Node > rterms;
61	3236	for( unsigned i=0; i<d_terms.size(); i++ ){
62	4580	Node r = d_terms[i];
63	2290	if( !TermUtil::hasInstConstAttr( d_terms[i] ) ){
64	2290	r = qs.getRepresentative(d_terms[i]);
65		}
66	2290	if( rterms.find( r )==rterms.end() ){
67	1926	rterms[r] = d_terms[i];
68		}
69		}
70	946	d_terms.clear();
71	2872	for( std::map< Node, Node >::iterator it = rterms.begin(); it != rterms.end(); ++it ){
72	1926	d_terms.push_back( it->second );
73		}
74	946	}
75
76	79	RelevantDomain::RelevantDomain(QuantifiersState& qs,
77		QuantifiersRegistry& qr,
78	79	TermRegistry& tr)
79	79	: d_qs(qs), d_qreg(qr), d_treg(tr)
80		{
81	79	d_is_computed = false;
82	79	}
83
84	237	RelevantDomain::~RelevantDomain() {
85	805	for( std::map< Node, std::map< int, RDomain * > >::iterator itr = d_rel_doms.begin(); itr != d_rel_doms.end(); ++itr ){
86	5858	for( std::map< int, RDomain * >::iterator itr2 = itr->second.begin(); itr2 != itr->second.end(); ++itr2 ){
87	5132	RDomain * current = (*itr2).second;
88	5132	Assert(current != NULL);
89	5132	delete current;
90		}
91		}
92	158	}
93
94	208726	RelevantDomain::RDomain * RelevantDomain::getRDomain( Node n, int i, bool getParent ) {
95	208726	if( d_rel_doms.find( n )==d_rel_doms.end() \|\| d_rel_doms[n].find( i )==d_rel_doms[n].end() ){
96	5132	d_rel_doms[n][i] = new RDomain;
97	5132	d_rn_map[d_rel_doms[n][i]] = n;
98	5132	d_ri_map[d_rel_doms[n][i]] = i;
99		}
100	208726	return getParent ? d_rel_doms[n][i]->getParent() : d_rel_doms[n][i];
101		}
102
103	1073	bool RelevantDomain::reset( Theory::Effort e ) {
104	1073	d_is_computed = false;
105	1073	return true;
106		}
107
108	3692	void RelevantDomain::registerQuantifier(Node q) {}
109	118	void RelevantDomain::compute(){
110	118	if( !d_is_computed ){
111	118	d_is_computed = true;
112	1612	for( std::map< Node, std::map< int, RDomain * > >::iterator it = d_rel_doms.begin(); it != d_rel_doms.end(); ++it ){
113	11177	for( std::map< int, RDomain * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
114	9683	it2->second->reset();
115		}
116		}
117	118	FirstOrderModel* fm = d_treg.getModel();
118	1638	for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
119	3040	Node q = fm->getAssertedQuantifier( i );
120	3040	Node icf = d_qreg.getInstConstantBody(q);
121	1520	Trace("rel-dom-debug") << "compute relevant domain for " << icf << std::endl;
122	1520	computeRelevantDomain( q, icf, true, true );
123		}
124
125	118	Trace("rel-dom-debug") << "account for ground terms" << std::endl;
126	118	TermDb* db = d_treg.getTermDatabase();
127	767	for (unsigned k = 0; k < db->getNumOperators(); k++)
128		{
129	1298	Node op = db->getOperator(k);
130	649	unsigned sz = db->getNumGroundTerms( op );
131	9550	for( unsigned i=0; i<sz; i++ ){
132	17802	Node n = db->getGroundTerm(op, i);
133		//if it is a non-redundant term
134	8901	if( db->isTermActive( n ) ){
135	24097	for( unsigned j=0; j<n.getNumChildren(); j++ ){
136	18135	RDomain * rf = getRDomain( op, j );
137	18135	rf->addTerm( n[j] );
138	18135	Trace("rel-dom-debug") << "...add ground term " << n[j] << " to rel dom " << op << "[" << j << "]" << std::endl;
139		}
140		}
141		}
142		}
143		//print debug
144	2324	for( std::map< Node, std::map< int, RDomain * > >::iterator it = d_rel_doms.begin(); it != d_rel_doms.end(); ++it ){
145	2206	Trace("rel-dom") << "Relevant domain for " << it->first << " : " << std::endl;
146	16985	for( std::map< int, RDomain * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
147	14779	Trace("rel-dom") << " " << it2->first << " : ";
148	14779	RDomain * r = it2->second;
149	14779	RDomain * rp = r->getParent();
150	14779	if( r==rp ){
151	946	r->removeRedundantTerms(d_qs);
152	2872	for( unsigned i=0; i<r->d_terms.size(); i++ ){
153	1926	Trace("rel-dom") << r->d_terms[i] << " ";
154		}
155		}else{
156	13833	Trace("rel-dom") << "Dom( " << d_rn_map[rp] << ", " << d_ri_map[rp] << " ) ";
157		}
158	14779	Trace("rel-dom") << std::endl;
159		}
160		}
161		}
162	118	}
163
164	106196	void RelevantDomain::computeRelevantDomain( Node q, Node n, bool hasPol, bool pol ) {
165	106196	Trace("rel-dom-debug") << "Compute relevant domain " << n << "..." << std::endl;
166	212392	Node op = d_treg.getTermDatabase()->getMatchOperator(n);
167	211061	for( unsigned i=0; i<n.getNumChildren(); i++ ){
168	104865	if( !op.isNull() ){
169	81416	RDomain * rf = getRDomain( op, i );
170	81416	if( n[i].getKind()==ITE ){
171		for( unsigned j=1; j<=2; j++ ){
172		computeRelevantDomainOpCh( rf, n[i][j] );
173		}
174		}else{
175	81416	computeRelevantDomainOpCh( rf, n[i] );
176		}
177		}
178		// do not recurse under nested closures
179	104865	if (!n[i].isClosure())
180		{
181		bool newHasPol;
182		bool newPol;
183	104676	QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
184	104676	computeRelevantDomain( q, n[i], newHasPol, newPol );
185		}
186		}
187
188	106196	if( ( ( n.getKind()==EQUAL && !n[0].getType().isBoolean() ) \|\| n.getKind()==GEQ ) && TermUtil::hasInstConstAttr( n ) ){
189		//compute the information for what this literal does
190	1240	computeRelevantDomainLit( q, hasPol, pol, n );
191	1240	if( d_rel_dom_lit[hasPol][pol][n].d_merge ){
192	148	Assert(d_rel_dom_lit[hasPol][pol][n].d_rd[0] != NULL
193		&& d_rel_dom_lit[hasPol][pol][n].d_rd[1] != NULL);
194	148	RDomain * rd1 = d_rel_dom_lit[hasPol][pol][n].d_rd[0]->getParent();
195	148	RDomain * rd2 = d_rel_dom_lit[hasPol][pol][n].d_rd[1]->getParent();
196	148	if( rd1!=rd2 ){
197	145	rd1->merge( rd2 );
198		}
199		}else{
200	1092	if( d_rel_dom_lit[hasPol][pol][n].d_rd[0]!=NULL ){
201	556	RDomain * rd = d_rel_dom_lit[hasPol][pol][n].d_rd[0]->getParent();
202	1109	for( unsigned i=0; i<d_rel_dom_lit[hasPol][pol][n].d_val.size(); i++ ){
203	553	rd->addTerm( d_rel_dom_lit[hasPol][pol][n].d_val[i] );
204		}
205		}
206		}
207		}
208	106196	Trace("rel-dom-debug") << "...finished Compute relevant domain " << n << std::endl;
209	106196	}
210
211	81416	void RelevantDomain::computeRelevantDomainOpCh( RDomain * rf, Node n ) {
212	81416	if( n.getKind()==INST_CONSTANT ){
213	157496	Node q = TermUtil::getInstConstAttr(n);
214		//merge the RDomains
215	78748	unsigned id = n.getAttribute(InstVarNumAttribute());
216	78748	Assert(q[0][id].getType() == n.getType());
217	78748	Trace("rel-dom-debug") << n << " is variable # " << id << " for " << q;
218	157496	Trace("rel-dom-debug") << " with body : " << d_qreg.getInstConstantBody(q)
219	78748	<< std::endl;
220	78748	RDomain * rq = getRDomain( q, id );
221	78748	if( rf!=rq ){
222	13688	rq->merge( rf );
223		}
224	2668	}else if( !TermUtil::hasInstConstAttr( n ) ){
225	2159	Trace("rel-dom-debug") << "...add ground term to rel dom " << n << std::endl;
226		//term to add
227	2159	rf->addTerm( n );
228		}
229	81416	}
230
231	1240	void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, Node n ) {
232	1240	if( d_rel_dom_lit[hasPol][pol].find( n )==d_rel_dom_lit[hasPol][pol].end() ){
233	416	d_rel_dom_lit[hasPol][pol][n].d_merge = false;
234	416	int varCount = 0;
235	416	int varCh = -1;
236	1248	for( unsigned i=0; i<n.getNumChildren(); i++ ){
237	832	if( n[i].getKind()==INST_CONSTANT ){
238		// must get the quantified formula this belongs to, which may be
239		// different from q
240	508	Node qi = TermUtil::getInstConstAttr(n[i]);
241	254	unsigned id = n[i].getAttribute(InstVarNumAttribute());
242	254	d_rel_dom_lit[hasPol][pol][n].d_rd[i] = getRDomain(qi, id, false);
243	254	varCount++;
244	254	varCh = i;
245		}else{
246	578	d_rel_dom_lit[hasPol][pol][n].d_rd[i] = NULL;
247		}
248		}
249
250	832	Node r_add;
251	416	bool varLhs = true;
252	416	if( varCount==2 ){
253	18	d_rel_dom_lit[hasPol][pol][n].d_merge = true;
254		}else{
255	398	if( varCount==1 ){
256	218	r_add = n[1-varCh];
257	218	varLhs = (varCh==0);
258	218	d_rel_dom_lit[hasPol][pol][n].d_rd[0] = d_rel_dom_lit[hasPol][pol][n].d_rd[varCh];
259	218	d_rel_dom_lit[hasPol][pol][n].d_rd[1] = NULL;
260		}else{
261		//solve the inequality for one/two variables, if possible
262	180	if( n[0].getType().isReal() ){
263	246	std::map< Node, Node > msum;
264	123	if (ArithMSum::getMonomialSumLit(n, msum))
265		{
266	246	Node var;
267	246	Node var2;
268	123	bool hasNonVar = false;
269	368	for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
270	722	if (!it->first.isNull() && it->first.getKind() == INST_CONSTANT
271	545	&& TermUtil::getInstConstAttr(it->first) == q)
272		{
273	55	if( var.isNull() ){
274	33	var = it->first;
275	22	}else if( var2.isNull() ){
276	22	var2 = it->first;
277		}else{
278		hasNonVar = true;
279		}
280		}else{
281	190	hasNonVar = true;
282		}
283		}
284	123	if( !var.isNull() ){
285	33	if( var2.isNull() ){
286		//single variable solve
287	22	Node veq_c;
288	22	Node val;
289		int ires =
290	11	ArithMSum::isolate(var, msum, veq_c, val, n.getKind());
291	11	if( ires!=0 ){
292	11	if( veq_c.isNull() ){
293	3	r_add = val;
294	3	varLhs = (ires==1);
295	3	d_rel_dom_lit[hasPol][pol][n].d_rd[0] = getRDomain( q, var.getAttribute(InstVarNumAttribute()), false );
296	3	d_rel_dom_lit[hasPol][pol][n].d_rd[1] = NULL;
297		}
298		}
299	22	}else if( !hasNonVar ){
300		//merge the domains
301	9	d_rel_dom_lit[hasPol][pol][n].d_rd[0] = getRDomain( q, var.getAttribute(InstVarNumAttribute()), false );
302	9	d_rel_dom_lit[hasPol][pol][n].d_rd[1] = getRDomain( q, var2.getAttribute(InstVarNumAttribute()), false );
303	9	d_rel_dom_lit[hasPol][pol][n].d_merge = true;
304		}
305		}
306		}
307		}
308		}
309		}
310	416	if( d_rel_dom_lit[hasPol][pol][n].d_merge ){
311		//do not merge if constant negative polarity
312	27	if( hasPol && !pol ){
313	9	d_rel_dom_lit[hasPol][pol][n].d_merge = false;
314		}
315	389	}else if( !r_add.isNull() && !TermUtil::hasInstConstAttr( r_add ) ){
316	204	Trace("rel-dom-debug") << "...add term " << r_add << ", pol = " << pol << ", kind = " << n.getKind() << std::endl;
317		//the negative occurrence adds the term to the domain
318	204	if( !hasPol \|\| !pol ){
319	170	d_rel_dom_lit[hasPol][pol][n].d_val.push_back( r_add );
320		}
321		//the positive occurence adds other terms
322	204	if( ( !hasPol \|\| pol ) && n[0].getType().isInteger() ){
323	36	if( n.getKind()==EQUAL ){
324	12	for( unsigned i=0; i<2; i++ ){
325	16	d_rel_dom_lit[hasPol][pol][n].d_val.push_back(
326	16	ArithMSum::offset(r_add, i == 0 ? 1 : -1));
327		}
328	32	}else if( n.getKind()==GEQ ){
329	64	d_rel_dom_lit[hasPol][pol][n].d_val.push_back(
330	64	ArithMSum::offset(r_add, varLhs ? 1 : -1));
331		}
332		}
333		}else{
334	185	d_rel_dom_lit[hasPol][pol][n].d_rd[0] = NULL;
335	185	d_rel_dom_lit[hasPol][pol][n].d_rd[1] = NULL;
336		}
337		}
338	1240	}
339
340		} // namespace quantifiers
341		} // namespace theory
342	27735	} // namespace cvc5