diff options
Diffstat (limited to 'src/smt_util')
-rw-r--r-- | src/smt_util/Makefile.am | 8 | ||||
-rw-r--r-- | src/smt_util/boolean_simplification.h | 4 | ||||
-rw-r--r-- | src/smt_util/dump.cpp | 197 | ||||
-rw-r--r-- | src/smt_util/dump.h | 10 | ||||
-rw-r--r-- | src/smt_util/lemma_channels.cpp | 54 | ||||
-rw-r--r-- | src/smt_util/lemma_channels.h | 77 |
6 files changed, 343 insertions, 7 deletions
diff --git a/src/smt_util/Makefile.am b/src/smt_util/Makefile.am index 3b457f641..ae1ea1f70 100644 --- a/src/smt_util/Makefile.am +++ b/src/smt_util/Makefile.am @@ -12,12 +12,14 @@ libsmtutil_la_SOURCES = \ boolean_simplification.h \ command.cpp \ command.h \ - dump.h \ dump.cpp \ - lemma_input_channel.h \ - lemma_output_channel.h \ + dump.h \ ite_removal.cpp \ ite_removal.h \ + lemma_channels.cpp \ + lemma_channels.h \ + lemma_input_channel.h \ + lemma_output_channel.h \ model.cpp \ model.h \ nary_builder.cpp \ diff --git a/src/smt_util/boolean_simplification.h b/src/smt_util/boolean_simplification.h index 2732eaea7..27fdc3d28 100644 --- a/src/smt_util/boolean_simplification.h +++ b/src/smt_util/boolean_simplification.h @@ -35,8 +35,8 @@ namespace CVC4 { */ class BooleanSimplification { // cannot construct one of these - BooleanSimplification() CVC4_UNUSED; - BooleanSimplification(const BooleanSimplification&) CVC4_UNUSED; + BooleanSimplification() CVC4_UNDEFINED; + BooleanSimplification(const BooleanSimplification&) CVC4_UNDEFINED; static bool push_back_associative_commute_recursive (Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode) diff --git a/src/smt_util/dump.cpp b/src/smt_util/dump.cpp index 56313f4d8..218691bd0 100644 --- a/src/smt_util/dump.cpp +++ b/src/smt_util/dump.cpp @@ -21,4 +21,201 @@ namespace CVC4 { DumpC DumpChannel CVC4_PUBLIC; +std::ostream& DumpC::setStream(std::ostream* os) { + DumpOut.setStream(os); + return *os; +} +std::ostream& DumpC::getStream() { return DumpOut.getStream(); } +std::ostream* DumpC::getStreamPointer() { return DumpOut.getStreamPointer(); } + + +void DumpC::setDumpFromString(const std::string& optarg) { +#ifdef CVC4_DUMPING + char* optargPtr = strdup(optarg.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."); + } + if(!strcmp(p, "everything")) { + } else if(!strcmp(p, "definition-expansion")) { + } else if(!strcmp(p, "boolean-terms")) { + } else if(!strcmp(p, "constrain-subtypes")) { + } else if(!strcmp(p, "substitution")) { + } else if(!strcmp(p, "strings-pp")) { + } else if(!strcmp(p, "skolem-quant")) { + } else if(!strcmp(p, "simplify")) { + } else if(!strcmp(p, "static-learning")) { + } else if(!strcmp(p, "ite-removal")) { + } else if(!strcmp(p, "repeat-simplify")) { + } else if(!strcmp(p, "rewrite-apply-to-const")) { + } else if(!strcmp(p, "theory-preprocessing")) { + } else if(!strcmp(p, "nonclausal")) { + } else if(!strcmp(p, "theorypp")) { + } else if(!strcmp(p, "itesimp")) { + } else if(!strcmp(p, "unconstrained")) { + } else if(!strcmp(p, "repeatsimp")) { + } 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")) { + // These are "non-state-dumping" modes. If state (SAT decisions, + // propagations, etc.) is dumped, it will interfere with the validity + // of these generated queries. + if(Dump.isOn("state")) { + throw OptionException(std::string("dump option `") + optargPtr + + "' conflicts with a previous, " + "state-dumping dump option. You cannot " + "mix stateful and non-stateful dumping modes; " + "see --dump help."); + } else { + Dump.on("no-permit-state"); + } + } else if(!strcmp(optargPtr, "state") || + !strcmp(optargPtr, "missed-t-conflicts") || + !strcmp(optargPtr, "t-propagations") || + !strcmp(optargPtr, "missed-t-propagations")) { + // These are "state-dumping" modes. If state (SAT decisions, + // propagations, etc.) is not dumped, it will interfere with the + // validity of these generated queries. + if(Dump.isOn("no-permit-state")) { + throw OptionException(std::string("dump option `") + optargPtr + + "' conflicts with a previous, " + "non-state-dumping dump option. You cannot " + "mix stateful and non-stateful dumping modes; " + "see --dump help."); + } else { + Dump.on("state"); + } + } else if(!strcmp(optargPtr, "help")) { + puts(s_dumpHelp.c_str()); + exit(1); + } else if(!strcmp(optargPtr, "bv-abstraction")) { + Dump.on("bv-abstraction"); + } else if(!strcmp(optargPtr, "bv-algebraic")) { + Dump.on("bv-algebraic"); + } 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")) { + Dump.on("skolems"); + } + } + } + free(optargPtr); +#else /* CVC4_DUMPING */ + throw OptionException("The dumping feature was disabled in this build of CVC4."); +#endif /* CVC4_DUMPING */ +} + + +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 strings-pp skolem-quant\n\ + simplify static-learning ite-removal repeat-simplify\n\ + 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\ +state\n\ ++ Dump all contextual assertions (e.g., SAT decisions, propagations..).\n\ + Implied by all \"stateful\" modes below and conflicts with all\n\ + non-stateful modes below.\n\ +\n\ +t-conflicts [non-stateful]\n\ ++ Output correctness queries for all theory conflicts\n\ +\n\ +missed-t-conflicts [stateful]\n\ ++ Output completeness queries for theory conflicts\n\ +\n\ +t-propagations [stateful]\n\ ++ Output correctness queries for all theory propagations\n\ +\n\ +missed-t-propagations [stateful]\n\ ++ Output completeness queries for theory propagations (LARGE and EXPENSIVE)\n\ +\n\ +t-lemmas [non-stateful]\n\ ++ Output correctness queries for all theory lemmas\n\ +\n\ +t-explanations [non-stateful]\n\ ++ Output correctness queries for all theory explanations\n\ +\n\ +bv-rewrites [non-stateful]\n\ ++ Output correctness queries for all bitvector rewrites\n\ +\n\ +bv-abstraction [non-stateful]\n\ ++ Output correctness queries for all bv abstraction \n\ +\n\ +bv-algebraic [non-stateful]\n\ ++ Output correctness queries for bv algebraic solver. \n\ +\n\ +theory::fullcheck [non-stateful]\n \ ++ Output completeness queries for all full-check effort-level theory checks\n\ +\n\ +Dump modes can be combined with multiple uses of --dump. Generally you want\n\ +one from the assertions category (either assertions or clauses), and\n\ +perhaps one or more stateful or non-stateful modes for checking correctness\n\ +and completeness of decision procedure implementations. Stateful modes dump\n\ +the contextual assertions made by the core solver (all decisions and\n\ +propagations as assertions; that affects the validity of the resulting\n\ +correctness and completeness queries, so of course stateful and non-stateful\n\ +modes cannot be mixed in the same run.\n\ +\n\ +The --output-language option controls the language used for dumping, and\n\ +this allows you to connect CVC4 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\ +"; + }/* CVC4 namespace */ diff --git a/src/smt_util/dump.h b/src/smt_util/dump.h index 1f4efe640..19f9118e3 100644 --- a/src/smt_util/dump.h +++ b/src/smt_util/dump.h @@ -75,6 +75,8 @@ class CVC4_PUBLIC DumpC { std::set<std::string> d_tags; CommandSequence d_commands; + static const std::string s_dumpHelp; + public: CVC4dumpstream operator()(const char* tag) { if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) { @@ -83,6 +85,7 @@ public: return CVC4dumpstream(); } } + CVC4dumpstream operator()(std::string tag) { if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) { return CVC4dumpstream(getStream(), d_commands); @@ -103,8 +106,11 @@ public: bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); } bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); } - std::ostream& setStream(std::ostream& os) { DumpOut.setStream(os); return os; } - std::ostream& getStream() { return DumpOut.getStream(); } + std::ostream& setStream(std::ostream* os); + std::ostream& getStream(); + std::ostream* getStreamPointer(); + + void setDumpFromString(const std::string& optarg); };/* class DumpC */ /** The dump singleton */ diff --git a/src/smt_util/lemma_channels.cpp b/src/smt_util/lemma_channels.cpp new file mode 100644 index 000000000..e75866c5e --- /dev/null +++ b/src/smt_util/lemma_channels.cpp @@ -0,0 +1,54 @@ +/********************* */ +/*! \file lemma_channels.cpp + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2015 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief This class is a light container for globals that used to live + ** in options. This is NOT a good long term solution, but is a reasonable + ** stop gap. + ** + ** This class is a light container for globals that used to live + ** in options. This is NOT a good long term solution, but is a reasonable + ** stop gap. + **/ + +#include "smt_util/lemma_channels.h" + +#include <cerrno> +#include <iostream> +#include <string> +#include <utility> + +#include "cvc4autoconfig.h" // Needed for CVC4_REPLAY +#include "expr/expr_stream.h" +#include "options/open_ostream.h" +#include "options/option_exception.h" +#include "options/parser_options.h" +#include "smt_util/lemma_input_channel.h" +#include "smt_util/lemma_output_channel.h" + +namespace CVC4 { + +LemmaChannels::LemmaChannels() + : d_lemmaInputChannel(NULL) + , d_lemmaOutputChannel(NULL) +{} + +LemmaChannels::~LemmaChannels(){} + +void LemmaChannels::setLemmaInputChannel(LemmaInputChannel* in) { + d_lemmaInputChannel = in; +} + +void LemmaChannels::setLemmaOutputChannel(LemmaOutputChannel* out) { + d_lemmaOutputChannel = out; +} + + +} /* namespace CVC4 */ diff --git a/src/smt_util/lemma_channels.h b/src/smt_util/lemma_channels.h new file mode 100644 index 000000000..6cd81795e --- /dev/null +++ b/src/smt_util/lemma_channels.h @@ -0,0 +1,77 @@ +/********************* */ +/*! \file lemma_channels.h + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2015 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief LemmaChannels is a light container for a pair of input and output + ** lemma channels. + ** + ** LemmaChannels is a light container for a pair of input and output + ** lemma channels. These contain paramaters for the infrequently + ** used Portfolio mode. There should be exactly one of these per SmtEngine + ** with the same lifetime as the SmtEngine. The user directly passes these as + ** pointers and is resonsible for cleaning up the memory. + ** + ** Basically, the problem this class is solving is that previously these were + ** using smt_options.h and the Options class as globals for these same + ** datastructures. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__SMT_UTIL__LEMMA_CHANNELS_H +#define __CVC4__SMT_UTIL__LEMMA_CHANNELS_H + +#include <iosfwd> +#include <string> +#include <utility> + +#include "options/option_exception.h" +#include "smt_util/lemma_input_channel.h" +#include "smt_util/lemma_output_channel.h" + +namespace CVC4 { + +/** + * LemmaChannels is a wrapper around two pointers: + * - getLemmaInputChannel() + * - getLemmaOutputChannel() + * + * The user can directly set these and is responsible for handling the + * memory for these. These datastructures are used for Portfolio mode. + */ +class CVC4_PUBLIC LemmaChannels { + public: + /** Creates an empty LemmaChannels with all 4 pointers initially NULL. */ + LemmaChannels(); + ~LemmaChannels(); + + void setLemmaInputChannel(LemmaInputChannel* in); + LemmaInputChannel* getLemmaInputChannel() { return d_lemmaInputChannel; } + + void setLemmaOutputChannel(LemmaOutputChannel* out); + LemmaOutputChannel* getLemmaOutputChannel() { return d_lemmaOutputChannel; } + + private: + // Disable copy constructor. + LemmaChannels(const LemmaChannels&) CVC4_UNDEFINED; + + // Disable assignment operator. + LemmaChannels& operator=(const LemmaChannels&) CVC4_UNDEFINED; + + /** This captures the old options::lemmaInputChannel .*/ + LemmaInputChannel* d_lemmaInputChannel; + + /** This captures the old options::lemmaOutputChannel .*/ + LemmaOutputChannel* d_lemmaOutputChannel; +}; /* class LemmaChannels */ + +} /* namespace CVC4 */ + +#endif /* __CVC4__SMT_UTIL__LEMMA_CHANNELS_H */ |