Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/datatypes/inference_manager.cpp	Lines:	65	65	100.0 %
Date:	2021-09-08	Branches:	135	244	55.3 %


/******************************************************************************
 * 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.
 * ****************************************************************************
 *
 * Datatypes inference manager.
 */

#include "theory/datatypes/inference_manager.h"

#include "expr/dtype.h"
#include "options/datatypes_options.h"
#include "proof/eager_proof_generator.h"
#include "smt/smt_statistics_registry.h"
#include "theory/rewriter.h"
#include "theory/theory.h"
#include "theory/theory_state.h"
#include "theory/trust_substitutions.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace datatypes {

InferenceManager::InferenceManager(Env& env,
                                   Theory& t,
                                   TheoryState& state,
                                   ProofNodeManager* pnm)
    : InferenceManagerBuffered(env, t, state, pnm, "theory::datatypes::"),
      d_pnm(pnm),
      d_ipc(pnm == nullptr ? nullptr
                           : new InferProofCons(state.getSatContext(), pnm)),
      d_lemPg(pnm == nullptr
                  ? nullptr
                  : new EagerProofGenerator(
                      pnm, state.getUserContext(), "datatypes::lemPg"))
{
  d_false = NodeManager::currentNM()->mkConst(false);
}

InferenceManager::~InferenceManager()
{
}

void InferenceManager::addPendingInference(Node conc,
                                           InferenceId id,
                                           Node exp,
                                           bool forceLemma)
{
  // if we are forcing the inference to be processed as a lemma, or if the
  // inference must be sent as a lemma based on the policy in
  // mustCommunicateFact.
  if (forceLemma || DatatypesInference::mustCommunicateFact(conc, exp))
  {
    d_pendingLem.emplace_back(new DatatypesInference(this, conc, exp, id));
  }
  else
  {
    d_pendingFact.emplace_back(new DatatypesInference(this, conc, exp, id));
  }
}

void InferenceManager::process()
{
  // if we are in conflict, immediately reset and clear pending
  if (d_theoryState.isInConflict())
  {
    reset();
    clearPending();
    return;
  }
  // process pending lemmas, used infrequently, only for definitional lemmas
  doPendingLemmas();
  // now process the pending facts
  doPendingFacts();
}

void InferenceManager::sendDtLemma(Node lem, InferenceId id, LemmaProperty p)
{
  if (isProofEnabled())
  {
    TrustNode trn = processDtLemma(lem, Node::null(), id);
    trustedLemma(trn, id);
    return;
  }
  // otherwise send as a normal lemma directly
  lemma(lem, id, p);
}

void InferenceManager::sendDtConflict(const std::vector<Node>& conf, InferenceId id)
{
  if (isProofEnabled())
  {
    Node exp = NodeManager::currentNM()->mkAnd(conf);
    prepareDtInference(d_false, exp, id, d_ipc.get());
  }
  conflictExp(id, conf, d_ipc.get());
}

bool InferenceManager::isProofEnabled() const { return d_ipc != nullptr; }

TrustNode InferenceManager::processDtLemma(Node conc, Node exp, InferenceId id)
{
  // set up a proof constructor
  std::shared_ptr<InferProofCons> ipcl;
  if (isProofEnabled())
  {
    ipcl = std::make_shared<InferProofCons>(nullptr, d_pnm);
  }
  conc = prepareDtInference(conc, exp, id, ipcl.get());
  // send it as a lemma
  Node lem;
  if (!exp.isNull() && !exp.isConst())
  {
    lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, exp, conc);
  }
  else
  {
    lem = conc;
  }
  if (isProofEnabled())
  {
    // store its proof
    std::shared_ptr<ProofNode> pbody = ipcl->getProofFor(conc);
    std::shared_ptr<ProofNode> pn = pbody;
    if (!exp.isNull() && !exp.isConst())
    {
      std::vector<Node> expv;
      expv.push_back(exp);
      pn = d_pnm->mkScope(pbody, expv);
    }
    d_lemPg->setProofFor(lem, pn);
  }
  return TrustNode::mkTrustLemma(lem, d_lemPg.get());
}

