Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/sets/theory_sets.cpp	Lines:	101	110	91.8 %
Date:	2021-08-12	Branches:	137	308	44.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Kshitij Bansal, 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.
 * ****************************************************************************
 *
 * Sets theory.
 */

#include "theory/sets/theory_sets.h"

#include "options/sets_options.h"
#include "theory/sets/theory_sets_private.h"
#include "theory/sets/theory_sets_rewriter.h"
#include "theory/theory_model.h"
#include "theory/trust_substitutions.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace sets {

TheorySets::TheorySets(context::Context* c,
                       context::UserContext* u,
                       OutputChannel& out,
                       Valuation valuation,
                       const LogicInfo& logicInfo,
                       ProofNodeManager* pnm)
    : Theory(THEORY_SETS, c, u, out, valuation, logicInfo, pnm),
      d_skCache(),
      d_state(c, u, valuation, d_skCache),
      d_im(*this, d_state, pnm),
      d_internal(new TheorySetsPrivate(*this, d_state, d_im, d_skCache, pnm)),
      d_notify(*d_internal.get(), d_im)
{
  // use the official theory state and inference manager objects
  d_theoryState = &d_state;
  d_inferManager = &d_im;
}

TheorySets::~TheorySets()
{
}

TheoryRewriter* TheorySets::getTheoryRewriter()
{
  return d_internal->getTheoryRewriter();
}

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

bool TheorySets::needsEqualityEngine(EeSetupInfo& esi)
{
  esi.d_notify = &d_notify;
  esi.d_name = "theory::sets::ee";
  esi.d_notifyNewClass = true;
  esi.d_notifyMerge = true;
  esi.d_notifyDisequal = true;
  return true;
}

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

  d_valuation.setUnevaluatedKind(COMPREHENSION);
  // choice is used to eliminate witness
  d_valuation.setUnevaluatedKind(WITNESS);
  // Universe set is not evaluated. This is moreover important for ensuring that
  // we do not eliminate terms whose value involves the universe set.
  d_valuation.setUnevaluatedKind(UNIVERSE_SET);

  // functions we are doing congruence over
  d_equalityEngine->addFunctionKind(SINGLETON);
  d_equalityEngine->addFunctionKind(UNION);
  d_equalityEngine->addFunctionKind(INTERSECTION);
  d_equalityEngine->addFunctionKind(SETMINUS);
  d_equalityEngine->addFunctionKind(MEMBER);
  d_equalityEngine->addFunctionKind(SUBSET);
  // relation operators
  d_equalityEngine->addFunctionKind(PRODUCT);
  d_equalityEngine->addFunctionKind(JOIN);
  d_equalityEngine->addFunctionKind(TRANSPOSE);
  d_equalityEngine->addFunctionKind(TCLOSURE);
  d_equalityEngine->addFunctionKind(JOIN_IMAGE);
  d_equalityEngine->addFunctionKind(IDEN);
  d_equalityEngine->addFunctionKind(APPLY_CONSTRUCTOR);
  // we do congruence over cardinality
  d_equalityEngine->addFunctionKind(CARD);

  // finish initialization internally
  d_internal->finishInit();
}

void TheorySets::postCheck(Effort level) { d_internal->postCheck(level); }

void TheorySets::notifyFact(TNode atom,
                            bool polarity,
                            TNode fact,
                            bool isInternal)
{
  d_internal->notifyFact(atom, polarity, fact);
}

bool TheorySets::collectModelValues(TheoryModel* m,
                                    const std::set<Node>& termSet)
{
  return d_internal->collectModelValues(m, termSet);
}

void TheorySets::computeCareGraph() {
  d_internal->computeCareGraph();
}

TrustNode TheorySets::explain(TNode node)
{
  Node exp = d_internal->explain(node);
  return TrustNode::mkTrustPropExp(node, exp, nullptr);
}

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

void TheorySets::preRegisterTerm(TNode node)
{
  d_internal->preRegisterTerm(node);
}

