Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bags/inference_generator.cpp	Lines:	139	154	90.3 %
Date:	2021-08-17	Branches:	301	930	32.4 %


/******************************************************************************
 * Top contributors (to current version):
 *   Mudathir Mohamed, Andrew Reynolds, Gereon Kremer
 *
 * 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.
 * ****************************************************************************
 *
 * Inference generator utility.
 */

#include "inference_generator.h"

#include "expr/attribute.h"
#include "expr/bound_var_manager.h"
#include "expr/skolem_manager.h"
#include "theory/bags/inference_manager.h"
#include "theory/bags/solver_state.h"
#include "theory/uf/equality_engine.h"
#include "util/rational.h"

namespace cvc5 {
namespace theory {
namespace bags {

InferenceGenerator::InferenceGenerator(SolverState* state, InferenceManager* im)
    : d_state(state), d_im(im)
{
  d_nm = NodeManager::currentNM();
  d_sm = d_nm->getSkolemManager();
  d_true = d_nm->mkConst(true);
  d_zero = d_nm->mkConst(Rational(0));
  d_one = d_nm->mkConst(Rational(1));
}

InferInfo InferenceGenerator::nonNegativeCount(Node n, Node e)
{
  Assert(n.getType().isBag());
  Assert(e.getType() == n.getType().getBagElementType());

  InferInfo inferInfo(d_im, InferenceId::BAG_NON_NEGATIVE_COUNT);
  Node count = d_nm->mkNode(kind::BAG_COUNT, e, n);

  Node gte = d_nm->mkNode(kind::GEQ, count, d_zero);
  inferInfo.d_conclusion = gte;
  return inferInfo;
}

InferInfo InferenceGenerator::mkBag(Node n, Node e)
{
  Assert(n.getKind() == kind::MK_BAG);
  Assert(e.getType() == n.getType().getBagElementType());

  if (n[0] == e)
  {
    // TODO issue #78: refactor this with BagRewriter
    // (=> true (= (bag.count e (bag e c)) c))
    InferInfo inferInfo(d_im, InferenceId::BAG_MK_BAG_SAME_ELEMENT);
    Node skolem = getSkolem(n, inferInfo);
    Node count = getMultiplicityTerm(e, skolem);
    inferInfo.d_conclusion = count.eqNode(n[1]);
    return inferInfo;
  }
  else
  {
    // (=>
    //   true
    //   (= (bag.count e (bag x c)) (ite (= e x) c 0)))
    InferInfo inferInfo(d_im, InferenceId::BAG_MK_BAG);
    Node skolem = getSkolem(n, inferInfo);
    Node count = getMultiplicityTerm(e, skolem);
    Node same = d_nm->mkNode(kind::EQUAL, n[0], e);
    Node ite = d_nm->mkNode(kind::ITE, same, n[1], d_zero);
    Node equal = count.eqNode(ite);
    inferInfo.d_conclusion = equal;
    return inferInfo;
  }
}

struct BagsDeqAttributeId
{
};
typedef expr::Attribute<BagsDeqAttributeId, Node> BagsDeqAttribute;

InferInfo InferenceGenerator::bagDisequality(Node n)
{
  Assert(n.getKind() == kind::EQUAL && n[0].getType().isBag());

  Node A = n[0];
  Node B = n[1];

  InferInfo inferInfo(d_im, InferenceId::BAG_DISEQUALITY);

  TypeNode elementType = A.getType().getBagElementType();
  BoundVarManager* bvm = d_nm->getBoundVarManager();
  Node element = bvm->mkBoundVar<BagsDeqAttribute>(n, elementType);
  Node skolem =
      d_sm->mkSkolem(element,
                     n,
                     "bag_disequal",
                     "an extensional lemma for disequality of two bags");

  Node countA = getMultiplicityTerm(skolem, A);
  Node countB = getMultiplicityTerm(skolem, B);

  Node disEqual = countA.eqNode(countB).notNode();

  inferInfo.d_premises.push_back(n.notNode());
  inferInfo.d_conclusion = disEqual;
  return inferInfo;
}

Node InferenceGenerator::getSkolem(Node& n, InferInfo& inferInfo)
{
  Node skolem = d_sm->mkPurifySkolem(n, "skolem_bag", "skolem bag");
  inferInfo.d_skolems[n] = skolem;
  return skolem;
}

InferInfo InferenceGenerator::empty(Node n, Node e)
{
  Assert(n.getKind() == kind::EMPTYBAG);
  Assert(e.getType() == n.getType().getBagElementType());

  InferInfo inferInfo(d_im, InferenceId::BAG_EMPTY);
  Node skolem = getSkolem(n, inferInfo);
  Node count = getMultiplicityTerm(e, skolem);

  Node equal = count.eqNode(d_zero);
  inferInfo.d_conclusion = equal;
  return inferInfo;
}

InferInfo InferenceGenerator::unionDisjoint(Node n, Node e)
{
  Assert(n.getKind() == kind::UNION_DISJOINT && n[0].getType().isBag());
  Assert(e.getType() == n[0].getType().getBagElementType());

  Node A = n[0];
  Node B = n[1];
  InferInfo inferInfo(d_im, InferenceId::BAG_UNION_DISJOINT);

  Node countA = getMultiplicityTerm(e, A);
  Node countB = getMultiplicityTerm(e, B);

  Node skolem = getSkolem(n, inferInfo);
  Node count = getMultiplicityTerm(e, skolem);

  Node sum = d_nm->mkNode(kind::PLUS, countA, countB);
  Node equal = count.eqNode(sum);

  inferInfo.d_conclusion = equal;
  return inferInfo;
}

InferInfo InferenceGenerator::unionMax(Node n, Node e)
{
  Assert(n.getKind() == kind::UNION_MAX && n[0].getType().isBag());
  Assert(e.getType() == n[0].getType().getBagElementType());

  Node A = n[0];
  Node B = n[1];
  InferInfo inferInfo(d_im, InferenceId::BAG_UNION_MAX);

  Node countA = getMultiplicityTerm(e, A);
  Node countB = getMultiplicityTerm(e, B);

  Node skolem = getSkolem(n, inferInfo);
  Node count = getMultiplicityTerm(e, skolem);

  Node gt = d_nm->mkNode(kind::GT, countA, countB);
  Node max = d_nm->mkNode(kind::ITE, gt, countA, countB);
  Node equal = count.eqNode(max);

  inferInfo.d_conclusion = equal;
  return inferInfo;
}

InferInfo InferenceGenerator::intersection(Node n, Node e)
{
  Assert(n.getKind() == kind::INTERSECTION_MIN && n[0].getType().isBag());
  Assert(e.getType() == n[0].getType().getBagElementType());

  Node A = n[0];
  Node B = n[1];
  InferInfo inferInfo(d_im, InferenceId::BAG_INTERSECTION_MIN);

  Node countA = getMultiplicityTerm(e, A);
  Node countB = getMultiplicityTerm(e, B);
  Node skolem = getSkolem(n, inferInfo);
  Node count = getMultiplicityTerm(e, skolem);

  Node lt = d_nm->mkNode(kind::LT, countA, countB);
  Node min = d_nm->mkNode(kind::ITE, lt, countA, countB);
  Node equal = count.eqNode(min);
  inferInfo.d_conclusion = equal;
  return inferInfo;
}

InferInfo InferenceGenerator::differenceSubtract(Node n, Node e)
{
  Assert(n.getKind() == kind::DIFFERENCE_SUBTRACT && n[0].getType().isBag());
  Assert(e.getType() == n[0].getType().getBagElementType());

  Node A = n[0];
  Node B = n[1];
  InferInfo inferInfo(d_im, InferenceId::BAG_DIFFERENCE_SUBTRACT);

  Node countA = getMultiplicityTerm(e, A);
  Node countB = getMultiplicityTerm(e, B);
  Node skolem = getSkolem(n, inferInfo);
  Node count = getMultiplicityTerm(e, skolem);

  Node subtract = d_nm->mkNode(kind::MINUS, countA, countB);
  Node gte = d_nm->mkNode(kind::GEQ, countA, countB);
  Node difference = d_nm->mkNode(kind::ITE, gte, subtract, d_zero);
  Node equal = count.eqNode(difference);
  inferInfo.d_conclusion = equal;
  return inferInfo;
}

InferInfo InferenceGenerator::differenceRemove(Node n, Node e)
{
  Assert(n.getKind() == kind::DIFFERENCE_REMOVE && n[0].getType().isBag());
  Assert(e.getType() == n[0].getType().getBagElementType());

  Node A = n[0];
  Node B = n[1];
  InferInfo inferInfo(d_im, InferenceId::BAG_DIFFERENCE_REMOVE);

  Node countA = getMultiplicityTerm(e, A);
  Node countB = getMultiplicityTerm(e, B);

  Node skolem = getSkolem(n, inferInfo);
  Node count = getMultiplicityTerm(e, skolem);

  Node notInB = d_nm->mkNode(kind::EQUAL, countB, d_zero);
  Node difference = d_nm->mkNode(kind::ITE, notInB, countA, d_zero);
  Node equal = count.eqNode(difference);
  inferInfo.d_conclusion = equal;
  return inferInfo;
}

InferInfo InferenceGenerator::duplicateRemoval(Node n, Node e)
{
  Assert(n.getKind() == kind::DUPLICATE_REMOVAL && n[0].getType().isBag());
  Assert(e.getType() == n[0].getType().getBagElementType());

  Node A = n[0];
  InferInfo inferInfo(d_im, InferenceId::BAG_DUPLICATE_REMOVAL);

  Node countA = getMultiplicityTerm(e, A);
  Node skolem = getSkolem(n, inferInfo);
  Node count = getMultiplicityTerm(e, skolem);

  Node gte = d_nm->mkNode(kind::GEQ, countA, d_one);
  Node ite = d_nm->mkNode(kind::ITE, gte, d_one, d_zero);
  Node equal = count.eqNode(ite);
  inferInfo.d_conclusion = equal;
  return inferInfo;
}

Node InferenceGenerator::getMultiplicityTerm(Node element, Node bag)
{
  Node count = d_nm->mkNode(kind::BAG_COUNT, element, bag);
  return count;
}

}  // namespace bags
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Mudathir Mohamed, Andrew Reynolds, Gereon Kremer
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		* Inference generator utility.
14		*/
15
16		#include "inference_generator.h"
17
18		#include "expr/attribute.h"
19		#include "expr/bound_var_manager.h"
20		#include "expr/skolem_manager.h"
21		#include "theory/bags/inference_manager.h"
22		#include "theory/bags/solver_state.h"
23		#include "theory/uf/equality_engine.h"
24		#include "util/rational.h"
25
26		namespace cvc5 {
27		namespace theory {
28		namespace bags {
29
30	19700	InferenceGenerator::InferenceGenerator(SolverState* state, InferenceManager* im)
31	19700	: d_state(state), d_im(im)
32		{
33	19700	d_nm = NodeManager::currentNM();
34	19700	d_sm = d_nm->getSkolemManager();
35	19700	d_true = d_nm->mkConst(true);
36	19700	d_zero = d_nm->mkConst(Rational(0));
37	19700	d_one = d_nm->mkConst(Rational(1));
38	19700	}
39
40	1465	InferInfo InferenceGenerator::nonNegativeCount(Node n, Node e)
41		{
42	1465	Assert(n.getType().isBag());
43	1465	Assert(e.getType() == n.getType().getBagElementType());
44
45	1465	InferInfo inferInfo(d_im, InferenceId::BAG_NON_NEGATIVE_COUNT);
46	2930	Node count = d_nm->mkNode(kind::BAG_COUNT, e, n);
47
48	2930	Node gte = d_nm->mkNode(kind::GEQ, count, d_zero);
49	1465	inferInfo.d_conclusion = gte;
50	2930	return inferInfo;
51		}
52
53	340	InferInfo InferenceGenerator::mkBag(Node n, Node e)
54		{
55	340	Assert(n.getKind() == kind::MK_BAG);
56	340	Assert(e.getType() == n.getType().getBagElementType());
57
58	340	if (n[0] == e)
59		{
60		// TODO issue #78: refactor this with BagRewriter
61		// (=> true (= (bag.count e (bag e c)) c))
62	380	InferInfo inferInfo(d_im, InferenceId::BAG_MK_BAG_SAME_ELEMENT);
63	380	Node skolem = getSkolem(n, inferInfo);
64	380	Node count = getMultiplicityTerm(e, skolem);
65	190	inferInfo.d_conclusion = count.eqNode(n[1]);
66	190	return inferInfo;
67		}
68		else
69		{
70		// (=>
71		// true
72		// (= (bag.count e (bag x c)) (ite (= e x) c 0)))
73	300	InferInfo inferInfo(d_im, InferenceId::BAG_MK_BAG);
74	300	Node skolem = getSkolem(n, inferInfo);
75	300	Node count = getMultiplicityTerm(e, skolem);
76	300	Node same = d_nm->mkNode(kind::EQUAL, n[0], e);
77	300	Node ite = d_nm->mkNode(kind::ITE, same, n[1], d_zero);
78	300	Node equal = count.eqNode(ite);
79	150	inferInfo.d_conclusion = equal;
80	150	return inferInfo;
81		}
82		}
83
84		struct BagsDeqAttributeId
85		{
86		};
87		typedef expr::Attribute<BagsDeqAttributeId, Node> BagsDeqAttribute;
88
89	344	InferInfo InferenceGenerator::bagDisequality(Node n)
90		{
91	344	Assert(n.getKind() == kind::EQUAL && n[0].getType().isBag());
92
93	688	Node A = n[0];
94	688	Node B = n[1];
95
96	344	InferInfo inferInfo(d_im, InferenceId::BAG_DISEQUALITY);
97
98	688	TypeNode elementType = A.getType().getBagElementType();
99	344	BoundVarManager* bvm = d_nm->getBoundVarManager();
100	688	Node element = bvm->mkBoundVar<BagsDeqAttribute>(n, elementType);
101		Node skolem =
102	344	d_sm->mkSkolem(element,
103		n,
104		"bag_disequal",
105	688	"an extensional lemma for disequality of two bags");
106
107	688	Node countA = getMultiplicityTerm(skolem, A);
108	688	Node countB = getMultiplicityTerm(skolem, B);
109
110	688	Node disEqual = countA.eqNode(countB).notNode();
111
112	344	inferInfo.d_premises.push_back(n.notNode());
113	344	inferInfo.d_conclusion = disEqual;
114	688	return inferInfo;
115		}
116
117	1074	Node InferenceGenerator::getSkolem(Node& n, InferInfo& inferInfo)
118		{
119	1074	Node skolem = d_sm->mkPurifySkolem(n, "skolem_bag", "skolem bag");
120	1074	inferInfo.d_skolems[n] = skolem;
121	1074	return skolem;
122		}
123
124	22	InferInfo InferenceGenerator::empty(Node n, Node e)
125		{
126	22	Assert(n.getKind() == kind::EMPTYBAG);
127	22	Assert(e.getType() == n.getType().getBagElementType());
128
129	22	InferInfo inferInfo(d_im, InferenceId::BAG_EMPTY);
130	44	Node skolem = getSkolem(n, inferInfo);
131	44	Node count = getMultiplicityTerm(e, skolem);
132
133	44	Node equal = count.eqNode(d_zero);
134	22	inferInfo.d_conclusion = equal;
135	44	return inferInfo;
136		}
137
138	292	InferInfo InferenceGenerator::unionDisjoint(Node n, Node e)
139		{
140	292	Assert(n.getKind() == kind::UNION_DISJOINT && n[0].getType().isBag());
141	292	Assert(e.getType() == n[0].getType().getBagElementType());
142
143	584	Node A = n[0];
144	584	Node B = n[1];
145	292	InferInfo inferInfo(d_im, InferenceId::BAG_UNION_DISJOINT);
146
147	584	Node countA = getMultiplicityTerm(e, A);
148	584	Node countB = getMultiplicityTerm(e, B);
149
150	584	Node skolem = getSkolem(n, inferInfo);
151	584	Node count = getMultiplicityTerm(e, skolem);
152
153	584	Node sum = d_nm->mkNode(kind::PLUS, countA, countB);
154	584	Node equal = count.eqNode(sum);
155
156	292	inferInfo.d_conclusion = equal;
157	584	return inferInfo;
158		}
159
160	188	InferInfo InferenceGenerator::unionMax(Node n, Node e)
161		{
162	188	Assert(n.getKind() == kind::UNION_MAX && n[0].getType().isBag());
163	188	Assert(e.getType() == n[0].getType().getBagElementType());
164
165	376	Node A = n[0];
166	376	Node B = n[1];
167	188	InferInfo inferInfo(d_im, InferenceId::BAG_UNION_MAX);
168
169	376	Node countA = getMultiplicityTerm(e, A);
170	376	Node countB = getMultiplicityTerm(e, B);
171
172	376	Node skolem = getSkolem(n, inferInfo);
173	376	Node count = getMultiplicityTerm(e, skolem);
174
175	376	Node gt = d_nm->mkNode(kind::GT, countA, countB);
176	376	Node max = d_nm->mkNode(kind::ITE, gt, countA, countB);
177	376	Node equal = count.eqNode(max);
178
179	188	inferInfo.d_conclusion = equal;
180	376	return inferInfo;
181		}
182
183	128	InferInfo InferenceGenerator::intersection(Node n, Node e)
184		{
185	128	Assert(n.getKind() == kind::INTERSECTION_MIN && n[0].getType().isBag());
186	128	Assert(e.getType() == n[0].getType().getBagElementType());
187
188	256	Node A = n[0];
189	256	Node B = n[1];
190	128	InferInfo inferInfo(d_im, InferenceId::BAG_INTERSECTION_MIN);
191
192	256	Node countA = getMultiplicityTerm(e, A);
193	256	Node countB = getMultiplicityTerm(e, B);
194	256	Node skolem = getSkolem(n, inferInfo);
195	256	Node count = getMultiplicityTerm(e, skolem);
196
197	256	Node lt = d_nm->mkNode(kind::LT, countA, countB);
198	256	Node min = d_nm->mkNode(kind::ITE, lt, countA, countB);
199	256	Node equal = count.eqNode(min);
200	128	inferInfo.d_conclusion = equal;
201	256	return inferInfo;
202		}
203
204	56	InferInfo InferenceGenerator::differenceSubtract(Node n, Node e)
205		{
206	56	Assert(n.getKind() == kind::DIFFERENCE_SUBTRACT && n[0].getType().isBag());
207	56	Assert(e.getType() == n[0].getType().getBagElementType());
208
209	112	Node A = n[0];
210	112	Node B = n[1];
211	56	InferInfo inferInfo(d_im, InferenceId::BAG_DIFFERENCE_SUBTRACT);
212
213	112	Node countA = getMultiplicityTerm(e, A);
214	112	Node countB = getMultiplicityTerm(e, B);
215	112	Node skolem = getSkolem(n, inferInfo);
216	112	Node count = getMultiplicityTerm(e, skolem);
217
218	112	Node subtract = d_nm->mkNode(kind::MINUS, countA, countB);
219	112	Node gte = d_nm->mkNode(kind::GEQ, countA, countB);
220	112	Node difference = d_nm->mkNode(kind::ITE, gte, subtract, d_zero);
221	112	Node equal = count.eqNode(difference);
222	56	inferInfo.d_conclusion = equal;
223	112	return inferInfo;
224		}
225
226		InferInfo InferenceGenerator::differenceRemove(Node n, Node e)
227		{
228		Assert(n.getKind() == kind::DIFFERENCE_REMOVE && n[0].getType().isBag());
229		Assert(e.getType() == n[0].getType().getBagElementType());
230
231		Node A = n[0];
232		Node B = n[1];
233		InferInfo inferInfo(d_im, InferenceId::BAG_DIFFERENCE_REMOVE);
234
235		Node countA = getMultiplicityTerm(e, A);
236		Node countB = getMultiplicityTerm(e, B);
237
238		Node skolem = getSkolem(n, inferInfo);
239		Node count = getMultiplicityTerm(e, skolem);
240
241		Node notInB = d_nm->mkNode(kind::EQUAL, countB, d_zero);
242		Node difference = d_nm->mkNode(kind::ITE, notInB, countA, d_zero);
243		Node equal = count.eqNode(difference);
244		inferInfo.d_conclusion = equal;
245		return inferInfo;
246		}
247
248	48	InferInfo InferenceGenerator::duplicateRemoval(Node n, Node e)
249		{
250	48	Assert(n.getKind() == kind::DUPLICATE_REMOVAL && n[0].getType().isBag());
251	48	Assert(e.getType() == n[0].getType().getBagElementType());
252
253	96	Node A = n[0];
254	48	InferInfo inferInfo(d_im, InferenceId::BAG_DUPLICATE_REMOVAL);
255
256	96	Node countA = getMultiplicityTerm(e, A);
257	96	Node skolem = getSkolem(n, inferInfo);
258	96	Node count = getMultiplicityTerm(e, skolem);
259
260	96	Node gte = d_nm->mkNode(kind::GEQ, countA, d_one);
261	96	Node ite = d_nm->mkNode(kind::ITE, gte, d_one, d_zero);
262	96	Node equal = count.eqNode(ite);
263	48	inferInfo.d_conclusion = equal;
264	96	return inferInfo;
265		}
266
267	3138	Node InferenceGenerator::getMultiplicityTerm(Node element, Node bag)
268		{
269	3138	Node count = d_nm->mkNode(kind::BAG_COUNT, element, bag);
270	3138	return count;
271		}
272
273		} // namespace bags
274		} // namespace theory
275	29337	} // namespace cvc5