Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/smt/smt_solver.cpp	Lines:	96	107	89.7 %
Date:	2021-05-21	Branches:	149	318	46.9 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Aina Niemetz, Morgan Deters
 *
 * 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.
 * ****************************************************************************
 *
 * The solver for SMT queries in an SmtEngine.
 */

#include "smt/smt_solver.h"

#include "options/smt_options.h"
#include "prop/prop_engine.h"
#include "smt/assertions.h"
#include "smt/env.h"
#include "smt/preprocessor.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_state.h"
#include "smt/smt_engine_stats.h"
#include "theory/logic_info.h"
#include "theory/theory_engine.h"
#include "theory/theory_traits.h"

using namespace std;

namespace cvc5 {
namespace smt {

SmtSolver::SmtSolver(SmtEngine& smt,
                     Env& env,
                     SmtEngineState& state,
                     Preprocessor& pp,
                     SmtEngineStatistics& stats)
    : d_smt(smt),
      d_env(env),
      d_state(state),
      d_pp(pp),
      d_stats(stats),
      d_pnm(nullptr),
      d_theoryEngine(nullptr),
      d_propEngine(nullptr)
{
}

SmtSolver::~SmtSolver() {}

void SmtSolver::finishInit(const LogicInfo& logicInfo)
{
  // We have mutual dependency here, so we add the prop engine to the theory
  // engine later (it is non-essential there)
  d_theoryEngine.reset(new TheoryEngine(
      d_env,
      d_smt.getOutputManager(),
      // Other than whether d_pm is set, theory engine proofs are conditioned on
      // the relationshup between proofs and unsat cores: the unsat cores are in
      // FULL_PROOF mode, no proofs are generated on theory engine.
      (options::unsatCores()
       && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF)
          ? nullptr
          : d_pnm));

  // Add the theories
  for (theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST;
       ++id)
  {
    theory::TheoryConstructor::addTheory(d_theoryEngine.get(), id);
  }
  // Add the proof checkers for each theory
  if (d_pnm)
  {
    d_theoryEngine->initializeProofChecker(d_pnm->getChecker());
  }
  Trace("smt-debug") << "Making prop engine..." << std::endl;
  /* force destruction of referenced PropEngine to enforce that statistics
   * are unregistered by the obsolete PropEngine object before registered
   * again by the new PropEngine object */
  d_propEngine.reset(nullptr);
  d_propEngine.reset(new prop::PropEngine(
      d_theoryEngine.get(), d_env, d_smt.getOutputManager(), d_pnm));

  Trace("smt-debug") << "Setting up theory engine..." << std::endl;
  d_theoryEngine->setPropEngine(getPropEngine());
  Trace("smt-debug") << "Finishing init for theory engine..." << std::endl;
  d_theoryEngine->finishInit();
  d_propEngine->finishInit();
}

void SmtSolver::resetAssertions()
{
  /* Create new PropEngine.
   * First force destruction of referenced PropEngine to enforce that
   * statistics are unregistered by the obsolete PropEngine object before
   * registered again by the new PropEngine object */
  d_propEngine.reset(nullptr);
  d_propEngine.reset(new prop::PropEngine(
      d_theoryEngine.get(), d_env, d_smt.getOutputManager(), d_pnm));
  d_theoryEngine->setPropEngine(getPropEngine());
  // Notice that we do not reset TheoryEngine, nor does it require calling
  // finishInit again. In particular, TheoryEngine::finishInit does not
  // depend on knowing the associated PropEngine.
  d_propEngine->finishInit();
}

void SmtSolver::interrupt()
{
  if (d_propEngine != nullptr)
  {
    d_propEngine->interrupt();
  }
  if (d_theoryEngine != nullptr)
  {
    d_theoryEngine->interrupt();
  }
}

void SmtSolver::shutdown()
{
  if (d_propEngine != nullptr)
  {
    d_propEngine->shutdown();
  }
  if (d_theoryEngine != nullptr)
  {
    d_theoryEngine->shutdown();
  }
}

Result SmtSolver::checkSatisfiability(Assertions& as,
                                      const std::vector<Node>& assumptions,
                                      bool inUnsatCore,
                                      bool isEntailmentCheck)
{
  // update the state to indicate we are about to run a check-sat
  bool hasAssumptions = !assumptions.empty();
  d_state.notifyCheckSat(hasAssumptions);

  // then, initialize the assertions
  as.initializeCheckSat(assumptions, inUnsatCore, isEntailmentCheck);

  // make the check
  Assert(d_smt.isFullyInited());

  Trace("smt") << "SmtSolver::check()" << endl;

  const std::string& filename = d_state.getFilename();
  ResourceManager* rm = d_env.getResourceManager();
  if (rm->out())
  {
    Result::UnknownExplanation why =
        rm->outOfResources() ? Result::RESOURCEOUT : Result::TIMEOUT;
    return Result(Result::ENTAILMENT_UNKNOWN, why, filename);
  }
  rm->beginCall();

  // Make sure the prop layer has all of the assertions
  Trace("smt") << "SmtSolver::check(): processing assertions" << endl;
  processAssertions(as);
  Trace("smt") << "SmtSolver::check(): done processing assertions" << endl;

  TimerStat::CodeTimer solveTimer(d_stats.d_solveTime);

  Chat() << "solving..." << endl;
  Trace("smt") << "SmtSolver::check(): running check" << endl;
  Result result = d_propEngine->checkSat();

  rm->endCall();
  Trace("limit") << "SmtSolver::check(): cumulative millis "
                 << rm->getTimeUsage() << ", resources "
                 << rm->getResourceUsage() << endl;

  if ((options::solveRealAsInt() || options::solveIntAsBV() > 0)
      && result.asSatisfiabilityResult().isSat() == Result::UNSAT)
  {
    result = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
  }
  // flipped if we did a global negation
  if (as.isGlobalNegated())
  {
    Trace("smt") << "SmtSolver::process global negate " << result << std::endl;
    if (result.asSatisfiabilityResult().isSat() == Result::UNSAT)
    {
      result = Result(Result::SAT);
    }
    else if (result.asSatisfiabilityResult().isSat() == Result::SAT)
    {
      // Only can answer unsat if the theory is satisfaction complete. This
      // includes linear arithmetic and bitvectors, which are the primary
      // targets for the global negate option. Other logics are possible here
      // but not considered.
      LogicInfo logic = d_env.getLogicInfo();
      if ((logic.isPure(theory::THEORY_ARITH) && logic.isLinear()) ||
          logic.isPure(theory::THEORY_BV))
      {
        result = Result(Result::UNSAT);
      }
      else
      {
        result = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
      }
    }
    Trace("smt") << "SmtSolver::global negate returned " << result << std::endl;
  }

  // set the filename on the result
  Result r = Result(result, filename);

  // notify our state of the check-sat result
  d_state.notifyCheckSatResult(hasAssumptions, r);

  return r;
}

void SmtSolver::processAssertions(Assertions& as)
{
  TimerStat::CodeTimer paTimer(d_stats.d_processAssertionsTime);
  d_env.getResourceManager()->spendResource(Resource::PreprocessStep);
  Assert(d_state.isFullyReady());

  preprocessing::AssertionPipeline& ap = as.getAssertionPipeline();

  if (ap.size() == 0)
  {
    // nothing to do
    return;
  }

  // process the assertions with the preprocessor
  d_pp.process(as);

  // end: INVARIANT to maintain: no reordering of assertions or
  // introducing new ones

  // Push the formula to SAT
  {
    Chat() << "converting to CNF..." << endl;
    TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime);
    const std::vector<Node>& assertions = ap.ref();
    // It is important to distinguish the input assertions from the skolem
    // definitions, as the decision justification heuristic treates the latter
    // specially.
    preprocessing::IteSkolemMap& ism = ap.getIteSkolemMap();
    d_propEngine->assertInputFormulas(assertions, ism);
  }