TrustNode TheorySets::ppRewrite(TNode n, std::vector<SkolemLemma>& lems)
{
  Kind nk = n.getKind();
  if (nk == UNIVERSE_SET || nk == COMPLEMENT || nk == JOIN_IMAGE
      || nk == COMPREHENSION)
  {
    if (!options::setsExt())
    {
      std::stringstream ss;
      ss << "Extended set operators are not supported in default mode, try "
            "--sets-ext.";
      throw LogicException(ss.str());
    }
  }
  if (nk == COMPREHENSION)
  {
    // set comprehension is an implicit quantifier, require it in the logic
    if (!getLogicInfo().isQuantified())
    {
      std::stringstream ss;
      ss << "Set comprehensions require quantifiers in the background logic.";
      throw LogicException(ss.str());
    }
  }
  return d_internal->ppRewrite(n, lems);
}

Theory::PPAssertStatus TheorySets::ppAssert(
    TrustNode tin, TrustSubstitutionMap& outSubstitutions)
{
  TNode in = tin.getNode();
  Debug("sets-proc") << "ppAssert : " << in << std::endl;
  Theory::PPAssertStatus status = Theory::PP_ASSERT_STATUS_UNSOLVED;

  // this is based off of Theory::ppAssert
  if (in.getKind() == EQUAL)
  {
    if (in[0].isVar() && isLegalElimination(in[0], in[1]))
    {
      // We cannot solve for sets if setsExt is enabled, since universe set
      // may appear when this option is enabled, and solving for such a set
      // impacts the semantics of universe set, see
      // regress0/sets/pre-proc-univ.smt2
      if (!in[0].getType().isSet() || !options::setsExt())
      {
        outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
        status = Theory::PP_ASSERT_STATUS_SOLVED;
      }
    }
    else if (in[1].isVar() && isLegalElimination(in[1], in[0]))
    {
      if (!in[0].getType().isSet() || !options::setsExt())
      {
        outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
        status = Theory::PP_ASSERT_STATUS_SOLVED;
      }
    }
    else if (in[0].isConst() && in[1].isConst())
    {
      if (in[0] != in[1])
      {
        status = Theory::PP_ASSERT_STATUS_CONFLICT;
      }
    }
  }
  return status;
}

void TheorySets::presolve() {
  d_internal->presolve();
}

bool TheorySets::isEntailed( Node n, bool pol ) {
  return d_internal->isEntailed( n, pol );
}

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

void TheorySets::NotifyClass::eqNotifyNewClass(TNode t)
{
  Debug("sets-eq") << "[sets-eq] eqNotifyNewClass:"
                   << " t = " << t << std::endl;
  d_theory.eqNotifyNewClass(t);
}

void TheorySets::NotifyClass::eqNotifyMerge(TNode t1, TNode t2)
{
  Debug("sets-eq") << "[sets-eq] eqNotifyMerge:"
                   << " t1 = " << t1 << " t2 = " << t2 << std::endl;
  d_theory.eqNotifyMerge(t1, t2);
}

