Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/arith_static_learner.cpp	Lines:	136	156	87.2 %
Date:	2021-08-14	Branches:	376	905	41.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Tim King, Dejan Jovanovic, Andres Noetzli
 *
 * 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.
 * ****************************************************************************
 *
 * [[ Add one-line brief description here ]]
 *
 * [[ Add lengthier description here ]]
 * \todo document this file
 */

#include <vector>

#include "base/output.h"
#include "expr/node_algorithm.h"
#include "options/arith_options.h"
#include "smt/smt_statistics_registry.h"
#include "theory/arith/arith_static_learner.h"
#include "theory/arith/arith_utilities.h"
#include "theory/arith/normal_form.h"
#include "theory/rewriter.h"

using namespace std;
using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace arith {


ArithStaticLearner::ArithStaticLearner(context::Context* userContext) :
  d_minMap(userContext),
  d_maxMap(userContext),
  d_statistics()
{
}

ArithStaticLearner::~ArithStaticLearner(){
}

ArithStaticLearner::Statistics::Statistics()
    : d_iteMinMaxApplications(smtStatisticsRegistry().registerInt(
        "theory::arith::iteMinMaxApplications")),
      d_iteConstantApplications(smtStatisticsRegistry().registerInt(
          "theory::arith::iteConstantApplications"))
{
}

void ArithStaticLearner::staticLearning(TNode n, NodeBuilder& learned)
{
  vector<TNode> workList;
  workList.push_back(n);
  TNodeSet processed;

  //Contains an underapproximation of nodes that must hold.
  TNodeSet defTrue;

  defTrue.insert(n);

  while(!workList.empty()) {
    n = workList.back();

    bool unprocessedChildren = false;
    for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) {
      if(processed.find(*i) == processed.end()) {
        // unprocessed child
        workList.push_back(*i);
        unprocessedChildren = true;
      }
    }
    if(n.getKind() == AND && defTrue.find(n) != defTrue.end() ){
      for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) {
        defTrue.insert(*i);
      }
    }

    if(unprocessedChildren) {
      continue;
    }

    workList.pop_back();
    // has node n been processed in the meantime ?
    if(processed.find(n) != processed.end()) {
      continue;
    }
    processed.insert(n);

    process(n,learned, defTrue);

  }
}

void ArithStaticLearner::process(TNode n,
                                 NodeBuilder& learned,
                                 const TNodeSet& defTrue)
{
  Debug("arith::static") << "===================== looking at " << n << endl;

  switch(n.getKind()){
  case ITE:
    if (expr::hasBoundVar(n))
    {
      // Unsafe with non-ground ITEs; do nothing
      Debug("arith::static")
          << "(potentially) non-ground ITE, ignoring..." << endl;
      break;
    }

    if(n[0].getKind() != EQUAL &&
       isRelationOperator(n[0].getKind())  ){
      iteMinMax(n, learned);
    }

    if((d_minMap.find(n[1]) != d_minMap.end() && d_minMap.find(n[2]) != d_minMap.end()) ||
       (d_maxMap.find(n[1]) != d_maxMap.end() && d_maxMap.find(n[2]) != d_maxMap.end())) {
      iteConstant(n, learned);
    }
    break;

  case CONST_RATIONAL:
    // Mark constants as minmax
    d_minMap.insert(n, n.getConst<Rational>());
    d_maxMap.insert(n, n.getConst<Rational>());
    break;
  default: // Do nothing
    break;
  }
}

