Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/main/command_executor.cpp	Lines:	74	99	74.7 %
Date:	2021-05-22	Branches:	113	210	53.8 %


/******************************************************************************
 * 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 "smt/command.h"
#include "smt/smt_engine.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(Options& options)
    : d_solver(new api::Solver(&options)),
      d_symman(new SymbolManager(d_solver.get())),
      d_options(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
{
  if (d_options.getStatistics())
  {
    getSmtEngine()->printStatistics(out);
  }
}

void CommandExecutor::printStatisticsSafe(int fd) const
{
  if (d_options.getStatistics())
  {
    getSmtEngine()->printStatisticsSafe(fd);
  }
}

bool CommandExecutor::doCommand(Command* cmd)
{
  if( d_options.getParseOnly() ) {
    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_options.getVerbosity() > 2) {
      *d_options.getOut() << "Invoking: " << *cmd << std::endl;
    }

    return doCommandSingleton(cmd);
  }
}

void CommandExecutor::reset()
{
  printStatistics(*d_options.getErr());
  /* We have to keep options passed via CL on reset. These options are stored
   * in CommandExecutor::d_options (populated and created in the driver), and
   * CommandExecutor::d_options only contains *these* options since the
   * NodeManager copies the options into a new options object before SmtEngine
   * configures additional options based on the given CL options.
   * We can thus safely reuse CommandExecutor::d_options here. */
  d_solver.reset(new api::Solver(&d_options));
}

