Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/smt/dump.cpp	Lines:	45	69	65.2 %
Date:	2021-09-30	Branches:	40	120	33.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andres Noetzli, Morgan Deters, Tim King
 *
 * 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.
 * ****************************************************************************
 *
 * Dump utility classes and functions.
 */

#include "smt/dump.h"

#include "base/configuration.h"
#include "base/output.h"
#include "lib/strtok_r.h"
#include "options/option_exception.h"
#include "preprocessing/preprocessing_pass_registry.h"
#include "smt/command.h"
#include "smt/node_command.h"

namespace cvc5 {

#if defined(CVC5_DUMPING) && !defined(CVC5_MUZZLE)

CVC5dumpstream& CVC5dumpstream::operator<<(const Command& c)
{
  if (d_os != nullptr)
  {
    (*d_os) << c;
  }
  return *this;
}

CVC5dumpstream& CVC5dumpstream::operator<<(const NodeCommand& nc)
{
  if (d_os != nullptr)
  {
    (*d_os) << nc;
  }
  return *this;
}

#else

CVC5dumpstream& CVC5dumpstream::operator<<(const Command& c) { return *this; }
CVC5dumpstream& CVC5dumpstream::operator<<(const NodeCommand& nc)
{
  return *this;
}

#endif /* CVC5_DUMPING && !CVC5_MUZZLE */

DumpC DumpChannel;

std::ostream& DumpC::setStream(std::ostream* os) {
  ::cvc5::DumpOutChannel.setStream(os);
  return *os;
}
std::ostream& DumpC::getStream() { return ::cvc5::DumpOutChannel.getStream(); }
std::ostream* DumpC::getStreamPointer()
{
  return ::cvc5::DumpOutChannel.getStreamPointer();
}

void DumpC::setDumpFromString(const std::string& optarg) {
  if (Configuration::isDumpingBuild())
  {
    // Make a copy of optarg for strtok_r to use.
    std::string optargCopy = optarg;
    char* optargPtr = const_cast<char*>(optargCopy.c_str());
    char* tokstr = optargPtr;
    char* toksave;
    while ((optargPtr = strtok_r(tokstr, ",", &toksave)) != NULL)
    {
      tokstr = NULL;
      if (!strcmp(optargPtr, "benchmark"))
      {
      }
      else if (!strcmp(optargPtr, "declarations"))
      {
      }
      else if (!strcmp(optargPtr, "assertions"))
      {
        Dump.on("assertions:post-everything");
      }
      else if (!strncmp(optargPtr, "assertions:", 11))
      {
        const char* p = optargPtr + 11;
        if (!strncmp(p, "pre-", 4))
        {
          p += 4;
        }
        else if (!strncmp(p, "post-", 5))
        {
          p += 5;
        }
        else
        {
          throw OptionException(std::string("don't know how to dump `")
                                + optargPtr
                                + "'.  Please consult --dump help.");
        }
        // hard-coded cases
        if (!strcmp(p, "everything") || !strcmp(p, "definition-expansion")
            || !strcmp(p, "simplify") || !strcmp(p, "repeat-simplify"))
        {
        }
        else if (preprocessing::PreprocessingPassRegistry::getInstance()
                     .hasPass(p))
        {
        }
        else
        {
          throw OptionException(std::string("don't know how to dump `")
                                + optargPtr
                                + "'.  Please consult --dump help.");
        }
        Dump.on("assertions");
      }
      else if (!strcmp(optargPtr, "skolems"))
      {
      }
      else if (!strcmp(optargPtr, "clauses"))
      {
      }
      else if (!strcmp(optargPtr, "t-conflicts")
               || !strcmp(optargPtr, "t-lemmas")
               || !strcmp(optargPtr, "t-explanations")
               || !strcmp(optargPtr, "theory::fullcheck"))
      {
      }
      else if (!strcmp(optargPtr, "help"))
      {
        puts(s_dumpHelp.c_str());

        std::stringstream ss;
        ss << "Available preprocessing passes:\n";
        for (const std::string& pass :
             preprocessing::PreprocessingPassRegistry::getInstance()
                 .getAvailablePasses())
        {
          ss << "- " << pass << "\n";
        }
        puts(ss.str().c_str());
        exit(1);
      }
      else
      {
        throw OptionException(std::string("unknown option for --dump: `")
                              + optargPtr + "'.  Try --dump help.");
      }

      Dump.on(optargPtr);
      Dump.on("benchmark");
      if (strcmp(optargPtr, "benchmark"))
      {
        Dump.on("declarations");
      }
    }
  }
  else
  {
    throw OptionException(
        "The dumping feature was disabled in this build of cvc5.");
  }
}

const std::string DumpC::s_dumpHelp =
    "\
Dump modes currently supported by the --dump option:\n\
\n\
benchmark\n\
+ Dump the benchmark structure (set-logic, push/pop, queries, etc.), but\n\
  does not include any declarations or assertions.  Implied by all following\n\
  modes.\n\
\n\
declarations\n\
+ Dump user declarations.  Implied by all following modes.\n\
\n\
skolems\n\
+ Dump internally-created skolem variable declarations.  These can\n\
  arise from preprocessing simplifications, existential elimination,\n\
  and a number of other things.  Implied by all following modes.\n\
\n\
assertions\n\
+ Output the assertions after preprocessing and before clausification.\n\
  Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\
  where PASS is one of the preprocessing passes: definition-expansion\n\
  boolean-terms constrain-subtypes substitution bv-to-bool bool-to-bv\n\
  strings-pp skolem-quant simplify static-learning ite-removal\n\
  repeat-simplify rewrite-apply-to-const theory-preprocessing.\n\
  PASS can also be the special value \"everything\", in which case the\n\
  assertions are printed before any preprocessing (with\n\
  \"assertions:pre-everything\") or after all preprocessing completes\n\
  (with \"assertions:post-everything\").\n\
\n\
clauses\n\
+ Do all the preprocessing outlined above, and dump the CNF-converted\n\
  output\n\
\n\
t-conflicts\n\
+ Output correctness queries for all theory conflicts\n\
\n\
t-lemmas\n\
+ Output correctness queries for all theory lemmas\n\
\n\
t-explanations\n\
+ Output correctness queries for all theory explanations\n\
\n\
theory::fullcheck\n\
+ Output completeness queries for all full-check effort-level theory checks\n\
\n\
Dump modes can be combined by concatenating the above values with \",\" in\n\
between them.  Generally you want one from the assertions category (either\n\
assertions or clauses), and perhaps one or more other modes for checking\n\
correctness and completeness of decision procedure implementations.\n\
\n\
The --output-language option controls the language used for dumping, and\n\
this allows you to connect cvc5 to another solver implementation via a UNIX\n\
pipe to perform on-line checking.  The --dump-to option can be used to dump\n\
to a file.\n\
";

}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andres Noetzli, Morgan Deters, Tim King
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		* Dump utility classes and functions.
14		*/
15
16		#include "smt/dump.h"
17
18		#include "base/configuration.h"
19		#include "base/output.h"
20		#include "lib/strtok_r.h"
21		#include "options/option_exception.h"
22		#include "preprocessing/preprocessing_pass_registry.h"
23		#include "smt/command.h"
24		#include "smt/node_command.h"
25
26		namespace cvc5 {
27
28		#if defined(CVC5_DUMPING) && !defined(CVC5_MUZZLE)
29
30	423	CVC5dumpstream& CVC5dumpstream::operator<<(const Command& c)
31		{
32	423	if (d_os != nullptr)
33		{
34		(*d_os) << c;
35		}
36	423	return *this;
37		}
38
39	2	CVC5dumpstream& CVC5dumpstream::operator<<(const NodeCommand& nc)
40		{
41	2	if (d_os != nullptr)
42		{
43	2	(*d_os) << nc;
44		}
45	2	return *this;
46		}
47
48		#else
49
50		CVC5dumpstream& CVC5dumpstream::operator<<(const Command& c) { return *this; }
51		CVC5dumpstream& CVC5dumpstream::operator<<(const NodeCommand& nc)
52		{
53		return *this;
54		}
55
56		#endif /* CVC5_DUMPING && !CVC5_MUZZLE */
57
58	7585	DumpC DumpChannel;
59
60		std::ostream& DumpC::setStream(std::ostream* os) {
61		::cvc5::DumpOutChannel.setStream(os);
62		return *os;
63		}
64	1400	std::ostream& DumpC::getStream() { return ::cvc5::DumpOutChannel.getStream(); }
65		std::ostream* DumpC::getStreamPointer()
66		{
67		return ::cvc5::DumpOutChannel.getStreamPointer();
68		}
69
70	2	void DumpC::setDumpFromString(const std::string& optarg) {
71	2	if (Configuration::isDumpingBuild())
72		{
73		// Make a copy of optarg for strtok_r to use.
74	4	std::string optargCopy = optarg;
75	2	char* optargPtr = const_cast<char*>(optargCopy.c_str());
76	2	char* tokstr = optargPtr;
77		char* toksave;
78	4	while ((optargPtr = strtok_r(tokstr, ",", &toksave)) != NULL)
79		{
80	2	tokstr = NULL;
81	2	if (!strcmp(optargPtr, "benchmark"))
82		{
83		}
84	2	else if (!strcmp(optargPtr, "declarations"))
85		{
86		}
87	2	else if (!strcmp(optargPtr, "assertions"))
88		{
89		Dump.on("assertions:post-everything");
90		}
91	2	else if (!strncmp(optargPtr, "assertions:", 11))
92		{
93	1	const char* p = optargPtr + 11;
94	1	if (!strncmp(p, "pre-", 4))
95		{
96		p += 4;
97		}
98	1	else if (!strncmp(p, "post-", 5))
99		{
100	1	p += 5;
101		}
102		else
103		{
104		throw OptionException(std::string("don't know how to dump `")
105		+ optargPtr
106		+ "'. Please consult --dump help.");
107		}
108		// hard-coded cases
109	1	if (!strcmp(p, "everything") \|\| !strcmp(p, "definition-expansion")
110	1	\|\| !strcmp(p, "simplify") \|\| !strcmp(p, "repeat-simplify"))
111		{
112		}
113	2	else if (preprocessing::PreprocessingPassRegistry::getInstance()
114	1	.hasPass(p))
115		{
116		}
117		else
118		{
119		throw OptionException(std::string("don't know how to dump `")
120		+ optargPtr
121		+ "'. Please consult --dump help.");
122		}
123	1	Dump.on("assertions");
124		}
125	1	else if (!strcmp(optargPtr, "skolems"))
126		{
127		}
128	1	else if (!strcmp(optargPtr, "clauses"))
129		{
130		}
131	1	else if (!strcmp(optargPtr, "t-conflicts")
132	1	\|\| !strcmp(optargPtr, "t-lemmas")
133	1	\|\| !strcmp(optargPtr, "t-explanations")
134	1	\|\| !strcmp(optargPtr, "theory::fullcheck"))
135		{
136		}
137	1	else if (!strcmp(optargPtr, "help"))
138		{
139		puts(s_dumpHelp.c_str());
140
141		std::stringstream ss;
142		ss << "Available preprocessing passes:\n";
143		for (const std::string& pass :
144		preprocessing::PreprocessingPassRegistry::getInstance()
145		.getAvailablePasses())
146		{
147		ss << "- " << pass << "\n";
148		}
149		puts(ss.str().c_str());
150		exit(1);
151		}
152		else
153		{
154	2	throw OptionException(std::string("unknown option for --dump: `")
155	3	+ optargPtr + "'. Try --dump help.");
156		}
157
158	1	Dump.on(optargPtr);
159	1	Dump.on("benchmark");
160	1	if (strcmp(optargPtr, "benchmark"))
161		{
162	1	Dump.on("declarations");
163		}
164		}
165		}
166		else
167		{
168		throw OptionException(
169		"The dumping feature was disabled in this build of cvc5.");
170		}
171	1	}
172
173	7585	const std::string DumpC::s_dumpHelp =
174		"\
175		Dump modes currently supported by the --dump option:\n\
176		\n\
177		benchmark\n\
178		+ Dump the benchmark structure (set-logic, push/pop, queries, etc.), but\n\
179		does not include any declarations or assertions. Implied by all following\n\
180		modes.\n\
181		\n\
182		declarations\n\
183		+ Dump user declarations. Implied by all following modes.\n\
184		\n\
185		skolems\n\
186		+ Dump internally-created skolem variable declarations. These can\n\
187		arise from preprocessing simplifications, existential elimination,\n\
188		and a number of other things. Implied by all following modes.\n\
189		\n\
190		assertions\n\
191		+ Output the assertions after preprocessing and before clausification.\n\
192		Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\
193		where PASS is one of the preprocessing passes: definition-expansion\n\
194		boolean-terms constrain-subtypes substitution bv-to-bool bool-to-bv\n\
195		strings-pp skolem-quant simplify static-learning ite-removal\n\
196		repeat-simplify rewrite-apply-to-const theory-preprocessing.\n\
197		PASS can also be the special value \"everything\", in which case the\n\
198		assertions are printed before any preprocessing (with\n\
199		\"assertions:pre-everything\") or after all preprocessing completes\n\
200		(with \"assertions:post-everything\").\n\
201		\n\
202		clauses\n\
203		+ Do all the preprocessing outlined above, and dump the CNF-converted\n\
204		output\n\
205		\n\
206		t-conflicts\n\
207		+ Output correctness queries for all theory conflicts\n\
208		\n\
209		t-lemmas\n\
210		+ Output correctness queries for all theory lemmas\n\
211		\n\
212		t-explanations\n\
213		+ Output correctness queries for all theory explanations\n\
214		\n\
215		theory::fullcheck\n\
216		+ Output completeness queries for all full-check effort-level theory checks\n\
217		\n\
218		Dump modes can be combined by concatenating the above values with \",\" in\n\
219		between them. Generally you want one from the assertions category (either\n\
220		assertions or clauses), and perhaps one or more other modes for checking\n\
221		correctness and completeness of decision procedure implementations.\n\
222		\n\
223		The --output-language option controls the language used for dumping, and\n\
224		this allows you to connect cvc5 to another solver implementation via a UNIX\n\
225		pipe to perform on-line checking. The --dump-to option can be used to dump\n\
226		to a file.\n\
227		";
228
229	22755	} // namespace cvc5