Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/smt/smt_engine_state.cpp	Lines:	124	137	90.5 %
Date:	2021-08-19	Branches:	93	251	37.1 %


/******************************************************************************
 * 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/env.h"
#include "smt/smt_engine.h"

namespace cvc5 {
namespace smt {

SmtEngineState::SmtEngineState(Env& env, SmtEngine& smt)
    : d_smt(smt),
      d_env(env),
      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_env.getFilename());
}

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 && getUserContext()->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() && getUserContext()->getLevel() > 1)
  {
    internalPop(true);
  }
}

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

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(getUserContext()->getLevel());
  internalPush();
  Trace("userpushpop") << "SmtEngineState: pushed to level "
                       << getUserContext()->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(getUserContext()->getLevel() > 0);
  AlwaysAssert(d_userLevels.back() < getUserContext()->getLevel());
  while (d_userLevels.back() < getUserContext()->getLevel())
  {
    internalPop(true);
  }
  d_userLevels.pop_back();
}
context::Context* SmtEngineState::getContext() { return d_env.getContext(); }
context::UserContext* SmtEngineState::getUserContext()
{
  return d_env.getUserContext();
}
void SmtEngineState::push()
{
  getUserContext()->push();
  getContext()->push();
}

void SmtEngineState::pop()
{
  getUserContext()->pop();
  getContext()->pop();
}

void SmtEngineState::popto(int toLevel)
{
  getContext()->popto(toLevel);
  getUserContext()->popto(toLevel);
}

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; }

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