Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bags/theory_bags.cpp	Lines:	109	121	90.1 %
Date:	2021-08-14	Branches:	161	396	40.7 %


/******************************************************************************
 * Top contributors (to current version):
 *   Mudathir Mohamed, Haniel Barbosa, Andrew Reynolds
 *
 * 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.
 * ****************************************************************************
 *
 * Bags theory.
 */

#include "theory/bags/theory_bags.h"

#include "proof/proof_checker.h"
#include "smt/logic_exception.h"
#include "theory/bags/normal_form.h"
#include "theory/rewriter.h"
#include "theory/theory_model.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace bags {

TheoryBags::TheoryBags(context::Context* c,
                       context::UserContext* u,
                       OutputChannel& out,
                       Valuation valuation,
                       const LogicInfo& logicInfo,
                       ProofNodeManager* pnm)
    : Theory(THEORY_BAGS, c, u, out, valuation, logicInfo, pnm),
      d_state(c, u, valuation),
      d_im(*this, d_state, pnm),
      d_ig(&d_state, &d_im),
      d_notify(*this, d_im),
      d_statistics(),
      d_rewriter(&d_statistics.d_rewrites),
      d_termReg(d_state, d_im),
      d_solver(d_state, d_im, d_termReg)
{
  // use the official theory state and inference manager objects
  d_theoryState = &d_state;
  d_inferManager = &d_im;
}

TheoryBags::~TheoryBags() {}

TheoryRewriter* TheoryBags::getTheoryRewriter() { return &d_rewriter; }

ProofRuleChecker* TheoryBags::getProofChecker() { return nullptr; }

bool TheoryBags::needsEqualityEngine(EeSetupInfo& esi)
{
  esi.d_notify = &d_notify;
  esi.d_name = "theory::bags::ee";
  return true;
}

void TheoryBags::finishInit()
{
  Assert(d_equalityEngine != nullptr);

  // choice is used to eliminate witness
  d_valuation.setUnevaluatedKind(WITNESS);

  // functions we are doing congruence over
  d_equalityEngine->addFunctionKind(UNION_MAX);
  d_equalityEngine->addFunctionKind(UNION_DISJOINT);
  d_equalityEngine->addFunctionKind(INTERSECTION_MIN);
  d_equalityEngine->addFunctionKind(DIFFERENCE_SUBTRACT);
  d_equalityEngine->addFunctionKind(DIFFERENCE_REMOVE);
  d_equalityEngine->addFunctionKind(BAG_COUNT);
  d_equalityEngine->addFunctionKind(DUPLICATE_REMOVAL);
  d_equalityEngine->addFunctionKind(MK_BAG);
  d_equalityEngine->addFunctionKind(BAG_CARD);
  d_equalityEngine->addFunctionKind(BAG_FROM_SET);
  d_equalityEngine->addFunctionKind(BAG_TO_SET);
}

