Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bags/inference_generator.cpp	Lines:	222	242	91.7 %
Date:	2021-11-07	Branches:	556	1598	34.8 %


/******************************************************************************
 * 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/quantifiers/fmf/bounded_integers.h"
#include "theory/uf/equality_engine.h"
#include "util/rational.h"

using namespace cvc5::kind;

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::BAGS_NON_NEGATIVE_COUNT);
  Node count = d_nm->mkNode(BAG_COUNT, e, n);

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

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

  Node x = n[0];
  Node c = n[1];
  Node geq = d_nm->mkNode(GEQ, c, d_one);
  if (d_state->areEqual(e, x))
  {
    // (= (bag.count e skolem) (ite (>= c 1) c 0)))
    InferInfo inferInfo(d_im, InferenceId::BAGS_MK_BAG_SAME_ELEMENT);
    Node skolem = getSkolem(n, inferInfo);
    Node count = getMultiplicityTerm(e, skolem);
    Node ite = d_nm->mkNode(ITE, geq, c, d_zero);
    inferInfo.d_conclusion = count.eqNode(ite);
    return inferInfo;
  }
  if (d_state->areDisequal(e, x))
  {
    //(= (bag.count e skolem) 0))
    InferInfo inferInfo(d_im, InferenceId::BAGS_MK_BAG_SAME_ELEMENT);
    Node skolem = getSkolem(n, inferInfo);
    Node count = getMultiplicityTerm(e, skolem);
    inferInfo.d_conclusion = count.eqNode(d_zero);
    return inferInfo;
  }
  else
  {
    // (= (bag.count e skolem) (ite (and (= e x) (>= c 1)) c 0)))
    InferInfo inferInfo(d_im, InferenceId::BAGS_MK_BAG);
    Node skolem = getSkolem(n, inferInfo);
    Node count = getMultiplicityTerm(e, skolem);
    Node same = d_nm->mkNode(EQUAL, e, x);
    Node andNode = same.andNode(geq);
    Node ite = d_nm->mkNode(ITE, andNode, c, d_zero);
    Node equal = count.eqNode(ite);
    inferInfo.d_conclusion = equal;
    return inferInfo;
  }
}

/**
 * A bound variable corresponding to the universally quantified integer
 * variable used to range over the distinct elements in a bag, used
 * for axiomatizing the behavior of some term.
 */
struct FirstIndexVarAttributeId
{
};
typedef expr::Attribute<FirstIndexVarAttributeId, Node> FirstIndexVarAttribute;

/**
 * A bound variable corresponding to the universally quantified integer
 * variable used to range over the distinct elements in a bag, used
 * for axiomatizing the behavior of some term.
 */
struct SecondIndexVarAttributeId
{
};
typedef expr::Attribute<SecondIndexVarAttributeId, Node>
    SecondIndexVarAttribute;

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

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

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

  InferInfo inferInfo(d_im, InferenceId::BAGS_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() == EMPTYBAG);
  Assert(e.getType() == n.getType().getBagElementType());

  InferInfo inferInfo(d_im, InferenceId::BAGS_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() == 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::BAGS_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(PLUS, countA, countB);
  Node equal = count.eqNode(sum);

  inferInfo.d_conclusion = equal;
  return inferInfo;
}