bool CommandExecutor::doCommandSingleton(Command* cmd)
{
  bool status = true;
  if(d_options.getVerbosity() >= -1) {
    status =
        solverInvoke(d_solver.get(), d_symman.get(), cmd, d_options.getOut());
  } 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();
  }

  if((cs != nullptr || q != nullptr) && d_options.getStatsEveryQuery()) {
    getSmtEngine()->printStatisticsDiff(*d_options.getErr());
  }

  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_options.getDumpModels()
        && (res.isSat()
            || (res.isSatUnknown()
                && res.getUnknownExplanation() == api::Result::INCOMPLETE)))
    {
      getterCommands.emplace_back(new GetModelCommand());
    }
    if (d_options.getDumpProofs() && isResultUnsat)
    {
      getterCommands.emplace_back(new GetProofCommand());
    }

    if (d_options.getDumpInstantiations()
        && ((d_options.getInstFormatMode() != options::InstFormatMode::SZS
             && (res.isSat()
                 || (res.isSatUnknown()
                     && res.getUnknownExplanation()
                            == api::Result::INCOMPLETE)))
            || isResultUnsat))
    {
      getterCommands.emplace_back(new GetInstantiationsCommand());
    }

    if (d_options.getDumpUnsatCores() && isResultUnsat)
    {
      getterCommands.emplace_back(new GetUnsatCoreCommand());
    }

    if (!getterCommands.empty()) {
      // set no time limit during dumping if applicable
      if (d_options.getForceNoLimitCpuWhileDump()) {
        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_options.getErr()));

  // make sure out and err streams are flushed too
  d_options.flushOut();
  d_options.flushErr();
}

}  // 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 "smt/command.h"
30		#include "smt/smt_engine.h"
31
32		namespace cvc5 {
33		namespace main {
34
35		// Function to cancel any (externally-imposed) limit on CPU time.
36		// This is used for competitions while a solution (proof or model)
37		// is being dumped (so that we don't give "sat" or "unsat" then get
38		// interrupted partway through outputting a proof!).
39		void setNoLimitCPU() {
40		// Windows doesn't have these things, just ignore
41		#ifndef __WIN32__
42		struct rlimit rlc;
43		int st = getrlimit(RLIMIT_CPU, &rlc);
44		if(st == 0) {
45		rlc.rlim_cur = rlc.rlim_max;
46		setrlimit(RLIMIT_CPU, &rlc);
47		}
48		#endif /* ! __WIN32__ */
49		}
50
51	5881	CommandExecutor::CommandExecutor(Options& options)
52	5882	: d_solver(new api::Solver(&options)),
53	5880	d_symman(new SymbolManager(d_solver.get())),
54		d_options(options),
55	17641	d_result()
56		{
57	5880	}
58	17640	CommandExecutor::~CommandExecutor()
59		{
60		// ensure that symbol manager is destroyed before solver
61	5880	d_symman.reset(nullptr);
62	5880	d_solver.reset(nullptr);
63	11760	}
64
65	5860	void CommandExecutor::printStatistics(std::ostream& out) const
66		{
67	5860	if (d_options.getStatistics())
68		{
69		getSmtEngine()->printStatistics(out);
70		}
71	5860	}
72
73		void CommandExecutor::printStatisticsSafe(int fd) const
74		{
75		if (d_options.getStatistics())
76		{
77		getSmtEngine()->printStatisticsSafe(fd);
78		}
79		}
80
81	306345	bool CommandExecutor::doCommand(Command* cmd)
82		{
83	306345	if( d_options.getParseOnly() ) {
84		return true;
85		}
86
87	306345	CommandSequence seq = dynamic_cast<CommandSequence>(cmd);
88	306345	if(seq != nullptr) {
89		// assume no error
90	5124	bool status = true;
91
92	13057	for (CommandSequence::iterator subcmd = seq->begin();
93	13057	status && subcmd != seq->end();
94		++subcmd)
95		{
96	7933	status = doCommand(*subcmd);
97		}
98
99	5124	return status;
100		} else {
101	301221	if(d_options.getVerbosity() > 2) {
102	11	d_options.getOut() << "Invoking: " << cmd << std::endl;
103		}
104
105	301221	return doCommandSingleton(cmd);
106		}
107		}
108
109		void CommandExecutor::reset()
110		{
111		printStatistics(*d_options.getErr());
112		/* We have to keep options passed via CL on reset. These options are stored
113		* in CommandExecutor::d_options (populated and created in the driver), and
114		* CommandExecutor::d_options only contains these options since the
115		* NodeManager copies the options into a new options object before SmtEngine
116		* configures additional options based on the given CL options.
117		* We can thus safely reuse CommandExecutor::d_options here. */
118		d_solver.reset(new api::Solver(&d_options));
119		}
120
121	301249	bool CommandExecutor::doCommandSingleton(Command* cmd)
122		{
123	301249	bool status = true;
124	301249	if(d_options.getVerbosity() >= -1) {
125	301249	status =
126	301249	solverInvoke(d_solver.get(), d_symman.get(), cmd, d_options.getOut());
127		} else {
128		status = solverInvoke(d_solver.get(), d_symman.get(), cmd, nullptr);
129		}
130
131	602498	api::Result res;
132	301249	const CheckSatCommand* cs = dynamic_cast<const CheckSatCommand*>(cmd);
133	301249	if(cs != nullptr) {
134	8854	d_result = res = cs->getResult();
135		}
136		const CheckSatAssumingCommand* csa =
137	301249	dynamic_cast<const CheckSatAssumingCommand*>(cmd);
138	301249	if (csa != nullptr)
139		{
140	990	d_result = res = csa->getResult();
141		}
142	301249	const QueryCommand* q = dynamic_cast<const QueryCommand*>(cmd);
143	301249	if(q != nullptr) {
144	612	d_result = res = q->getResult();
145		}
146
147	301249	if((cs != nullptr \|\| q != nullptr) && d_options.getStatsEveryQuery()) {
148		getSmtEngine()->printStatisticsDiff(*d_options.getErr());
149		}
150
151	301249	bool isResultUnsat = res.isUnsat() \|\| res.isEntailed();
152
153		// dump the model/proof/unsat core if option is set
154	301249	if (status) {
155	602428	std::vector<std::unique_ptr<Command> > getterCommands;
156	602428	if (d_options.getDumpModels()
157	301224	&& (res.isSat()
158	34	\|\| (res.isSatUnknown()
159		&& res.getUnknownExplanation() == api::Result::INCOMPLETE)))
160		{
161	10	getterCommands.emplace_back(new GetModelCommand());
162		}
163	301214	if (d_options.getDumpProofs() && isResultUnsat)
164		{
165		getterCommands.emplace_back(new GetProofCommand());
166		}
167
168	602428	if (d_options.getDumpInstantiations()
169	301229	&& ((d_options.getInstFormatMode() != options::InstFormatMode::SZS
170	153	&& (res.isSat()
171	153	\|\| (res.isSatUnknown()
172		&& res.getUnknownExplanation()
173		== api::Result::INCOMPLETE)))
174	153	\|\| isResultUnsat))
175		{
176	15	getterCommands.emplace_back(new GetInstantiationsCommand());
177		}
178
179	301214	if (d_options.getDumpUnsatCores() && isResultUnsat)
180		{
181	3	getterCommands.emplace_back(new GetUnsatCoreCommand());
182		}
183
184	301214	if (!getterCommands.empty()) {
185		// set no time limit during dumping if applicable
186	28	if (d_options.getForceNoLimitCpuWhileDump()) {
187		setNoLimitCPU();
188		}
189	56	for (const auto& getterCommand : getterCommands) {
190	28	status = doCommandSingleton(getterCommand.get());
191	28	if (!status)
192		{
193		break;
194		}
195		}
196		}
197		}
198	602498	return status;
199		}
200
201	301249	bool solverInvoke(api::Solver* solver,
202		SymbolManager* sm,
203		Command* cmd,
204		std::ostream* out)
205		{
206	301249	if (out == NULL)
207		{
208		cmd->invoke(solver, sm);
209		}
210		else
211		{
212	301249	cmd->invoke(solver, sm, *out);
213		}
214		// ignore the error if the command-verbosity is 0 for this command
215		std::string commandName =
216	602498	std::string("command-verbosity:") + cmd->getCommandName();
217	301249	if (solver->getOption(commandName) == "0")
218		{
219		return true;
220		}
221	301249	return !cmd->fail();
222		}
223
224	5860	void CommandExecutor::flushOutputStreams() {
225	5860	printStatistics(*(d_options.getErr()));
226
227		// make sure out and err streams are flushed too
228	5860	d_options.flushOut();
229	5860	d_options.flushErr();
230	5860	}
231
232		} // namespace main
233	28176	} // namespace cvc5