void TheorySets::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
{
  Debug("sets-eq") << "[sets-eq] eqNotifyDisequal:"
                   << " t1 = " << t1 << " t2 = " << t2 << " reason = " << reason
                   << std::endl;
  d_theory.eqNotifyDisequal(t1, t2, reason);
}

}  // namespace sets
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Kshitij Bansal, 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		* Sets theory.
14		*/
15
16		#include "theory/sets/theory_sets.h"
17
18		#include "options/sets_options.h"
19		#include "theory/sets/theory_sets_private.h"
20		#include "theory/sets/theory_sets_rewriter.h"
21		#include "theory/theory_model.h"
22		#include "theory/trust_substitutions.h"
23
24		using namespace cvc5::kind;
25
26		namespace cvc5 {
27		namespace theory {
28		namespace sets {
29
30	9851	TheorySets::TheorySets(context::Context* c,
31		context::UserContext* u,
32		OutputChannel& out,
33		Valuation valuation,
34		const LogicInfo& logicInfo,
35	9851	ProofNodeManager* pnm)
36		: Theory(THEORY_SETS, c, u, out, valuation, logicInfo, pnm),
37		d_skCache(),
38		d_state(c, u, valuation, d_skCache),
39		d_im(*this, d_state, pnm),
40	9851	d_internal(new TheorySetsPrivate(*this, d_state, d_im, d_skCache, pnm)),
41	19702	d_notify(*d_internal.get(), d_im)
42		{
43		// use the official theory state and inference manager objects
44	9851	d_theoryState = &d_state;
45	9851	d_inferManager = &d_im;
46	9851	}
47
48	19702	TheorySets::~TheorySets()
49		{
50	19702	}
51
52	9851	TheoryRewriter* TheorySets::getTheoryRewriter()
53		{
54	9851	return d_internal->getTheoryRewriter();
55		}
56
57	3766	ProofRuleChecker* TheorySets::getProofChecker() { return nullptr; }
58
59	9851	bool TheorySets::needsEqualityEngine(EeSetupInfo& esi)
60		{
61	9851	esi.d_notify = &d_notify;
62	9851	esi.d_name = "theory::sets::ee";
63	9851	esi.d_notifyNewClass = true;
64	9851	esi.d_notifyMerge = true;
65	9851	esi.d_notifyDisequal = true;
66	9851	return true;
67		}
68
69	9851	void TheorySets::finishInit()
70		{
71	9851	Assert(d_equalityEngine != nullptr);
72
73	9851	d_valuation.setUnevaluatedKind(COMPREHENSION);
74		// choice is used to eliminate witness
75	9851	d_valuation.setUnevaluatedKind(WITNESS);
76		// Universe set is not evaluated. This is moreover important for ensuring that
77		// we do not eliminate terms whose value involves the universe set.
78	9851	d_valuation.setUnevaluatedKind(UNIVERSE_SET);
79
80		// functions we are doing congruence over
81	9851	d_equalityEngine->addFunctionKind(SINGLETON);
82	9851	d_equalityEngine->addFunctionKind(UNION);
83	9851	d_equalityEngine->addFunctionKind(INTERSECTION);
84	9851	d_equalityEngine->addFunctionKind(SETMINUS);
85	9851	d_equalityEngine->addFunctionKind(MEMBER);
86	9851	d_equalityEngine->addFunctionKind(SUBSET);
87		// relation operators
88	9851	d_equalityEngine->addFunctionKind(PRODUCT);
89	9851	d_equalityEngine->addFunctionKind(JOIN);
90	9851	d_equalityEngine->addFunctionKind(TRANSPOSE);
91	9851	d_equalityEngine->addFunctionKind(TCLOSURE);
92	9851	d_equalityEngine->addFunctionKind(JOIN_IMAGE);
93	9851	d_equalityEngine->addFunctionKind(IDEN);
94	9851	d_equalityEngine->addFunctionKind(APPLY_CONSTRUCTOR);
95		// we do congruence over cardinality
96	9851	d_equalityEngine->addFunctionKind(CARD);
97
98		// finish initialization internally
99	9851	d_internal->finishInit();
100	9851	}
101
102	105995	void TheorySets::postCheck(Effort level) { d_internal->postCheck(level); }
103
104	229125	void TheorySets::notifyFact(TNode atom,
105		bool polarity,
106		TNode fact,
107		bool isInternal)
108		{
109	229125	d_internal->notifyFact(atom, polarity, fact);
110	229125	}
111
112	4956	bool TheorySets::collectModelValues(TheoryModel* m,
113		const std::set<Node>& termSet)
114		{
115	4956	return d_internal->collectModelValues(m, termSet);
116		}
117
118	6672	void TheorySets::computeCareGraph() {
119	6672	d_internal->computeCareGraph();
120	6672	}
121
122	2807	TrustNode TheorySets::explain(TNode node)
123		{
124	5614	Node exp = d_internal->explain(node);
125	5614	return TrustNode::mkTrustPropExp(node, exp, nullptr);
126		}
127
128		Node TheorySets::getModelValue(TNode node) {
129		return Node::null();
130		}
131
132	75657	void TheorySets::preRegisterTerm(TNode node)
133		{
134	75657	d_internal->preRegisterTerm(node);
135	75657	}
136
137	45570	TrustNode TheorySets::ppRewrite(TNode n, std::vector<SkolemLemma>& lems)
138		{
139	45570	Kind nk = n.getKind();
140	45570	if (nk == UNIVERSE_SET \|\| nk == COMPLEMENT \|\| nk == JOIN_IMAGE
141	45073	\|\| nk == COMPREHENSION)
142		{
143	520	if (!options::setsExt())
144		{
145	4	std::stringstream ss;
146	2	ss << "Extended set operators are not supported in default mode, try "
147		"--sets-ext.";
148	2	throw LogicException(ss.str());
149		}
150		}
151	45568	if (nk == COMPREHENSION)
152		{
153		// set comprehension is an implicit quantifier, require it in the logic
154	23	if (!getLogicInfo().isQuantified())
155		{
156	2	std::stringstream ss;
157	1	ss << "Set comprehensions require quantifiers in the background logic.";
158	1	throw LogicException(ss.str());
159		}
160		}
161	45567	return d_internal->ppRewrite(n, lems);
162		}
163
164	2297	Theory::PPAssertStatus TheorySets::ppAssert(
165		TrustNode tin, TrustSubstitutionMap& outSubstitutions)
166		{
167	4594	TNode in = tin.getNode();
168	2297	Debug("sets-proc") << "ppAssert : " << in << std::endl;
169	2297	Theory::PPAssertStatus status = Theory::PP_ASSERT_STATUS_UNSOLVED;
170
171		// this is based off of Theory::ppAssert
172	2297	if (in.getKind() == EQUAL)
173		{
174	682	if (in[0].isVar() && isLegalElimination(in[0], in[1]))
175		{
176		// We cannot solve for sets if setsExt is enabled, since universe set
177		// may appear when this option is enabled, and solving for such a set
178		// impacts the semantics of universe set, see
179		// regress0/sets/pre-proc-univ.smt2
180	305	if (!in[0].getType().isSet() \|\| !options::setsExt())
181		{
182	277	outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
183	277	status = Theory::PP_ASSERT_STATUS_SOLVED;
184		}
185		}
186	377	else if (in[1].isVar() && isLegalElimination(in[1], in[0]))
187		{
188		if (!in[0].getType().isSet() \|\| !options::setsExt())
189		{
190		outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
191		status = Theory::PP_ASSERT_STATUS_SOLVED;
192		}
193		}
194	377	else if (in[0].isConst() && in[1].isConst())
195		{
196		if (in[0] != in[1])
197		{
198		status = Theory::PP_ASSERT_STATUS_CONFLICT;
199		}
200		}
201		}
202	4594	return status;
203		}
204
205	15202	void TheorySets::presolve() {
206	15202	d_internal->presolve();
207	15202	}
208
209		bool TheorySets::isEntailed( Node n, bool pol ) {
210		return d_internal->isEntailed( n, pol );
211		}
212
213		/************************** eq::NotifyClass ***************************/
214
215	84337	void TheorySets::NotifyClass::eqNotifyNewClass(TNode t)
216		{
217	168674	Debug("sets-eq") << "[sets-eq] eqNotifyNewClass:"
218	84337	<< " t = " << t << std::endl;
219	84337	d_theory.eqNotifyNewClass(t);
220	84337	}
221
222	266534	void TheorySets::NotifyClass::eqNotifyMerge(TNode t1, TNode t2)
223		{
224	533068	Debug("sets-eq") << "[sets-eq] eqNotifyMerge:"
225	266534	<< " t1 = " << t1 << " t2 = " << t2 << std::endl;
226	266534	d_theory.eqNotifyMerge(t1, t2);
227	266534	}
228
229	33876	void TheorySets::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
230		{
231	67752	Debug("sets-eq") << "[sets-eq] eqNotifyDisequal:"
232	33876	<< " t1 = " << t1 << " t2 = " << t2 << " reason = " << reason
233	33876	<< std::endl;
234	33876	d_theory.eqNotifyDisequal(t1, t2, reason);
235	33876	}
236
237		} // namespace sets
238		} // namespace theory
239	29337	} // namespace cvc5