void TheoryBags::postCheck(Effort effort)
{
  d_im.doPendingFacts();
  // TODO issue #78: add Assert(d_strat.isStrategyInit());
  if (!d_state.isInConflict() && !d_valuation.needCheck())
  // TODO issue #78:  add && d_strat.hasStrategyEffort(e))
  {
    Trace("bags::TheoryBags::postCheck") << "effort: " << std::endl;

    // TODO issue #78: add ++(d_statistics.d_checkRuns);
    bool sentLemma = false;
    bool hadPending = false;
    Trace("bags-check") << "Full effort check..." << std::endl;
    do
    {
      d_im.reset();
      // TODO issue #78: add ++(d_statistics.d_strategyRuns);
      Trace("bags-check") << "  * Run strategy..." << std::endl;
      // TODO issue #78: add runStrategy(e);

      d_solver.postCheck();

      // remember if we had pending facts or lemmas
      hadPending = d_im.hasPending();
      // Send the facts *and* the lemmas. We send lemmas regardless of whether
      // we send facts since some lemmas cannot be dropped. Other lemmas are
      // otherwise avoided by aborting the strategy when a fact is ready.
      d_im.doPending();
      // Did we successfully send a lemma? Notice that if hasPending = true
      // and sentLemma = false, then the above call may have:
      // (1) had no pending lemmas, but successfully processed pending facts,
      // (2) unsuccessfully processed pending lemmas.
      // In either case, we repeat the strategy if we are not in conflict.
      sentLemma = d_im.hasSentLemma();
      if (Trace.isOn("bags-check"))
      {
        // TODO: clean this Trace("bags-check") << "  ...finish run strategy: ";
        Trace("bags-check") << (hadPending ? "hadPending " : "");
        Trace("bags-check") << (sentLemma ? "sentLemma " : "");
        Trace("bags-check") << (d_state.isInConflict() ? "conflict " : "");
        if (!hadPending && !sentLemma && !d_state.isInConflict())
        {
          Trace("bags-check") << "(none)";
        }
        Trace("bags-check") << std::endl;
      }
      // repeat if we did not add a lemma or conflict, and we had pending
      // facts or lemmas.
    } while (!d_state.isInConflict() && !sentLemma && hadPending);
  }
  Trace("bags-check") << "Theory of bags, done check : " << effort << std::endl;
  Assert(!d_im.hasPendingFact());
  Assert(!d_im.hasPendingLemma());
}

void TheoryBags::notifyFact(TNode atom,
                            bool polarity,
                            TNode fact,
                            bool isInternal)
{
}

bool TheoryBags::collectModelValues(TheoryModel* m,
                                    const std::set<Node>& termSet)
{
  Trace("bags-model") << "TheoryBags : Collect model values" << std::endl;

  Trace("bags-model") << "Term set: " << termSet << std::endl;

  std::set<Node> processedBags;

  // get the relevant bag equivalence classes
  for (const Node& n : termSet)
  {
    TypeNode tn = n.getType();
    if (!tn.isBag())
    {
      // we are only concerned here about bag terms
      continue;
    }
    Node r = d_state.getRepresentative(n);
    if (processedBags.find(r) != processedBags.end())
    {
      // skip bags whose representatives are already processed
      continue;
    }

    processedBags.insert(r);

    std::set<Node> solverElements = d_state.getElements(r);
    std::set<Node> elements;
    // only consider terms in termSet and ignore other elements in the solver
    std::set_intersection(termSet.begin(),
                          termSet.end(),
                          solverElements.begin(),
                          solverElements.end(),
                          std::inserter(elements, elements.begin()));
    Trace("bags-model") << "Elements of bag " << n << " are: " << std::endl
                        << elements << std::endl;
    std::map<Node, Node> elementReps;
    for (const Node& e : elements)
    {
      Node key = d_state.getRepresentative(e);
      Node countTerm = NodeManager::currentNM()->mkNode(BAG_COUNT, e, r);
      Node value = d_state.getRepresentative(countTerm);
      elementReps[key] = value;
    }
    Node rep = NormalForm::constructBagFromElements(tn, elementReps);
    rep = Rewriter::rewrite(rep);

    Trace("bags-model") << "rep of " << n << " is: " << rep << std::endl;
    for (std::pair<Node, Node> pair : elementReps)
    {
      m->assertSkeleton(pair.first);
      m->assertSkeleton(pair.second);
    }
    m->assertEquality(rep, n, true);
    m->assertSkeleton(rep);
  }
  return true;
}

TrustNode TheoryBags::explain(TNode node) { return d_im.explainLit(node); }

Node TheoryBags::getModelValue(TNode node) { return Node::null(); }

void TheoryBags::preRegisterTerm(TNode n)
{
  Trace("bags::TheoryBags::preRegisterTerm") << n << std::endl;
  switch (n.getKind())
  {
    case BAG_CARD:
    case BAG_FROM_SET:
    case BAG_TO_SET:
    case BAG_IS_SINGLETON:
    {
      std::stringstream ss;
      ss << "Term of kind " << n.getKind() << " is not supported yet";
      throw LogicException(ss.str());
    }
    default: break;
  }
}

