Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/prop/theory_proxy.cpp	Lines:	97	103	94.2 %
Date:	2021-05-24	Branches:	138	328	42.1 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Haniel Barbosa, Dejan Jovanovic
 *
 * 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.
 * ****************************************************************************
 *
 * [[ Add one-line brief description here ]]
 *
 * [[ Add lengthier description here ]]
 * \todo document this file
 */
#include "prop/theory_proxy.h"

#include "context/context.h"
#include "decision/decision_engine.h"
#include "options/decision_options.h"
#include "options/smt_options.h"
#include "prop/cnf_stream.h"
#include "prop/prop_engine.h"
#include "prop/skolem_def_manager.h"
#include "smt/smt_statistics_registry.h"
#include "theory/rewriter.h"
#include "theory/theory_engine.h"
#include "util/statistics_stats.h"

namespace cvc5 {
namespace prop {

TheoryProxy::TheoryProxy(PropEngine* propEngine,
                         TheoryEngine* theoryEngine,
                         decision::DecisionEngine* decisionEngine,
                         SkolemDefManager* skdm,
                         context::Context* context,
                         context::UserContext* userContext,
                         ProofNodeManager* pnm)
    : d_propEngine(propEngine),
      d_cnfStream(nullptr),
      d_decisionEngine(decisionEngine),
      d_theoryEngine(theoryEngine),
      d_queue(context),
      d_tpp(*theoryEngine, userContext, pnm),
      d_skdm(skdm)
{
}

TheoryProxy::~TheoryProxy() {
  /* nothing to do for now */
}

void TheoryProxy::finishInit(CnfStream* cnfStream) { d_cnfStream = cnfStream; }

void TheoryProxy::notifyAssertion(Node a, TNode skolem)
{
  if (skolem.isNull())
  {
    d_decisionEngine->addAssertion(a);
  }
  else
  {
    d_skdm->notifySkolemDefinition(skolem, a);
    d_decisionEngine->addSkolemDefinition(a, skolem);
  }
}

void TheoryProxy::variableNotify(SatVariable var) {
  d_theoryEngine->preRegister(getNode(SatLiteral(var)));
}

void TheoryProxy::theoryCheck(theory::Theory::Effort effort) {
  while (!d_queue.empty()) {
    TNode assertion = d_queue.front();
    d_queue.pop();
    d_theoryEngine->assertFact(assertion);
  }
  d_theoryEngine->check(effort);
}

void TheoryProxy::theoryPropagate(std::vector<SatLiteral>& output) {
  // Get the propagated literals
  std::vector<TNode> outputNodes;
  d_theoryEngine->getPropagatedLiterals(outputNodes);
  for (unsigned i = 0, i_end = outputNodes.size(); i < i_end; ++ i) {
    Debug("prop-explain") << "theoryPropagate() => " << outputNodes[i] << std::endl;
    output.push_back(d_cnfStream->getLiteral(outputNodes[i]));
  }
}

void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
  TNode lNode = d_cnfStream->getNode(l);
  Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl;

