Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/smt/smt_engine_state.cpp	Lines:	126	141	89.4 %
Date:	2021-08-03	Branches:	92	253	36.4 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Morgan Deters, Ying Sheng
 *
 * 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.
 * ****************************************************************************
 *
 * Utility for maintaining the state of the SMT engine.
 */

#include "smt/smt_engine_state.h"

#include "base/modal_exception.h"
#include "options/base_options.h"
#include "options/option_exception.h"
#include "options/smt_options.h"
#include "smt/smt_engine.h"

namespace cvc5 {
namespace smt {

SmtEngineState::SmtEngineState(context::Context* c,
                               context::UserContext* u,
                               SmtEngine& smt)
    : d_smt(smt),
      d_context(c),
      d_userContext(u),
      d_pendingPops(0),
      d_fullyInited(false),
      d_queryMade(false),
      d_needPostsolve(false),
      d_status(),
      d_expectedStatus(),
      d_smtMode(SmtMode::START)
{
}

void SmtEngineState::notifyExpectedStatus(const std::string& status)
{
  Assert(status == "sat" || status == "unsat" || status == "unknown")
      << "SmtEngineState::notifyExpectedStatus: unexpected status string "
      << status;
  d_expectedStatus = Result(status, d_filename);
}

void SmtEngineState::notifyResetAssertions()
{
  doPendingPops();
  while (!d_userLevels.empty())
  {
    userPop();
  }
  // Remember the global push/pop around everything when beyond Start mode
  // (see solver execution modes in the SMT-LIB standard)
  Assert(d_userLevels.size() == 0 && d_userContext->getLevel() == 1);
  popto(0);
}

void SmtEngineState::notifyCheckSat(bool hasAssumptions)
{
  // process the pending pops
  doPendingPops();
  if (d_queryMade && !options::incrementalSolving())
  {
    throw ModalException(
        "Cannot make multiple queries unless "
        "incremental solving is enabled "
        "(try --incremental)");
  }

  // Note that a query has been made and we are in assert mode
  d_queryMade = true;
  d_smtMode = SmtMode::ASSERT;

  // push if there are assumptions
  if (hasAssumptions)
  {
    internalPush();
  }
}

void SmtEngineState::notifyCheckSatResult(bool hasAssumptions, Result r)
{
  d_needPostsolve = true;

  // Pop the context
  if (hasAssumptions)
  {
    internalPop();
  }

  // Remember the status
  d_status = r;
  // Check against expected status
  if (!d_expectedStatus.isUnknown() && !d_status.isUnknown()
      && d_status != d_expectedStatus)
  {
    CVC5_FATAL() << "Expected result " << d_expectedStatus << " but got "
                 << d_status;
  }
  // clear expected status
  d_expectedStatus = Result();
  // Update the SMT mode
  switch (d_status.asSatisfiabilityResult().isSat())
  {
    case Result::UNSAT: d_smtMode = SmtMode::UNSAT; break;
    case Result::SAT: d_smtMode = SmtMode::SAT; break;
    default: d_smtMode = SmtMode::SAT_UNKNOWN;
  }
}

void SmtEngineState::notifyGetAbduct(bool success)
{
  if (success)
  {
    // successfully generated an abduct, update to abduct state
    d_smtMode = SmtMode::ABDUCT;
  }
  else
  {
    // failed, we revert to the assert state
    d_smtMode = SmtMode::ASSERT;
  }
}

void SmtEngineState::notifyGetInterpol(bool success)
{
  if (success)
  {
    // successfully generated an interpolant, update to interpol state
    d_smtMode = SmtMode::INTERPOL;
  }
  else
  {
    // failed, we revert to the assert state
    d_smtMode = SmtMode::ASSERT;
  }
}

void SmtEngineState::setup()
{
  // push a context
  push();
}

void SmtEngineState::finishInit()
{
  // set the flag to remember that we are fully initialized
  d_fullyInited = true;
}

void SmtEngineState::shutdown()
{
  doPendingPops();

  while (options::incrementalSolving() && d_userContext->getLevel() > 1)
  {
    internalPop(true);
  }
}

void SmtEngineState::cleanup()
{
  // pop to level zero
  popto(0);
}

void SmtEngineState::setFilename(const std::string& filename)
{
  d_filename = filename;
}

void SmtEngineState::userPush()
{
  if (!options::incrementalSolving())
  {
    throw ModalException(
        "Cannot push when not solving incrementally (use --incremental)");
  }
  // The problem isn't really "extended" yet, but this disallows
  // get-model after a push, simplifying our lives somewhat and
  // staying symmetric with pop.
  d_smtMode = SmtMode::ASSERT;

  d_userLevels.push_back(d_userContext->getLevel());
  internalPush();
  Trace("userpushpop") << "SmtEngineState: pushed to level "
                       << d_userContext->getLevel() << std::endl;
}

void SmtEngineState::userPop()
{
  if (!options::incrementalSolving())
  {
    throw ModalException(
        "Cannot pop when not solving incrementally (use --incremental)");
  }
  if (d_userLevels.size() == 0)
  {
    throw ModalException("Cannot pop beyond the first user frame");
  }
  // The problem isn't really "extended" yet, but this disallows
  // get-model after a pop, simplifying our lives somewhat.  It might
  // not be strictly necessary to do so, since the pops occur lazily,
  // but also it would be weird to have a legally-executed (get-model)
  // that only returns a subset of the assignment (because the rest
  // is no longer in scope!).
  d_smtMode = SmtMode::ASSERT;

  AlwaysAssert(d_userContext->getLevel() > 0);
  AlwaysAssert(d_userLevels.back() < d_userContext->getLevel());
  while (d_userLevels.back() < d_userContext->getLevel())
  {
    internalPop(true);
  }
  d_userLevels.pop_back();
}

void SmtEngineState::push()
{
  d_userContext->push();
  d_context->push();
}

void SmtEngineState::pop()
{
  d_userContext->pop();
  d_context->pop();
}

void SmtEngineState::popto(int toLevel)
{
  d_context->popto(toLevel);
  d_userContext->popto(toLevel);
}

context::UserContext* SmtEngineState::getUserContext() { return d_userContext; }

context::Context* SmtEngineState::getContext() { return d_context; }

Result SmtEngineState::getStatus() const { return d_status; }

bool SmtEngineState::isFullyInited() const { return d_fullyInited; }
bool SmtEngineState::isFullyReady() const
{
  return d_fullyInited && d_pendingPops == 0;
}
bool SmtEngineState::isQueryMade() const { return d_queryMade; }
size_t SmtEngineState::getNumUserLevels() const { return d_userLevels.size(); }

SmtMode SmtEngineState::getMode() const { return d_smtMode; }

const std::string& SmtEngineState::getFilename() const { return d_filename; }

void SmtEngineState::internalPush()
{
  Assert(d_fullyInited);
  Trace("smt") << "SmtEngineState::internalPush()" << std::endl;
  doPendingPops();
  if (options::incrementalSolving())
  {
    // notifies the SmtEngine to process the assertions immediately
    d_smt.notifyPushPre();
    d_userContext->push();
    // the context push is done inside of the SAT solver
    d_smt.notifyPushPost();
  }
}

void SmtEngineState::internalPop(bool immediate)
{
  Assert(d_fullyInited);
  Trace("smt") << "SmtEngineState::internalPop()" << std::endl;
  if (options::incrementalSolving())
  {
    ++d_pendingPops;
  }
  if (immediate)
  {
    doPendingPops();
  }
}

void SmtEngineState::doPendingPops()
{
  Trace("smt") << "SmtEngineState::doPendingPops()" << std::endl;
  Assert(d_pendingPops == 0 || options::incrementalSolving());
  // check to see if a postsolve() is pending
  if (d_needPostsolve)
  {
    d_smt.notifyPostSolvePre();
  }
  while (d_pendingPops > 0)
  {
    // the context pop is done inside of the SAT solver
    d_smt.notifyPopPre();
    // pop the context
    d_userContext->pop();
    --d_pendingPops;
    // no need for pop post (for now)
  }
  if (d_needPostsolve)
  {
    d_smt.notifyPostSolvePost();
    d_needPostsolve = false;
  }
}

}  // namespace smt
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Morgan Deters, Ying Sheng
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		* Utility for maintaining the state of the SMT engine.
14		*/
15
16		#include "smt/smt_engine_state.h"
17
18		#include "base/modal_exception.h"
19		#include "options/base_options.h"
20		#include "options/option_exception.h"
21		#include "options/smt_options.h"
22		#include "smt/smt_engine.h"
23
24		namespace cvc5 {
25		namespace smt {
26
27	10484	SmtEngineState::SmtEngineState(context::Context* c,
28		context::UserContext* u,
29	10484	SmtEngine& smt)
30		: d_smt(smt),
31		d_context(c),
32		d_userContext(u),
33		d_pendingPops(0),
34		d_fullyInited(false),
35		d_queryMade(false),
36		d_needPostsolve(false),
37		d_status(),
38		d_expectedStatus(),
39	10484	d_smtMode(SmtMode::START)
40		{
41	10484	}
42
43	3661	void SmtEngineState::notifyExpectedStatus(const std::string& status)
44		{
45	3661	Assert(status == "sat" \|\| status == "unsat" \|\| status == "unknown")
46		<< "SmtEngineState::notifyExpectedStatus: unexpected status string "
47		<< status;
48	3661	d_expectedStatus = Result(status, d_filename);
49	3661	}
50
51	67	void SmtEngineState::notifyResetAssertions()
52		{
53	67	doPendingPops();
54	99	while (!d_userLevels.empty())
55		{
56	16	userPop();
57		}
58		// Remember the global push/pop around everything when beyond Start mode
59		// (see solver execution modes in the SMT-LIB standard)
60	67	Assert(d_userLevels.size() == 0 && d_userContext->getLevel() == 1);
61	67	popto(0);
62	67	}
63
64	15206	void SmtEngineState::notifyCheckSat(bool hasAssumptions)
65		{
66		// process the pending pops
67	15206	doPendingPops();
68	15206	if (d_queryMade && !options::incrementalSolving())
69		{
70		throw ModalException(
71		"Cannot make multiple queries unless "
72		"incremental solving is enabled "
73		"(try --incremental)");
74		}
75
76		// Note that a query has been made and we are in assert mode
77	15206	d_queryMade = true;
78	15206	d_smtMode = SmtMode::ASSERT;
79
80		// push if there are assumptions
81	15206	if (hasAssumptions)
82		{
83	2452	internalPush();
84		}
85	15206	}
86
87	15176	void SmtEngineState::notifyCheckSatResult(bool hasAssumptions, Result r)
88		{
89	15176	d_needPostsolve = true;
90
91		// Pop the context
92	15176	if (hasAssumptions)
93		{
94	2438	internalPop();
95		}
96
97		// Remember the status
98	15176	d_status = r;
99		// Check against expected status
100	33949	if (!d_expectedStatus.isUnknown() && !d_status.isUnknown()
101	18770	&& d_status != d_expectedStatus)
102		{
103		CVC5_FATAL() << "Expected result " << d_expectedStatus << " but got "
104		<< d_status;
105		}
106		// clear expected status
107	15176	d_expectedStatus = Result();
108		// Update the SMT mode
109	15176	switch (d_status.asSatisfiabilityResult().isSat())
110		{
111	7683	case Result::UNSAT: d_smtMode = SmtMode::UNSAT; break;
112	7377	case Result::SAT: d_smtMode = SmtMode::SAT; break;
113	116	default: d_smtMode = SmtMode::SAT_UNKNOWN;
114		}
115	15176	}
116
117	14	void SmtEngineState::notifyGetAbduct(bool success)
118		{
119	14	if (success)
120		{
121		// successfully generated an abduct, update to abduct state
122	14	d_smtMode = SmtMode::ABDUCT;
123		}
124		else
125		{
126		// failed, we revert to the assert state
127		d_smtMode = SmtMode::ASSERT;
128		}
129	14	}
130
131	10	void SmtEngineState::notifyGetInterpol(bool success)
132		{
133	10	if (success)
134		{
135		// successfully generated an interpolant, update to interpol state
136	10	d_smtMode = SmtMode::INTERPOL;
137		}
138		else
139		{
140		// failed, we revert to the assert state
141		d_smtMode = SmtMode::ASSERT;
142		}
143	10	}
144
145	9908	void SmtEngineState::setup()
146		{
147		// push a context
148	9908	push();
149	9908	}
150
151	9841	void SmtEngineState::finishInit()
152		{
153		// set the flag to remember that we are fully initialized
154	9841	d_fullyInited = true;
155	9841	}
156
157	10483	void SmtEngineState::shutdown()
158		{
159	10483	doPendingPops();
160
161	11529	while (options::incrementalSolving() && d_userContext->getLevel() > 1)
162		{
163	523	internalPop(true);
164		}
165	10483	}
166
167	10483	void SmtEngineState::cleanup()
168		{
169		// pop to level zero
170	10483	popto(0);
171	10483	}
172
173	6173	void SmtEngineState::setFilename(const std::string& filename)
174		{
175	6173	d_filename = filename;
176	6173	}
177
178	4036	void SmtEngineState::userPush()
179		{
180	4036	if (!options::incrementalSolving())
181		{
182		throw ModalException(
183		"Cannot push when not solving incrementally (use --incremental)");
184		}
185		// The problem isn't really "extended" yet, but this disallows
186		// get-model after a push, simplifying our lives somewhat and
187		// staying symmetric with pop.
188	4036	d_smtMode = SmtMode::ASSERT;
189
190	4036	d_userLevels.push_back(d_userContext->getLevel());
191	4036	internalPush();
192	8072	Trace("userpushpop") << "SmtEngineState: pushed to level "
193	4036	<< d_userContext->getLevel() << std::endl;
194	4036	}
195
196	3513	void SmtEngineState::userPop()
197		{
198	3513	if (!options::incrementalSolving())
199		{
200		throw ModalException(
201		"Cannot pop when not solving incrementally (use --incremental)");
202		}
203	3513	if (d_userLevels.size() == 0)
204		{
205		throw ModalException("Cannot pop beyond the first user frame");
206		}
207		// The problem isn't really "extended" yet, but this disallows
208		// get-model after a pop, simplifying our lives somewhat. It might
209		// not be strictly necessary to do so, since the pops occur lazily,
210		// but also it would be weird to have a legally-executed (get-model)
211		// that only returns a subset of the assignment (because the rest
212		// is no longer in scope!).
213	3513	d_smtMode = SmtMode::ASSERT;
214
215	3513	AlwaysAssert(d_userContext->getLevel() > 0);
216	3513	AlwaysAssert(d_userLevels.back() < d_userContext->getLevel());
217	10539	while (d_userLevels.back() < d_userContext->getLevel())
218		{
219	3513	internalPop(true);
220		}
221	3513	d_userLevels.pop_back();
222	3513	}
223
224	9908	void SmtEngineState::push()
225		{
226	9908	d_userContext->push();
227	9908	d_context->push();
228	9908	}
229
230		void SmtEngineState::pop()
231		{
232		d_userContext->pop();
233		d_context->pop();
234		}
235
236	10550	void SmtEngineState::popto(int toLevel)
237		{
238	10550	d_context->popto(toLevel);
239	10550	d_userContext->popto(toLevel);
240	10550	}
241
242		context::UserContext* SmtEngineState::getUserContext() { return d_userContext; }
243
244		context::Context* SmtEngineState::getContext() { return d_context; }
245
246	11	Result SmtEngineState::getStatus() const { return d_status; }
247
248	257919	bool SmtEngineState::isFullyInited() const { return d_fullyInited; }
249	24179	bool SmtEngineState::isFullyReady() const
250		{
251	24179	return d_fullyInited && d_pendingPops == 0;
252		}
253	10943	bool SmtEngineState::isQueryMade() const { return d_queryMade; }
254	2825	size_t SmtEngineState::getNumUserLevels() const { return d_userLevels.size(); }
255
256	6778	SmtMode SmtEngineState::getMode() const { return d_smtMode; }
257
258	104805	const std::string& SmtEngineState::getFilename() const { return d_filename; }
259
260	6488	void SmtEngineState::internalPush()
261		{
262	6488	Assert(d_fullyInited);
263	6488	Trace("smt") << "SmtEngineState::internalPush()" << std::endl;
264	6488	doPendingPops();
265	6488	if (options::incrementalSolving())
266		{
267		// notifies the SmtEngine to process the assertions immediately
268	4869	d_smt.notifyPushPre();
269	4869	d_userContext->push();
270		// the context push is done inside of the SAT solver
271	4869	d_smt.notifyPushPost();
272		}
273	6488	}
274
275	6474	void SmtEngineState::internalPop(bool immediate)
276		{
277	6474	Assert(d_fullyInited);
278	6474	Trace("smt") << "SmtEngineState::internalPop()" << std::endl;
279	6474	if (options::incrementalSolving())
280		{
281	4869	++d_pendingPops;
282		}
283	6474	if (immediate)
284		{
285	4036	doPendingPops();
286		}
287	6474	}
288
289	134696	void SmtEngineState::doPendingPops()
290		{
291	134696	Trace("smt") << "SmtEngineState::doPendingPops()" << std::endl;
292	134696	Assert(d_pendingPops == 0 \|\| options::incrementalSolving());
293		// check to see if a postsolve() is pending
294	134696	if (d_needPostsolve)
295		{
296	15176	d_smt.notifyPostSolvePre();
297		}
298	144434	while (d_pendingPops > 0)
299		{
300		// the context pop is done inside of the SAT solver
301	4869	d_smt.notifyPopPre();
302		// pop the context
303	4869	d_userContext->pop();
304	4869	--d_pendingPops;
305		// no need for pop post (for now)
306		}
307	134696	if (d_needPostsolve)
308		{
309	15176	d_smt.notifyPostSolvePost();
310	15176	d_needPostsolve = false;
311		}
312	134696	}
313
314		} // namespace smt
315	29286	} // namespace cvc5