Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/sets/inference_manager.cpp	Lines:	47	90	52.2 %
Date:	2021-09-14	Branches:	102	396	25.8 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Gereon Kremer, Aina Niemetz
 *
 * 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.
 * ****************************************************************************
 *
 * Implementation of the inference manager for the theory of sets.
 */

#include "theory/sets/inference_manager.h"

#include "options/sets_options.h"
#include "theory/rewriter.h"

using namespace std;
using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace sets {

InferenceManager::InferenceManager(Env& env,
                                   Theory& t,
                                   SolverState& s,
                                   ProofNodeManager* pnm)
    : InferenceManagerBuffered(env, t, s, pnm, "theory::sets::"), d_state(s)
{
  d_true = NodeManager::currentNM()->mkConst(true);
  d_false = NodeManager::currentNM()->mkConst(false);
}

bool InferenceManager::assertFactRec(Node fact, InferenceId id, Node exp, int inferType)
{
  // should we send this fact out as a lemma?
  if ((options::setsInferAsLemmas() && inferType != -1) || inferType == 1)
  {
    if (d_state.isEntailed(fact, true))
    {
      return false;
    }
    Node lem = fact;
    if (exp != d_true)
    {
      lem = NodeManager::currentNM()->mkNode(IMPLIES, exp, fact);
    }
    addPendingLemma(lem, id);
    return true;
  }
  Trace("sets-fact") << "Assert fact rec : " << fact << ", exp = " << exp
                     << std::endl;
  if (fact.isConst())
  {
    // either trivial or a conflict
    if (fact == d_false)
    {
      Trace("sets-lemma") << "Conflict : " << exp << std::endl;
      conflict(exp, id);
      return true;
    }
    return false;
  }
  else if (fact.getKind() == AND
           || (fact.getKind() == NOT && fact[0].getKind() == OR))
  {
    bool ret = false;
    Node f = fact.getKind() == NOT ? fact[0] : fact;
    for (unsigned i = 0; i < f.getNumChildren(); i++)
    {
      Node factc = fact.getKind() == NOT ? f[i].negate() : f[i];
      bool tret = assertFactRec(factc, id, exp, inferType);
      ret = ret || tret;
      if (d_state.isInConflict())
      {
        return true;
      }
    }
    return ret;
  }
  bool polarity = fact.getKind() != NOT;
  TNode atom = polarity ? fact : fact[0];
  if (d_state.isEntailed(atom, polarity))
  {
    return false;
  }
  // things we can assert to equality engine
  if (atom.getKind() == MEMBER
      || (atom.getKind() == EQUAL && atom[0].getType().isSet()))
  {
    // send to equality engine
    if (assertSetsFact(atom, polarity, id, exp))
    {
      // return true if this wasn't redundant
      return true;
    }
  }
  else
  {
    // must send as lemma
    Node lem = fact;
    if (exp != d_true)
    {
      lem = NodeManager::currentNM()->mkNode(IMPLIES, exp, fact);
    }
    addPendingLemma(lem, id);
    return true;
  }
  return false;
}

bool InferenceManager::assertSetsFact(Node atom,
                                      bool polarity,
                                      InferenceId id,
                                      Node exp)
{
  Node conc = polarity ? atom : atom.notNode();
  return assertInternalFact(
      atom, polarity, id, PfRule::THEORY_INFERENCE, {exp}, {conc});
}

void InferenceManager::assertInference(Node fact,
                                       InferenceId id,
                                       Node exp,
                                       int inferType)
{
  if (assertFactRec(fact, id, exp, inferType))
  {
    Trace("sets-lemma") << "Sets::Lemma : " << fact << " from " << exp << " by "
                        << id << std::endl;
    Trace("sets-assertion") << "(assert (=> " << exp << " " << fact
                            << ")) ; by " << id << std::endl;
  }
}

void InferenceManager::assertInference(Node fact,
                                       InferenceId id,
                                       std::vector<Node>& exp,
                                       int inferType)
{
  Node exp_n = exp.empty() ? d_true
                           : (exp.size() == 1
                                  ? exp[0]
                                  : NodeManager::currentNM()->mkNode(AND, exp));
  assertInference(fact, id, exp_n, inferType);
}

void InferenceManager::assertInference(std::vector<Node>& conc,
                                       InferenceId id,
                                       Node exp,
                                       int inferType)
{
  if (!conc.empty())
  {
    Node fact = conc.size() == 1 ? conc[0]
                                 : NodeManager::currentNM()->mkNode(AND, conc);
    assertInference(fact, id, exp, inferType);
  }
}
void InferenceManager::assertInference(std::vector<Node>& conc,
                                       InferenceId id,
                                       std::vector<Node>& exp,
                                       int inferType)
{
  Node exp_n = exp.empty() ? d_true
                           : (exp.size() == 1
                                  ? exp[0]
                                  : NodeManager::currentNM()->mkNode(AND, exp));
  assertInference(conc, id, exp_n, inferType);
}

void InferenceManager::split(Node n, InferenceId id, int reqPol)
{
  n = Rewriter::rewrite(n);
  Node lem = NodeManager::currentNM()->mkNode(OR, n, n.negate());
  // send the lemma
  lemma(lem, id);
  Trace("sets-lemma") << "Sets::Lemma split : " << lem << std::endl;
  if (reqPol != 0)
  {
    Trace("sets-lemma") << "Sets::Require phase " << n << " " << (reqPol > 0)
                        << std::endl;
    requirePhase(n, reqPol > 0);
  }
}

}  // 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, Gereon Kremer, Aina Niemetz
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		* Implementation of the inference manager for the theory of sets.
14		*/
15
16		#include "theory/sets/inference_manager.h"
17
18		#include "options/sets_options.h"
19		#include "theory/rewriter.h"
20
21		using namespace std;
22		using namespace cvc5::kind;
23
24		namespace cvc5 {
25		namespace theory {
26		namespace sets {
27
28	9917	InferenceManager::InferenceManager(Env& env,
29		Theory& t,
30		SolverState& s,
31	9917	ProofNodeManager* pnm)
32	9917	: InferenceManagerBuffered(env, t, s, pnm, "theory::sets::"), d_state(s)
33		{
34	9917	d_true = NodeManager::currentNM()->mkConst(true);
35	9917	d_false = NodeManager::currentNM()->mkConst(false);
36	9917	}
37
38	75683	bool InferenceManager::assertFactRec(Node fact, InferenceId id, Node exp, int inferType)
39		{
40		// should we send this fact out as a lemma?
41	75683	if ((options::setsInferAsLemmas() && inferType != -1) \|\| inferType == 1)
42		{
43	75683	if (d_state.isEntailed(fact, true))
44		{
45	58109	return false;
46		}
47	35148	Node lem = fact;
48	17574	if (exp != d_true)
49		{
50	12682	lem = NodeManager::currentNM()->mkNode(IMPLIES, exp, fact);
51		}
52	17574	addPendingLemma(lem, id);
53	17574	return true;
54		}
55		Trace("sets-fact") << "Assert fact rec : " << fact << ", exp = " << exp
56		<< std::endl;
57		if (fact.isConst())
58		{
59		// either trivial or a conflict
60		if (fact == d_false)
61		{
62		Trace("sets-lemma") << "Conflict : " << exp << std::endl;
63		conflict(exp, id);
64		return true;
65		}
66		return false;
67		}
68		else if (fact.getKind() == AND
69		\|\| (fact.getKind() == NOT && fact[0].getKind() == OR))
70		{
71		bool ret = false;
72		Node f = fact.getKind() == NOT ? fact[0] : fact;
73		for (unsigned i = 0; i < f.getNumChildren(); i++)
74		{
75		Node factc = fact.getKind() == NOT ? f[i].negate() : f[i];
76		bool tret = assertFactRec(factc, id, exp, inferType);
77		ret = ret \|\| tret;
78		if (d_state.isInConflict())
79		{
80		return true;
81		}
82		}
83		return ret;
84		}
85		bool polarity = fact.getKind() != NOT;
86		TNode atom = polarity ? fact : fact[0];
87		if (d_state.isEntailed(atom, polarity))
88		{
89		return false;
90		}
91		// things we can assert to equality engine
92		if (atom.getKind() == MEMBER
93		\|\| (atom.getKind() == EQUAL && atom[0].getType().isSet()))
94		{
95		// send to equality engine
96		if (assertSetsFact(atom, polarity, id, exp))
97		{
98		// return true if this wasn't redundant
99		return true;
100		}
101		}
102		else
103		{
104		// must send as lemma
105		Node lem = fact;
106		if (exp != d_true)
107		{
108		lem = NodeManager::currentNM()->mkNode(IMPLIES, exp, fact);
109		}
110		addPendingLemma(lem, id);
111		return true;
112		}
113		return false;
114		}
115
116	14267	bool InferenceManager::assertSetsFact(Node atom,
117		bool polarity,
118		InferenceId id,
119		Node exp)
120		{
121	28534	Node conc = polarity ? atom : atom.notNode();
122	57068	return assertInternalFact(
123	57068	atom, polarity, id, PfRule::THEORY_INFERENCE, {exp}, {conc});
124		}
125
126	75683	void InferenceManager::assertInference(Node fact,
127		InferenceId id,
128		Node exp,
129		int inferType)
130		{
131	75683	if (assertFactRec(fact, id, exp, inferType))
132		{
133	35148	Trace("sets-lemma") << "Sets::Lemma : " << fact << " from " << exp << " by "
134	17574	<< id << std::endl;
135	35148	Trace("sets-assertion") << "(assert (=> " << exp << " " << fact
136	17574	<< ")) ; by " << id << std::endl;
137		}
138	75683	}
139
140	63080	void InferenceManager::assertInference(Node fact,
141		InferenceId id,
142		std::vector<Node>& exp,
143		int inferType)
144		{
145	63080	Node exp_n = exp.empty() ? d_true
146	59661	: (exp.size() == 1
147	2668	? exp[0]
148	188489	: NodeManager::currentNM()->mkNode(AND, exp));
149	63080	assertInference(fact, id, exp_n, inferType);
150	63080	}
151
152	5422	void InferenceManager::assertInference(std::vector<Node>& conc,
153		InferenceId id,
154		Node exp,
155		int inferType)
156		{
157	5422	if (!conc.empty())
158		{
159	829	Node fact = conc.size() == 1 ? conc[0]
160	1268	: NodeManager::currentNM()->mkNode(AND, conc);
161	439	assertInference(fact, id, exp, inferType);
162		}
163	5422	}
164		void InferenceManager::assertInference(std::vector<Node>& conc,
165		InferenceId id,
166		std::vector<Node>& exp,
167		int inferType)
168		{
169		Node exp_n = exp.empty() ? d_true
170		: (exp.size() == 1
171		? exp[0]
172		: NodeManager::currentNM()->mkNode(AND, exp));
173		assertInference(conc, id, exp_n, inferType);
174		}
175
176	393	void InferenceManager::split(Node n, InferenceId id, int reqPol)
177		{
178	393	n = Rewriter::rewrite(n);
179	786	Node lem = NodeManager::currentNM()->mkNode(OR, n, n.negate());
180		// send the lemma
181	393	lemma(lem, id);
182	393	Trace("sets-lemma") << "Sets::Lemma split : " << lem << std::endl;
183	393	if (reqPol != 0)
184		{
185		Trace("sets-lemma") << "Sets::Require phase " << n << " " << (reqPol > 0)
186		<< std::endl;
187		requirePhase(n, reqPol > 0);
188		}
189	393	}
190
191		} // namespace sets
192		} // namespace theory
193	29517	} // namespace cvc5