void TheoryBags::presolve() {}

/**************************** eq::NotifyClass *****************************/

void TheoryBags::eqNotifyNewClass(TNode n) {}

void TheoryBags::eqNotifyMerge(TNode n1, TNode n2) {}

void TheoryBags::eqNotifyDisequal(TNode n1, TNode n2, TNode reason) {}

void TheoryBags::NotifyClass::eqNotifyNewClass(TNode n)
{
  Debug("bags-eq") << "[bags-eq] eqNotifyNewClass:"
                   << " n = " << n << std::endl;
  d_theory.eqNotifyNewClass(n);
}

void TheoryBags::NotifyClass::eqNotifyMerge(TNode n1, TNode n2)
{
  Debug("bags-eq") << "[bags-eq] eqNotifyMerge:"
                   << " n1 = " << n1 << " n2 = " << n2 << std::endl;
  d_theory.eqNotifyMerge(n1, n2);
}

void TheoryBags::NotifyClass::eqNotifyDisequal(TNode n1, TNode n2, TNode reason)
{
  Debug("bags-eq") << "[bags-eq] eqNotifyDisequal:"
                   << " n1 = " << n1 << " n2 = " << n2 << " reason = " << reason
                   << std::endl;
  d_theory.eqNotifyDisequal(n1, n2, reason);
}

}  // 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, Haniel Barbosa, Andrew Reynolds
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		* Bags theory.
14		*/
15
16		#include "theory/bags/theory_bags.h"
17
18		#include "proof/proof_checker.h"
19		#include "smt/logic_exception.h"
20		#include "theory/bags/normal_form.h"
21		#include "theory/rewriter.h"
22		#include "theory/theory_model.h"
23
24		using namespace cvc5::kind;
25
26		namespace cvc5 {
27		namespace theory {
28		namespace bags {
29
30	9853	TheoryBags::TheoryBags(context::Context* c,
31		context::UserContext* u,
32		OutputChannel& out,
33		Valuation valuation,
34		const LogicInfo& logicInfo,
35	9853	ProofNodeManager* pnm)
36		: Theory(THEORY_BAGS, c, u, out, valuation, logicInfo, pnm),
37		d_state(c, u, valuation),
38		d_im(*this, d_state, pnm),
39		d_ig(&d_state, &d_im),
40		d_notify(*this, d_im),
41		d_statistics(),
42		d_rewriter(&d_statistics.d_rewrites),
43		d_termReg(d_state, d_im),
44	9853	d_solver(d_state, d_im, d_termReg)
45		{
46		// use the official theory state and inference manager objects
47	9853	d_theoryState = &d_state;
48	9853	d_inferManager = &d_im;
49	9853	}
50
51	19706	TheoryBags::~TheoryBags() {}
52
53	9853	TheoryRewriter* TheoryBags::getTheoryRewriter() { return &d_rewriter; }
54
55	3768	ProofRuleChecker* TheoryBags::getProofChecker() { return nullptr; }
56
57	9853	bool TheoryBags::needsEqualityEngine(EeSetupInfo& esi)
58		{
59	9853	esi.d_notify = &d_notify;
60	9853	esi.d_name = "theory::bags::ee";
61	9853	return true;
62		}
63
64	9853	void TheoryBags::finishInit()
65		{
66	9853	Assert(d_equalityEngine != nullptr);
67
68		// choice is used to eliminate witness
69	9853	d_valuation.setUnevaluatedKind(WITNESS);
70
71		// functions we are doing congruence over
72	9853	d_equalityEngine->addFunctionKind(UNION_MAX);
73	9853	d_equalityEngine->addFunctionKind(UNION_DISJOINT);
74	9853	d_equalityEngine->addFunctionKind(INTERSECTION_MIN);
75	9853	d_equalityEngine->addFunctionKind(DIFFERENCE_SUBTRACT);
76	9853	d_equalityEngine->addFunctionKind(DIFFERENCE_REMOVE);
77	9853	d_equalityEngine->addFunctionKind(BAG_COUNT);
78	9853	d_equalityEngine->addFunctionKind(DUPLICATE_REMOVAL);
79	9853	d_equalityEngine->addFunctionKind(MK_BAG);
80	9853	d_equalityEngine->addFunctionKind(BAG_CARD);
81	9853	d_equalityEngine->addFunctionKind(BAG_FROM_SET);
82	9853	d_equalityEngine->addFunctionKind(BAG_TO_SET);
83	9853	}
84
85	24625	void TheoryBags::postCheck(Effort effort)
86		{
87	24625	d_im.doPendingFacts();
88		// TODO issue #78: add Assert(d_strat.isStrategyInit());
89	24625	if (!d_state.isInConflict() && !d_valuation.needCheck())
90		// TODO issue #78: add && d_strat.hasStrategyEffort(e))
91		{
92	15057	Trace("bags::TheoryBags::postCheck") << "effort: " << std::endl;
93
94		// TODO issue #78: add ++(d_statistics.d_checkRuns);
95	15057	bool sentLemma = false;
96	15057	bool hadPending = false;
97	15057	Trace("bags-check") << "Full effort check..." << std::endl;
98		do
99		{
100	15057	d_im.reset();
101		// TODO issue #78: add ++(d_statistics.d_strategyRuns);
102	15057	Trace("bags-check") << " * Run strategy..." << std::endl;
103		// TODO issue #78: add runStrategy(e);
104
105	15057	d_solver.postCheck();
106
107		// remember if we had pending facts or lemmas
108	15057	hadPending = d_im.hasPending();
109		// Send the facts and the lemmas. We send lemmas regardless of whether
110		// we send facts since some lemmas cannot be dropped. Other lemmas are
111		// otherwise avoided by aborting the strategy when a fact is ready.
112	15057	d_im.doPending();
113		// Did we successfully send a lemma? Notice that if hasPending = true
114		// and sentLemma = false, then the above call may have:
115		// (1) had no pending lemmas, but successfully processed pending facts,
116		// (2) unsuccessfully processed pending lemmas.
117		// In either case, we repeat the strategy if we are not in conflict.
118	15057	sentLemma = d_im.hasSentLemma();
119	15057	if (Trace.isOn("bags-check"))
120		{
121		// TODO: clean this Trace("bags-check") << " ...finish run strategy: ";
122		Trace("bags-check") << (hadPending ? "hadPending " : "");
123		Trace("bags-check") << (sentLemma ? "sentLemma " : "");
124		Trace("bags-check") << (d_state.isInConflict() ? "conflict " : "");
125		if (!hadPending && !sentLemma && !d_state.isInConflict())
126		{
127		Trace("bags-check") << "(none)";
128		}
129		Trace("bags-check") << std::endl;
130		}
131		// repeat if we did not add a lemma or conflict, and we had pending
132		// facts or lemmas.
133	15057	} while (!d_state.isInConflict() && !sentLemma && hadPending);
134		}
135	24625	Trace("bags-check") << "Theory of bags, done check : " << effort << std::endl;
136	24625	Assert(!d_im.hasPendingFact());
137	24625	Assert(!d_im.hasPendingLemma());
138	24625	}
139
140	2649	void TheoryBags::notifyFact(TNode atom,
141		bool polarity,
142		TNode fact,
143		bool isInternal)
144		{
145	2649	}
146
147	4928	bool TheoryBags::collectModelValues(TheoryModel* m,
148		const std::set<Node>& termSet)
149		{
150	4928	Trace("bags-model") << "TheoryBags : Collect model values" << std::endl;
151
152	4928	Trace("bags-model") << "Term set: " << termSet << std::endl;
153
154	9856	std::set<Node> processedBags;
155
156		// get the relevant bag equivalence classes
157	5135	for (const Node& n : termSet)
158		{
159	237	TypeNode tn = n.getType();
160	207	if (!tn.isBag())
161		{
162		// we are only concerned here about bag terms
163	151	continue;
164		}
165	86	Node r = d_state.getRepresentative(n);
166	56	if (processedBags.find(r) != processedBags.end())
167		{
168		// skip bags whose representatives are already processed
169	26	continue;
170		}
171
172	30	processedBags.insert(r);
173
174	60	std::set<Node> solverElements = d_state.getElements(r);
175	60	std::set<Node> elements;
176		// only consider terms in termSet and ignore other elements in the solver
177	30	std::set_intersection(termSet.begin(),
178		termSet.end(),
179		solverElements.begin(),
180		solverElements.end(),
181	30	std::inserter(elements, elements.begin()));
182	60	Trace("bags-model") << "Elements of bag " << n << " are: " << std::endl
183	30	<< elements << std::endl;
184	60	std::map<Node, Node> elementReps;
185	72	for (const Node& e : elements)
186		{
187	84	Node key = d_state.getRepresentative(e);
188	84	Node countTerm = NodeManager::currentNM()->mkNode(BAG_COUNT, e, r);
189	84	Node value = d_state.getRepresentative(countTerm);
190	42	elementReps[key] = value;
191		}
192	60	Node rep = NormalForm::constructBagFromElements(tn, elementReps);
193	30	rep = Rewriter::rewrite(rep);
194
195	30	Trace("bags-model") << "rep of " << n << " is: " << rep << std::endl;
196	72	for (std::pair<Node, Node> pair : elementReps)
197		{
198	42	m->assertSkeleton(pair.first);
199	42	m->assertSkeleton(pair.second);
200		}
201	30	m->assertEquality(rep, n, true);
202	30	m->assertSkeleton(rep);
203		}
204	9856	return true;
205		}
206
207	925	TrustNode TheoryBags::explain(TNode node) { return d_im.explainLit(node); }
208
209		Node TheoryBags::getModelValue(TNode node) { return Node::null(); }
210
211	1367	void TheoryBags::preRegisterTerm(TNode n)
212		{
213	1367	Trace("bags::TheoryBags::preRegisterTerm") << n << std::endl;
214	1367	switch (n.getKind())
215		{
216		case BAG_CARD:
217		case BAG_FROM_SET:
218		case BAG_TO_SET:
219		case BAG_IS_SINGLETON:
220		{
221		std::stringstream ss;
222		ss << "Term of kind " << n.getKind() << " is not supported yet";
223		throw LogicException(ss.str());
224		}
225	1367	default: break;
226		}
227	1367	}
228
229	15204	void TheoryBags::presolve() {}
230
231		/************************** eq::NotifyClass ***************************/
232
233	1181	void TheoryBags::eqNotifyNewClass(TNode n) {}
234
235	1941	void TheoryBags::eqNotifyMerge(TNode n1, TNode n2) {}
236
237	246	void TheoryBags::eqNotifyDisequal(TNode n1, TNode n2, TNode reason) {}
238
239	1181	void TheoryBags::NotifyClass::eqNotifyNewClass(TNode n)
240		{
241	2362	Debug("bags-eq") << "[bags-eq] eqNotifyNewClass:"
242	1181	<< " n = " << n << std::endl;
243	1181	d_theory.eqNotifyNewClass(n);
244	1181	}
245
246	1941	void TheoryBags::NotifyClass::eqNotifyMerge(TNode n1, TNode n2)
247		{
248	3882	Debug("bags-eq") << "[bags-eq] eqNotifyMerge:"
249	1941	<< " n1 = " << n1 << " n2 = " << n2 << std::endl;
250	1941	d_theory.eqNotifyMerge(n1, n2);
251	1941	}
252
253	246	void TheoryBags::NotifyClass::eqNotifyDisequal(TNode n1, TNode n2, TNode reason)
254		{
255	492	Debug("bags-eq") << "[bags-eq] eqNotifyDisequal:"
256	246	<< " n1 = " << n1 << " n2 = " << n2 << " reason = " << reason
257	246	<< std::endl;
258	246	d_theory.eqNotifyDisequal(n1, n2, reason);
259	246	}
260
261		} // namespace bags
262		} // namespace theory
263	29340	} // namespace cvc5