void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder& learned)
{
  Assert(n.getKind() == kind::ITE);
  Assert(n[0].getKind() != EQUAL);
  Assert(isRelationOperator(n[0].getKind()));

  TNode c = n[0];
  Kind k = oldSimplifiedKind(c);
  TNode t = n[1];
  TNode e = n[2];
  TNode cleft = (c.getKind() == NOT) ? c[0][0] : c[0];
  TNode cright = (c.getKind() == NOT) ? c[0][1] : c[1];

  if((t == cright) && (e == cleft)){
    TNode tmp = t;
    t = e;
    e = tmp;
    k = reverseRelationKind(k);
  }
  //(ite (< x y) x y)
  //(ite (x < y) x y)
  //(ite (x - y < 0) x y)
  // ----------------
  // (ite (x - y < -c) )

  if(t == cleft && e == cright){
    // t == cleft && e == cright
    Assert(t == cleft);
    Assert(e == cright);
    switch(k){
    case LT:   // (ite (< x y) x y)
    case LEQ: { // (ite (<= x y) x y)
      Node nLeqX = NodeBuilder(LEQ) << n << t;
      Node nLeqY = NodeBuilder(LEQ) << n << e;
      Debug("arith::static") << n << "is a min =>"  << nLeqX << nLeqY << endl;
      learned << nLeqX << nLeqY;
      ++(d_statistics.d_iteMinMaxApplications);
      break;
    }
    case GT: // (ite (> x y) x y)
    case GEQ: { // (ite (>= x y) x y)
      Node nGeqX = NodeBuilder(GEQ) << n << t;
      Node nGeqY = NodeBuilder(GEQ) << n << e;
      Debug("arith::static") << n << "is a max =>"  << nGeqX << nGeqY << endl;
      learned << nGeqX << nGeqY;
      ++(d_statistics.d_iteMinMaxApplications);
      break;
    }
    default: Unreachable();
    }
  }
}

void ArithStaticLearner::iteConstant(TNode n, NodeBuilder& learned)
{
  Assert(n.getKind() == ITE);

  Debug("arith::static") << "iteConstant(" << n << ")" << endl;

  if (d_minMap.find(n[1]) != d_minMap.end() && d_minMap.find(n[2]) != d_minMap.end()) {
    const DeltaRational& first = d_minMap[n[1]];
    const DeltaRational& second = d_minMap[n[2]];
    DeltaRational min = std::min(first, second);
    CDNodeToMinMaxMap::const_iterator minFind = d_minMap.find(n);
    if (minFind == d_minMap.end() || (*minFind).second < min) {
      d_minMap.insert(n, min);
      Node nGeqMin;
      if (min.getInfinitesimalPart() == 0) {
        nGeqMin = NodeBuilder(kind::GEQ)
                  << n << mkRationalNode(min.getNoninfinitesimalPart());
      } else {
        nGeqMin = NodeBuilder(kind::GT)
                  << n << mkRationalNode(min.getNoninfinitesimalPart());
      }
      learned << nGeqMin;
      Debug("arith::static") << n << " iteConstant"  << nGeqMin << endl;
      ++(d_statistics.d_iteConstantApplications);
    }
  }

  if (d_maxMap.find(n[1]) != d_maxMap.end() && d_maxMap.find(n[2]) != d_maxMap.end()) {
    const DeltaRational& first = d_maxMap[n[1]];
    const DeltaRational& second = d_maxMap[n[2]];
    DeltaRational max = std::max(first, second);
    CDNodeToMinMaxMap::const_iterator maxFind = d_maxMap.find(n);
    if (maxFind == d_maxMap.end() || (*maxFind).second > max) {
      d_maxMap.insert(n, max);
      Node nLeqMax;
      if (max.getInfinitesimalPart() == 0) {
        nLeqMax = NodeBuilder(kind::LEQ)
                  << n << mkRationalNode(max.getNoninfinitesimalPart());
      } else {
        nLeqMax = NodeBuilder(kind::LT)
                  << n << mkRationalNode(max.getNoninfinitesimalPart());
      }
      learned << nLeqMax;
      Debug("arith::static") << n << " iteConstant"  << nLeqMax << endl;
      ++(d_statistics.d_iteConstantApplications);
    }
  }
}

std::set<Node> listToSet(TNode l){
  std::set<Node> ret;
  while(l.getKind() == OR){
    Assert(l.getNumChildren() == 2);
    ret.insert(l[0]);
    l = l[1];
  }
  return ret;
}

