Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/smt/solver_engine_state.cpp	Lines:	123	135	91.1 %
Date:	2021-11-05	Branches:	94	251	37.5 %


/******************************************************************************
 * 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/solver_engine_state.h"

#include "base/modal_exception.h"
#include "options/base_options.h"
#include "options/main_options.h"
#include "options/option_exception.h"
#include "options/smt_options.h"
#include "smt/env.h"
#include "smt/solver_engine.h"

namespace cvc5 {
namespace smt {

SolverEngineState::SolverEngineState(Env& env, SolverEngine& slv)
    : EnvObj(env),
      d_slv(slv),
      d_pendingPops(0),
      d_fullyInited(false),
      d_queryMade(false),
      d_needPostsolve(false),
      d_status(),
      d_expectedStatus(),
      d_smtMode(SmtMode::START)
{
}

void SolverEngineState::notifyExpectedStatus(const std::string& status)
{
  Assert(status == "sat" || status == "unsat" || status == "unknown")
      << "SolverEngineState::notifyExpectedStatus: unexpected status string "
      << status;
  d_expectedStatus = Result(status, options().driver.filename);
}

void SolverEngineState::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 && userContext()->getLevel() == 1);
  popto(0);
}

void SolverEngineState::notifyCheckSat(bool hasAssumptions)
{
  // process the pending pops
  doPendingPops();
  if (d_queryMade && !options().base.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 SolverEngineState::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 SolverEngineState::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 SolverEngineState::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 SolverEngineState::setup()
{
  // push a context
  push();
}

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

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

  while (options().base.incrementalSolving && userContext()->getLevel() > 1)
  {
    internalPop(true);
  }
}

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

void SolverEngineState::userPush()
{
  if (!options().base.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(userContext()->getLevel());
  internalPush();
  Trace("userpushpop") << "SolverEngineState: pushed to level "
                       << userContext()->getLevel() << std::endl;
}

void SolverEngineState::userPop()
{
  if (!options().base.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(userContext()->getLevel() > 0);
  AlwaysAssert(d_userLevels.back() < userContext()->getLevel());
  while (d_userLevels.back() < userContext()->getLevel())
  {
    internalPop(true);
  }
  d_userLevels.pop_back();
}
void SolverEngineState::push()
{
  userContext()->push();
  context()->push();
}

void SolverEngineState::pop()
{
  userContext()->pop();
  context()->pop();
}

void SolverEngineState::popto(int toLevel)
{
  context()->popto(toLevel);
  userContext()->popto(toLevel);
}

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

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

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

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

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

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