Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/smt/smt_solver.cpp	Lines:	90	100	90.0 %
Date:	2021-11-07	Branches:	137	286	47.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 SolverEngine.
 */

#include "smt/smt_solver.h"

#include "options/main_options.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/solver_engine.h"
#include "smt/solver_engine_state.h"
#include "smt/solver_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(Env& env,
                     SolverEngineState& state,
                     AbstractValues& abs,
                     SolverEngineStatistics& stats)
    : d_env(env),
      d_state(state),
      d_pp(env, abs, stats),
      d_stats(stats),
      d_theoryEngine(nullptr),
      d_propEngine(nullptr)
{
}

SmtSolver::~SmtSolver() {}

void SmtSolver::finishInit()
{
  // 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));

  // 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
  ProofNodeManager* pnm = d_env.getProofNodeManager();
  if (pnm)
  {
    d_theoryEngine->initializeProofChecker(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));

  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();

  d_pp.finishInit(d_theoryEngine.get(), d_propEngine.get());
}

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_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();
  // must reset the preprocessor as well
  d_pp.finishInit(d_theoryEngine.get(), d_propEngine.get());
}

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 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, isEntailmentCheck);

  // make the check, where notice smt engine should be fully inited by now

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

  const std::string& filename = d_env.getOptions().driver.filename;
  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);

  d_env.verbose(2) << "solving..." << std::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
  {
    d_env.verbose(2) << "converting to CNF..." << endl;
    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();
}

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 SolverEngine.
14		*/
15
16		#include "smt/smt_solver.h"
17
18		#include "options/main_options.h"
19		#include "options/smt_options.h"
20		#include "prop/prop_engine.h"
21		#include "smt/assertions.h"
22		#include "smt/env.h"
23		#include "smt/preprocessor.h"
24		#include "smt/solver_engine.h"
25		#include "smt/solver_engine_state.h"
26		#include "smt/solver_engine_stats.h"
27		#include "theory/logic_info.h"
28		#include "theory/theory_engine.h"
29		#include "theory/theory_traits.h"
30
31		using namespace std;
32
33		namespace cvc5 {
34		namespace smt {
35
36	18633	SmtSolver::SmtSolver(Env& env,
37		SolverEngineState& state,
38		AbstractValues& abs,
39	18633	SolverEngineStatistics& stats)
40		: d_env(env),
41		d_state(state),
42		d_pp(env, abs, stats),
43		d_stats(stats),
44		d_theoryEngine(nullptr),
45	18633	d_propEngine(nullptr)
46		{
47	18633	}
48
49	15884	SmtSolver::~SmtSolver() {}
50
51	15273	void SmtSolver::finishInit()
52		{
53		// We have mutual dependency here, so we add the prop engine to the theory
54		// engine later (it is non-essential there)
55	15273	d_theoryEngine.reset(new TheoryEngine(d_env));
56
57		// Add the theories
58	213822	for (theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST;
59		++id)
60		{
61	198549	theory::TheoryConstructor::addTheory(d_theoryEngine.get(), id);
62		}
63		// Add the proof checkers for each theory
64	15273	ProofNodeManager* pnm = d_env.getProofNodeManager();
65	15273	if (pnm)
66		{
67	7989	d_theoryEngine->initializeProofChecker(pnm->getChecker());
68		}
69	15273	Trace("smt-debug") << "Making prop engine..." << std::endl;
70		/* force destruction of referenced PropEngine to enforce that statistics
71		* are unregistered by the obsolete PropEngine object before registered
72		* again by the new PropEngine object */
73	15273	d_propEngine.reset(nullptr);
74	15273	d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(), d_env));
75
76	15273	Trace("smt-debug") << "Setting up theory engine..." << std::endl;
77	15273	d_theoryEngine->setPropEngine(getPropEngine());
78	15273	Trace("smt-debug") << "Finishing init for theory engine..." << std::endl;
79	15273	d_theoryEngine->finishInit();
80	15273	d_propEngine->finishInit();
81
82	15273	d_pp.finishInit(d_theoryEngine.get(), d_propEngine.get());
83	15273	}
84
85	67	void SmtSolver::resetAssertions()
86		{
87		/* Create new PropEngine.
88		* First force destruction of referenced PropEngine to enforce that
89		* statistics are unregistered by the obsolete PropEngine object before
90		* registered again by the new PropEngine object */
91	67	d_propEngine.reset(nullptr);
92	67	d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(), d_env));
93	67	d_theoryEngine->setPropEngine(getPropEngine());
94		// Notice that we do not reset TheoryEngine, nor does it require calling
95		// finishInit again. In particular, TheoryEngine::finishInit does not
96		// depend on knowing the associated PropEngine.
97	67	d_propEngine->finishInit();
98		// must reset the preprocessor as well
99	67	d_pp.finishInit(d_theoryEngine.get(), d_propEngine.get());
100	67	}
101
102		void SmtSolver::interrupt()
103		{
104		if (d_propEngine != nullptr)
105		{
106		d_propEngine->interrupt();
107		}
108		if (d_theoryEngine != nullptr)
109		{
110		d_theoryEngine->interrupt();
111		}
112		}
113
114	15884	void SmtSolver::shutdown()
115		{
116	15884	if (d_propEngine != nullptr)
117		{
118	15268	d_propEngine->shutdown();
119		}
120	15884	if (d_theoryEngine != nullptr)
121		{
122	15268	d_theoryEngine->shutdown();
123		}
124	15884	}
125
126	20579	Result SmtSolver::checkSatisfiability(Assertions& as,
127		const std::vector<Node>& assumptions,
128		bool isEntailmentCheck)
129		{
130		// update the state to indicate we are about to run a check-sat
131	20579	bool hasAssumptions = !assumptions.empty();
132	20579	d_state.notifyCheckSat(hasAssumptions);
133
134		// then, initialize the assertions
135	20579	as.initializeCheckSat(assumptions, isEntailmentCheck);
136
137		// make the check, where notice smt engine should be fully inited by now
138
139	20579	Trace("smt") << "SmtSolver::check()" << endl;
140
141	20579	const std::string& filename = d_env.getOptions().driver.filename;
142	20579	ResourceManager* rm = d_env.getResourceManager();
143	20579	if (rm->out())
144		{
145		Result::UnknownExplanation why =
146		rm->outOfResources() ? Result::RESOURCEOUT : Result::TIMEOUT;
147		return Result(Result::ENTAILMENT_UNKNOWN, why, filename);
148		}
149	20579	rm->beginCall();
150
151		// Make sure the prop layer has all of the assertions
152	20579	Trace("smt") << "SmtSolver::check(): processing assertions" << endl;
153	20579	processAssertions(as);
154	20560	Trace("smt") << "SmtSolver::check(): done processing assertions" << endl;
155
156	41120	TimerStat::CodeTimer solveTimer(d_stats.d_solveTime);
157
158	20560	d_env.verbose(2) << "solving..." << std::endl;
159	20560	Trace("smt") << "SmtSolver::check(): running check" << endl;
160	41097	Result result = d_propEngine->checkSat();
161
162	20537	rm->endCall();
163	41074	Trace("limit") << "SmtSolver::check(): cumulative millis "
164	41074	<< rm->getTimeUsage() << ", resources "
165	20537	<< rm->getResourceUsage() << endl;
166
167	61598	if ((options::solveRealAsInt() \|\| options::solveIntAsBV() > 0)
168	41103	&& result.asSatisfiabilityResult().isSat() == Result::UNSAT)
169		{
170	6	result = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
171		}
172		// flipped if we did a global negation
173	20537	if (as.isGlobalNegated())
174		{
175	6	Trace("smt") << "SmtSolver::process global negate " << result << std::endl;
176	6	if (result.asSatisfiabilityResult().isSat() == Result::UNSAT)
177		{
178	4	result = Result(Result::SAT);
179		}
180	2	else if (result.asSatisfiabilityResult().isSat() == Result::SAT)
181		{
182		// Only can answer unsat if the theory is satisfaction complete. This
183		// includes linear arithmetic and bitvectors, which are the primary
184		// targets for the global negate option. Other logics are possible here
185		// but not considered.
186	4	LogicInfo logic = d_env.getLogicInfo();
187	2	if ((logic.isPure(theory::THEORY_ARITH) && logic.isLinear()) \|\|
188		logic.isPure(theory::THEORY_BV))
189		{
190	2	result = Result(Result::UNSAT);
191		}
192		else
193		{
194		result = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
195		}
196		}
197	6	Trace("smt") << "SmtSolver::global negate returned " << result << std::endl;
198		}
199
200		// set the filename on the result
201	41074	Result r = Result(result, filename);
202
203		// notify our state of the check-sat result
204	20537	d_state.notifyCheckSatResult(hasAssumptions, r);
205
206	20537	return r;
207		}
208
209	29698	void SmtSolver::processAssertions(Assertions& as)
210		{
211	48808	TimerStat::CodeTimer paTimer(d_stats.d_processAssertionsTime);
212	29698	d_env.getResourceManager()->spendResource(Resource::PreprocessStep);
213	29698	Assert(d_state.isFullyReady());
214
215	29698	preprocessing::AssertionPipeline& ap = as.getAssertionPipeline();
216
217	29698	if (ap.size() == 0)
218		{
219		// nothing to do
220	10588	return;
221		}
222
223		// process the assertions with the preprocessor
224	19110	d_pp.process(as);
225
226		// end: INVARIANT to maintain: no reordering of assertions or
227		// introducing new ones
228
229		// Push the formula to SAT
230		{
231	19095	d_env.verbose(2) << "converting to CNF..." << endl;
232	19095	const std::vector<Node>& assertions = ap.ref();
233		// It is important to distinguish the input assertions from the skolem
234		// definitions, as the decision justification heuristic treates the latter
235		// specially.
236	19095	preprocessing::IteSkolemMap& ism = ap.getIteSkolemMap();
237	19095	d_propEngine->assertInputFormulas(assertions, ism);
238		}
239
240		// clear the current assertions
241	19091	as.clearCurrent();
242		}
243
244	52420	TheoryEngine* SmtSolver::getTheoryEngine() { return d_theoryEngine.get(); }
245
246	73699	prop::PropEngine* SmtSolver::getPropEngine() { return d_propEngine.get(); }
247
248	448	theory::QuantifiersEngine* SmtSolver::getQuantifiersEngine()
249		{
250	448	Assert(d_theoryEngine != nullptr);
251	448	return d_theoryEngine->getQuantifiersEngine();
252		}
253
254	39838	Preprocessor* SmtSolver::getPreprocessor() { return &d_pp; }
255
256		} // namespace smt
257	31137	} // namespace cvc5