void ArithStaticLearner::addBound(TNode n) {

  CDNodeToMinMaxMap::const_iterator minFind = d_minMap.find(n[0]);
  CDNodeToMinMaxMap::const_iterator maxFind = d_maxMap.find(n[0]);

  Rational constant = n[1].getConst<Rational>();
  DeltaRational bound = constant;

  switch(Kind k = n.getKind()) {
    case kind::LT: bound = DeltaRational(constant, -1); CVC5_FALLTHROUGH;
    case kind::LEQ:
      if (maxFind == d_maxMap.end() || (*maxFind).second > bound)
      {
        d_maxMap.insert(n[0], bound);
        Debug("arith::static") << "adding bound " << n << endl;
      }
      break;
    case kind::GT: bound = DeltaRational(constant, 1); CVC5_FALLTHROUGH;
    case kind::GEQ:
      if (minFind == d_minMap.end() || (*minFind).second < bound)
      {
        d_minMap.insert(n[0], bound);
        Debug("arith::static") << "adding bound " << n << endl;
      }
      break;
    default: Unhandled() << k; break;
  }
}

}  // namespace arith
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Tim King, Dejan Jovanovic, Andres Noetzli
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		* [[ Add one-line brief description here ]]
14		*
15		* [[ Add lengthier description here ]]
16		* \todo document this file
17		*/
18
19		#include <vector>
20
21		#include "base/output.h"
22		#include "expr/node_algorithm.h"
23		#include "options/arith_options.h"
24		#include "smt/smt_statistics_registry.h"
25		#include "theory/arith/arith_static_learner.h"
26		#include "theory/arith/arith_utilities.h"
27		#include "theory/arith/normal_form.h"
28		#include "theory/rewriter.h"
29
30		using namespace std;
31		using namespace cvc5::kind;
32
33		namespace cvc5 {
34		namespace theory {
35		namespace arith {
36
37
38	9853	ArithStaticLearner::ArithStaticLearner(context::Context* userContext) :
39		d_minMap(userContext),
40		d_maxMap(userContext),
41	9853	d_statistics()
42		{
43	9853	}
44
45	9853	ArithStaticLearner::~ArithStaticLearner(){
46	9853	}
47
48	9853	ArithStaticLearner::Statistics::Statistics()
49	9853	: d_iteMinMaxApplications(smtStatisticsRegistry().registerInt(
50	19706	"theory::arith::iteMinMaxApplications")),
51	9853	d_iteConstantApplications(smtStatisticsRegistry().registerInt(
52	19706	"theory::arith::iteConstantApplications"))
53		{
54	9853	}
55
56	105238	void ArithStaticLearner::staticLearning(TNode n, NodeBuilder& learned)
57		{
58	210476	vector<TNode> workList;
59	105238	workList.push_back(n);
60	210476	TNodeSet processed;
61
62		//Contains an underapproximation of nodes that must hold.
63	210476	TNodeSet defTrue;
64
65	105238	defTrue.insert(n);
66
67	6088400	while(!workList.empty()) {
68	2991581	n = workList.back();
69
70	2991581	bool unprocessedChildren = false;
71	9455023	for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) {
72	6463442	if(processed.find(*i) == processed.end()) {
73		// unprocessed child
74	1915216	workList.push_back(*i);
75	1915216	unprocessedChildren = true;
76		}
77		}
78	2991581	if(n.getKind() == AND && defTrue.find(n) != defTrue.end() ){
79	836210	for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) {
80	824682	defTrue.insert(*i);
81		}
82		}
83
84	2991581	if(unprocessedChildren) {
85	971127	continue;
86		}
87
88	2020454	workList.pop_back();
89		// has node n been processed in the meantime ?
90	2020454	if(processed.find(n) != processed.end()) {
91	24162	continue;
92		}
93	1996292	processed.insert(n);
94
95	1996292	process(n,learned, defTrue);
96
97		}
98	105238	}
99
100	1996292	void ArithStaticLearner::process(TNode n,
101		NodeBuilder& learned,
102		const TNodeSet& defTrue)
103		{
104	1996292	Debug("arith::static") << "===================== looking at " << n << endl;
105
106	1996292	switch(n.getKind()){
107	30664	case ITE:
108	30664	if (expr::hasBoundVar(n))
109		{
110		// Unsafe with non-ground ITEs; do nothing
111	9004	Debug("arith::static")
112	4502	<< "(potentially) non-ground ITE, ignoring..." << endl;
113	4502	break;
114		}
115
116	90158	if(n[0].getKind() != EQUAL &&
117	63996	isRelationOperator(n[0].getKind()) ){
118	1850	iteMinMax(n, learned);
119		}
120
121	78486	if((d_minMap.find(n[1]) != d_minMap.end() && d_minMap.find(n[2]) != d_minMap.end()) \|\|
122	51994	(d_maxMap.find(n[1]) != d_maxMap.end() && d_maxMap.find(n[2]) != d_maxMap.end())) {
123	1930	iteConstant(n, learned);
124		}
125	26162	break;
126
127	97832	case CONST_RATIONAL:
128		// Mark constants as minmax
129	97832	d_minMap.insert(n, n.getConst<Rational>());
130	97832	d_maxMap.insert(n, n.getConst<Rational>());
131	97832	break;
132	1867796	default: // Do nothing
133	1867796	break;
134		}
135	1996292	}
136
137	1850	void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder& learned)
138		{
139	1850	Assert(n.getKind() == kind::ITE);
140	1850	Assert(n[0].getKind() != EQUAL);
141	1850	Assert(isRelationOperator(n[0].getKind()));
142
143	3700	TNode c = n[0];
144	1850	Kind k = oldSimplifiedKind(c);
145	3700	TNode t = n[1];
146	3700	TNode e = n[2];
147	3700	TNode cleft = (c.getKind() == NOT) ? c[0][0] : c[0];
148	3700	TNode cright = (c.getKind() == NOT) ? c[0][1] : c[1];
149
150	1850	if((t == cright) && (e == cleft)){
151	42	TNode tmp = t;
152	21	t = e;
153	21	e = tmp;
154	21	k = reverseRelationKind(k);
155		}
156		//(ite (< x y) x y)
157		//(ite (x < y) x y)
158		//(ite (x - y < 0) x y)
159		// ----------------
160		// (ite (x - y < -c) )
161
162	1850	if(t == cleft && e == cright){
163		// t == cleft && e == cright
164	24	Assert(t == cleft);
165	24	Assert(e == cright);
166	24	switch(k){
167	21	case LT: // (ite (< x y) x y)
168		case LEQ: { // (ite (<= x y) x y)
169	42	Node nLeqX = NodeBuilder(LEQ) << n << t;
170	42	Node nLeqY = NodeBuilder(LEQ) << n << e;
171	21	Debug("arith::static") << n << "is a min =>" << nLeqX << nLeqY << endl;
172	21	learned << nLeqX << nLeqY;
173	21	++(d_statistics.d_iteMinMaxApplications);
174	21	break;
175		}
176	3	case GT: // (ite (> x y) x y)
177		case GEQ: { // (ite (>= x y) x y)
178	6	Node nGeqX = NodeBuilder(GEQ) << n << t;
179	6	Node nGeqY = NodeBuilder(GEQ) << n << e;
180	3	Debug("arith::static") << n << "is a max =>" << nGeqX << nGeqY << endl;
181	3	learned << nGeqX << nGeqY;
182	3	++(d_statistics.d_iteMinMaxApplications);
183	3	break;
184		}
185		default: Unreachable();
186		}
187		}
188	1850	}
189
190	1930	void ArithStaticLearner::iteConstant(TNode n, NodeBuilder& learned)
191		{
192	1930	Assert(n.getKind() == ITE);
193
194	1930	Debug("arith::static") << "iteConstant(" << n << ")" << endl;
195
196	1930	if (d_minMap.find(n[1]) != d_minMap.end() && d_minMap.find(n[2]) != d_minMap.end()) {
197	3860	const DeltaRational& first = d_minMap[n[1]];
198	3860	const DeltaRational& second = d_minMap[n[2]];
199	3860	DeltaRational min = std::min(first, second);
200	1930	CDNodeToMinMaxMap::const_iterator minFind = d_minMap.find(n);
201	1930	if (minFind == d_minMap.end() \|\| (*minFind).second < min) {
202	1608	d_minMap.insert(n, min);
203	3216	Node nGeqMin;
204	1608	if (min.getInfinitesimalPart() == 0) {
205	4824	nGeqMin = NodeBuilder(kind::GEQ)
206	3216	<< n << mkRationalNode(min.getNoninfinitesimalPart());
207		} else {
208		nGeqMin = NodeBuilder(kind::GT)
209		<< n << mkRationalNode(min.getNoninfinitesimalPart());
210		}
211	1608	learned << nGeqMin;
212	1608	Debug("arith::static") << n << " iteConstant" << nGeqMin << endl;
213	1608	++(d_statistics.d_iteConstantApplications);
214		}
215		}
216
217	1930	if (d_maxMap.find(n[1]) != d_maxMap.end() && d_maxMap.find(n[2]) != d_maxMap.end()) {
218	3552	const DeltaRational& first = d_maxMap[n[1]];
219	3552	const DeltaRational& second = d_maxMap[n[2]];
220	3552	DeltaRational max = std::max(first, second);
221	1776	CDNodeToMinMaxMap::const_iterator maxFind = d_maxMap.find(n);
222	1776	if (maxFind == d_maxMap.end() \|\| (*maxFind).second > max) {
223	1478	d_maxMap.insert(n, max);
224	2956	Node nLeqMax;
225	1478	if (max.getInfinitesimalPart() == 0) {
226	4434	nLeqMax = NodeBuilder(kind::LEQ)
227	2956	<< n << mkRationalNode(max.getNoninfinitesimalPart());
228		} else {
229		nLeqMax = NodeBuilder(kind::LT)
230		<< n << mkRationalNode(max.getNoninfinitesimalPart());
231		}
232	1478	learned << nLeqMax;
233	1478	Debug("arith::static") << n << " iteConstant" << nLeqMax << endl;
234	1478	++(d_statistics.d_iteConstantApplications);
235		}
236		}
237	1930	}
238
239		std::set<Node> listToSet(TNode l){
240		std::set<Node> ret;
241		while(l.getKind() == OR){
242		Assert(l.getNumChildren() == 2);
243		ret.insert(l[0]);
244		l = l[1];
245		}
246		return ret;
247		}
248
249	2503	void ArithStaticLearner::addBound(TNode n) {
250
251	2503	CDNodeToMinMaxMap::const_iterator minFind = d_minMap.find(n[0]);
252	2503	CDNodeToMinMaxMap::const_iterator maxFind = d_maxMap.find(n[0]);
253
254	5006	Rational constant = n[1].getConst<Rational>();
255	5006	DeltaRational bound = constant;
256
257	2503	switch(Kind k = n.getKind()) {
258		case kind::LT: bound = DeltaRational(constant, -1); CVC5_FALLTHROUGH;
259		case kind::LEQ:
260		if (maxFind == d_maxMap.end() \|\| (*maxFind).second > bound)
261		{
262		d_maxMap.insert(n[0], bound);
263		Debug("arith::static") << "adding bound " << n << endl;
264		}
265		break;
266		case kind::GT: bound = DeltaRational(constant, 1); CVC5_FALLTHROUGH;
267	2503	case kind::GEQ:
268	2503	if (minFind == d_minMap.end() \|\| (*minFind).second < bound)
269		{
270	2243	d_minMap.insert(n[0], bound);
271	2243	Debug("arith::static") << "adding bound " << n << endl;
272		}
273	2503	break;
274		default: Unhandled() << k; break;
275		}
276	2503	}
277
278		} // namespace arith
279		} // namespace theory
280	29340	} // namespace cvc5