InferInfo InferenceGenerator::unionMax(Node n, Node e)
{
  Assert(n.getKind() == 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::BAGS_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(GT, countA, countB);
  Node max = d_nm->mkNode(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() == 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::BAGS_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(LT, countA, countB);
  Node min = d_nm->mkNode(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() == 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::BAGS_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(MINUS, countA, countB);
  Node gte = d_nm->mkNode(GEQ, countA, countB);
  Node difference = d_nm->mkNode(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() == 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::BAGS_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(LEQ, countB, d_zero);
  Node difference = d_nm->mkNode(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() == DUPLICATE_REMOVAL && n[0].getType().isBag());
  Assert(e.getType() == n[0].getType().getBagElementType());

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

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

  Node gte = d_nm->mkNode(GEQ, countA, d_one);
  Node ite = d_nm->mkNode(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(BAG_COUNT, element, bag);
  return count;
}

std::tuple<InferInfo, Node, Node> InferenceGenerator::mapDownwards(Node n,
                                                                   Node e)
{
  Assert(n.getKind() == BAG_MAP && n[1].getType().isBag());
  Assert(n[0].getType().isFunction()
         && n[0].getType().getArgTypes().size() == 1);
  Assert(e.getType() == n[0].getType().getRangeType());

  InferInfo inferInfo(d_im, InferenceId::BAGS_MAP);

  Node f = n[0];
  Node A = n[1];
  // declare an uninterpreted function uf: Int -> T
  TypeNode domainType = f.getType().getArgTypes()[0];
  TypeNode ufType = d_nm->mkFunctionType(d_nm->integerType(), domainType);
  Node uf =
      d_sm->mkSkolemFunction(SkolemFunId::BAGS_MAP_PREIMAGE, ufType, {n, e});

  // declare uninterpreted function sum: Int -> Int
  TypeNode sumType =
      d_nm->mkFunctionType(d_nm->integerType(), d_nm->integerType());
  Node sum = d_sm->mkSkolemFunction(SkolemFunId::BAGS_MAP_SUM, sumType, {n, e});

  // (= (sum 0) 0)
  Node sum_zero = d_nm->mkNode(APPLY_UF, sum, d_zero);
  Node baseCase = d_nm->mkNode(EQUAL, sum_zero, d_zero);

  // guess the size of the preimage of e
  Node preImageSize = d_sm->mkDummySkolem("preImageSize", d_nm->integerType());

  // (= (sum preImageSize) (bag.count e skolem))
  Node mapSkolem = getSkolem(n, inferInfo);
  Node countE = getMultiplicityTerm(e, mapSkolem);
  Node totalSum = d_nm->mkNode(APPLY_UF, sum, preImageSize);
  Node totalSumEqualCountE = d_nm->mkNode(EQUAL, totalSum, countE);

  // (forall ((i Int))
  //        (let ((uf_i (uf i)))
  //          (let ((count_uf_i (bag.count uf_i A)))
  //            (=>
  //             (and (>= i 1) (<= i preImageSize))
  //             (and
  //               (= (f uf_i) e)
  //               (>= count_uf_i 1)
  //               (= (sum i) (+ (sum (- i 1)) count_uf_i))
  //               (forall ((j Int))
  //                 (=>
  //                  (and (< i j) (<= j preImageSize))
  //                  (not (= (uf i) (uf j))))))
  //               )))))

  BoundVarManager* bvm = d_nm->getBoundVarManager();
  Node i = bvm->mkBoundVar<FirstIndexVarAttribute>(n, "i", d_nm->integerType());
  Node j =
      bvm->mkBoundVar<SecondIndexVarAttribute>(n, "j", d_nm->integerType());
  Node iList = d_nm->mkNode(BOUND_VAR_LIST, i);
  Node jList = d_nm->mkNode(BOUND_VAR_LIST, j);
  Node iPlusOne = d_nm->mkNode(PLUS, i, d_one);
  Node iMinusOne = d_nm->mkNode(MINUS, i, d_one);
  Node uf_i = d_nm->mkNode(APPLY_UF, uf, i);
  Node uf_j = d_nm->mkNode(APPLY_UF, uf, j);
  Node f_uf_i = d_nm->mkNode(APPLY_UF, f, uf_i);
  Node uf_iPlusOne = d_nm->mkNode(APPLY_UF, uf, iPlusOne);
  Node uf_iMinusOne = d_nm->mkNode(APPLY_UF, uf, iMinusOne);
  Node interval_i = d_nm->mkNode(
      AND, d_nm->mkNode(GEQ, i, d_one), d_nm->mkNode(LEQ, i, preImageSize));
  Node sum_i = d_nm->mkNode(APPLY_UF, sum, i);
  Node sum_iPlusOne = d_nm->mkNode(APPLY_UF, sum, iPlusOne);
  Node sum_iMinusOne = d_nm->mkNode(APPLY_UF, sum, iMinusOne);
  Node count_iMinusOne = d_nm->mkNode(BAG_COUNT, uf_iMinusOne, A);
  Node count_uf_i = d_nm->mkNode(BAG_COUNT, uf_i, A);
  Node inductiveCase =
      d_nm->mkNode(EQUAL, sum_i, d_nm->mkNode(PLUS, sum_iMinusOne, count_uf_i));
  Node f_iEqualE = d_nm->mkNode(EQUAL, f_uf_i, e);
  Node geqOne = d_nm->mkNode(GEQ, count_uf_i, d_one);

  // i < j <= preImageSize
  Node interval_j = d_nm->mkNode(
      AND, d_nm->mkNode(LT, i, j), d_nm->mkNode(LEQ, j, preImageSize));
  // uf(i) != uf(j)
  Node uf_i_equals_uf_j = d_nm->mkNode(EQUAL, uf_i, uf_j);
  Node notEqual = d_nm->mkNode(EQUAL, uf_i, uf_j).negate();
  Node body_j = d_nm->mkNode(OR, interval_j.negate(), notEqual);
  Node forAll_j = quantifiers::BoundedIntegers::mkBoundedForall(jList, body_j);
  Node andNode =
      d_nm->mkNode(AND, {f_iEqualE, geqOne, inductiveCase, forAll_j});
  Node body_i = d_nm->mkNode(OR, interval_i.negate(), andNode);
  Node forAll_i = quantifiers::BoundedIntegers::mkBoundedForall(iList, body_i);
  Node preImageGTE_zero = d_nm->mkNode(GEQ, preImageSize, d_zero);
  Node conclusion = d_nm->mkNode(
      AND, {baseCase, totalSumEqualCountE, forAll_i, preImageGTE_zero});
  inferInfo.d_conclusion = conclusion;

  std::map<Node, Node> m;
  m[e] = conclusion;
  return std::tuple(inferInfo, uf, preImageSize);
}

InferInfo InferenceGenerator::mapUpwards(
    Node n, Node uf, Node preImageSize, Node y, Node x)
{
  Assert(n.getKind() == BAG_MAP && n[1].getType().isBag());
  Assert(n[0].getType().isFunction()
         && n[0].getType().getArgTypes().size() == 1);

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

  Node countA = getMultiplicityTerm(x, A);
  Node xInA = d_nm->mkNode(GEQ, countA, d_one);
  Node notEqual = d_nm->mkNode(EQUAL, d_nm->mkNode(APPLY_UF, f, x), y).negate();

  Node k = d_sm->mkDummySkolem("k", d_nm->integerType());
  Node inRange = d_nm->mkNode(
      AND, d_nm->mkNode(GEQ, k, d_one), d_nm->mkNode(LEQ, k, preImageSize));
  Node equal = d_nm->mkNode(EQUAL, d_nm->mkNode(APPLY_UF, uf, k), x);
  Node andNode = d_nm->mkNode(AND, inRange, equal);
  Node orNode = d_nm->mkNode(OR, notEqual, andNode);
  Node implies = d_nm->mkNode(IMPLIES, xInA, orNode);
  inferInfo.d_conclusion = implies;
  std::cout << "Upwards conclusion: " << inferInfo.d_conclusion << std::endl
            << std::endl;
  return inferInfo;
}

}  // 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/quantifiers/fmf/bounded_integers.h"
24		#include "theory/uf/equality_engine.h"
25		#include "util/rational.h"
26
27		using namespace cvc5::kind;
28
29		namespace cvc5 {
30		namespace theory {
31		namespace bags {
32
33	30546	InferenceGenerator::InferenceGenerator(SolverState* state, InferenceManager* im)
34	30546	: d_state(state), d_im(im)
35		{
36	30546	d_nm = NodeManager::currentNM();
37	30546	d_sm = d_nm->getSkolemManager();
38	30546	d_true = d_nm->mkConst(true);
39	30546	d_zero = d_nm->mkConst(Rational(0));
40	30546	d_one = d_nm->mkConst(Rational(1));
41	30546	}
42
43	2195	InferInfo InferenceGenerator::nonNegativeCount(Node n, Node e)
44		{
45	2195	Assert(n.getType().isBag());
46	2195	Assert(e.getType() == n.getType().getBagElementType());
47
48	2195	InferInfo inferInfo(d_im, InferenceId::BAGS_NON_NEGATIVE_COUNT);
49	4390	Node count = d_nm->mkNode(BAG_COUNT, e, n);
50
51	4390	Node gte = d_nm->mkNode(GEQ, count, d_zero);
52	2195	inferInfo.d_conclusion = gte;
53	4390	return inferInfo;
54		}
55
56	911	InferInfo InferenceGenerator::mkBag(Node n, Node e)
57		{
58	911	Assert(n.getKind() == MK_BAG);
59	911	Assert(e.getType() == n.getType().getBagElementType());
60
61	1822	Node x = n[0];
62	1822	Node c = n[1];
63	1822	Node geq = d_nm->mkNode(GEQ, c, d_one);
64	911	if (d_state->areEqual(e, x))
65		{
66		// (= (bag.count e skolem) (ite (>= c 1) c 0)))
67	1160	InferInfo inferInfo(d_im, InferenceId::BAGS_MK_BAG_SAME_ELEMENT);
68	1160	Node skolem = getSkolem(n, inferInfo);
69	1160	Node count = getMultiplicityTerm(e, skolem);
70	1160	Node ite = d_nm->mkNode(ITE, geq, c, d_zero);
71	580	inferInfo.d_conclusion = count.eqNode(ite);
72	580	return inferInfo;
73		}
74	331	if (d_state->areDisequal(e, x))
75		{
76		//(= (bag.count e skolem) 0))
77	90	InferInfo inferInfo(d_im, InferenceId::BAGS_MK_BAG_SAME_ELEMENT);
78	90	Node skolem = getSkolem(n, inferInfo);
79	90	Node count = getMultiplicityTerm(e, skolem);
80	45	inferInfo.d_conclusion = count.eqNode(d_zero);
81	45	return inferInfo;
82		}
83		else
84		{
85		// (= (bag.count e skolem) (ite (and (= e x) (>= c 1)) c 0)))
86	572	InferInfo inferInfo(d_im, InferenceId::BAGS_MK_BAG);
87	572	Node skolem = getSkolem(n, inferInfo);
88	572	Node count = getMultiplicityTerm(e, skolem);
89	572	Node same = d_nm->mkNode(EQUAL, e, x);
90	572	Node andNode = same.andNode(geq);
91	572	Node ite = d_nm->mkNode(ITE, andNode, c, d_zero);
92	572	Node equal = count.eqNode(ite);
93	286	inferInfo.d_conclusion = equal;
94	286	return inferInfo;
95		}
96		}
97
98		/**
99		* A bound variable corresponding to the universally quantified integer
100		* variable used to range over the distinct elements in a bag, used
101		* for axiomatizing the behavior of some term.
102		*/
103		struct FirstIndexVarAttributeId
104		{
105		};
106		typedef expr::Attribute<FirstIndexVarAttributeId, Node> FirstIndexVarAttribute;
107
108		/**
109		* A bound variable corresponding to the universally quantified integer
110		* variable used to range over the distinct elements in a bag, used
111		* for axiomatizing the behavior of some term.
112		*/
113		struct SecondIndexVarAttributeId
114		{
115		};
116		typedef expr::Attribute<SecondIndexVarAttributeId, Node>
117		SecondIndexVarAttribute;
118
119		struct BagsDeqAttributeId
120		{
121		};
122		typedef expr::Attribute<BagsDeqAttributeId, Node> BagsDeqAttribute;
123
124	445	InferInfo InferenceGenerator::bagDisequality(Node n)
125		{
126	445	Assert(n.getKind() == EQUAL && n[0].getType().isBag());
127
128	890	Node A = n[0];
129	890	Node B = n[1];
130
131	445	InferInfo inferInfo(d_im, InferenceId::BAGS_DISEQUALITY);
132
133	890	TypeNode elementType = A.getType().getBagElementType();
134	445	BoundVarManager* bvm = d_nm->getBoundVarManager();
135	890	Node element = bvm->mkBoundVar<BagsDeqAttribute>(n, elementType);
136		Node skolem =
137	445	d_sm->mkSkolem(element,
138		n,
139		"bag_disequal",
140	890	"an extensional lemma for disequality of two bags");
141
142	890	Node countA = getMultiplicityTerm(skolem, A);
143	890	Node countB = getMultiplicityTerm(skolem, B);
144
145	890	Node disEqual = countA.eqNode(countB).notNode();
146
147	445	inferInfo.d_premises.push_back(n.notNode());
148	445	inferInfo.d_conclusion = disEqual;
149	890	return inferInfo;
150		}
151
152	1897	Node InferenceGenerator::getSkolem(Node& n, InferInfo& inferInfo)
153		{
154	1897	Node skolem = d_sm->mkPurifySkolem(n, "skolem_bag", "skolem bag");
155	1897	inferInfo.d_skolems[n] = skolem;
156	1897	return skolem;
157		}
158
159	26	InferInfo InferenceGenerator::empty(Node n, Node e)
160		{
161	26	Assert(n.getKind() == EMPTYBAG);
162	26	Assert(e.getType() == n.getType().getBagElementType());
163
164	26	InferInfo inferInfo(d_im, InferenceId::BAGS_EMPTY);
165	52	Node skolem = getSkolem(n, inferInfo);
166	52	Node count = getMultiplicityTerm(e, skolem);
167
168	52	Node equal = count.eqNode(d_zero);
169	26	inferInfo.d_conclusion = equal;
170	52	return inferInfo;
171		}
172
173	280	InferInfo InferenceGenerator::unionDisjoint(Node n, Node e)
174		{
175	280	Assert(n.getKind() == UNION_DISJOINT && n[0].getType().isBag());
176	280	Assert(e.getType() == n[0].getType().getBagElementType());
177
178	560	Node A = n[0];
179	560	Node B = n[1];
180	280	InferInfo inferInfo(d_im, InferenceId::BAGS_UNION_DISJOINT);
181
182	560	Node countA = getMultiplicityTerm(e, A);
183	560	Node countB = getMultiplicityTerm(e, B);
184
185	560	Node skolem = getSkolem(n, inferInfo);
186	560	Node count = getMultiplicityTerm(e, skolem);
187
188	560	Node sum = d_nm->mkNode(PLUS, countA, countB);
189	560	Node equal = count.eqNode(sum);
190
191	280	inferInfo.d_conclusion = equal;
192	560	return inferInfo;
193		}
194
195	184	InferInfo InferenceGenerator::unionMax(Node n, Node e)
196		{
197	184	Assert(n.getKind() == UNION_MAX && n[0].getType().isBag());
198	184	Assert(e.getType() == n[0].getType().getBagElementType());
199
200	368	Node A = n[0];
201	368	Node B = n[1];
202	184	InferInfo inferInfo(d_im, InferenceId::BAGS_UNION_MAX);
203
204	368	Node countA = getMultiplicityTerm(e, A);
205	368	Node countB = getMultiplicityTerm(e, B);
206
207	368	Node skolem = getSkolem(n, inferInfo);
208	368	Node count = getMultiplicityTerm(e, skolem);
209
210	368	Node gt = d_nm->mkNode(GT, countA, countB);
211	368	Node max = d_nm->mkNode(ITE, gt, countA, countB);
212	368	Node equal = count.eqNode(max);
213
214	184	inferInfo.d_conclusion = equal;
215	368	return inferInfo;
216		}
217
218	146	InferInfo InferenceGenerator::intersection(Node n, Node e)
219		{
220	146	Assert(n.getKind() == INTERSECTION_MIN && n[0].getType().isBag());
221	146	Assert(e.getType() == n[0].getType().getBagElementType());
222
223	292	Node A = n[0];
224	292	Node B = n[1];
225	146	InferInfo inferInfo(d_im, InferenceId::BAGS_INTERSECTION_MIN);
226
227	292	Node countA = getMultiplicityTerm(e, A);
228	292	Node countB = getMultiplicityTerm(e, B);
229	292	Node skolem = getSkolem(n, inferInfo);
230	292	Node count = getMultiplicityTerm(e, skolem);
231
232	292	Node lt = d_nm->mkNode(LT, countA, countB);
233	292	Node min = d_nm->mkNode(ITE, lt, countA, countB);
234	292	Node equal = count.eqNode(min);
235	146	inferInfo.d_conclusion = equal;
236	292	return inferInfo;
237		}
238
239	80	InferInfo InferenceGenerator::differenceSubtract(Node n, Node e)
240		{
241	80	Assert(n.getKind() == DIFFERENCE_SUBTRACT && n[0].getType().isBag());
242	80	Assert(e.getType() == n[0].getType().getBagElementType());
243
244	160	Node A = n[0];
245	160	Node B = n[1];
246	80	InferInfo inferInfo(d_im, InferenceId::BAGS_DIFFERENCE_SUBTRACT);
247
248	160	Node countA = getMultiplicityTerm(e, A);
249	160	Node countB = getMultiplicityTerm(e, B);
250	160	Node skolem = getSkolem(n, inferInfo);
251	160	Node count = getMultiplicityTerm(e, skolem);
252
253	160	Node subtract = d_nm->mkNode(MINUS, countA, countB);
254	160	Node gte = d_nm->mkNode(GEQ, countA, countB);
255	160	Node difference = d_nm->mkNode(ITE, gte, subtract, d_zero);
256	160	Node equal = count.eqNode(difference);
257	80	inferInfo.d_conclusion = equal;
258	160	return inferInfo;
259		}
260
261	218	InferInfo InferenceGenerator::differenceRemove(Node n, Node e)
262		{
263	218	Assert(n.getKind() == DIFFERENCE_REMOVE && n[0].getType().isBag());
264	218	Assert(e.getType() == n[0].getType().getBagElementType());
265
266	436	Node A = n[0];
267	436	Node B = n[1];
268	218	InferInfo inferInfo(d_im, InferenceId::BAGS_DIFFERENCE_REMOVE);
269
270	436	Node countA = getMultiplicityTerm(e, A);
271	436	Node countB = getMultiplicityTerm(e, B);
272
273	436	Node skolem = getSkolem(n, inferInfo);
274	436	Node count = getMultiplicityTerm(e, skolem);
275
276	436	Node notInB = d_nm->mkNode(LEQ, countB, d_zero);
277	436	Node difference = d_nm->mkNode(ITE, notInB, countA, d_zero);
278	436	Node equal = count.eqNode(difference);
279	218	inferInfo.d_conclusion = equal;
280	436	return inferInfo;
281		}
282
283	48	InferInfo InferenceGenerator::duplicateRemoval(Node n, Node e)
284		{
285	48	Assert(n.getKind() == DUPLICATE_REMOVAL && n[0].getType().isBag());
286	48	Assert(e.getType() == n[0].getType().getBagElementType());
287
288	96	Node A = n[0];
289	48	InferInfo inferInfo(d_im, InferenceId::BAGS_DUPLICATE_REMOVAL);
290
291	96	Node countA = getMultiplicityTerm(e, A);
292	96	Node skolem = getSkolem(n, inferInfo);
293	96	Node count = getMultiplicityTerm(e, skolem);
294
295	96	Node gte = d_nm->mkNode(GEQ, countA, d_one);
296	96	Node ite = d_nm->mkNode(ITE, gte, d_one, d_zero);
297	96	Node equal = count.eqNode(ite);
298	48	inferInfo.d_conclusion = equal;
299	96	return inferInfo;
300		}
301
302	4651	Node InferenceGenerator::getMultiplicityTerm(Node element, Node bag)
303		{
304	4651	Node count = d_nm->mkNode(BAG_COUNT, element, bag);
305	4651	return count;
306		}
307
308	4	std::tuple<InferInfo, Node, Node> InferenceGenerator::mapDownwards(Node n,
309		Node e)
310		{
311	4	Assert(n.getKind() == BAG_MAP && n[1].getType().isBag());
312	4	Assert(n[0].getType().isFunction()
313		&& n[0].getType().getArgTypes().size() == 1);
314	4	Assert(e.getType() == n[0].getType().getRangeType());
315
316	8	InferInfo inferInfo(d_im, InferenceId::BAGS_MAP);
317
318	8	Node f = n[0];
319	8	Node A = n[1];
320		// declare an uninterpreted function uf: Int -> T
321	8	TypeNode domainType = f.getType().getArgTypes()[0];
322	8	TypeNode ufType = d_nm->mkFunctionType(d_nm->integerType(), domainType);
323		Node uf =
324	8	d_sm->mkSkolemFunction(SkolemFunId::BAGS_MAP_PREIMAGE, ufType, {n, e});
325
326		// declare uninterpreted function sum: Int -> Int
327		TypeNode sumType =
328	8	d_nm->mkFunctionType(d_nm->integerType(), d_nm->integerType());
329	8	Node sum = d_sm->mkSkolemFunction(SkolemFunId::BAGS_MAP_SUM, sumType, {n, e});
330
331		// (= (sum 0) 0)
332	8	Node sum_zero = d_nm->mkNode(APPLY_UF, sum, d_zero);
333	8	Node baseCase = d_nm->mkNode(EQUAL, sum_zero, d_zero);
334
335		// guess the size of the preimage of e
336	8	Node preImageSize = d_sm->mkDummySkolem("preImageSize", d_nm->integerType());
337
338		// (= (sum preImageSize) (bag.count e skolem))
339	8	Node mapSkolem = getSkolem(n, inferInfo);
340	8	Node countE = getMultiplicityTerm(e, mapSkolem);
341	8	Node totalSum = d_nm->mkNode(APPLY_UF, sum, preImageSize);
342	8	Node totalSumEqualCountE = d_nm->mkNode(EQUAL, totalSum, countE);
343
344		// (forall ((i Int))
345		// (let ((uf_i (uf i)))
346		// (let ((count_uf_i (bag.count uf_i A)))
347		// (=>
348		// (and (>= i 1) (<= i preImageSize))
349		// (and
350		// (= (f uf_i) e)
351		// (>= count_uf_i 1)
352		// (= (sum i) (+ (sum (- i 1)) count_uf_i))
353		// (forall ((j Int))
354		// (=>
355		// (and (< i j) (<= j preImageSize))
356		// (not (= (uf i) (uf j))))))
357		// )))))
358
359	4	BoundVarManager* bvm = d_nm->getBoundVarManager();
360	8	Node i = bvm->mkBoundVar<FirstIndexVarAttribute>(n, "i", d_nm->integerType());
361		Node j =
362	8	bvm->mkBoundVar<SecondIndexVarAttribute>(n, "j", d_nm->integerType());
363	8	Node iList = d_nm->mkNode(BOUND_VAR_LIST, i);
364	8	Node jList = d_nm->mkNode(BOUND_VAR_LIST, j);
365	8	Node iPlusOne = d_nm->mkNode(PLUS, i, d_one);
366	8	Node iMinusOne = d_nm->mkNode(MINUS, i, d_one);
367	8	Node uf_i = d_nm->mkNode(APPLY_UF, uf, i);
368	8	Node uf_j = d_nm->mkNode(APPLY_UF, uf, j);
369	8	Node f_uf_i = d_nm->mkNode(APPLY_UF, f, uf_i);
370	8	Node uf_iPlusOne = d_nm->mkNode(APPLY_UF, uf, iPlusOne);
371	8	Node uf_iMinusOne = d_nm->mkNode(APPLY_UF, uf, iMinusOne);
372	4	Node interval_i = d_nm->mkNode(
373	8	AND, d_nm->mkNode(GEQ, i, d_one), d_nm->mkNode(LEQ, i, preImageSize));
374	8	Node sum_i = d_nm->mkNode(APPLY_UF, sum, i);
375	8	Node sum_iPlusOne = d_nm->mkNode(APPLY_UF, sum, iPlusOne);
376	8	Node sum_iMinusOne = d_nm->mkNode(APPLY_UF, sum, iMinusOne);
377	8	Node count_iMinusOne = d_nm->mkNode(BAG_COUNT, uf_iMinusOne, A);
378	8	Node count_uf_i = d_nm->mkNode(BAG_COUNT, uf_i, A);
379		Node inductiveCase =
380	8	d_nm->mkNode(EQUAL, sum_i, d_nm->mkNode(PLUS, sum_iMinusOne, count_uf_i));
381	8	Node f_iEqualE = d_nm->mkNode(EQUAL, f_uf_i, e);
382	8	Node geqOne = d_nm->mkNode(GEQ, count_uf_i, d_one);
383
384		// i < j <= preImageSize
385	4	Node interval_j = d_nm->mkNode(
386	8	AND, d_nm->mkNode(LT, i, j), d_nm->mkNode(LEQ, j, preImageSize));
387		// uf(i) != uf(j)
388	8	Node uf_i_equals_uf_j = d_nm->mkNode(EQUAL, uf_i, uf_j);
389	8	Node notEqual = d_nm->mkNode(EQUAL, uf_i, uf_j).negate();
390	8	Node body_j = d_nm->mkNode(OR, interval_j.negate(), notEqual);
391	8	Node forAll_j = quantifiers::BoundedIntegers::mkBoundedForall(jList, body_j);
392		Node andNode =
393	8	d_nm->mkNode(AND, {f_iEqualE, geqOne, inductiveCase, forAll_j});
394	8	Node body_i = d_nm->mkNode(OR, interval_i.negate(), andNode);
395	8	Node forAll_i = quantifiers::BoundedIntegers::mkBoundedForall(iList, body_i);
396	8	Node preImageGTE_zero = d_nm->mkNode(GEQ, preImageSize, d_zero);
397	4	Node conclusion = d_nm->mkNode(
398	8	AND, {baseCase, totalSumEqualCountE, forAll_i, preImageGTE_zero});
399	4	inferInfo.d_conclusion = conclusion;
400
401	8	std::map<Node, Node> m;
402	4	m[e] = conclusion;
403	8	return std::tuple(inferInfo, uf, preImageSize);
404		}
405
406		InferInfo InferenceGenerator::mapUpwards(
407		Node n, Node uf, Node preImageSize, Node y, Node x)
408		{
409		Assert(n.getKind() == BAG_MAP && n[1].getType().isBag());
410		Assert(n[0].getType().isFunction()
411		&& n[0].getType().getArgTypes().size() == 1);
412
413		InferInfo inferInfo(d_im, InferenceId::BAGS_MAP);
414		Node f = n[0];
415		Node A = n[1];
416
417		Node countA = getMultiplicityTerm(x, A);
418		Node xInA = d_nm->mkNode(GEQ, countA, d_one);
419		Node notEqual = d_nm->mkNode(EQUAL, d_nm->mkNode(APPLY_UF, f, x), y).negate();
420
421		Node k = d_sm->mkDummySkolem("k", d_nm->integerType());
422		Node inRange = d_nm->mkNode(
423		AND, d_nm->mkNode(GEQ, k, d_one), d_nm->mkNode(LEQ, k, preImageSize));
424		Node equal = d_nm->mkNode(EQUAL, d_nm->mkNode(APPLY_UF, uf, k), x);
425		Node andNode = d_nm->mkNode(AND, inRange, equal);
426		Node orNode = d_nm->mkNode(OR, notEqual, andNode);
427		Node implies = d_nm->mkNode(IMPLIES, xInA, orNode);
428		inferInfo.d_conclusion = implies;
429		std::cout << "Upwards conclusion: " << inferInfo.d_conclusion << std::endl
430		<< std::endl;
431		return inferInfo;
432		}
433
434		} // namespace bags
435		} // namespace theory
436	31137	} // namespace cvc5