  // clear the current assertions
  as.clearCurrent();
}

void SmtSolver::setProofNodeManager(ProofNodeManager* pnm) { d_pnm = pnm; }

TheoryEngine* SmtSolver::getTheoryEngine() { return d_theoryEngine.get(); }

prop::PropEngine* SmtSolver::getPropEngine() { return d_propEngine.get(); }

theory::QuantifiersEngine* SmtSolver::getQuantifiersEngine()
{
  Assert(d_theoryEngine != nullptr);
  return d_theoryEngine->getQuantifiersEngine();
}

Preprocessor* SmtSolver::getPreprocessor() { return &d_pp; }

}  // namespace smt
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Aina Niemetz, Morgan Deters
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		* The solver for SMT queries in an SmtEngine.
14		*/
15
16		#include "smt/smt_solver.h"
17
18		#include "options/smt_options.h"
19		#include "prop/prop_engine.h"
20		#include "smt/assertions.h"
21		#include "smt/env.h"
22		#include "smt/preprocessor.h"
23		#include "smt/smt_engine.h"
24		#include "smt/smt_engine_state.h"
25		#include "smt/smt_engine_stats.h"
26		#include "theory/logic_info.h"
27		#include "theory/theory_engine.h"
28		#include "theory/theory_traits.h"
29
30		using namespace std;
31
32		namespace cvc5 {
33		namespace smt {
34
35	9586	SmtSolver::SmtSolver(SmtEngine& smt,
36		Env& env,
37		SmtEngineState& state,
38		Preprocessor& pp,
39	9586	SmtEngineStatistics& stats)
40		: d_smt(smt),
41		d_env(env),
42		d_state(state),
43		d_pp(pp),
44		d_stats(stats),
45		d_pnm(nullptr),
46		d_theoryEngine(nullptr),
47	9586	d_propEngine(nullptr)
48		{
49	9586	}
50
51	9586	SmtSolver::~SmtSolver() {}
52
53	8954	void SmtSolver::finishInit(const LogicInfo& logicInfo)
54		{
55		// We have mutual dependency here, so we add the prop engine to the theory
56		// engine later (it is non-essential there)
57	26862	d_theoryEngine.reset(new TheoryEngine(
58		d_env,
59	8954	d_smt.getOutputManager(),
60		// Other than whether d_pm is set, theory engine proofs are conditioned on
61		// the relationshup between proofs and unsat cores: the unsat cores are in
62		// FULL_PROOF mode, no proofs are generated on theory engine.
63	8954	(options::unsatCores()
64	3122	&& options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF)
65	16000	? nullptr
66	8954	: d_pnm));
67
68		// Add the theories
69	125356	for (theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST;
70		++id)
71		{
72	116402	theory::TheoryConstructor::addTheory(d_theoryEngine.get(), id);
73		}
74		// Add the proof checkers for each theory
75	8954	if (d_pnm)
76		{
77	3117	d_theoryEngine->initializeProofChecker(d_pnm->getChecker());
78		}
79	8954	Trace("smt-debug") << "Making prop engine..." << std::endl;
80		/* force destruction of referenced PropEngine to enforce that statistics
81		* are unregistered by the obsolete PropEngine object before registered
82		* again by the new PropEngine object */
83	8954	d_propEngine.reset(nullptr);
84	26862	d_propEngine.reset(new prop::PropEngine(
85	17908	d_theoryEngine.get(), d_env, d_smt.getOutputManager(), d_pnm));
86
87	8954	Trace("smt-debug") << "Setting up theory engine..." << std::endl;
88	8954	d_theoryEngine->setPropEngine(getPropEngine());
89	8954	Trace("smt-debug") << "Finishing init for theory engine..." << std::endl;
90	8954	d_theoryEngine->finishInit();
91	8954	d_propEngine->finishInit();
92	8954	}
93
94	34	void SmtSolver::resetAssertions()
95		{
96		/* Create new PropEngine.
97		* First force destruction of referenced PropEngine to enforce that
98		* statistics are unregistered by the obsolete PropEngine object before
99		* registered again by the new PropEngine object */
100	34	d_propEngine.reset(nullptr);
101	102	d_propEngine.reset(new prop::PropEngine(
102	68	d_theoryEngine.get(), d_env, d_smt.getOutputManager(), d_pnm));
103	34	d_theoryEngine->setPropEngine(getPropEngine());
104		// Notice that we do not reset TheoryEngine, nor does it require calling
105		// finishInit again. In particular, TheoryEngine::finishInit does not
106		// depend on knowing the associated PropEngine.
107	34	d_propEngine->finishInit();
108	34	}
109
110		void SmtSolver::interrupt()
111		{
112		if (d_propEngine != nullptr)
113		{
114		d_propEngine->interrupt();
115		}
116		if (d_theoryEngine != nullptr)
117		{
118		d_theoryEngine->interrupt();
119		}
120		}
121
122	9586	void SmtSolver::shutdown()
123		{
124	9586	if (d_propEngine != nullptr)
125		{
126	8954	d_propEngine->shutdown();
127		}
128	9586	if (d_theoryEngine != nullptr)
129		{
130	8954	d_theoryEngine->shutdown();
131		}
132	9586	}
133
134	12761	Result SmtSolver::checkSatisfiability(Assertions& as,
135		const std::vector<Node>& assumptions,
136		bool inUnsatCore,
137		bool isEntailmentCheck)
138		{
139		// update the state to indicate we are about to run a check-sat
140	12761	bool hasAssumptions = !assumptions.empty();
141	12761	d_state.notifyCheckSat(hasAssumptions);
142
143		// then, initialize the assertions
144	12761	as.initializeCheckSat(assumptions, inUnsatCore, isEntailmentCheck);
145
146		// make the check
147	12761	Assert(d_smt.isFullyInited());
148
149	12761	Trace("smt") << "SmtSolver::check()" << endl;
150
151	12761	const std::string& filename = d_state.getFilename();
152	12761	ResourceManager* rm = d_env.getResourceManager();
153	12761	if (rm->out())
154		{
155		Result::UnknownExplanation why =
156		rm->outOfResources() ? Result::RESOURCEOUT : Result::TIMEOUT;
157		return Result(Result::ENTAILMENT_UNKNOWN, why, filename);
158		}
159	12761	rm->beginCall();
160
161		// Make sure the prop layer has all of the assertions
162	12761	Trace("smt") << "SmtSolver::check(): processing assertions" << endl;
163	12761	processAssertions(as);
164	12748	Trace("smt") << "SmtSolver::check(): done processing assertions" << endl;
165
166	25496	TimerStat::CodeTimer solveTimer(d_stats.d_solveTime);
167
168	12748	Chat() << "solving..." << endl;
169	12748	Trace("smt") << "SmtSolver::check(): running check" << endl;
170	25480	Result result = d_propEngine->checkSat();
171
172	12732	rm->endCall();
173	25464	Trace("limit") << "SmtSolver::check(): cumulative millis "
174	25464	<< rm->getTimeUsage() << ", resources "
175	12732	<< rm->getResourceUsage() << endl;
176
177	38183	if ((options::solveRealAsInt() \|\| options::solveIntAsBV() > 0)
178	25485	&& result.asSatisfiabilityResult().isSat() == Result::UNSAT)
179		{
180	4	result = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
181		}
182		// flipped if we did a global negation
183	12732	if (as.isGlobalNegated())
184		{
185	6	Trace("smt") << "SmtSolver::process global negate " << result << std::endl;
186	6	if (result.asSatisfiabilityResult().isSat() == Result::UNSAT)
187		{
188	4	result = Result(Result::SAT);
189		}
190	2	else if (result.asSatisfiabilityResult().isSat() == Result::SAT)
191		{
192		// Only can answer unsat if the theory is satisfaction complete. This
193		// includes linear arithmetic and bitvectors, which are the primary
194		// targets for the global negate option. Other logics are possible here
195		// but not considered.
196	4	LogicInfo logic = d_env.getLogicInfo();
197	2	if ((logic.isPure(theory::THEORY_ARITH) && logic.isLinear()) \|\|
198		logic.isPure(theory::THEORY_BV))
199		{
200	2	result = Result(Result::UNSAT);
201		}
202		else
203		{
204		result = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
205		}
206		}
207	6	Trace("smt") << "SmtSolver::global negate returned " << result << std::endl;
208		}
209
210		// set the filename on the result
211	25464	Result r = Result(result, filename);
212
213		// notify our state of the check-sat result
214	12732	d_state.notifyCheckSatResult(hasAssumptions, r);
215
216	12732	return r;
217		}
218
219	19263	void SmtSolver::processAssertions(Assertions& as)
220		{
221	30903	TimerStat::CodeTimer paTimer(d_stats.d_processAssertionsTime);
222	19263	d_env.getResourceManager()->spendResource(Resource::PreprocessStep);
223	19263	Assert(d_state.isFullyReady());
224
225	19263	preprocessing::AssertionPipeline& ap = as.getAssertionPipeline();
226
227	19263	if (ap.size() == 0)
228		{
229		// nothing to do
230	7623	return;
231		}
232
233		// process the assertions with the preprocessor
234	11640	d_pp.process(as);
235
236		// end: INVARIANT to maintain: no reordering of assertions or
237		// introducing new ones
238
239		// Push the formula to SAT
240		{
241	11631	Chat() << "converting to CNF..." << endl;
242	23262	TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime);
243	11631	const std::vector<Node>& assertions = ap.ref();
244		// It is important to distinguish the input assertions from the skolem
245		// definitions, as the decision justification heuristic treates the latter
246		// specially.
247	11631	preprocessing::IteSkolemMap& ism = ap.getIteSkolemMap();
248	11631	d_propEngine->assertInputFormulas(assertions, ism);
249		}
250
251		// clear the current assertions
252	11627	as.clearCurrent();
253		}
254
255	3117	void SmtSolver::setProofNodeManager(ProofNodeManager* pnm) { d_pnm = pnm; }
256
257	340401	TheoryEngine* SmtSolver::getTheoryEngine() { return d_theoryEngine.get(); }
258
259	55442	prop::PropEngine* SmtSolver::getPropEngine() { return d_propEngine.get(); }
260
261	364	theory::QuantifiersEngine* SmtSolver::getQuantifiersEngine()
262		{
263	364	Assert(d_theoryEngine != nullptr);
264	364	return d_theoryEngine->getQuantifiersEngine();
265		}
266
267		Preprocessor* SmtSolver::getPreprocessor() { return &d_pp; }
268
269		} // namespace smt
270	27735	} // namespace cvc5