Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/main/command_executor.cpp	Lines:	75	101	74.3 %
Date:	2021-08-03	Branches:	106	212	50.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Kshitij Bansal, Andrew Reynolds, 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.
 * ****************************************************************************
 *
 * An additional layer between commands and invoking them.
 */

#include "main/command_executor.h"

#ifndef __WIN32__
#  include <sys/resource.h>
#endif /* ! __WIN32__ */

#include <iomanip>
#include <iostream>
#include <memory>
#include <string>
#include <vector>

#include "main/main.h"
#include "options/base_options.h"
#include "options/main_options.h"
#include "smt/command.h"

namespace cvc5 {
namespace main {

// Function to cancel any (externally-imposed) limit on CPU time.
// This is used for competitions while a solution (proof or model)
// is being dumped (so that we don't give "sat" or "unsat" then get
// interrupted partway through outputting a proof!).
void setNoLimitCPU() {
  // Windows doesn't have these things, just ignore
#ifndef __WIN32__
  struct rlimit rlc;
  int st = getrlimit(RLIMIT_CPU, &rlc);
  if(st == 0) {
    rlc.rlim_cur = rlc.rlim_max;
    setrlimit(RLIMIT_CPU, &rlc);
  }
#endif /* ! __WIN32__ */
}

CommandExecutor::CommandExecutor(const Options& options)
    : d_solver(new api::Solver(&options)),
      d_symman(new SymbolManager(d_solver.get())),
      d_driverOptions(&options),
      d_result()
{
}
CommandExecutor::~CommandExecutor()
{
  // ensure that symbol manager is destroyed before solver
  d_symman.reset(nullptr);
  d_solver.reset(nullptr);
}

void CommandExecutor::printStatistics(std::ostream& out) const
{
  const auto& baseopts = d_solver->getOptions().base;
  if (baseopts.statistics)
  {
    const auto& stats = d_solver->getStatistics();
    auto it = stats.begin(baseopts.statisticsExpert, baseopts.statisticsAll);
    for (; it != stats.end(); ++it)
    {
      out << it->first << " = " << it->second << std::endl;
    }
  }
}

void CommandExecutor::printStatisticsSafe(int fd) const
{
  if (d_solver->getOptions().base.statistics)
  {
    d_solver->printStatisticsSafe(fd);
  }
}

bool CommandExecutor::doCommand(Command* cmd)
{
  if (d_solver->getOptions().base.parseOnly)
  {
    return true;
  }

  CommandSequence *seq = dynamic_cast<CommandSequence*>(cmd);
  if(seq != nullptr) {
    // assume no error
    bool status = true;

    for (CommandSequence::iterator subcmd = seq->begin();
         status && subcmd != seq->end();
         ++subcmd)
    {
      status = doCommand(*subcmd);
    }

    return status;
  } else {
    if (d_solver->getOptions().base.verbosity > 2)
    {
      *d_solver->getOptions().base.out << "Invoking: " << *cmd << std::endl;
    }

    return doCommandSingleton(cmd);
  }
}

void CommandExecutor::reset()
{
  printStatistics(*d_solver->getOptions().base.err);
  /* We have to keep options passed via CL on reset. These options are stored
   * in CommandExecutor::d_driverOptions (populated and created in the driver),
   * and CommandExecutor::d_driverOptions only contains *these* options since
   * the SmtEngine copies them into its own options object before configuring
   * additional options based on the given CL options.
   * We can thus safely reuse CommandExecutor::d_driverOptions here.
   */
  d_solver.reset(new api::Solver(d_driverOptions));
}

bool CommandExecutor::doCommandSingleton(Command* cmd)
{
  bool status = true;
  if (d_solver->getOptions().base.verbosity >= -1)
  {
    status = solverInvoke(
        d_solver.get(), d_symman.get(), cmd, d_solver->getOptions().base.out);
  }
  else
  {
    status = solverInvoke(d_solver.get(), d_symman.get(), cmd, nullptr);
  }

  api::Result res;
  const CheckSatCommand* cs = dynamic_cast<const CheckSatCommand*>(cmd);
  if(cs != nullptr) {
    d_result = res = cs->getResult();
  }
  const CheckSatAssumingCommand* csa =
      dynamic_cast<const CheckSatAssumingCommand*>(cmd);
  if (csa != nullptr)
  {
    d_result = res = csa->getResult();
  }
  const QueryCommand* q = dynamic_cast<const QueryCommand*>(cmd);
  if(q != nullptr) {
    d_result = res = q->getResult();
  }

  bool isResultUnsat = res.isUnsat() || res.isEntailed();

  // dump the model/proof/unsat core if option is set
  if (status) {
    std::vector<std::unique_ptr<Command> > getterCommands;
    if (d_solver->getOptions().driver.dumpModels
        && (res.isSat()
            || (res.isSatUnknown()
                && res.getUnknownExplanation() == api::Result::INCOMPLETE)))
    {
      getterCommands.emplace_back(new GetModelCommand());
    }
    if (d_solver->getOptions().driver.dumpProofs && isResultUnsat)
    {
      getterCommands.emplace_back(new GetProofCommand());
    }

    if (d_solver->getOptions().driver.dumpInstantiations
        && GetInstantiationsCommand::isEnabled(d_solver.get(), res))
    {
      getterCommands.emplace_back(new GetInstantiationsCommand());
    }

    if ((d_solver->getOptions().driver.dumpUnsatCores
         || d_solver->getOptions().driver.dumpUnsatCoresFull)
        && isResultUnsat)
    {
      getterCommands.emplace_back(new GetUnsatCoreCommand());
    }

    if (!getterCommands.empty()) {
      // set no time limit during dumping if applicable
      if (d_solver->getOptions().driver.forceNoLimitCpuWhileDump)
      {
        setNoLimitCPU();
      }
      for (const auto& getterCommand : getterCommands) {
        status = doCommandSingleton(getterCommand.get());
        if (!status)
        {
          break;
        }
      }
    }
  }
  return status;
}

bool solverInvoke(api::Solver* solver,
                  SymbolManager* sm,
                  Command* cmd,
                  std::ostream* out)
{
  if (out == NULL)
  {
    cmd->invoke(solver, sm);
  }
  else
  {
    cmd->invoke(solver, sm, *out);
  }
  // ignore the error if the command-verbosity is 0 for this command
  std::string commandName =
      std::string("command-verbosity:") + cmd->getCommandName();
  if (solver->getOption(commandName) == "0")
  {
    return true;
  }
  return !cmd->fail();
}

void CommandExecutor::flushOutputStreams() {
  printStatistics(*d_solver->getOptions().base.err);

  // make sure out and err streams are flushed too

  if (d_solver->getOptions().base.out != nullptr)
  {
    *d_solver->getOptions().base.out << std::flush;
  }
  if (d_solver->getOptions().base.err != nullptr)
  {
    *d_solver->getOptions().base.err << std::flush;
  }
}

}  // namespace main
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Kshitij Bansal, Andrew Reynolds, 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		* An additional layer between commands and invoking them.
14		*/
15
16		#include "main/command_executor.h"
17
18		#ifndef __WIN32__
19		# include <sys/resource.h>
20		#endif /* ! __WIN32__ */
21
22		#include <iomanip>
23		#include <iostream>
24		#include <memory>
25		#include <string>
26		#include <vector>
27
28		#include "main/main.h"
29		#include "options/base_options.h"
30		#include "options/main_options.h"
31		#include "smt/command.h"
32
33		namespace cvc5 {
34		namespace main {
35
36		// Function to cancel any (externally-imposed) limit on CPU time.
37		// This is used for competitions while a solution (proof or model)
38		// is being dumped (so that we don't give "sat" or "unsat" then get
39		// interrupted partway through outputting a proof!).
40		void setNoLimitCPU() {
41		// Windows doesn't have these things, just ignore
42		#ifndef __WIN32__
43		struct rlimit rlc;
44		int st = getrlimit(RLIMIT_CPU, &rlc);
45		if(st == 0) {
46		rlc.rlim_cur = rlc.rlim_max;
47		setrlimit(RLIMIT_CPU, &rlc);
48		}
49		#endif /* ! __WIN32__ */
50		}
51
52	6124	CommandExecutor::CommandExecutor(const Options& options)
53	6125	: d_solver(new api::Solver(&options)),
54	6123	d_symman(new SymbolManager(d_solver.get())),
55		d_driverOptions(&options),
56	18370	d_result()
57		{
58	6123	}
59	18369	CommandExecutor::~CommandExecutor()
60		{
61		// ensure that symbol manager is destroyed before solver
62	6123	d_symman.reset(nullptr);
63	6123	d_solver.reset(nullptr);
64	12246	}
65
66	6103	void CommandExecutor::printStatistics(std::ostream& out) const
67		{
68	6103	const auto& baseopts = d_solver->getOptions().base;
69	6103	if (baseopts.statistics)
70		{
71		const auto& stats = d_solver->getStatistics();
72		auto it = stats.begin(baseopts.statisticsExpert, baseopts.statisticsAll);
73		for (; it != stats.end(); ++it)
74		{
75		out << it->first << " = " << it->second << std::endl;
76		}
77		}
78	6103	}
79
80		void CommandExecutor::printStatisticsSafe(int fd) const
81		{
82		if (d_solver->getOptions().base.statistics)
83		{
84		d_solver->printStatisticsSafe(fd);
85		}
86		}
87
88	306553	bool CommandExecutor::doCommand(Command* cmd)
89		{
90	306553	if (d_solver->getOptions().base.parseOnly)
91		{
92		return true;
93		}
94
95	306553	CommandSequence seq = dynamic_cast<CommandSequence>(cmd);
96	306553	if(seq != nullptr) {
97		// assume no error
98	5080	bool status = true;
99
100	12967	for (CommandSequence::iterator subcmd = seq->begin();
101	12967	status && subcmd != seq->end();
102		++subcmd)
103		{
104	7887	status = doCommand(*subcmd);
105		}
106
107	5080	return status;
108		} else {
109	301473	if (d_solver->getOptions().base.verbosity > 2)
110		{
111	11	d_solver->getOptions().base.out << "Invoking: " << cmd << std::endl;
112		}
113
114	301473	return doCommandSingleton(cmd);
115		}
116		}
117
118		void CommandExecutor::reset()
119		{
120		printStatistics(*d_solver->getOptions().base.err);
121		/* We have to keep options passed via CL on reset. These options are stored
122		* in CommandExecutor::d_driverOptions (populated and created in the driver),
123		* and CommandExecutor::d_driverOptions only contains these options since
124		* the SmtEngine copies them into its own options object before configuring
125		* additional options based on the given CL options.
126		* We can thus safely reuse CommandExecutor::d_driverOptions here.
127		*/
128		d_solver.reset(new api::Solver(d_driverOptions));
129		}
130
131	301501	bool CommandExecutor::doCommandSingleton(Command* cmd)
132		{
133	301501	bool status = true;
134	301501	if (d_solver->getOptions().base.verbosity >= -1)
135		{
136	301501	status = solverInvoke(
137	301501	d_solver.get(), d_symman.get(), cmd, d_solver->getOptions().base.out);
138		}
139		else
140		{
141		status = solverInvoke(d_solver.get(), d_symman.get(), cmd, nullptr);
142		}
143
144	603002	api::Result res;
145	301501	const CheckSatCommand* cs = dynamic_cast<const CheckSatCommand*>(cmd);
146	301501	if(cs != nullptr) {
147	9190	d_result = res = cs->getResult();
148		}
149		const CheckSatAssumingCommand* csa =
150	301501	dynamic_cast<const CheckSatAssumingCommand*>(cmd);
151	301501	if (csa != nullptr)
152		{
153	992	d_result = res = csa->getResult();
154		}
155	301501	const QueryCommand* q = dynamic_cast<const QueryCommand*>(cmd);
156	301501	if(q != nullptr) {
157	609	d_result = res = q->getResult();
158		}
159
160	301501	bool isResultUnsat = res.isUnsat() \|\| res.isEntailed();
161
162		// dump the model/proof/unsat core if option is set
163	301501	if (status) {
164	602926	std::vector<std::unique_ptr<Command> > getterCommands;
165	602926	if (d_solver->getOptions().driver.dumpModels
166	301473	&& (res.isSat()
167	34	\|\| (res.isSatUnknown()
168		&& res.getUnknownExplanation() == api::Result::INCOMPLETE)))
169		{
170	10	getterCommands.emplace_back(new GetModelCommand());
171		}
172	301463	if (d_solver->getOptions().driver.dumpProofs && isResultUnsat)
173		{
174		getterCommands.emplace_back(new GetProofCommand());
175		}
176
177	602926	if (d_solver->getOptions().driver.dumpInstantiations
178	301463	&& GetInstantiationsCommand::isEnabled(d_solver.get(), res))
179		{
180	15	getterCommands.emplace_back(new GetInstantiationsCommand());
181		}
182
183	602926	if ((d_solver->getOptions().driver.dumpUnsatCores
184	301454	\|\| d_solver->getOptions().driver.dumpUnsatCoresFull)
185	301487	&& isResultUnsat)
186		{
187	3	getterCommands.emplace_back(new GetUnsatCoreCommand());
188		}
189
190	301463	if (!getterCommands.empty()) {
191		// set no time limit during dumping if applicable
192	28	if (d_solver->getOptions().driver.forceNoLimitCpuWhileDump)
193		{
194		setNoLimitCPU();
195		}
196	56	for (const auto& getterCommand : getterCommands) {
197	28	status = doCommandSingleton(getterCommand.get());
198	28	if (!status)
199		{
200		break;
201		}
202		}
203		}
204		}
205	603002	return status;
206		}
207
208	301501	bool solverInvoke(api::Solver* solver,
209		SymbolManager* sm,
210		Command* cmd,
211		std::ostream* out)
212		{
213	301501	if (out == NULL)
214		{
215		cmd->invoke(solver, sm);
216		}
217		else
218		{
219	301501	cmd->invoke(solver, sm, *out);
220		}
221		// ignore the error if the command-verbosity is 0 for this command
222		std::string commandName =
223	603002	std::string("command-verbosity:") + cmd->getCommandName();
224	301501	if (solver->getOption(commandName) == "0")
225		{
226		return true;
227		}
228	301501	return !cmd->fail();
229		}
230
231	6103	void CommandExecutor::flushOutputStreams() {
232	6103	printStatistics(*d_solver->getOptions().base.err);
233
234		// make sure out and err streams are flushed too
235
236	6103	if (d_solver->getOptions().base.out != nullptr)
237		{
238	6103	*d_solver->getOptions().base.out << std::flush;
239		}
240	6103	if (d_solver->getOptions().base.err != nullptr)
241		{
242	6103	*d_solver->getOptions().base.err << std::flush;
243		}
244	6103	}
245
246		} // namespace main
247	29265	} // namespace cvc5