Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bags/inference_generator.cpp	Lines:	139	154	90.3 %
Date:	2021-05-24	Branches:	301	932	32.3 %


/******************************************************************************
 * 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"

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