Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/main/command_executor.cpp	Lines:	76	101	75.2 %
Date:	2021-11-07	Branches:	178	410	43.4 %


/******************************************************************************
 * 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/solver_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(std::unique_ptr<api::Solver>& solver)
    : d_solver(solver),
      d_symman(new SymbolManager(d_solver.get())),
      d_result()
{
}
CommandExecutor::~CommandExecutor()
{
}

void CommandExecutor::storeOptionsAsOriginal()
{
  d_solver->d_originalOptions->copyValues(d_solver->d_slv->getOptions());
}

void CommandExecutor::printStatistics(std::ostream& out) const
{
  if (d_solver->getOptionInfo("stats").boolValue())
  {
    const auto& stats = d_solver->getStatistics();
    auto it = stats.begin(d_solver->getOptionInfo("stats-expert").boolValue(),
                          d_solver->getOptionInfo("stats-all").boolValue());
    for (; it != stats.end(); ++it)
    {
      out << it->first << " = " << it->second << std::endl;
    }
  }
}

void CommandExecutor::printStatisticsSafe(int fd) const
{
  if (d_solver->getOptionInfo("stats").boolValue())
  {
    d_solver->printStatisticsSafe(fd);
  }
}

bool CommandExecutor::doCommand(Command* cmd)
{
  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->getOptionInfo("verbosity").intValue() > 2)
    {
      d_solver->getDriverOptions().out() << "Invoking: " << *cmd << std::endl;
    }

    return doCommandSingleton(cmd);
  }
}

void CommandExecutor::reset()
{
  printStatistics(d_solver->getDriverOptions().err());
  Command::resetSolver(d_solver.get());
}

bool CommandExecutor::doCommandSingleton(Command* cmd)
{
  bool status = solverInvoke(
      d_solver.get(), d_symman.get(), cmd, d_solver->getDriverOptions().out());

  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();
  bool isResultSat = res.isSat() || res.isNotEntailed();

  // dump the model/proof/unsat core if option is set
  if (status) {
    std::vector<std::unique_ptr<Command> > getterCommands;
    if (d_solver->getOptionInfo("dump-models").boolValue()
        && (isResultSat
            || (res.isSatUnknown()
                && res.getUnknownExplanation() == api::Result::INCOMPLETE)))
    {
      getterCommands.emplace_back(new GetModelCommand());
    }
    if (d_solver->getOptionInfo("dump-proofs").boolValue() && isResultUnsat)
    {
      getterCommands.emplace_back(new GetProofCommand());
    }

    if ((d_solver->getOptionInfo("dump-instantiations").boolValue()
         || d_solver->getOptionInfo("dump-instantiations-debug").boolValue())
        && GetInstantiationsCommand::isEnabled(d_solver.get(), res))
    {
      getterCommands.emplace_back(new GetInstantiationsCommand());
    }

    if (d_solver->getOptionInfo("dump-unsat-cores").boolValue()
        && isResultUnsat)
    {
      getterCommands.emplace_back(new GetUnsatCoreCommand());
    }

    if (d_solver->getOptionInfo("dump-difficulty").boolValue()
        && (isResultUnsat || isResultSat || res.isSatUnknown()))
    {
      getterCommands.emplace_back(new GetDifficultyCommand());
    }

    if (!getterCommands.empty()) {
      // set no time limit during dumping if applicable
      if (d_solver->getOptionInfo("force-no-limit-cpu-while-dump").boolValue())
      {
        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)
{
  // print output for -o raw-benchmark
  if (solver->isOutputOn("raw-benchmark"))
  {
    cmd->toStream(solver->getOutput("raw-benchmark"));
  }

  // In parse-only mode, we do not invoke any of the commands except define-fun
  // commands. We invoke define-fun commands because they add function names
  // to the symbol table.
  if (solver->getOptionInfo("parse-only").boolValue()
      && dynamic_cast<DefineFunctionCommand*>(cmd) == nullptr)
  {
    return true;
  }

  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->getDriverOptions().err());

  // make sure out and err streams are flushed too
  d_solver->getDriverOptions().out() << std::flush;
  d_solver->getDriverOptions().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 "smt/command.h"
30		#include "smt/solver_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	9312	CommandExecutor::CommandExecutor(std::unique_ptr<api::Solver>& solver)
52		: d_solver(solver),
53	9312	d_symman(new SymbolManager(d_solver.get())),
54	18624	d_result()
55		{
56	9312	}
57	18624	CommandExecutor::~CommandExecutor()
58		{
59	18624	}
60
61	6583	void CommandExecutor::storeOptionsAsOriginal()
62		{
63	6583	d_solver->d_originalOptions->copyValues(d_solver->d_slv->getOptions());
64	6583	}
65
66	6563	void CommandExecutor::printStatistics(std::ostream& out) const
67		{
68	6563	if (d_solver->getOptionInfo("stats").boolValue())
69		{
70		const auto& stats = d_solver->getStatistics();
71		auto it = stats.begin(d_solver->getOptionInfo("stats-expert").boolValue(),
72		d_solver->getOptionInfo("stats-all").boolValue());
73		for (; it != stats.end(); ++it)
74		{
75		out << it->first << " = " << it->second << std::endl;
76		}
77		}
78	6563	}
79
80		void CommandExecutor::printStatisticsSafe(int fd) const
81		{
82		if (d_solver->getOptionInfo("stats").boolValue())
83		{
84		d_solver->printStatisticsSafe(fd);
85		}
86		}
87
88	242553	bool CommandExecutor::doCommand(Command* cmd)
89		{
90	242553	CommandSequence seq = dynamic_cast<CommandSequence>(cmd);
91	242553	if(seq != nullptr) {
92		// assume no error
93	140	bool status = true;
94
95	493	for (CommandSequence::iterator subcmd = seq->begin();
96	493	status && subcmd != seq->end();
97		++subcmd)
98		{
99	353	status = doCommand(*subcmd);
100		}
101
102	140	return status;
103		} else {
104	242413	if (d_solver->getOptionInfo("verbosity").intValue() > 2)
105		{
106	11	d_solver->getDriverOptions().out() << "Invoking: " << *cmd << std::endl;
107		}
108
109	242413	return doCommandSingleton(cmd);
110		}
111		}
112
113		void CommandExecutor::reset()
114		{
115		printStatistics(d_solver->getDriverOptions().err());
116		Command::resetSolver(d_solver.get());
117		}
118
119	242442	bool CommandExecutor::doCommandSingleton(Command* cmd)
120		{
121	484884	bool status = solverInvoke(
122	727326	d_solver.get(), d_symman.get(), cmd, d_solver->getDriverOptions().out());
123
124	484884	api::Result res;
125	242442	const CheckSatCommand* cs = dynamic_cast<const CheckSatCommand*>(cmd);
126	242442	if(cs != nullptr) {
127	9443	d_result = res = cs->getResult();
128		}
129		const CheckSatAssumingCommand* csa =
130	242442	dynamic_cast<const CheckSatAssumingCommand*>(cmd);
131	242442	if (csa != nullptr)
132		{
133	1563	d_result = res = csa->getResult();
134		}
135	242442	const QueryCommand* q = dynamic_cast<const QueryCommand*>(cmd);
136	242442	if(q != nullptr) {
137	23	d_result = res = q->getResult();
138		}
139
140	242442	bool isResultUnsat = res.isUnsat() \|\| res.isEntailed();
141	242442	bool isResultSat = res.isSat() \|\| res.isNotEntailed();
142
143		// dump the model/proof/unsat core if option is set
144	242442	if (status) {
145	484788	std::vector<std::unique_ptr<Command> > getterCommands;
146	727182	if (d_solver->getOptionInfo("dump-models").boolValue()
147	727192	&& (isResultSat
148	34	\|\| (res.isSatUnknown()
149		&& res.getUnknownExplanation() == api::Result::INCOMPLETE)))
150		{
151	10	getterCommands.emplace_back(new GetModelCommand());
152		}
153	242394	if (d_solver->getOptionInfo("dump-proofs").boolValue() && isResultUnsat)
154		{
155	1	getterCommands.emplace_back(new GetProofCommand());
156		}
157
158	727182	if ((d_solver->getOptionInfo("dump-instantiations").boolValue()
159	484641	\|\| d_solver->getOptionInfo("dump-instantiations-debug").boolValue())
160	727329	&& GetInstantiationsCommand::isEnabled(d_solver.get(), res))
161		{
162	15	getterCommands.emplace_back(new GetInstantiationsCommand());
163		}
164
165	727182	if (d_solver->getOptionInfo("dump-unsat-cores").boolValue()
166	727182	&& isResultUnsat)
167		{
168	3	getterCommands.emplace_back(new GetUnsatCoreCommand());
169		}
170
171	727182	if (d_solver->getOptionInfo("dump-difficulty").boolValue()
172	727182	&& (isResultUnsat \|\| isResultSat \|\| res.isSatUnknown()))
173		{
174		getterCommands.emplace_back(new GetDifficultyCommand());
175		}
176
177	242394	if (!getterCommands.empty()) {
178		// set no time limit during dumping if applicable
179	29	if (d_solver->getOptionInfo("force-no-limit-cpu-while-dump").boolValue())
180		{
181		setNoLimitCPU();
182		}
183	58	for (const auto& getterCommand : getterCommands) {
184	29	status = doCommandSingleton(getterCommand.get());
185	29	if (!status)
186		{
187		break;
188		}
189		}
190		}
191		}
192	484884	return status;
193		}
194
195	242442	bool solverInvoke(api::Solver* solver,
196		SymbolManager* sm,
197		Command* cmd,
198		std::ostream& out)
199		{
200		// print output for -o raw-benchmark
201	242442	if (solver->isOutputOn("raw-benchmark"))
202		{
203	21	cmd->toStream(solver->getOutput("raw-benchmark"));
204		}
205
206		// In parse-only mode, we do not invoke any of the commands except define-fun
207		// commands. We invoke define-fun commands because they add function names
208		// to the symbol table.
209	727326	if (solver->getOptionInfo("parse-only").boolValue()
210	727326	&& dynamic_cast<DefineFunctionCommand*>(cmd) == nullptr)
211		{
212		return true;
213		}
214
215	242442	cmd->invoke(solver, sm, out);
216		// ignore the error if the command-verbosity is 0 for this command
217		std::string commandName =
218	484884	std::string("command-verbosity:") + cmd->getCommandName();
219	242442	if (solver->getOption(commandName) == "0")
220		{
221		return true;
222		}
223	242442	return !cmd->fail();
224		}
225
226	6563	void CommandExecutor::flushOutputStreams() {
227	6563	printStatistics(d_solver->getDriverOptions().err());
228
229		// make sure out and err streams are flushed too
230	6563	d_solver->getDriverOptions().out() << std::flush;
231	6563	d_solver->getDriverOptions().err() << std::flush;
232	6563	}
233
234		} // namespace main
235	31110	} // namespace cvc5