Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/smt/dump.cpp	Lines:	52	74	70.3 %
Date:	2021-05-22	Branches:	47	130	36.2 %


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