Node InferenceManager::processDtFact(Node conc,
                                     Node exp,
                                     InferenceId id,
                                     ProofGenerator*& pg)
{
  pg = d_ipc.get();
  return prepareDtInference(conc, exp, id, d_ipc.get());
}

Node InferenceManager::prepareDtInference(Node conc,
                                          Node exp,
                                          InferenceId id,
                                          InferProofCons* ipc)
{
  Trace("dt-lemma-debug") << "prepareDtInference : " << conc << " via " << exp
                          << " by " << id << std::endl;
  if (conc.getKind() == EQUAL && conc[0].getType().isBoolean())
  {
    // must turn (= conc false) into (not conc)
    conc = Rewriter::rewrite(conc);
  }
  if (isProofEnabled())
  {
    Assert(ipc != nullptr);
    // If proofs are enabled, notify the proof constructor.
    // Notice that we have to reconstruct a datatypes inference here. This is
    // because the inference in the pending vector may be destroyed as we are
    // processing this inference, if we triggered to backtrack based on the
    // call below, since it is a unique pointer.
    std::shared_ptr<DatatypesInference> di =
        std::make_shared<DatatypesInference>(this, conc, exp, id);
    ipc->notifyFact(di);
  }
  return conc;
}

}  // namespace datatypes
}  // 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		* Datatypes inference manager.
14		*/
15
16		#include "theory/datatypes/inference_manager.h"
17
18		#include "expr/dtype.h"
19		#include "options/datatypes_options.h"
20		#include "proof/eager_proof_generator.h"
21		#include "smt/smt_statistics_registry.h"
22		#include "theory/rewriter.h"
23		#include "theory/theory.h"
24		#include "theory/theory_state.h"
25		#include "theory/trust_substitutions.h"
26
27		using namespace cvc5::kind;
28
29		namespace cvc5 {
30		namespace theory {
31		namespace datatypes {
32
33	9924	InferenceManager::InferenceManager(Env& env,
34		Theory& t,
35		TheoryState& state,
36	9924	ProofNodeManager* pnm)
37		: InferenceManagerBuffered(env, t, state, pnm, "theory::datatypes::"),
38		d_pnm(pnm),
39		d_ipc(pnm == nullptr ? nullptr
40	1243	: new InferProofCons(state.getSatContext(), pnm)),
41		d_lemPg(pnm == nullptr
42		? nullptr
43		: new EagerProofGenerator(
44	11167	pnm, state.getUserContext(), "datatypes::lemPg"))
45		{
46	9924	d_false = NodeManager::currentNM()->mkConst(false);
47	9924	}
48
49	9921	InferenceManager::~InferenceManager()
50		{
51	9921	}
52
53	303194	void InferenceManager::addPendingInference(Node conc,
54		InferenceId id,
55		Node exp,
56		bool forceLemma)
57		{
58		// if we are forcing the inference to be processed as a lemma, or if the
59		// inference must be sent as a lemma based on the policy in
60		// mustCommunicateFact.
61	303194	if (forceLemma \|\| DatatypesInference::mustCommunicateFact(conc, exp))
62		{
63	22520	d_pendingLem.emplace_back(new DatatypesInference(this, conc, exp, id));
64		}
65		else
66		{
67	280674	d_pendingFact.emplace_back(new DatatypesInference(this, conc, exp, id));
68		}
69	303194	}
70
71	2605161	void InferenceManager::process()
72		{
73		// if we are in conflict, immediately reset and clear pending
74	2605161	if (d_theoryState.isInConflict())
75		{
76	11401	reset();
77	11401	clearPending();
78	11401	return;
79		}
80		// process pending lemmas, used infrequently, only for definitional lemmas
81	2593760	doPendingLemmas();
82		// now process the pending facts
83	2593760	doPendingFacts();
84		}
85
86	1281	void InferenceManager::sendDtLemma(Node lem, InferenceId id, LemmaProperty p)
87		{
88	1281	if (isProofEnabled())
89		{
90	182	TrustNode trn = processDtLemma(lem, Node::null(), id);
91	91	trustedLemma(trn, id);
92	91	return;
93		}
94		// otherwise send as a normal lemma directly
95	1190	lemma(lem, id, p);
96		}
97
98	2470	void InferenceManager::sendDtConflict(const std::vector<Node>& conf, InferenceId id)
99		{
100	2470	if (isProofEnabled())
101		{
102	372	Node exp = NodeManager::currentNM()->mkAnd(conf);
103	186	prepareDtInference(d_false, exp, id, d_ipc.get());
104		}
105	2470	conflictExp(id, conf, d_ipc.get());
106	2470	}
107
108	348763	bool InferenceManager::isProofEnabled() const { return d_ipc != nullptr; }
109
110	22456	TrustNode InferenceManager::processDtLemma(Node conc, Node exp, InferenceId id)
111		{
112		// set up a proof constructor
113	44912	std::shared_ptr<InferProofCons> ipcl;
114	22456	if (isProofEnabled())
115		{
116	981	ipcl = std::make_shared<InferProofCons>(nullptr, d_pnm);
117		}
118	22456	conc = prepareDtInference(conc, exp, id, ipcl.get());
119		// send it as a lemma
120	44912	Node lem;
121	22456	if (!exp.isNull() && !exp.isConst())
122		{
123	21698	lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, exp, conc);
124		}
125		else
126		{
127	758	lem = conc;
128		}
129	22456	if (isProofEnabled())
130		{
131		// store its proof
132	1962	std::shared_ptr<ProofNode> pbody = ipcl->getProofFor(conc);
133	1962	std::shared_ptr<ProofNode> pn = pbody;
134	981	if (!exp.isNull() && !exp.isConst())
135		{
136	1546	std::vector<Node> expv;
137	773	expv.push_back(exp);
138	773	pn = d_pnm->mkScope(pbody, expv);
139		}
140	981	d_lemPg->setProofFor(lem, pn);
141		}
142	44912	return TrustNode::mkTrustLemma(lem, d_lemPg.get());
143		}
144
145	277458	Node InferenceManager::processDtFact(Node conc,
146		Node exp,
147		InferenceId id,
148		ProofGenerator*& pg)
149		{
150	277458	pg = d_ipc.get();
151	277458	return prepareDtInference(conc, exp, id, d_ipc.get());
152		}
153
154	300100	Node InferenceManager::prepareDtInference(Node conc,
155		Node exp,
156		InferenceId id,
157		InferProofCons* ipc)
158		{
159	600200	Trace("dt-lemma-debug") << "prepareDtInference : " << conc << " via " << exp
160	300100	<< " by " << id << std::endl;
161	300100	if (conc.getKind() == EQUAL && conc[0].getType().isBoolean())
162		{
163		// must turn (= conc false) into (not conc)
164	508	conc = Rewriter::rewrite(conc);
165		}
166	300100	if (isProofEnabled())
167		{
168	11381	Assert(ipc != nullptr);
169		// If proofs are enabled, notify the proof constructor.
170		// Notice that we have to reconstruct a datatypes inference here. This is
171		// because the inference in the pending vector may be destroyed as we are
172		// processing this inference, if we triggered to backtrack based on the
173		// call below, since it is a unique pointer.
174		std::shared_ptr<DatatypesInference> di =
175	22762	std::make_shared<DatatypesInference>(this, conc, exp, id);
176	11381	ipc->notifyFact(di);
177		}
178	300100	return conc;
179		}
180
181		} // namespace datatypes
182		} // namespace theory
183	29499	} // namespace cvc5