  theory::TrustNode tte = d_theoryEngine->getExplanation(lNode);
  Node theoryExplanation = tte.getNode();
  if (options::produceProofs()
      && options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS)
  {
    Assert(options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF
           || tte.getGenerator());
    d_propEngine->getProofCnfStream()->convertPropagation(tte);
  }
  Debug("prop-explain") << "explainPropagation() => " << theoryExplanation
                        << std::endl;
  explanation.push_back(l);
  if (theoryExplanation.getKind() == kind::AND)
  {
    for (const Node& n : theoryExplanation)
    {
      explanation.push_back(~d_cnfStream->getLiteral(n));
    }
  }
  else
  {
    explanation.push_back(~d_cnfStream->getLiteral(theoryExplanation));
  }
  if (Trace.isOn("sat-proof"))
  {
    std::stringstream ss;
    ss << "TheoryProxy::explainPropagation: clause for lit is ";
    for (unsigned i = 0, size = explanation.size(); i < size; ++i)
    {
      ss << explanation[i] << " [" << d_cnfStream->getNode(explanation[i])
         << "] ";
    }
    Trace("sat-proof") << ss.str() << "\n";
  }
}

void TheoryProxy::enqueueTheoryLiteral(const SatLiteral& l) {
  Node literalNode = d_cnfStream->getNode(l);
  Debug("prop") << "enqueueing theory literal " << l << " " << literalNode << std::endl;
  Assert(!literalNode.isNull());
  d_queue.push(literalNode);
}

SatLiteral TheoryProxy::getNextTheoryDecisionRequest() {
  TNode n = d_theoryEngine->getNextDecisionRequest();
  return n.isNull() ? undefSatLiteral : d_cnfStream->getLiteral(n);
}

SatLiteral TheoryProxy::getNextDecisionEngineRequest(bool &stopSearch) {
  Assert(d_decisionEngine != NULL);
  Assert(stopSearch != true);
  SatLiteral ret = d_decisionEngine->getNext(stopSearch);
  if(stopSearch) {
    Trace("decision") << "  ***  Decision Engine stopped search *** " << std::endl;
  }
  return options::decisionStopOnly() ? undefSatLiteral : ret;
}

bool TheoryProxy::theoryNeedCheck() const {
  return d_theoryEngine->needCheck();
}

TNode TheoryProxy::getNode(SatLiteral lit) {
  return d_cnfStream->getNode(lit);
}

void TheoryProxy::notifyRestart() {
  d_propEngine->spendResource(Resource::RestartStep);
  d_theoryEngine->notifyRestart();
}

void TheoryProxy::spendResource(Resource r)
{
  d_theoryEngine->spendResource(r);
}

bool TheoryProxy::isDecisionRelevant(SatVariable var) { return true; }

bool TheoryProxy::isDecisionEngineDone() {
  return d_decisionEngine->isDone();
}

SatValue TheoryProxy::getDecisionPolarity(SatVariable var) {
  return SAT_VALUE_UNKNOWN;
}

CnfStream* TheoryProxy::getCnfStream() { return d_cnfStream; }

theory::TrustNode TheoryProxy::preprocessLemma(
    theory::TrustNode trn,
    std::vector<theory::TrustNode>& newLemmas,
    std::vector<Node>& newSkolems)
{
  return d_tpp.preprocessLemma(trn, newLemmas, newSkolems);
}

theory::TrustNode TheoryProxy::preprocess(
    TNode node,
    std::vector<theory::TrustNode>& newLemmas,
    std::vector<Node>& newSkolems)
{
  return d_tpp.preprocess(node, newLemmas, newSkolems);
}

theory::TrustNode TheoryProxy::removeItes(
    TNode node,
    std::vector<theory::TrustNode>& newLemmas,
    std::vector<Node>& newSkolems)
{
  RemoveTermFormulas& rtf = d_tpp.getRemoveTermFormulas();
  return rtf.run(node, newLemmas, newSkolems, true);
}

void TheoryProxy::getSkolems(TNode node,
                             std::vector<Node>& skAsserts,
                             std::vector<Node>& sks)
{
  std::unordered_set<Node> skolems;
  d_skdm->getSkolems(node, skolems);
  for (const Node& k : skolems)
  {
    sks.push_back(k);
    skAsserts.push_back(d_skdm->getDefinitionForSkolem(k));
  }
}

void TheoryProxy::preRegister(Node n) { d_theoryEngine->preRegister(n); }

}  // namespace prop
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Haniel Barbosa, Dejan Jovanovic
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		* [[ Add one-line brief description here ]]
14		*
15		* [[ Add lengthier description here ]]
16		* \todo document this file
17		*/
18		#include "prop/theory_proxy.h"
19
20		#include "context/context.h"
21		#include "decision/decision_engine.h"
22		#include "options/decision_options.h"
23		#include "options/smt_options.h"
24		#include "prop/cnf_stream.h"
25		#include "prop/prop_engine.h"
26		#include "prop/skolem_def_manager.h"
27		#include "smt/smt_statistics_registry.h"
28		#include "theory/rewriter.h"
29		#include "theory/theory_engine.h"
30		#include "util/statistics_stats.h"
31
32		namespace cvc5 {
33		namespace prop {
34
35	9494	TheoryProxy::TheoryProxy(PropEngine* propEngine,
36		TheoryEngine* theoryEngine,
37		decision::DecisionEngine* decisionEngine,
38		SkolemDefManager* skdm,
39		context::Context* context,
40		context::UserContext* userContext,
41	9494	ProofNodeManager* pnm)
42		: d_propEngine(propEngine),
43		d_cnfStream(nullptr),
44		d_decisionEngine(decisionEngine),
45		d_theoryEngine(theoryEngine),
46		d_queue(context),
47		d_tpp(*theoryEngine, userContext, pnm),
48	9494	d_skdm(skdm)
49		{
50	9494	}
51
52	18988	TheoryProxy::~TheoryProxy() {
53		/* nothing to do for now */
54	18988	}
55
56	9494	void TheoryProxy::finishInit(CnfStream* cnfStream) { d_cnfStream = cnfStream; }
57
58	434429	void TheoryProxy::notifyAssertion(Node a, TNode skolem)
59		{
60	434429	if (skolem.isNull())
61		{
62	403559	d_decisionEngine->addAssertion(a);
63		}
64		else
65		{
66	30870	d_skdm->notifySkolemDefinition(skolem, a);
67	30870	d_decisionEngine->addSkolemDefinition(a, skolem);
68		}
69	434429	}
70
71	348669	void TheoryProxy::variableNotify(SatVariable var) {
72	348669	d_theoryEngine->preRegister(getNode(SatLiteral(var)));
73	348669	}
74
75	13244654	void TheoryProxy::theoryCheck(theory::Theory::Effort effort) {
76	23413550	while (!d_queue.empty()) {
77	20337792	TNode assertion = d_queue.front();
78	10168896	d_queue.pop();
79	10168896	d_theoryEngine->assertFact(assertion);
80		}
81	3075758	d_theoryEngine->check(effort);
82	3075744	}
83
84	3075744	void TheoryProxy::theoryPropagate(std::vector<SatLiteral>& output) {
85		// Get the propagated literals
86	6151488	std::vector<TNode> outputNodes;
87	3075744	d_theoryEngine->getPropagatedLiterals(outputNodes);
88	9447136	for (unsigned i = 0, i_end = outputNodes.size(); i < i_end; ++ i) {
89	6371392	Debug("prop-explain") << "theoryPropagate() => " << outputNodes[i] << std::endl;
90	6371392	output.push_back(d_cnfStream->getLiteral(outputNodes[i]));
91		}
92	3075744	}
93
94	122918	void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
95	245836	TNode lNode = d_cnfStream->getNode(l);
96	122918	Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl;
97
98	245836	theory::TrustNode tte = d_theoryEngine->getExplanation(lNode);
99	245836	Node theoryExplanation = tte.getNode();
100	245836	if (options::produceProofs()
101	122918	&& options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS)
102		{
103	21449	Assert(options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF
104		\|\| tte.getGenerator());
105	21449	d_propEngine->getProofCnfStream()->convertPropagation(tte);
106		}
107	245836	Debug("prop-explain") << "explainPropagation() => " << theoryExplanation
108	122918	<< std::endl;
109	122918	explanation.push_back(l);
110	122918	if (theoryExplanation.getKind() == kind::AND)
111		{
112	962058	for (const Node& n : theoryExplanation)
113		{
114	845918	explanation.push_back(~d_cnfStream->getLiteral(n));
115		}
116		}
117		else
118		{
119	6778	explanation.push_back(~d_cnfStream->getLiteral(theoryExplanation));
120		}
121	122918	if (Trace.isOn("sat-proof"))
122		{
123		std::stringstream ss;
124		ss << "TheoryProxy::explainPropagation: clause for lit is ";
125		for (unsigned i = 0, size = explanation.size(); i < size; ++i)
126		{
127		ss << explanation[i] << " [" << d_cnfStream->getNode(explanation[i])
128		<< "] ";
129		}
130		Trace("sat-proof") << ss.str() << "\n";
131		}
132	122918	}
133
134	14281088	void TheoryProxy::enqueueTheoryLiteral(const SatLiteral& l) {
135	28562176	Node literalNode = d_cnfStream->getNode(l);
136	14281088	Debug("prop") << "enqueueing theory literal " << l << " " << literalNode << std::endl;
137	14281088	Assert(!literalNode.isNull());
138	14281088	d_queue.push(literalNode);
139	14281088	}
140
141	2010617	SatLiteral TheoryProxy::getNextTheoryDecisionRequest() {
142	4021232	TNode n = d_theoryEngine->getNextDecisionRequest();
143	4021230	return n.isNull() ? undefSatLiteral : d_cnfStream->getLiteral(n);
144		}
145
146	1962548	SatLiteral TheoryProxy::getNextDecisionEngineRequest(bool &stopSearch) {
147	1962548	Assert(d_decisionEngine != NULL);
148	1962548	Assert(stopSearch != true);
149	1962548	SatLiteral ret = d_decisionEngine->getNext(stopSearch);
150	1962548	if(stopSearch) {
151	41528	Trace("decision") << " * Decision Engine stopped search * " << std::endl;
152		}
153	1962548	return options::decisionStopOnly() ? undefSatLiteral : ret;
154		}
155
156	19964	bool TheoryProxy::theoryNeedCheck() const {
157	19964	return d_theoryEngine->needCheck();
158		}
159
160	348669	TNode TheoryProxy::getNode(SatLiteral lit) {
161	348669	return d_cnfStream->getNode(lit);
162		}
163
164	2527	void TheoryProxy::notifyRestart() {
165	2527	d_propEngine->spendResource(Resource::RestartStep);
166	2527	d_theoryEngine->notifyRestart();
167	2527	}
168
169	2518959	void TheoryProxy::spendResource(Resource r)
170		{
171	2518959	d_theoryEngine->spendResource(r);
172	2518959	}
173
174	4368766	bool TheoryProxy::isDecisionRelevant(SatVariable var) { return true; }
175
176	55380	bool TheoryProxy::isDecisionEngineDone() {
177	55380	return d_decisionEngine->isDone();
178		}
179
180	1307172	SatValue TheoryProxy::getDecisionPolarity(SatVariable var) {
181	1307172	return SAT_VALUE_UNKNOWN;
182		}
183
184	1197	CnfStream* TheoryProxy::getCnfStream() { return d_cnfStream; }
185
186	414663	theory::TrustNode TheoryProxy::preprocessLemma(
187		theory::TrustNode trn,
188		std::vector<theory::TrustNode>& newLemmas,
189		std::vector<Node>& newSkolems)
190		{
191	414663	return d_tpp.preprocessLemma(trn, newLemmas, newSkolems);
192		}
193
194	262732	theory::TrustNode TheoryProxy::preprocess(
195		TNode node,
196		std::vector<theory::TrustNode>& newLemmas,
197		std::vector<Node>& newSkolems)
198		{
199	262732	return d_tpp.preprocess(node, newLemmas, newSkolems);
200		}
201
202	4	theory::TrustNode TheoryProxy::removeItes(
203		TNode node,
204		std::vector<theory::TrustNode>& newLemmas,
205		std::vector<Node>& newSkolems)
206		{
207	4	RemoveTermFormulas& rtf = d_tpp.getRemoveTermFormulas();
208	4	return rtf.run(node, newLemmas, newSkolems, true);
209		}
210
211	2619	void TheoryProxy::getSkolems(TNode node,
212		std::vector<Node>& skAsserts,
213		std::vector<Node>& sks)
214		{
215	5238	std::unordered_set<Node> skolems;
216	2619	d_skdm->getSkolems(node, skolems);
217	4804	for (const Node& k : skolems)
218		{
219	2185	sks.push_back(k);
220	2185	skAsserts.push_back(d_skdm->getDefinitionForSkolem(k));
221		}
222	2619	}
223
224	540626	void TheoryProxy::preRegister(Node n) { d_theoryEngine->preRegister(n); }
225
226		} // namespace prop
227	28191	} // namespace cvc5