Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/prop/theory_proxy.cpp	Lines:	108	114	94.7 %
Date:	2021-11-06	Branches:	140	338	41.4 %


/******************************************************************************
 * 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/env.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,
                         Env& env)
    : d_propEngine(propEngine),
      d_cnfStream(nullptr),
      d_decisionEngine(decisionEngine),
      d_dmNeedsActiveDefs(d_decisionEngine->needsActiveSkolemDefs()),
      d_theoryEngine(theoryEngine),
      d_queue(env.getContext()),
      d_tpp(env, *theoryEngine),
      d_skdm(skdm),
      d_env(env)
{
}

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

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

void TheoryProxy::presolve()
{
  d_decisionEngine->presolve();
  d_theoryEngine->presolve();
}

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

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();
    // now, assert to theory engine
    d_theoryEngine->assertFact(assertion);
    if (d_dmNeedsActiveDefs)
    {
      Assert(d_skdm != nullptr);
      Trace("sat-rlv-assert")
          << "Assert to theory engine: " << assertion << std::endl;
      // Assertion makes all skolems in assertion active,
      // which triggers their definitions to becoming active.
      std::vector<TNode> activeSkolemDefs;
      d_skdm->notifyAsserted(assertion, activeSkolemDefs, true);
      // notify the decision engine of the skolem definitions that have become
      // active due to the assertion.
      d_decisionEngine->notifyActiveSkolemDefs(activeSkolemDefs);
    }
  }
  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;

  TrustNode tte = d_theoryEngine->getExplanation(lNode);
  Node theoryExplanation = tte.getNode();
  if (d_env.isSatProofProducing())
  {
    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 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; }

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

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

TrustNode TheoryProxy::removeItes(TNode node,
                                  std::vector<theory::SkolemLemma>& newLemmas)
{
  RemoveTermFormulas& rtf = d_tpp.getRemoveTermFormulas();
  return rtf.run(node, newLemmas, 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/env.h"
28		#include "smt/smt_statistics_registry.h"
29		#include "theory/rewriter.h"
30		#include "theory/theory_engine.h"
31		#include "util/statistics_stats.h"
32
33		namespace cvc5 {
34		namespace prop {
35
36	15339	TheoryProxy::TheoryProxy(PropEngine* propEngine,
37		TheoryEngine* theoryEngine,
38		decision::DecisionEngine* decisionEngine,
39		SkolemDefManager* skdm,
40	15339	Env& env)
41		: d_propEngine(propEngine),
42		d_cnfStream(nullptr),
43		d_decisionEngine(decisionEngine),
44	15339	d_dmNeedsActiveDefs(d_decisionEngine->needsActiveSkolemDefs()),
45		d_theoryEngine(theoryEngine),
46		d_queue(env.getContext()),
47		d_tpp(env, *theoryEngine),
48		d_skdm(skdm),
49	30678	d_env(env)
50		{
51	15339	}
52
53	30668	TheoryProxy::~TheoryProxy() {
54		/* nothing to do for now */
55	30668	}
56
57	15339	void TheoryProxy::finishInit(CnfStream* cnfStream) { d_cnfStream = cnfStream; }
58
59	20562	void TheoryProxy::presolve()
60		{
61	20562	d_decisionEngine->presolve();
62	20562	d_theoryEngine->presolve();
63	20562	}
64
65	512226	void TheoryProxy::notifyAssertion(Node a, TNode skolem, bool isLemma)
66		{
67	512226	if (skolem.isNull())
68		{
69	482466	d_decisionEngine->addAssertion(a, isLemma);
70		}
71		else
72		{
73	29760	d_skdm->notifySkolemDefinition(skolem, a);
74	29760	d_decisionEngine->addSkolemDefinition(a, skolem, isLemma);
75		}
76	512226	}
77
78	514111	void TheoryProxy::variableNotify(SatVariable var) {
79	514111	d_theoryEngine->preRegister(getNode(SatLiteral(var)));
80	514111	}
81
82	20635370	void TheoryProxy::theoryCheck(theory::Theory::Effort effort) {
83	36157719	while (!d_queue.empty()) {
84	31044698	TNode assertion = d_queue.front();
85	15522349	d_queue.pop();
86		// now, assert to theory engine
87	15522349	d_theoryEngine->assertFact(assertion);
88	15522349	if (d_dmNeedsActiveDefs)
89		{
90	7662981	Assert(d_skdm != nullptr);
91	15325962	Trace("sat-rlv-assert")
92	7662981	<< "Assert to theory engine: " << assertion << std::endl;
93		// Assertion makes all skolems in assertion active,
94		// which triggers their definitions to becoming active.
95	15325962	std::vector<TNode> activeSkolemDefs;
96	7662981	d_skdm->notifyAsserted(assertion, activeSkolemDefs, true);
97		// notify the decision engine of the skolem definitions that have become
98		// active due to the assertion.
99	7662981	d_decisionEngine->notifyActiveSkolemDefs(activeSkolemDefs);
100		}
101		}
102	5113021	d_theoryEngine->check(effort);
103	5113002	}
104
105	5113002	void TheoryProxy::theoryPropagate(std::vector<SatLiteral>& output) {
106		// Get the propagated literals
107	10226004	std::vector<TNode> outputNodes;
108	5113002	d_theoryEngine->getPropagatedLiterals(outputNodes);
109	14831958	for (unsigned i = 0, i_end = outputNodes.size(); i < i_end; ++ i) {
110	9718956	Debug("prop-explain") << "theoryPropagate() => " << outputNodes[i] << std::endl;
111	9718956	output.push_back(d_cnfStream->getLiteral(outputNodes[i]));
112		}
113	5113002	}
114
115	120449	void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
116	240898	TNode lNode = d_cnfStream->getNode(l);
117	120449	Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl;
118
119	240898	TrustNode tte = d_theoryEngine->getExplanation(lNode);
120	240898	Node theoryExplanation = tte.getNode();
121	120449	if (d_env.isSatProofProducing())
122		{
123	15234	Assert(options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF
124		\|\| tte.getGenerator());
125	15234	d_propEngine->getProofCnfStream()->convertPropagation(tte);
126		}
127	240898	Debug("prop-explain") << "explainPropagation() => " << theoryExplanation
128	120449	<< std::endl;
129	120449	explanation.push_back(l);
130	120449	if (theoryExplanation.getKind() == kind::AND)
131		{
132	897380	for (const Node& n : theoryExplanation)
133		{
134	783756	explanation.push_back(~d_cnfStream->getLiteral(n));
135		}
136		}
137		else
138		{
139	6825	explanation.push_back(~d_cnfStream->getLiteral(theoryExplanation));
140		}
141	120449	if (Trace.isOn("sat-proof"))
142		{
143		std::stringstream ss;
144		ss << "TheoryProxy::explainPropagation: clause for lit is ";
145		for (unsigned i = 0, size = explanation.size(); i < size; ++i)
146		{
147		ss << explanation[i] << " [" << d_cnfStream->getNode(explanation[i])
148		<< "] ";
149		}
150		Trace("sat-proof") << ss.str() << "\n";
151		}
152	120449	}
153
154	20799945	void TheoryProxy::enqueueTheoryLiteral(const SatLiteral& l) {
155	41599890	Node literalNode = d_cnfStream->getNode(l);
156	20799945	Debug("prop") << "enqueueing theory literal " << l << " " << literalNode << std::endl;
157	20799945	Assert(!literalNode.isNull());
158	20799945	d_queue.push(literalNode);
159	20799945	}
160
161	3423072	SatLiteral TheoryProxy::getNextTheoryDecisionRequest() {
162	6846140	TNode n = d_theoryEngine->getNextDecisionRequest();
163	6846136	return n.isNull() ? undefSatLiteral : d_cnfStream->getLiteral(n);
164		}
165
166	3343232	SatLiteral TheoryProxy::getNextDecisionEngineRequest(bool &stopSearch) {
167	3343232	Assert(d_decisionEngine != NULL);
168	3343232	Assert(stopSearch != true);
169	3343232	SatLiteral ret = d_decisionEngine->getNext(stopSearch);
170	3343232	if(stopSearch) {
171	57402	Trace("decision") << " * Decision Engine stopped search * " << std::endl;
172		}
173	3343232	return ret;
174		}
175
176	19178	bool TheoryProxy::theoryNeedCheck() const {
177	19178	return d_theoryEngine->needCheck();
178		}
179
180	514111	TNode TheoryProxy::getNode(SatLiteral lit) {
181	514111	return d_cnfStream->getNode(lit);
182		}
183
184	2680	void TheoryProxy::notifyRestart() {
185	2680	d_propEngine->spendResource(Resource::RestartStep);
186	2680	d_theoryEngine->notifyRestart();
187	2680	}
188
189	4058563	void TheoryProxy::spendResource(Resource r)
190		{
191	4058563	d_theoryEngine->spendResource(r);
192	4058563	}
193
194	6268998	bool TheoryProxy::isDecisionRelevant(SatVariable var) { return true; }
195
196	72954	bool TheoryProxy::isDecisionEngineDone() {
197	72954	return d_decisionEngine->isDone();
198		}
199
200	1939049	SatValue TheoryProxy::getDecisionPolarity(SatVariable var) {
201	1939049	return SAT_VALUE_UNKNOWN;
202		}
203
204	5381	CnfStream* TheoryProxy::getCnfStream() { return d_cnfStream; }
205
206	515559	TrustNode TheoryProxy::preprocessLemma(
207		TrustNode trn, std::vector<theory::SkolemLemma>& newLemmas)
208		{
209	515559	return d_tpp.preprocessLemma(trn, newLemmas);
210		}
211
212	370394	TrustNode TheoryProxy::preprocess(TNode node,
213		std::vector<theory::SkolemLemma>& newLemmas)
214		{
215	370394	return d_tpp.preprocess(node, newLemmas);
216		}
217
218	2	TrustNode TheoryProxy::removeItes(TNode node,
219		std::vector<theory::SkolemLemma>& newLemmas)
220		{
221	2	RemoveTermFormulas& rtf = d_tpp.getRemoveTermFormulas();
222	2	return rtf.run(node, newLemmas, true);
223		}
224
225	3677	void TheoryProxy::getSkolems(TNode node,
226		std::vector<Node>& skAsserts,
227		std::vector<Node>& sks)
228		{
229	7354	std::unordered_set<Node> skolems;
230	3677	d_skdm->getSkolems(node, skolems);
231	6200	for (const Node& k : skolems)
232		{
233	2523	sks.push_back(k);
234	2523	skAsserts.push_back(d_skdm->getDefinitionForSkolem(k));
235		}
236	3677	}
237
238	706615	void TheoryProxy::preRegister(Node n) { d_theoryEngine->preRegister(n); }
239
240		} // namespace prop
241	31137	} // namespace cvc5