- The options replayStream, lemmaInputChannel, lemmaOutputChannel have been removed due to their datatypes. These datatypes were previously pointers to types that were not usable from the options/ library.
- The option replayLog has been removed due to inconsistent memory management.
- SmtGlobals is a class that wraps a pointer to each of these removed options. These can each be set independently.
- There is a single SmtGlobals per SmtEngine with the lifetime of the SmtEngine.
- A pointer to this is freely given to the user of an SmtEngine to parameterize the solver after construction.
- Selected classes have been given a copy of this pointer in their constructors.
- Removed the dependence on Node from Result. Moving Result back into util/.
context::UserContext* u,
OutputChannel& out,
Valuation valuation,
- const LogicInfo& logicInfo) :
- Theory(THEORY_$alt_id, c, u, out, valuation, logicInfo) {
+ const LogicInfo& logicInfo,
+ SmtGlobals* globals) :
+ Theory(THEORY_$alt_id, c, u, out, valuation, logicInfo, globals) {
}/* Theory$camel::Theory$camel() */
void Theory$camel::check(Effort level) {
context::UserContext* u,
OutputChannel& out,
Valuation valuation,
- const LogicInfo& logicInfo);
+ const LogicInfo& logicInfo,
+ SmtGlobals* globals);
void check(Effort);
context::UserContext* u,
OutputChannel& out,
Valuation valuation,
- const LogicInfo& logicInfo) :
- Theory(THEORY_$id, c, u, out, valuation, logicInfo) {
+ const LogicInfo& logicInfo,
+ SmtGlobals* globals) :
+ Theory(THEORY_$id, c, u, out, valuation, logicInfo, globals) {
}/* Theory$camel::Theory$camel() */
void Theory$camel::check(Effort level) {
context::UserContext* u,
OutputChannel& out,
Valuation valuation,
- const LogicInfo& logicInfo);
+ const LogicInfo& logicInfo,
+ SmtGlobals* globals);
void check(Effort);
string input,
const vector<string>& info_tags,
const vector<string>& info_data,
- const map<Expr, unsigned>& variables,
+ const map<Expr, unsigned>& variables,
const vector<Expr>& assertions);
-int main(int argc, char* argv[])
+int main(int argc, char* argv[])
{
- // Get the filename
+ // Get the filename
string input(argv[1]);
// Create the expression manager
Options options;
options.set(inputLanguage, language::input::LANG_SMTLIB_V2);
ExprManager exprManager(options);
-
+
// Create the parser
ParserBuilder parserBuilder(&exprManager, input, options);
Parser* parser = parserBuilder.build();
}
}
-
};
-int main(int argc, char* argv[])
+int main(int argc, char* argv[])
{
try {
- // Get the filename
+ // Get the filename
string input;
- if(argc > 1) input = string(argv[1]);
- else input = "<stdin>";
+ if(argc > 1){
+ input = string(argv[1]);
+ } else {
+ input = "<stdin>";
+ }
// Create the expression manager
Options options;
vector<string> info_tags;
vector<string> info_data;
vector<Expr> assertions;
-
+
Command* cmd = NULL;
CommandSequence commandsSequence;
bool logicisset = false;
smt/smt_engine.cpp \
smt/smt_engine_check_proof.cpp \
smt/smt_engine.h \
+ smt/smt_globals.cpp \
+ smt/smt_globals.h \
smt/model_postprocessor.cpp \
smt/model_postprocessor.h \
smt/smt_options_handler.cpp \
cvc4_assert.h \
exception.cpp \
exception.h \
- lemma_input_channel_forward.h \
- lemma_output_channel_forward.h \
modal_exception.h \
output.cpp \
output.h
+++ /dev/null
-/********************* */
-/*! \file lemma_input_channel_forward.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-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Forward declaration of LemmaInputChannel.
- **
- ** This forward declaration of LemmaInputChannel is needed for the option
- ** lemmaInputChannel (defined in smt_options) can be a LemmaInputChannel*
- ** without including expr.h.
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__LEMMA_INPUT_CHANNEL_FORWARD_H
-#define __CVC4__LEMMA_INPUT_CHANNEL_FORWARD_H
-
-namespace CVC4 {
-
-class CVC4_PUBLIC LemmaInputChannel;
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__LEMMA_INPUT_CHANNEL_FORWARD_H */
+++ /dev/null
-/********************* */
-/*! \file lemma_output_channel_forward.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-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Forward declaration of the LemmaOutputChannel
- **
- ** This forward declaration of LemmaOutputChannel is needed for the option
- ** lemmaOutputChannel (defined in smt_options) can be a LemmaInputChannel*
- ** without including expr.h.
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__LEMMA_OUTPUT_CHANNEL_FORWARD_H
-#define __CVC4__LEMMA_OUTPUT_CHANNEL_FORWARD_H
-
-namespace CVC4 {
-
-/**
- * This interface describes a mechanism for the propositional and theory
- * engines to communicate with the "outside world" about new lemmas being
- * discovered.
- */
-class CVC4_PUBLIC LemmaOutputChannel;
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__LEMMA_OUTPUT_CHANNEL_FORWARD_H */
%include "util/hash.i"
%include "util/proof.i"
%include "util/regexp.i"
+%include "util/result.i"
%include "util/subrange_bound.i"
%include "util/tuple.i"
//%include "util/floatingpoint.i"
%include "expr/predicate.i"
%include "expr/record.i"
%include "expr/resource_manager.i"
-%include "expr/result.i"
%include "proof/unsat_core.i"
// TIM:
predicate.cpp \
record.cpp \
record.h \
- result.cpp \
- result.h \
uninterpreted_constant.cpp \
uninterpreted_constant.h
resource_manager.i \
sexpr.i \
record.i \
- result.i \
predicate.i \
variable_type_map.i \
uninterpreted_constant.i
+++ /dev/null
-/********************* */
-/*! \file result.cpp
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Encapsulation of the result of a query.
- **
- ** Encapsulation of the result of a query.
- **/
-#include "expr/result.h"
-
-#include <algorithm>
-#include <cctype>
-#include <iostream>
-#include <string>
-
-#include "base/cvc4_assert.h"
-#include "expr/node.h"
-
-using namespace std;
-
-#warning "TODO: Move Node::setLanguage out of Node and into util/. Then move Result back into util/."
-
-namespace CVC4 {
-
-Result::Result()
- : d_sat(SAT_UNKNOWN)
- , d_validity(VALIDITY_UNKNOWN)
- , d_which(TYPE_NONE)
- , d_unknownExplanation(UNKNOWN_REASON)
- , d_inputName("")
-{ }
-
-
-Result::Result(enum Sat s, std::string inputName)
- : d_sat(s)
- , d_validity(VALIDITY_UNKNOWN)
- , d_which(TYPE_SAT)
- , d_unknownExplanation(UNKNOWN_REASON)
- , d_inputName(inputName)
-{
- PrettyCheckArgument(s != SAT_UNKNOWN,
- "Must provide a reason for satisfiability being unknown");
-}
-
-Result::Result(enum Validity v, std::string inputName)
- : d_sat(SAT_UNKNOWN)
- , d_validity(v)
- , d_which(TYPE_VALIDITY)
- , d_unknownExplanation(UNKNOWN_REASON)
- , d_inputName(inputName)
-{
- PrettyCheckArgument(v != VALIDITY_UNKNOWN,
- "Must provide a reason for validity being unknown");
-}
-
-
-Result::Result(enum Sat s, enum UnknownExplanation unknownExplanation,
- std::string inputName)
- : d_sat(s)
- , d_validity(VALIDITY_UNKNOWN)
- , d_which(TYPE_SAT)
- , d_unknownExplanation(unknownExplanation)
- , d_inputName(inputName)
-{
- PrettyCheckArgument(s == SAT_UNKNOWN,
- "improper use of unknown-result constructor");
-}
-
-Result::Result(enum Validity v, enum UnknownExplanation unknownExplanation,
- std::string inputName)
- : d_sat(SAT_UNKNOWN)
- , d_validity(v)
- , d_which(TYPE_VALIDITY)
- , d_unknownExplanation(unknownExplanation)
- , d_inputName(inputName)
-{
- PrettyCheckArgument(v == VALIDITY_UNKNOWN,
- "improper use of unknown-result constructor");
-}
-
-Result::Result(const std::string& instr, std::string inputName) :
- d_sat(SAT_UNKNOWN),
- d_validity(VALIDITY_UNKNOWN),
- d_which(TYPE_NONE),
- d_unknownExplanation(UNKNOWN_REASON),
- d_inputName(inputName) {
- string s = instr;
- transform(s.begin(), s.end(), s.begin(), ::tolower);
- if(s == "sat" || s == "satisfiable") {
- d_which = TYPE_SAT;
- d_sat = SAT;
- } else if(s == "unsat" || s == "unsatisfiable") {
- d_which = TYPE_SAT;
- d_sat = UNSAT;
- } else if(s == "valid") {
- d_which = TYPE_VALIDITY;
- d_validity = VALID;
- } else if(s == "invalid") {
- d_which = TYPE_VALIDITY;
- d_validity = INVALID;
- } else if(s == "incomplete") {
- d_which = TYPE_SAT;
- d_sat = SAT_UNKNOWN;
- d_unknownExplanation = INCOMPLETE;
- } else if(s == "timeout") {
- d_which = TYPE_SAT;
- d_sat = SAT_UNKNOWN;
- d_unknownExplanation = TIMEOUT;
- } else if(s == "resourceout") {
- d_which = TYPE_SAT;
- d_sat = SAT_UNKNOWN;
- d_unknownExplanation = RESOURCEOUT;
- } else if(s == "memout") {
- d_which = TYPE_SAT;
- d_sat = SAT_UNKNOWN;
- d_unknownExplanation = MEMOUT;
- } else if(s == "interrupted") {
- d_which = TYPE_SAT;
- d_sat = SAT_UNKNOWN;
- d_unknownExplanation = INTERRUPTED;
- } else if(s.size() >= 7 && s.compare(0, 7, "unknown") == 0) {
- d_which = TYPE_SAT;
- d_sat = SAT_UNKNOWN;
- } else {
- IllegalArgument(s, "expected satisfiability/validity result, "
- "instead got `%s'", s.c_str());
- }
-}
-
-Result::UnknownExplanation Result::whyUnknown() const {
- PrettyCheckArgument( isUnknown(), this,
- "This result is not unknown, so the reason for "
- "being unknown cannot be inquired of it" );
- return d_unknownExplanation;
-}
-
-bool Result::operator==(const Result& r) const throw() {
- if(d_which != r.d_which) {
- return false;
- }
- if(d_which == TYPE_SAT) {
- return d_sat == r.d_sat &&
- ( d_sat != SAT_UNKNOWN ||
- d_unknownExplanation == r.d_unknownExplanation );
- }
- if(d_which == TYPE_VALIDITY) {
- return d_validity == r.d_validity &&
- ( d_validity != VALIDITY_UNKNOWN ||
- d_unknownExplanation == r.d_unknownExplanation );
- }
- return false;
-}
-
-bool operator==(enum Result::Sat sr, const Result& r) throw() {
- return r == sr;
-}
-
-bool operator==(enum Result::Validity vr, const Result& r) throw() {
- return r == vr;
-}
-bool operator!=(enum Result::Sat s, const Result& r) throw(){
- return !(s == r);
-}
-bool operator!=(enum Result::Validity v, const Result& r) throw(){
- return !(v == r);
-}
-
-Result Result::asSatisfiabilityResult() const throw() {
- if(d_which == TYPE_SAT) {
- return *this;
- }
-
- if(d_which == TYPE_VALIDITY) {
- switch(d_validity) {
-
- case INVALID:
- return Result(SAT, d_inputName);
-
- case VALID:
- return Result(UNSAT, d_inputName);
-
- case VALIDITY_UNKNOWN:
- return Result(SAT_UNKNOWN, d_unknownExplanation, d_inputName);
-
- default:
- Unhandled(d_validity);
- }
- }
-
- // TYPE_NONE
- return Result(SAT_UNKNOWN, NO_STATUS, d_inputName);
-}
-
-Result Result::asValidityResult() const throw() {
- if(d_which == TYPE_VALIDITY) {
- return *this;
- }
-
- if(d_which == TYPE_SAT) {
- switch(d_sat) {
-
- case SAT:
- return Result(INVALID, d_inputName);
-
- case UNSAT:
- return Result(VALID, d_inputName);
-
- case SAT_UNKNOWN:
- return Result(VALIDITY_UNKNOWN, d_unknownExplanation, d_inputName);
-
- default:
- Unhandled(d_sat);
- }
- }
-
- // TYPE_NONE
- return Result(VALIDITY_UNKNOWN, NO_STATUS, d_inputName);
-}
-
-string Result::toString() const {
- stringstream ss;
- ss << *this;
- return ss.str();
-}
-
-ostream& operator<<(ostream& out, enum Result::Sat s) {
- switch(s) {
- case Result::UNSAT: out << "UNSAT"; break;
- case Result::SAT: out << "SAT"; break;
- case Result::SAT_UNKNOWN: out << "SAT_UNKNOWN"; break;
- default: Unhandled(s);
- }
- return out;
-}
-
-ostream& operator<<(ostream& out, enum Result::Validity v) {
- switch(v) {
- case Result::INVALID: out << "INVALID"; break;
- case Result::VALID: out << "VALID"; break;
- case Result::VALIDITY_UNKNOWN: out << "VALIDITY_UNKNOWN"; break;
- default: Unhandled(v);
- }
- return out;
-}
-
-ostream& operator<<(ostream& out, enum Result::UnknownExplanation e) {
- switch(e) {
- case Result::REQUIRES_FULL_CHECK: out << "REQUIRES_FULL_CHECK"; break;
- case Result::INCOMPLETE: out << "INCOMPLETE"; break;
- case Result::TIMEOUT: out << "TIMEOUT"; break;
- case Result::RESOURCEOUT: out << "RESOURCEOUT"; break;
- case Result::MEMOUT: out << "MEMOUT"; break;
- case Result::INTERRUPTED: out << "INTERRUPTED"; break;
- case Result::NO_STATUS: out << "NO_STATUS"; break;
- case Result::UNSUPPORTED: out << "UNSUPPORTED"; break;
- case Result::OTHER: out << "OTHER"; break;
- case Result::UNKNOWN_REASON: out << "UNKNOWN_REASON"; break;
- default: Unhandled(e);
- }
- return out;
-}
-
-ostream& operator<<(ostream& out, const Result& r) {
- r.toStream(out, Node::setlanguage::getLanguage(out));
- return out;
-}/* operator<<(ostream&, const Result&) */
-
-
-void Result::toStreamDefault(std::ostream& out) const throw() {
- if(getType() == Result::TYPE_SAT) {
- switch(isSat()) {
- case Result::UNSAT:
- out << "unsat";
- break;
- case Result::SAT:
- out << "sat";
- break;
- case Result::SAT_UNKNOWN:
- out << "unknown";
- if(whyUnknown() != Result::UNKNOWN_REASON) {
- out << " (" << whyUnknown() << ")";
- }
- break;
- }
- } else {
- switch(isValid()) {
- case Result::INVALID:
- out << "invalid";
- break;
- case Result::VALID:
- out << "valid";
- break;
- case Result::VALIDITY_UNKNOWN:
- out << "unknown";
- if(whyUnknown() != Result::UNKNOWN_REASON) {
- out << " (" << whyUnknown() << ")";
- }
- break;
- }
- }
-}/* Result::toStreamDefault() */
-
-
-void Result::toStreamSmt2(ostream& out) const throw(){
- if(getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN) {
- out << "unknown";
- } else {
- toStreamDefault(out);
- }
-}
-
-void Result::toStreamTptp(std::ostream& out) const throw() {
- out << "% SZS status ";
- if(isSat() == Result::SAT) {
- out << "Satisfiable";
- } else if(isSat() == Result::UNSAT) {
- out << "Unsatisfiable";
- } else if(isValid() == Result::VALID) {
- out << "Theorem";
- } else if(isValid() == Result::INVALID) {
- out << "CounterSatisfiable";
- } else {
- out << "GaveUp";
- }
- out << " for " << getInputName();
-}
-
-void Result::toStream(std::ostream& out, OutputLanguage language) const throw() {
- switch(language) {
- case language::output::LANG_SMTLIB_V2_0:
- case language::output::LANG_SMTLIB_V2_5:
- case language::output::LANG_SYGUS:
- case language::output::LANG_Z3STR:
- toStreamSmt2(out);
- break;
- case language::output::LANG_TPTP:
- toStreamTptp(out);
- break;
- case language::output::LANG_AST:
- case language::output::LANG_AUTO:
- case language::output::LANG_CVC3:
- case language::output::LANG_CVC4:
- case language::output::LANG_MAX:
- case language::output::LANG_SMTLIB_V1:
- default:
- toStreamDefault(out);
- break;
- };
-}
-
-}/* CVC4 namespace */
+++ /dev/null
-/********************* */
-/*! \file result.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Encapsulation of the result of a query.
- **
- ** Encapsulation of the result of a query.
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__RESULT_H
-#define __CVC4__RESULT_H
-
-#include <iostream>
-#include <string>
-
-#include "base/exception.h"
-#include "options/language.h"
-
-namespace CVC4 {
-
-class Result;
-
-std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_PUBLIC;
-
-/**
- * Three-valued SMT result, with optional explanation.
- */
-class CVC4_PUBLIC Result {
-public:
- enum Sat {
- UNSAT = 0,
- SAT = 1,
- SAT_UNKNOWN = 2
- };
-
- enum Validity {
- INVALID = 0,
- VALID = 1,
- VALIDITY_UNKNOWN = 2
- };
-
- enum Type {
- TYPE_SAT,
- TYPE_VALIDITY,
- TYPE_NONE
- };
-
- enum UnknownExplanation {
- REQUIRES_FULL_CHECK,
- INCOMPLETE,
- TIMEOUT,
- RESOURCEOUT,
- MEMOUT,
- INTERRUPTED,
- NO_STATUS,
- UNSUPPORTED,
- OTHER,
- UNKNOWN_REASON
- };
-
-private:
- enum Sat d_sat;
- enum Validity d_validity;
- enum Type d_which;
- enum UnknownExplanation d_unknownExplanation;
- std::string d_inputName;
-
-public:
-
- Result();
-
- Result(enum Sat s, std::string inputName = "");
-
- Result(enum Validity v, std::string inputName = "");
-
- Result(enum Sat s,
- enum UnknownExplanation unknownExplanation,
- std::string inputName = "");
-
- Result(enum Validity v, enum UnknownExplanation unknownExplanation,
- std::string inputName = "");
-
- Result(const std::string& s, std::string inputName = "");
-
- Result(const Result& r, std::string inputName) {
- *this = r;
- d_inputName = inputName;
- }
-
- enum Sat isSat() const {
- return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN;
- }
-
- enum Validity isValid() const {
- return d_which == TYPE_VALIDITY ? d_validity : VALIDITY_UNKNOWN;
- }
-
- bool isUnknown() const {
- return isSat() == SAT_UNKNOWN && isValid() == VALIDITY_UNKNOWN;
- }
-
- Type getType() const {
- return d_which;
- }
-
- bool isNull() const {
- return d_which == TYPE_NONE;
- }
-
- enum UnknownExplanation whyUnknown() const;
-
- bool operator==(const Result& r) const throw();
- inline bool operator!=(const Result& r) const throw();
- Result asSatisfiabilityResult() const throw();
- Result asValidityResult() const throw();
-
- std::string toString() const;
-
- std::string getInputName() const { return d_inputName; }
-
- /**
- * Write a Result out to a stream in this language.
- */
- void toStream(std::ostream& out, OutputLanguage language) const throw();
-
- /**
- * This is mostly the same the default
- * If getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN,
- *
- */
- void toStreamSmt2(std::ostream& out) const throw();
-
- /**
- * Write a Result out to a stream in the Tptp format
- */
- void toStreamTptp(std::ostream& out) const throw();
-
- /**
- * Write a Result out to a stream.
- *
- * The default implementation writes a reasonable string in lowercase
- * for sat, unsat, valid, invalid, or unknown results. This behavior
- * is overridable by each Printer, since sometimes an output language
- * has a particular preference for how results should appear.
- */
- void toStreamDefault(std::ostream& out) const throw();
-};/* class Result */
-
-inline bool Result::operator!=(const Result& r) const throw() {
- return !(*this == r);
-}
-
-std::ostream& operator<<(std::ostream& out,
- enum Result::Sat s) CVC4_PUBLIC;
-std::ostream& operator<<(std::ostream& out,
- enum Result::Validity v) CVC4_PUBLIC;
-std::ostream& operator<<(std::ostream& out,
- enum Result::UnknownExplanation e) CVC4_PUBLIC;
-
-bool operator==(enum Result::Sat s, const Result& r) throw() CVC4_PUBLIC;
-bool operator==(enum Result::Validity v, const Result& r) throw() CVC4_PUBLIC;
-
-bool operator!=(enum Result::Sat s, const Result& r) throw() CVC4_PUBLIC;
-bool operator!=(enum Result::Validity v, const Result& r) throw() CVC4_PUBLIC;
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__RESULT_H */
+++ /dev/null
-%{
-#include "expr/result.h"
-%}
-
-%ignore CVC4::operator<<(std::ostream&, const Result& r);
-
-%rename(equals) CVC4::Result::operator==(const Result& r) const;
-%ignore CVC4::Result::operator!=(const Result& r) const;
-
-%ignore CVC4::operator<<(std::ostream&, enum Result::Sat);
-%ignore CVC4::operator<<(std::ostream&, enum Result::Validity);
-%ignore CVC4::operator<<(std::ostream&, enum Result::UnknownExplanation);
-
-%ignore CVC4::operator==(enum Result::Sat, const Result&);
-%ignore CVC4::operator!=(enum Result::Sat, const Result&);
-
-%ignore CVC4::operator==(enum Result::Validity, const Result&);
-%ignore CVC4::operator!=(enum Result::Validity, const Result&);
-
-%include "expr/result.h"
d_stats.flushInformation(out);
}
+ SmtGlobals* globals() { return d_smtEngine->globals(); }
+
protected:
/** Executes treating cmd as a singleton */
virtual bool doCommandSingleton(CVC4::Command* cmd);
};/* class CommandExecutor */
-bool smtEngineInvoke(SmtEngine* smt,
- Command* cmd,
- std::ostream *out);
+bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out);
}/* CVC4::main namespace */
}/* CVC4 namespace */
const unsigned int sharingChannelSize = 1000000;
for(unsigned i = 0; i < d_numThreads; ++i){
- d_channelsOut.push_back
- (new SynchronizedSharedChannel<ChannelFormat>(sharingChannelSize));
- d_channelsIn.push_back
- (new SynchronizedSharedChannel<ChannelFormat>(sharingChannelSize));
+ d_channelsOut.push_back(
+ new SynchronizedSharedChannel<ChannelFormat>(sharingChannelSize));
+ d_channelsIn.push_back(
+ new SynchronizedSharedChannel<ChannelFormat>(sharingChannelSize));
}
/* Lemma I/O channels */
for(unsigned i = 0; i < d_numThreads; ++i) {
string tag = "thread #" +
boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]);
- d_threadOptions[i].set
- (options::lemmaOutputChannel,
- new PortfolioLemmaOutputChannel(tag, d_channelsOut[i], d_exprMgrs[i],
- d_vmaps[i]->d_from, d_vmaps[i]->d_to));
- d_threadOptions[i].set
- (options::lemmaInputChannel,
- new PortfolioLemmaInputChannel(tag, d_channelsIn[i], d_exprMgrs[i],
- d_vmaps[i]->d_from, d_vmaps[i]->d_to));
+ LemmaOutputChannel* outputChannel =
+ new PortfolioLemmaOutputChannel(tag, d_channelsOut[i], d_exprMgrs[i],
+ d_vmaps[i]->d_from, d_vmaps[i]->d_to);
+ LemmaInputChannel* inputChannel =
+ new PortfolioLemmaInputChannel(tag, d_channelsIn[i], d_exprMgrs[i],
+ d_vmaps[i]->d_from, d_vmaps[i]->d_to);
+ d_smts[i]->globals()->setLemmaInputChannel(inputChannel);
+ d_smts[i]->globals()->setLemmaOutputChannel(outputChannel);
}
/* Output to string stream */
for(unsigned i = 0; i < d_numThreads; ++i) {
delete d_channelsIn[i];
delete d_channelsOut[i];
- d_threadOptions[i].set(options::lemmaInputChannel, NULL);
- d_threadOptions[i].set(options::lemmaOutputChannel, NULL);
+ delete d_smts[i]->globals()->getLemmaInputChannel();
+ d_smts[i]->globals()->setLemmaInputChannel(NULL);
+ delete d_smts[i]->globals()->getLemmaOutputChannel();
+ d_smts[i]->globals()->setLemmaOutputChannel(NULL);
}
d_channelsIn.clear();
d_channelsOut.clear();
#include "base/output.h"
#include "expr/expr_iomanip.h"
#include "expr/expr_manager.h"
-#include "expr/result.h"
#include "expr/statistics_registry.h"
#include "main/command_executor.h"
#include "smt/smt_options_handler.h"
#include "smt_util/command.h"
#include "util/configuration.h"
+#include "util/result.h"
using namespace std;
using namespace CVC4;
replayParserBuilder.withStreamInput(cin);
}
replayParser = replayParserBuilder.build();
- opts.set(options::replayStream, new Parser::ExprStream(replayParser));
+ pExecutor->globals()->setReplayStream(new Parser::ExprStream(replayParser));
}
- if( opts[options::replayLog] != NULL ) {
- *opts[options::replayLog] << language::SetLanguage(opts[options::outputLanguage])
- << expr::ExprSetDepth(-1);
+ if( pExecutor->globals()->getReplayLog() != NULL ) {
+ *(pExecutor->globals()->getReplayLog()) <<
+ language::SetLanguage(opts[options::outputLanguage]) << expr::ExprSetDepth(-1);
}
int returnValue = 0;
delete parser;
}
- if( opts[options::replayStream] != NULL ) {
+ if( pExecutor->globals()->getReplayStream() != NULL ) {
+ ExprStream* replayStream = pExecutor->globals()->getReplayStream();
+ pExecutor->globals()->setReplayStream(NULL);
// this deletes the expression parser too
- delete opts[options::replayStream];
- opts.set(options::replayStream, NULL);
+ delete replayStream;
}
Result result;
}
// make sure to flush replay output log before early-exit
- if( opts[options::replayLog] != NULL ) {
- *opts[options::replayLog] << flush;
+ if( pExecutor->globals()->getReplayLog() != NULL ) {
+ *(pExecutor->globals()->getReplayLog()) << flush;
}
// make sure out and err streams are flushed too
#include "base/output.h"
#include "expr/expr_manager.h"
-#include "expr/result.h"
#include "expr/statistics.h"
#include "main/command_executor.h"
#include "main/interactive_shell.h"
#include "smt/smt_engine.h"
#include "smt_util/command.h"
#include "util/configuration.h"
+#include "util/result.h"
using namespace std;
using namespace CVC4;
#include <boost/exception_ptr.hpp>
#include "base/output.h"
-#include "expr/result.h"
#include "expr/statistics_registry.h"
#include "options/options.h"
#include "smt/smt_engine.h"
-
+#include "util/result.h"
namespace CVC4 {
class OptionsHandler;
}/* CVC4::options namespace */
-// Forward declaration for smt_options
-class ExprStream;
-
class CVC4_PUBLIC Options {
/** The struct that holds all option values. */
options::OptionsHolder* d_holder;
return handler->checkReplayFilename(option, optarg);
}
-std::ostream* checkReplayLogFilename(std::string option, std::string optarg, OptionsHandler* handler) {
- PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
- return handler->checkReplayLogFilename(option, optarg);
-}
// ensure we are a stats-enabled build of CVC4
void statsEnabledBuild(std::string option, bool value, OptionsHandler* handler) throw(OptionException) {
virtual void setRegularOutputChannel(std::string option, std::string optarg) = 0;
virtual void setDiagnosticOutputChannel(std::string option, std::string optarg) = 0;
virtual std::string checkReplayFilename(std::string option, std::string optarg) = 0;
- virtual std::ostream* checkReplayLogFilename(std::string option, std::string optarg) = 0;
virtual void statsEnabledBuild(std::string option, bool value) throw(OptionException) = 0;
virtual unsigned long tlimitHandler(std::string option, std::string optarg) throw(OptionException) = 0;
virtual unsigned long tlimitPerHandler(std::string option, std::string optarg) throw(OptionException) = 0;
std::string checkReplayFilename(std::string option, std::string optarg, OptionsHandler* handler);
-std::ostream* checkReplayLogFilename(std::string option, std::string optarg, OptionsHandler* handler);
-
// ensure we are a stats-enabled build of CVC4
void statsEnabledBuild(std::string option, bool value, OptionsHandler* handler) throw(OptionException);
** Contains code for handling command-line options
**/
-#warning "TODO: Remove ExprStream forward declaration from options.h."
-
#if !defined(_BSD_SOURCE) && defined(__MINGW32__) && !defined(__MINGW64__)
// force use of optreset; mingw32 croaks on argv-switching otherwise
# include "cvc4autoconfig.h"
# --replay is currently broken; don't document it for 1.0
undocumented-option replayFilename --replay=FILE std::string :handler CVC4::options::checkReplayFilename :handler-include "options/options_handler_interface.h"
replay decisions from file
-undocumented-option replayLog --replay-log=FILE std::ostream* :handler CVC4::options::checkReplayLogFilename :handler-include "options/options_handler_interface.h"
- log decisions and propagations to file
-option replayStream ExprStream*
-
-# portfolio options
-option lemmaInputChannel LemmaInputChannel* :default NULL :include "base/lemma_input_channel_forward.h"
- The input channel to receive notfication events for new lemmas
-option lemmaOutputChannel LemmaOutputChannel* :default NULL :include "base/lemma_output_channel_forward.h"
- The output channel to receive notfication events for new lemmas
+
option forceNoLimitCpuWhileDump --force-no-limit-cpu-while-dump bool :default false
Force no CPU limit when dumping models and proofs
namespace CVC4 {
namespace prop {
-CnfStream::CnfStream(SatSolver *satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap) :
- d_satSolver(satSolver),
- d_booleanVariables(context),
- d_nodeToLiteralMap(context),
- d_literalToNodeMap(context),
- d_fullLitToNodeMap(fullLitToNodeMap),
- d_convertAndAssertCounter(0),
- d_registrar(registrar),
- d_assertionTable(context),
- d_removable(false) {
+CnfStream::CnfStream(SatSolver* satSolver, Registrar* registrar,
+ context::Context* context, SmtGlobals* globals,
+ bool fullLitToNodeMap)
+ : d_satSolver(satSolver),
+ d_booleanVariables(context),
+ d_nodeToLiteralMap(context),
+ d_literalToNodeMap(context),
+ d_fullLitToNodeMap(fullLitToNodeMap),
+ d_convertAndAssertCounter(0),
+ d_registrar(registrar),
+ d_assertionTable(context),
+ d_globals(globals),
+ d_removable(false) {
}
-TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap) :
- CnfStream(satSolver, registrar, context, fullLitToNodeMap) {
-}
+TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver, Registrar* registrar,
+ context::Context* context,
+ SmtGlobals* globals, bool fullLitToNodeMap)
+ : CnfStream(satSolver, registrar, context, globals, fullLitToNodeMap)
+{}
void CnfStream::assertClause(TNode node, SatClause& c, ProofRule proof_id) {
Debug("cnf") << "Inserting into stream " << c << " node = " << node << ", proof id = " << proof_id << endl;
// If it's a theory literal, need to store it for back queries
if ( isTheoryAtom || d_fullLitToNodeMap ||
- ( CVC4_USE_REPLAY && options::replayLog() != NULL ) ||
+ ( CVC4_USE_REPLAY && d_globals->getReplayLog() != NULL ) ||
(Dump.isOn("clauses")) ) {
d_literalToNodeMap.insert_safe(lit, node);
#ifndef __CVC4__PROP__CNF_STREAM_H
#define __CVC4__PROP__CNF_STREAM_H
+#include <ext/hash_map>
+
+#include "context/cdinsert_hashmap.h"
+#include "context/cdlist.h"
#include "expr/node.h"
-#include "prop/theory_proxy.h"
-#include "prop/registrar.h"
#include "proof/proof_manager.h"
-#include "context/cdlist.h"
-#include "context/cdinsert_hashmap.h"
-
-#include <ext/hash_map>
+#include "prop/registrar.h"
+#include "prop/theory_proxy.h"
+#include "smt/smt_globals.h"
namespace CVC4 {
namespace prop {
/** A table of assertions, used for regenerating proofs. */
context::CDList<Node> d_assertionTable;
+ /** Container for misc. globals. */
+ SmtGlobals* d_globals;
+
/**
* How many literals were already mapped at the top-level when we
* tried to convertAndAssert() something. This
* @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping,
* even for non-theory literals
*/
- CnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap = false);
+ CnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, SmtGlobals* globals, bool fullLitToNodeMap = false);
/**
* Destructs a CnfStream. This implementation does nothing, but we
* @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping,
* even for non-theory literals
*/
- TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap = false);
+ TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, SmtGlobals* globals, bool fullLitToNodeMap = false);
private:
#include "decision/decision_engine.h"
#include "expr/expr.h"
#include "expr/resource_manager.h"
-#include "expr/result.h"
#include "options/base_options.h"
#include "options/decision_options.h"
#include "options/main_options.h"
#include "smt_util/command.h"
#include "theory/theory_engine.h"
#include "theory/theory_registrar.h"
-
+#include "util/result.h"
using namespace std;
using namespace CVC4::context;
}
};
-PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext, Context* userContext) :
+PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext, Context* userContext, SmtGlobals* globals) :
d_inCheckSat(false),
d_theoryEngine(te),
d_decisionEngine(de),
d_registrar(NULL),
d_cnfStream(NULL),
d_interrupted(false),
- d_resourceManager(NodeManager::currentResourceManager()) {
+ d_resourceManager(NodeManager::currentResourceManager()),
+ d_globals(globals)
+{
Debug("prop") << "Constructing the PropEngine" << endl;
d_registrar = new theory::TheoryRegistrar(d_theoryEngine);
d_cnfStream = new CVC4::prop::TseitinCnfStream
- (d_satSolver, d_registrar,
- userContext,
+ (d_satSolver, d_registrar, userContext, d_globals,
// fullLitToNode Map =
options::threads() > 1 ||
options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY
);
- d_theoryProxy = new TheoryProxy(this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream);
+ d_theoryProxy = new TheoryProxy(this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream, d_globals);
d_satSolver->initialize(d_context, d_theoryProxy);
d_decisionEngine->setSatSolver(d_satSolver);
#include "base/modal_exception.h"
#include "expr/node.h"
-#include "expr/result.h"
#include "options/options.h"
#include "proof/proof_manager.h"
+#include "smt/smt_globals.h"
#include "util/unsafe_interrupt_exception.h"
+#include "util/result.h"
namespace CVC4 {
/** Dump out the satisfying assignment (after SAT result) */
void printSatisfyingAssignment();
+ /** Container for misc. globals. */
+ SmtGlobals* d_globals;
+
public:
/**
* Create a PropEngine with a particular decision and theory engine.
*/
- PropEngine(TheoryEngine*, DecisionEngine*, context::Context* satContext, context::Context* userContext);
+ PropEngine(TheoryEngine*, DecisionEngine*, context::Context* satContext, context::Context* userContext, SmtGlobals* global);
/**
* Destructor.
namespace CVC4 {
namespace prop {
+TheoryProxy::TheoryProxy(PropEngine* propEngine,
+ TheoryEngine* theoryEngine,
+ DecisionEngine* decisionEngine,
+ context::Context* context,
+ CnfStream* cnfStream,
+ SmtGlobals* globals)
+ : d_propEngine(propEngine),
+ d_cnfStream(cnfStream),
+ d_decisionEngine(decisionEngine),
+ d_theoryEngine(theoryEngine),
+ d_globals(globals),
+ d_queue(context)
+{}
+
+TheoryProxy::~TheoryProxy() {
+ /* nothing to do for now */
+}
+
+/** The lemma input channel we are using. */
+LemmaInputChannel* TheoryProxy::inputChannel() {
+ return d_globals->getLemmaInputChannel();
+}
+
+/** The lemma output channel we are using. */
+LemmaOutputChannel* TheoryProxy::outputChannel() {
+ return d_globals->getLemmaOutputChannel();
+}
+
+std::ostream* TheoryProxy::replayLog() {
+ return d_globals->getReplayLog();
+}
+
+ExprStream* TheoryProxy::replayStream() {
+ return d_globals->getReplayStream();
+}
+
+
void TheoryProxy::variableNotify(SatVariable var) {
d_theoryEngine->preRegister(getNode(SatLiteral(var)));
}
static uint32_t lemmaCount = 0;
- if(options::lemmaInputChannel() != NULL) {
- while(options::lemmaInputChannel()->hasNewLemma()) {
+ if(inputChannel() != NULL) {
+ while(inputChannel()->hasNewLemma()) {
Debug("shared") << "shared" << std::endl;
- Expr lemma = options::lemmaInputChannel()->getNewLemma();
+ Expr lemma = inputChannel()->getNewLemma();
Node asNode = lemma.getNode();
asNode = theory::Rewriter::rewrite(asNode);
void TheoryProxy::notifyNewLemma(SatClause& lemma) {
Assert(lemma.size() > 0);
- if(options::lemmaOutputChannel() != NULL) {
+ if(outputChannel() != NULL) {
if(lemma.size() == 1) {
// cannot share units yet
//options::lemmaOutputChannel()->notifyNewLemma(d_cnfStream->getNode(lemma[0]).toExpr());
if(d_shared.find(n) == d_shared.end()) {
d_shared.insert(n);
- options::lemmaOutputChannel()->notifyNewLemma(n.toExpr());
+ outputChannel()->notifyNewLemma(n.toExpr());
} else {
Debug("shared") <<"drop new " << n << std::endl;
}
SatLiteral TheoryProxy::getNextReplayDecision() {
#ifdef CVC4_REPLAY
- if(options::replayStream() != NULL) {
- Expr e = options::replayStream()->nextExpr();
+ if(replayStream() != NULL) {
+ Expr e = replayStream()->nextExpr();
if(!e.isNull()) { // we get null node when out of decisions to replay
// convert & return
++d_replayedDecisions;
void TheoryProxy::logDecision(SatLiteral lit) {
#ifdef CVC4_REPLAY
- if(options::replayLog() != NULL) {
+ if(replayLog() != NULL) {
Assert(lit != undefSatLiteral, "logging an `undef' decision ?!");
- *options::replayLog() << d_cnfStream->getNode(lit) << std::endl;
+ (*replayLog()) << d_cnfStream->getNode(lit) << std::endl;
}
#endif /* CVC4_REPLAY */
}
// Optional blocks below will be unconditionally included
#define __CVC4_USE_MINISAT
+#include <iosfwd>
+
#include "context/cdqueue.h"
+#include "expr/node.h"
#include "expr/statistics_registry.h"
#include "prop/sat_solver.h"
+#include "smt/smt_globals.h"
+#include "smt_util/lemma_output_channel.h"
+#include "smt_util/lemma_input_channel.h"
#include "theory/theory.h"
namespace CVC4 {
* The proxy class that allows the SatSolver to communicate with the theories
*/
class TheoryProxy {
-
- /** The prop engine we are using */
- PropEngine* d_propEngine;
-
- /** The CNF engine we are using */
- CnfStream* d_cnfStream;
-
- /** The decision engine we are using */
- DecisionEngine* d_decisionEngine;
-
- /** The theory engine we are using */
- TheoryEngine* d_theoryEngine;
-
- /** Queue of asserted facts */
- context::CDQueue<TNode> d_queue;
-
- /**
- * Set of all lemmas that have been "shared" in the portfolio---i.e.,
- * all imported and exported lemmas.
- */
- std::hash_set<Node, NodeHashFunction> d_shared;
-
- /**
- * Statistic: the number of replayed decisions (via --replay).
- */
- KEEP_STATISTIC(IntStat, d_replayedDecisions,
- "prop::theoryproxy::replayedDecisions", 0);
-
public:
TheoryProxy(PropEngine* propEngine,
TheoryEngine* theoryEngine,
DecisionEngine* decisionEngine,
context::Context* context,
- CnfStream* cnfStream);
+ CnfStream* cnfStream,
+ SmtGlobals* globals);
~TheoryProxy();
SatValue getDecisionPolarity(SatVariable var);
-};/* class SatSolver */
+ private:
+ /** The prop engine we are using. */
+ PropEngine* d_propEngine;
-/* Functions that delegate to the concrete SAT solver. */
-
-inline TheoryProxy::TheoryProxy(PropEngine* propEngine,
- TheoryEngine* theoryEngine,
- DecisionEngine* decisionEngine,
- context::Context* context,
- CnfStream* cnfStream) :
- d_propEngine(propEngine),
- d_cnfStream(cnfStream),
- d_decisionEngine(decisionEngine),
- d_theoryEngine(theoryEngine),
- d_queue(context)
-{}
-
-inline TheoryProxy::~TheoryProxy() {
- /* nothing to do for now */
-}
+ /** The CNF engine we are using. */
+ CnfStream* d_cnfStream;
+
+ /** The decision engine we are using. */
+ DecisionEngine* d_decisionEngine;
+
+ /** The theory engine we are using. */
+ TheoryEngine* d_theoryEngine;
+
+
+ /**
+ * Container for inputChannel, outputChannel, replayLog, and
+ * replayStream.
+ */
+ SmtGlobals* d_globals;
+
+ /** The lemma input channel we are using. */
+ LemmaInputChannel* inputChannel();
+
+ /** The lemma output channel we are using. */
+ LemmaOutputChannel* outputChannel();
+
+ std::ostream* replayLog();
+ ExprStream* replayStream();
+
+ /** Queue of asserted facts */
+ context::CDQueue<TNode> d_queue;
+
+ /**
+ * Set of all lemmas that have been "shared" in the portfolio---i.e.,
+ * all imported and exported lemmas.
+ */
+ std::hash_set<Node, NodeHashFunction> d_shared;
+
+ /**
+ * Statistic: the number of replayed decisions (via --replay).
+ */
+ KEEP_STATISTIC(IntStat, d_replayedDecisions,
+ "prop::theoryproxy::replayedDecisions", 0);
+};/* class SatSolver */
}/* CVC4::prop namespace */
d_private(NULL),
d_smtAttributes(NULL),
d_statisticsRegistry(NULL),
- d_stats(NULL) {
+ d_stats(NULL),
+ d_globals(new SmtGlobals())
+{
SmtScope smts(this);
d_smtAttributes = new expr::attr::SmtAttributes(d_context);
d_stats->d_resourceUnitsUsed.setData(d_private->getResourceManager()->d_cumulativeResourceUsed);
// We have mutual dependency here, so we add the prop engine to the theory
// engine later (it is non-essential there)
- d_theoryEngine = new TheoryEngine(d_context, d_userContext, d_private->d_iteRemover, const_cast<const LogicInfo&>(d_logic));
+ d_theoryEngine = new TheoryEngine(d_context, d_userContext,
+ d_private->d_iteRemover,
+ const_cast<const LogicInfo&>(d_logic),
+ d_globals);
// Add the theories
for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
d_decisionEngine = new DecisionEngine(d_context, d_userContext);
d_decisionEngine->init(); // enable appropriate strategies
- d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context, d_userContext);
+ d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context,
+ d_userContext, d_globals);
d_theoryEngine->setPropEngine(d_propEngine);
d_theoryEngine->setDecisionEngine(d_decisionEngine);
delete d_context;
d_context = NULL;
+ delete d_globals;
+ d_globals = NULL;
+
} catch(Exception& e) {
Warning() << "CVC4 threw an exception during cleanup." << endl
<< e << endl;
#include "context/cdlist_forward.h"
#include "expr/expr.h"
#include "expr/expr_manager.h"
-#include "expr/result.h"
#include "expr/sexpr.h"
#include "expr/statistics.h"
#include "options/options.h"
#include "proof/unsat_core.h"
#include "smt/logic_exception.h"
+#include "smt/smt_globals.h"
#include "theory/logic_info.h"
#include "util/hash.h"
#include "util/proof.h"
+#include "util/result.h"
#include "util/unsafe_interrupt_exception.h"
// In terms of abstraction, this is below (and provides services to)
smt::SmtEngineStatistics* d_stats;
+ SmtGlobals* d_globals;
+
/**
* Add to Model command. This is used for recording a command
* that should be reported during a get-model call.
* Throws a ModalException if smt is non-null and the SmtEngine has not been fully initialized.
*/
static void beforeSearch(SmtEngine* smt, const std::string& option) throw(ModalException);
+
+ SmtGlobals* globals() { return d_globals; }
};/* class SmtEngine */
}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file smt_globals.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/smt_globals.h"
+
+#include <cerrno>
+#include <iostream>
+#include <string>
+#include <utility>
+
+#include "cvc4autoconfig.h" // Needed for CVC4_REPLAY
+#include "expr/expr_stream.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"
+#include "smt/smt_options_handler.h"
+
+namespace CVC4 {
+
+SmtGlobals::SmtGlobals()
+ : d_gcReplayLog(false)
+ , d_replayLog(NULL)
+ , d_replayStream(NULL)
+ , d_lemmaInputChannel(NULL)
+ , d_lemmaOutputChannel(NULL)
+{}
+
+SmtGlobals::~SmtGlobals(){
+ if(d_gcReplayLog){
+ delete d_replayLog;
+ d_gcReplayLog = false;
+ d_replayLog = NULL;
+ }
+}
+
+void SmtGlobals::setReplayLog(std::ostream* log){
+ d_replayLog = log;
+}
+
+void SmtGlobals::setReplayStream(ExprStream* stream) {
+ d_replayStream = stream;
+}
+
+void SmtGlobals::setLemmaInputChannel(LemmaInputChannel* in) {
+ d_lemmaInputChannel = in;
+}
+
+void SmtGlobals::setLemmaOutputChannel(LemmaOutputChannel* out) {
+ d_lemmaOutputChannel = out;
+}
+
+void SmtGlobals::parseReplayLog(std::string optarg) throw (OptionException) {
+ if(d_gcReplayLog){
+ delete d_replayLog;
+ d_gcReplayLog = false;
+ d_replayLog = NULL;
+ }
+
+ std::pair<bool, std::ostream*> checkResult = checkReplayLogFilename(optarg);
+ d_gcReplayLog = checkResult.first;
+ d_replayLog = checkResult.second;
+}
+
+#warning "TODO: Move checkReplayLogFilename back into options and has calling setReplayLog as a side effect."
+std::pair<bool, std::ostream*> SmtGlobals::checkReplayLogFilename(std::string optarg)
+ throw (OptionException)
+{
+#ifdef CVC4_REPLAY
+ if(optarg == "") {
+ throw OptionException(std::string("Bad file name for --replay-log"));
+ } else if(optarg == "-") {
+ return std::make_pair(false, &std::cout);
+ } else if(!options::filesystemAccess()) {
+ throw OptionException(std::string("Filesystem access not permitted"));
+ } else {
+ errno = 0;
+ std::ios_base::openmode out_trunc = std::ofstream::out | std::ofstream::trunc;
+ std::ostream* replayLog = new std::ofstream(optarg.c_str(), out_trunc);
+ if(replayLog == NULL || !*replayLog) {
+ std::stringstream ss;
+ ss << "Cannot open replay-log file: `" << optarg << "': "
+ << smt::SmtOptionsHandler::__cvc4_errno_failreason();
+ throw OptionException(ss.str());
+ }
+ return std::make_pair(true, replayLog);
+ }
+#else /* CVC4_REPLAY */
+ throw OptionException("The replay feature was disabled in this build of CVC4.");
+#endif /* CVC4_REPLAY */
+}
+
+
+} /* namespace CVC4 */
--- /dev/null
+/********************* */
+/*! \file smt_globals.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 SmtGlobals is a light container for psuedo-global datastructures
+ ** that are set by the user.
+ **
+ ** SmtGlobals is a light container for psuedo-global datastructures
+ ** that are set by the user. These contain paramaters for infrequently
+ ** used modes: Portfolio and Replay. There should be exactly one of these
+ ** per SmtEngine with the same lifetime as the SmtEngine.
+ ** A 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.
+ **
+ ** This class is NOT a good long term solution, but is a reasonable stop gap.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__SMT__SMT_GLOBALS_H
+#define __CVC4__SMT__SMT_GLOBALS_H
+
+#include <iosfwd>
+#include <string>
+#include <utility>
+
+#include "expr/expr_stream.h"
+#include "options/option_exception.h"
+#include "smt_util/lemma_input_channel.h"
+#include "smt_util/lemma_output_channel.h"
+
+namespace CVC4 {
+
+/**
+ * SmtGlobals is a wrapper around 4 pointers:
+ * - getReplayLog()
+ * - getReplayStream()
+ * - getLemmaInputChannel()
+ * - getLemmaOutputChannel()
+ *
+ * The user can directly set these and is responsible for handling the
+ * memory for these. These datastructures are used for the Replay and Portfolio
+ * modes.
+ */
+class CVC4_PUBLIC SmtGlobals {
+ public:
+ /** Creates an empty SmtGlobals with all 4 pointers initially NULL. */
+ SmtGlobals();
+ ~SmtGlobals();
+
+ /** This setsReplayLog based on --replay-log */
+ void parseReplayLog(std::string optarg) throw (OptionException);
+ void setReplayLog(std::ostream*);
+ std::ostream* getReplayLog() { return d_replayLog; }
+
+ void setReplayStream(ExprStream* stream);
+ ExprStream* getReplayStream() { return d_replayStream; }
+
+ void setLemmaInputChannel(LemmaInputChannel* in);
+ LemmaInputChannel* getLemmaInputChannel() { return d_lemmaInputChannel; }
+
+ void setLemmaOutputChannel(LemmaOutputChannel* out);
+ LemmaOutputChannel* getLemmaOutputChannel() { return d_lemmaOutputChannel; }
+
+ private:
+ // Disable copy constructor.
+ SmtGlobals(const SmtGlobals&) CVC4_UNDEFINED;
+
+ // Disable assignment operator.
+ SmtGlobals& operator=(const SmtGlobals&) CVC4_UNDEFINED;
+
+ static std::pair<bool, std::ostream*>
+ checkReplayLogFilename(std::string optarg) throw (OptionException);
+
+ /**
+ * d_gcReplayLog is true iff d_replayLog was allocated by parseReplayLog.
+ */
+ bool d_gcReplayLog;
+
+ /** This captures the old options::replayLog .*/
+ std::ostream* d_replayLog;
+
+ /** This captures the old options::replayStream .*/
+ ExprStream* d_replayStream;
+
+ /** This captures the old options::lemmaInputChannel .*/
+ LemmaInputChannel* d_lemmaInputChannel;
+
+ /** This captures the old options::lemmaOutputChannel .*/
+ LemmaOutputChannel* d_lemmaOutputChannel;
+}; /* class SmtGlobals */
+
+} /* namespace CVC4 */
+
+#endif /* __CVC4__SMT__SMT_GLOBALS_H */
std::string SmtOptionsHandler::checkReplayFilename(std::string option, std::string optarg) {
#ifdef CVC4_REPLAY
if(optarg == "") {
- throw OptionException(std::string("Bad file name for --replay"));
+ throw OptionException (std::string("Bad file name for --replay"));
} else {
return optarg;
}
#endif /* CVC4_REPLAY */
}
-std::ostream* SmtOptionsHandler::checkReplayLogFilename(std::string option, std::string optarg) {
-#ifdef CVC4_REPLAY
- if(optarg == "") {
- throw OptionException(std::string("Bad file name for --replay-log"));
- } else if(optarg == "-") {
- return &std::cout;
- } else if(!options::filesystemAccess()) {
- throw OptionException(std::string("Filesystem access not permitted"));
- } else {
- errno = 0;
- std::ostream* replayLog = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
- if(replayLog == NULL || !*replayLog) {
- std::stringstream ss;
- ss << "Cannot open replay-log file: `" << optarg << "': " << __cvc4_errno_failreason();
- throw OptionException(ss.str());
- }
- return replayLog;
- }
-#else /* CVC4_REPLAY */
- throw OptionException("The replay feature was disabled in this build of CVC4.");
-#endif /* CVC4_REPLAY */
-}
void SmtOptionsHandler::statsEnabledBuild(std::string option, bool value) throw(OptionException) {
#ifndef CVC4_STATISTICS_ON
virtual void setRegularOutputChannel(std::string option, std::string optarg);
virtual void setDiagnosticOutputChannel(std::string option, std::string optarg);
virtual std::string checkReplayFilename(std::string option, std::string optarg);
- virtual std::ostream* checkReplayLogFilename(std::string option, std::string optarg);
virtual void statsEnabledBuild(std::string option, bool value) throw(OptionException);
virtual unsigned long tlimitHandler(std::string option, std::string optarg) throw(OptionException);
virtual unsigned long tlimitPerHandler(std::string option, std::string optarg) throw(OptionException);
virtual void addDebugTag(std::string option, std::string optarg);
virtual void setPrintSuccess(std::string option, bool value);
+ static std::string __cvc4_errno_failreason();
+
private:
SmtEngine* d_smtEngine;
/* Helper utilities */
static std::string suggestTags(char const* const* validTags, std::string inputTag,
char const* const* additionalTags = NULL);
- static std::string __cvc4_errno_failreason();
/* Help strings */
static const std::string s_bitblastingModeHelp;
#include "expr/datatype.h"
#include "expr/expr.h"
-#include "expr/result.h"
#include "expr/sexpr.h"
#include "expr/type.h"
#include "expr/variable_type_map.h"
#include "proof/unsat_core.h"
#include "util/proof.h"
+#include "util/result.h"
namespace CVC4 {
#ifndef __CVC4__LEMMA_INPUT_CHANNEL_H
#define __CVC4__LEMMA_INPUT_CHANNEL_H
-#include "base/lemma_input_channel_forward.h"
#include "expr/expr.h"
namespace CVC4 {
#ifndef __CVC4__LEMMA_OUTPUT_CHANNEL_H
#define __CVC4__LEMMA_OUTPUT_CHANNEL_H
-#include "base/lemma_output_channel_forward.h"
#include "expr/expr.h"
namespace CVC4 {
#pragma once
-#include "expr/result.h"
#include "theory/arith/arithvar.h"
#include "theory/arith/delta_rational.h"
#include "theory/arith/error_set.h"
#include "theory/arith/partial_model.h"
#include "theory/arith/tableau.h"
#include "util/dense_map.h"
+#include "util/result.h"
namespace CVC4 {
namespace theory {
namespace theory {
namespace arith {
-TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo)
- : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo)
- , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo))
+TheoryArith::TheoryArith(context::Context* c, context::UserContext* u,
+ OutputChannel& out, Valuation valuation,
+ const LogicInfo& logicInfo, SmtGlobals* globals)
+ : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, globals)
+ , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo))
{}
TheoryArith::~TheoryArith(){
KEEP_STATISTIC(TimerStat, d_ppRewriteTimer, "theory::arith::ppRewriteTimer");
public:
- TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
+ TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out,
+ Valuation valuation, const LogicInfo& logicInfo,
+ SmtGlobals* globals);
virtual ~TheoryArith();
/**
#include "expr/metakind.h"
#include "expr/node.h"
#include "expr/node_builder.h"
-#include "expr/result.h"
#include "expr/statistics_registry.h"
#include "options/arith_options.h"
#include "options/smt_options.h" // for incrementalSolving()
#include "util/dense_map.h"
#include "util/integer.h"
#include "util/rational.h"
+#include "util/result.h"
using namespace std;
using namespace CVC4::kind;
#include "expr/metakind.h"
#include "expr/node.h"
#include "expr/node_builder.h"
-#include "expr/result.h"
#include "expr/statistics_registry.h"
#include "options/arith_options.h"
#include "smt/logic_exception.h"
#include "util/dense_map.h"
#include "util/integer.h"
#include "util/rational.h"
+#include "util/result.h"
namespace CVC4 {
namespace theory {
//bool d_lazyRIntro1 = true;
//bool d_eagerIndexSplitting = false;
-TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
- Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo),
- d_numRow("theory::arrays::number of Row lemmas", 0),
- d_numExt("theory::arrays::number of Ext lemmas", 0),
- d_numProp("theory::arrays::number of propagations", 0),
- d_numExplain("theory::arrays::number of explanations", 0),
- d_numNonLinear("theory::arrays::number of calls to setNonLinear", 0),
- d_numSharedArrayVarSplits("theory::arrays::number of shared array var splits", 0),
- d_numGetModelValSplits("theory::arrays::number of getModelVal splits", 0),
- d_numGetModelValConflicts("theory::arrays::number of getModelVal conflicts", 0),
- d_numSetModelValSplits("theory::arrays::number of setModelVal splits", 0),
- d_numSetModelValConflicts("theory::arrays::number of setModelVal conflicts", 0),
- d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP" , true),
- d_ppFacts(u),
- // d_ppCache(u),
- d_literalsToPropagate(c),
- d_literalsToPropagateIndex(c, 0),
- d_isPreRegistered(c),
- d_mayEqualEqualityEngine(c, "theory::arrays::TheoryArraysMayEqual", true),
- d_notify(*this),
- d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays", true),
- d_conflict(c, false),
- d_backtracker(c),
- d_infoMap(c, &d_backtracker),
- d_mergeQueue(c),
- d_mergeInProgress(false),
- d_RowQueue(c),
- d_RowAlreadyAdded(u),
- d_sharedArrays(c),
- d_sharedOther(c),
- d_sharedTerms(c, false),
- d_reads(c),
- d_constReadsList(c),
- d_constReadsContext(new context::Context()),
- d_contextPopper(c, d_constReadsContext),
- d_skolemIndex(c, 0),
- d_decisionRequests(c),
- d_permRef(c),
- d_modelConstraints(c),
- d_lemmasSaved(c),
- d_defValues(c),
- d_readTableContext(new context::Context()),
- d_arrayMerges(c),
- d_inCheckModel(false)
+TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u,
+ OutputChannel& out, Valuation valuation,
+ const LogicInfo& logicInfo, SmtGlobals* globals)
+ : Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo, globals),
+ d_numRow("theory::arrays::number of Row lemmas", 0),
+ d_numExt("theory::arrays::number of Ext lemmas", 0),
+ d_numProp("theory::arrays::number of propagations", 0),
+ d_numExplain("theory::arrays::number of explanations", 0),
+ d_numNonLinear("theory::arrays::number of calls to setNonLinear", 0),
+ d_numSharedArrayVarSplits("theory::arrays::number of shared array var splits", 0),
+ d_numGetModelValSplits("theory::arrays::number of getModelVal splits", 0),
+ d_numGetModelValConflicts("theory::arrays::number of getModelVal conflicts", 0),
+ d_numSetModelValSplits("theory::arrays::number of setModelVal splits", 0),
+ d_numSetModelValConflicts("theory::arrays::number of setModelVal conflicts", 0),
+ d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP" , true),
+ d_ppFacts(u),
+ // d_ppCache(u),
+ d_literalsToPropagate(c),
+ d_literalsToPropagateIndex(c, 0),
+ d_isPreRegistered(c),
+ d_mayEqualEqualityEngine(c, "theory::arrays::TheoryArraysMayEqual", true),
+ d_notify(*this),
+ d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays", true),
+ d_conflict(c, false),
+ d_backtracker(c),
+ d_infoMap(c, &d_backtracker),
+ d_mergeQueue(c),
+ d_mergeInProgress(false),
+ d_RowQueue(c),
+ d_RowAlreadyAdded(u),
+ d_sharedArrays(c),
+ d_sharedOther(c),
+ d_sharedTerms(c, false),
+ d_reads(c),
+ d_constReadsList(c),
+ d_constReadsContext(new context::Context()),
+ d_contextPopper(c, d_constReadsContext),
+ d_skolemIndex(c, 0),
+ d_decisionRequests(c),
+ d_permRef(c),
+ d_modelConstraints(c),
+ d_lemmasSaved(c),
+ d_defValues(c),
+ d_readTableContext(new context::Context()),
+ d_arrayMerges(c),
+ d_inCheckModel(false)
{
StatisticsRegistry::registerStat(&d_numRow);
StatisticsRegistry::registerStat(&d_numExt);
public:
- TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
+ TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out,
+ Valuation valuation, const LogicInfo& logicInfo,
+ SmtGlobals* globals);
~TheoryArrays();
void setMasterEqualityEngine(eq::EqualityEngine* eq);
class TheoryBool : public Theory {
public:
- TheoryBool(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
- Theory(THEORY_BOOL, c, u, out, valuation, logicInfo) {
- }
+ TheoryBool(context::Context* c, context::UserContext* u, OutputChannel& out,
+ Valuation valuation, const LogicInfo& logicInfo,
+ SmtGlobals* globals)
+ : Theory(THEORY_BOOL, c, u, out, valuation, logicInfo, globals)
+ {}
PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
class TheoryBuiltin : public Theory {
public:
- TheoryBuiltin(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
- Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo) {}
+ TheoryBuiltin(context::Context* c, context::UserContext* u,
+ OutputChannel& out, Valuation valuation,
+ const LogicInfo& logicInfo, SmtGlobals* globals)
+ : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo, globals) {}
std::string identify() const { return std::string("TheoryBuiltin"); }
};/* class TheoryBuiltin */
#ifndef __CVC4__BITBLASTER_TEMPLATE_H
#define __CVC4__BITBLASTER_TEMPLATE_H
-
-#include "expr/node.h"
-#include <vector>
#include <ext/hash_map>
+#include <vector>
-#include "context/cdhashmap.h"
#include "bitblast_strategies_template.h"
+#include "context/cdhashmap.h"
+#include "expr/node.h"
#include "expr/resource_manager.h"
#include "prop/sat_solver.h"
-#include "theory/valuation.h"
+#include "smt/smt_globals.h"
#include "theory/theory_registrar.h"
+#include "theory/valuation.h"
class Abc_Obj_t_;
typedef Abc_Obj_t_ Abc_Obj_t;
// caches and mappings
TermDefMap d_termCache;
ModelCache d_modelCache;
-
+
void initAtomBBStrategies();
void initTermBBStrategies();
protected:
/// function tables for the various bitblasting strategies indexed by node kind
TermBBStrategy d_termBBStrategies[kind::LAST_KIND];
- AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND];
- virtual Node getModelFromSatSolver(TNode node, bool fullModel) = 0;
+ AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND];
+ virtual Node getModelFromSatSolver(TNode node, bool fullModel) = 0;
public:
- TBitblaster();
+ TBitblaster();
virtual ~TBitblaster() {}
- virtual void bbAtom(TNode node) = 0;
+ virtual void bbAtom(TNode node) = 0;
virtual void bbTerm(TNode node, Bits& bits) = 0;
virtual void makeVariable(TNode node, Bits& bits) = 0;
virtual T getBBAtom(TNode atom) const = 0;
virtual bool hasBBAtom(TNode atom) const = 0;
virtual void storeBBAtom(TNode atom, T atom_bb) = 0;
-
-
+
+
bool hasBBTerm(TNode node) const;
void getBBTerm(TNode node, Bits& bits) const;
void storeBBTerm(TNode term, const Bits& bits);
*/
Node getTermModel(TNode node, bool fullModel);
void invalidateModelCache();
-};
+};
-class TheoryBV;
+class TheoryBV;
class TLazyBitblaster : public TBitblaster<Node> {
typedef std::vector<Node> Bits;
class MinisatNotify : public prop::BVSatSolverInterface::Notify {
prop::CnfStream* d_cnf;
TheoryBV *d_bv;
- TLazyBitblaster* d_lazyBB;
+ TLazyBitblaster* d_lazyBB;
public:
MinisatNotify(prop::CnfStream* cnf, TheoryBV *bv, TLazyBitblaster* lbv)
: d_cnf(cnf)
, d_bv(bv)
, d_lazyBB(lbv)
{}
+
bool notify(prop::SatLiteral lit);
void notify(prop::SatClause& clause);
void spendResource(unsigned ammount);
void safePoint(unsigned ammount);
};
-
+
TheoryBV *d_bv;
context::Context* d_ctx;
ExplanationMap* d_explanations; /**< context dependent list of explanations for the propagated literals.
Only used when bvEagerPropagate option enabled. */
TNodeSet d_variables;
- TNodeSet d_bbAtoms;
+ TNodeSet d_bbAtoms;
AbstractionModule* d_abstraction;
bool d_emptyNotify;
context::CDO<bool> d_satSolverFullModel;
-
+
void addAtom(TNode atom);
bool hasValue(TNode a);
- Node getModelFromSatSolver(TNode a, bool fullModel);
+ Node getModelFromSatSolver(TNode a, bool fullModel);
+
public:
void bbTerm(TNode node, Bits& bits);
void bbAtom(TNode node);
Node getBBAtom(TNode atom) const;
void storeBBAtom(TNode atom, Node atom_bb);
- bool hasBBAtom(TNode atom) const;
+ bool hasBBAtom(TNode atom) const;
TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name="", bool emptyNotify = false);
~TLazyBitblaster() throw();
- /**
+ /**
* Pushes the assumption literal associated with node to the SAT
* solver assumption queue.
*
TNodeSet d_variables;
Node getModelFromSatSolver(TNode a, bool fullModel);
- bool isSharedTerm(TNode node);
+ bool isSharedTerm(TNode node);
public:
+ EagerBitblaster(theory::bv::TheoryBV* theory_bv);
+ ~EagerBitblaster();
+
void addAtom(TNode atom);
void makeVariable(TNode node, Bits& bits);
void bbTerm(TNode node, Bits& bits);
void bbAtom(TNode node);
Node getBBAtom(TNode node) const;
- bool hasBBAtom(TNode atom) const;
+ bool hasBBAtom(TNode atom) const;
void bbFormula(TNode formula);
void storeBBAtom(TNode atom, Node atom_bb);
- EagerBitblaster(theory::bv::TheoryBV* theory_bv);
- ~EagerBitblaster();
bool assertToSat(TNode node, bool propagate = true);
bool solve();
void collectModelInfo(TheoryModel* m, bool fullModel);
};
class BitblastingRegistrar: public prop::Registrar {
- EagerBitblaster* d_bitblaster;
+ EagerBitblaster* d_bitblaster;
public:
BitblastingRegistrar(EagerBitblaster* bb)
: d_bitblaster(bb)
* BitblastSolver
*/
class EagerBitblastSolver {
- typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AssertionSet;
+ typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AssertionSet;
AssertionSet d_assertionSet;
/** Bitblasters */
EagerBitblaster* d_bitblaster;
AigBitblaster* d_aigBitblaster;
bool d_useAig;
- TheoryBV* d_bv;
+ TheoryBV* d_bv;
+
public:
- EagerBitblastSolver(theory::bv::TheoryBV* bv);
+ EagerBitblastSolver(theory::bv::TheoryBV* bv);
~EagerBitblastSolver();
bool checkSat();
void assertFormula(TNode formula);
namespace bv {
-class TLazyBitblaster;
+class TLazyBitblaster;
class TheoryBV;
class BVQuickCheck {
#pragma once
-#include "theory/bv/bv_subtheory.h"
#include "theory/bv/bitblaster_template.h"
+#include "theory/bv/bv_subtheory.h"
namespace CVC4 {
namespace theory {
BVQuickCheck* d_quickCheck;
QuickXPlain* d_quickXplain;
// Node getModelValueRec(TNode node);
- void setConflict(TNode conflict);
+ void setConflict(TNode conflict);
public:
BitblastSolver(context::Context* c, TheoryBV* bv);
~BitblastSolver();
d_nullContext = new context::Context();
d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, "EagerBitblaster");
- d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar, d_nullContext);
+ d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar,
+ d_nullContext, d_bv->globals());
MinisatEmptyNotify* notify = new MinisatEmptyNotify();
d_satSolver->setNotify(notify);
#include "theory/theory_model.h"
#include "theory_bv_utils.h"
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::bv;
+namespace CVC4 {
+namespace theory {
+namespace bv {
-TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name, bool emptyNotify)
+TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv,
+ const std::string name, bool emptyNotify)
: TBitblaster<Node>()
, d_bv(bv)
, d_ctx(c)
, d_satSolverFullModel(c, false)
, d_name(name)
, d_statistics(name) {
+
d_satSolver = prop::SatSolverFactory::createMinisat(c, name);
d_nullRegistrar = new prop::NullRegistrar();
d_nullContext = new context::Context();
- d_cnfStream = new prop::TseitinCnfStream(d_satSolver,
- d_nullRegistrar,
- d_nullContext);
-
+ d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar,
+ d_nullContext, d_bv->globals());
+
d_satSolverNotify = d_emptyNotify ?
(prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() :
(prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, bv, this);
}
void TLazyBitblaster::setAbstraction(AbstractionModule* abs) {
- d_abstraction = abs;
+ d_abstraction = abs;
}
TLazyBitblaster::~TLazyBitblaster() throw() {
if (expansion.getKind() == kind::CONST_BOOLEAN) {
atom_bb = expansion;
} else {
- Assert (expansion.getKind() == kind::AND);
- std::vector<Node> atoms;
+ Assert (expansion.getKind() == kind::AND);
+ std::vector<Node> atoms;
for (unsigned i = 0; i < expansion.getNumChildren(); ++i) {
Node normalized_i = Rewriter::rewrite(expansion[i]);
Node atom_i = normalized_i.getKind() != kind::CONST_BOOLEAN ?
}
void TLazyBitblaster::clearSolver() {
- Assert (d_ctx->getLevel() == 0);
+ Assert (d_ctx->getLevel() == 0);
delete d_satSolver;
delete d_satSolverNotify;
delete d_cnfStream;
d_bbAtoms.clear();
d_variables.clear();
d_termCache.clear();
-
- invalidateModelCache();
+
+ invalidateModelCache();
// recreate sat solver
d_satSolver = prop::SatSolverFactory::createMinisat(d_ctx);
- d_cnfStream = new prop::TseitinCnfStream(d_satSolver,
- d_nullRegistrar,
- d_nullContext);
+ d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar,
+ d_nullContext, d_bv->globals());
d_satSolverNotify = d_emptyNotify ?
(prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() :
(prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, d_bv, this);
d_satSolver->setNotify(d_satSolverNotify);
}
+
+} /* namespace CVC4::theory::bv */
+} /* namespace CVC4::theory */
+} /* namespace CVC4 */
#include "theory/theory_model.h"
#include "theory/valuation.h"
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::bv;
using namespace CVC4::context;
-
-using namespace std;
using namespace CVC4::theory::bv::utils;
+using namespace std;
-TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo)
- : Theory(THEORY_BV, c, u, out, valuation, logicInfo),
- d_context(c),
- d_alreadyPropagatedSet(c),
- d_sharedTermsSet(c),
- d_subtheories(),
- d_subtheoryMap(),
- d_statistics(),
- d_staticLearnCache(),
- d_lemmasAdded(c, false),
- d_conflict(c, false),
- d_invalidateModelCache(c, true),
- d_literalsToPropagate(c),
- d_literalsToPropagateIndex(c, 0),
- d_propagatedBy(c),
- d_eagerSolver(NULL),
- d_abstractionModule(new AbstractionModule()),
- d_isCoreTheory(false),
- d_calledPreregister(false)
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+TheoryBV::TheoryBV(context::Context* c, context::UserContext* u,
+ OutputChannel& out, Valuation valuation,
+ const LogicInfo& logicInfo, SmtGlobals* globals)
+ : Theory(THEORY_BV, c, u, out, valuation, logicInfo, globals),
+ d_context(c),
+ d_alreadyPropagatedSet(c),
+ d_sharedTermsSet(c),
+ d_subtheories(),
+ d_subtheoryMap(),
+ d_statistics(),
+ d_staticLearnCache(),
+ d_lemmasAdded(c, false),
+ d_conflict(c, false),
+ d_invalidateModelCache(c, true),
+ d_literalsToPropagate(c),
+ d_literalsToPropagateIndex(c, 0),
+ d_propagatedBy(c),
+ d_eagerSolver(NULL),
+ d_abstractionModule(new AbstractionModule()),
+ d_isCoreTheory(false),
+ d_calledPreregister(false)
{
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
d_eagerSolver = new EagerBitblastSolver(this);
- return;
+ return;
}
if (options::bitvectorEqualitySolver()) {
d_subtheories.push_back(core_solver);
d_subtheoryMap[SUB_CORE] = core_solver;
}
-
+
if (options::bitvectorInequalitySolver()) {
SubtheorySolver* ineq_solver = new InequalitySolver(c, this);
d_subtheories.push_back(ineq_solver);
void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
- return;
+ return;
}
if (options::bitvectorEqualitySolver()) {
dynamic_cast<CoreSolver*>(d_subtheoryMap[SUB_CORE])->setMasterEqualityEngine(eq);
d_BVDivByZeroAckerman[size] = TNodeSet();
}
d_BVDivByZeroAckerman[size].insert(term[0]);
- seen.insert(term);
+ seen.insert(term);
} else if (term.getKind() == kind::BITVECTOR_ACKERMANIZE_UREM) {
unsigned size = utils::getSize(term[0]);
if (d_BVRemByZeroAckerman.find(size) == d_BVRemByZeroAckerman.end()) {
d_BVRemByZeroAckerman[size] = TNodeSet();
}
d_BVRemByZeroAckerman[size].insert(term[0]);
- seen.insert(term);
+ seen.insert(term);
}
for (unsigned i = 0; i < term.getNumChildren(); ++i) {
- collectNumerators(term[i], seen);
+ collectNumerators(term[i], seen);
}
- seen.insert(term);
+ seen.insert(term);
}
void TheoryBV::mkAckermanizationAsssertions(std::vector<Node>& assertions) {
Debug("bv-ackermanize") << "TheoryBV::mkAckermanizationAsssertions\n";
-
+
Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER);
AlwaysAssert(!options::incrementalSolving());
- TNodeSet seen;
+ TNodeSet seen;
for (unsigned i = 0; i < assertions.size(); ++i) {
- collectNumerators(assertions[i], seen);
+ collectNumerators(assertions[i], seen);
}
-
+
// process division UF
Debug("bv-ackermanize") << "Process division UF...\n";
for (WidthToNumerators::const_iterator it = d_BVDivByZeroAckerman.begin(); it != d_BVDivByZeroAckerman.end(); ++it) {
TNode arg1 = *i;
TNode arg2 = *j;
TNode acker1 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UDIV, arg1);
- TNode acker2 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UDIV, arg2);
+ TNode acker2 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UDIV, arg2);
Node arg_eq = utils::mkNode(kind::EQUAL, arg1, arg2);
Node acker_eq = utils::mkNode(kind::EQUAL, acker1, acker2);
Node lemma = utils::mkNode(kind::IMPLIES, arg_eq, acker_eq);
Debug("bv-ackermanize") << " " << lemma << "\n";
- assertions.push_back(lemma);
+ assertions.push_back(lemma);
}
}
}
TNode arg1 = *i;
TNode arg2 = *j;
TNode acker1 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UREM, arg1);
- TNode acker2 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UREM, arg2);
+ TNode acker2 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UREM, arg2);
Node arg_eq = utils::mkNode(kind::EQUAL, arg1, arg2);
Node acker_eq = utils::mkNode(kind::EQUAL, acker1, acker2);
Node lemma = utils::mkNode(kind::IMPLIES, arg_eq, acker_eq);
Debug("bv-ackermanize") << " " << lemma << "\n";
- assertions.push_back(lemma);
+ assertions.push_back(lemma);
}
}
}
if (options::bitvectorDivByZeroConst()) {
Kind kind = node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL : kind::BITVECTOR_UREM_TOTAL;
- return nm->mkNode(kind, node[0], node[1]);
+ return nm->mkNode(kind, node[0], node[1]);
}
TNode num = node[0], den = node[1];
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
// Ackermanize UF if using eager bit-blasting
- Node ackerman_var = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_ACKERMANIZE_UDIV : kind::BITVECTOR_ACKERMANIZE_UREM, num);
+ Node ackerman_var = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_ACKERMANIZE_UDIV : kind::BITVECTOR_ACKERMANIZE_UREM, num);
node = nm->mkNode(kind::ITE, den_eq_0, ackerman_var, divTotalNumDen);
- return node;
+ return node;
} else {
Node divByZero = getBVDivByZero(node.getKind(), width);
Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num);
void TheoryBV::preRegisterTerm(TNode node) {
d_calledPreregister = true;
Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
-
+
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
// the aig bit-blaster option is set heuristically
// if bv abstraction is not used
}
if (node.getKind() == kind::BITVECTOR_EAGER_ATOM) {
- Node formula = node[0];
+ Node formula = node[0];
d_eagerSolver->assertFormula(formula);
}
// nothing to do for the other terms
- return;
+ return;
}
-
+
for (unsigned i = 0; i < d_subtheories.size(); ++i) {
d_subtheories[i]->preRegister(node);
}
Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer);
// we may be getting new assertions so the model cache may not be sound
- d_invalidateModelCache.set(true);
+ d_invalidateModelCache.set(true);
// if we are using the eager solver
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
// this can only happen on an empty benchmark
if (!Theory::fullEffort(e))
return;
- std::vector<TNode> assertions;
+ std::vector<TNode> assertions;
while (!done()) {
TNode fact = get().assertion;
Assert (fact.getKind() == kind::BITVECTOR_EAGER_ATOM);
- assertions.push_back(fact);
+ assertions.push_back(fact);
}
- Assert (d_eagerSolver->hasAssertions(assertions));
-
+ Assert (d_eagerSolver->hasAssertions(assertions));
+
bool ok = d_eagerSolver->checkSat();
if (!ok) {
if (assertions.size() == 1) {
d_out->conflict(assertions[0]);
- return;
+ return;
}
Node conflict = NodeManager::currentNM()->mkNode(kind::AND, assertions);
d_out->conflict(conflict);
- return;
+ return;
}
return;
}
-
-
+
+
if (Theory::fullEffort(e)) {
++(d_statistics.d_numCallsToCheckFullEffort);
} else {
void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){
Assert(!inConflict());
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
- d_eagerSolver->collectModelInfo(m, fullModel);
+ d_eagerSolver->collectModelInfo(m, fullModel);
}
for (unsigned i = 0; i < d_subtheories.size(); ++i) {
if (d_subtheories[i]->isComplete()) {
void TheoryBV::propagate(Effort e) {
Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl;
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
- return;
+ return;
}
if (inConflict()) {
outSubstitutions.addSubstitution(in[1], in[0]);
return PP_ASSERT_STATUS_SOLVED;
}
- Node node = Rewriter::rewrite(in);
+ Node node = Rewriter::rewrite(in);
if ((node[0].getKind() == kind::BITVECTOR_EXTRACT && node[1].isConst()) ||
(node[1].getKind() == kind::BITVECTOR_EXTRACT && node[0].isConst())) {
Node extract = node[0].isConst() ? node[1] : node[0];
if (extract[0].getKind() == kind::VARIABLE) {
Node c = node[0].isConst() ? node[0] : node[1];
-
+
unsigned high = utils::getExtractHigh(extract);
unsigned low = utils::getExtractLow(extract);
unsigned var_bitwidth = utils::getSize(extract[0]);
std::vector<Node> children;
-
+
if (low == 0) {
Assert (high != var_bitwidth - 1);
unsigned skolem_size = var_bitwidth - high - 1;
Node skolem = utils::mkVar(skolem_size);
- children.push_back(skolem);
+ children.push_back(skolem);
children.push_back(c);
} else if (high == var_bitwidth - 1) {
unsigned skolem_size = low;
Node skolem = utils::mkVar(skolem_size);
children.push_back(c);
- children.push_back(skolem);
+ children.push_back(skolem);
} else {
unsigned skolem1_size = low;
unsigned skolem2_size = var_bitwidth - high - 1;
children.push_back(skolem1);
}
Node concat = utils::mkNode(kind::BITVECTOR_CONCAT, children);
- Assert (utils::getSize(concat) == utils::getSize(extract[0]));
+ Assert (utils::getSize(concat) == utils::getSize(extract[0]));
outSubstitutions.addSubstitution(extract[0], concat);
return PP_ASSERT_STATUS_SOLVED;
}
case kind::BITVECTOR_SLT:
case kind::BITVECTOR_ULE:
case kind::BITVECTOR_SLE:
-
+
default:
// TODO other predicates
break;
Node TheoryBV::ppRewrite(TNode t)
{
- Debug("bv-pp-rewrite") << "TheoryBV::ppRewrite " << t << "\n";
+ Debug("bv-pp-rewrite") << "TheoryBV::ppRewrite " << t << "\n";
Node res = t;
if (RewriteRule<BitwiseEq>::applies(t)) {
Node result = RewriteRule<BitwiseEq>::run<false>(t);
} else {
res = t;
}
- }
-
+ }
+
// if(t.getKind() == kind::EQUAL &&
// ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() == kind::BITVECTOR_PLUS) ||
// return new_eq;
// }
// }
-
+
// if (new_eq.getKind() == kind::CONST_BOOLEAN) {
// ++(d_statistics.d_numMultSlice);
// return new_eq;
// }
// }
// }
-
+
if (options::bvAbstraction() && t.getType().isBoolean()) {
- d_abstractionModule->addInputAtom(res);
+ d_abstractionModule->addInputAtom(res);
}
- Debug("bv-pp-rewrite") << "to " << res << "\n";
+ Debug("bv-pp-rewrite") << "to " << res << "\n";
return res;
}
Debug("bitvector") << "TheoryBV::presolve" << endl;
}
-static int prop_count = 0;
+static int prop_count = 0;
bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
{
Debug("bitvector::propagate") << indent() << getSatContext()->getLevel() << " " << "TheoryBV::storePropagation(" << literal << ", " << subtheory << ")" << std::endl;
- prop_count++;
-
+ prop_count++;
+
// If already in conflict, no more propagation
if (d_conflict) {
Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << "): already in conflict" << std::endl;
EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
{
- Assert (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY);
+ Assert (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY);
for (unsigned i = 0; i < d_subtheories.size(); ++i) {
EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b);
if (status != EQUALITY_UNKNOWN) {
d_isCoreTheory = true;
if (d_subtheoryMap.find(SUB_CORE) != d_subtheoryMap.end()) {
CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
- core->enableSlicer();
+ core->enableSlicer();
}
}
return;
}
d_staticLearnCache.insert(in);
-
+
if (in.getKind() == kind::EQUAL) {
if((in[0].getKind() == kind::BITVECTOR_PLUS && in[1].getKind() == kind::BITVECTOR_SHL) ||
(in[1].getKind() == kind::BITVECTOR_PLUS && in[0].getKind() == kind::BITVECTOR_SHL)) {
TNode s = in[0].getKind() == kind::BITVECTOR_PLUS ? in[1] : in[0];
if(p.getNumChildren() == 2
- && p[0].getKind() == kind::BITVECTOR_SHL
+ && p[0].getKind() == kind::BITVECTOR_SHL
&& p[1].getKind() == kind::BITVECTOR_SHL ){
unsigned size = utils::getSize(s);
Node one = utils::mkConst(size, 1u);
void TheoryBV::setConflict(Node conflict) {
if (options::bvAbstraction()) {
Node new_conflict = d_abstractionModule->simplifyConflict(conflict);
-
+
std::vector<Node> lemmas;
- lemmas.push_back(new_conflict);
+ lemmas.push_back(new_conflict);
d_abstractionModule->generalizeConflict(new_conflict, lemmas);
for (unsigned i = 0; i < lemmas.size(); ++i) {
- lemma(utils::mkNode(kind::NOT, lemmas[i]));
+ lemma(utils::mkNode(kind::NOT, lemmas[i]));
}
}
d_conflict = true;
d_conflictNode = conflict;
}
+
+} /* namespace CVC4::theory::bv */
+} /* namespace CVC4::theory */
+} /* namespace CVC4 */
#include "context/cdlist.h"
#include "context/context.h"
#include "expr/statistics_registry.h"
+#include "smt/smt_globals.h"
#include "theory/bv/bv_subtheory.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/theory.h"
class CoreSolver;
class InequalitySolver;
class AlgebraicSolver;
-class BitblastSolver;
+class BitblastSolver;
class EagerBitblastSolver;
-
+
class AbstractionModule;
class TheoryBV : public Theory {
/** Context dependent set of atoms we already propagated */
context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet;
context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet;
-
- std::vector<SubtheorySolver*> d_subtheories;
- __gnu_cxx::hash_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap;
+ std::vector<SubtheorySolver*> d_subtheories;
+ __gnu_cxx::hash_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap;
public:
- TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
+ TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, SmtGlobals* globals);
+
~TheoryBV();
void setMasterEqualityEngine(eq::EqualityEngine* eq);
PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
void enableCoreTheorySlicer();
-
+
Node ppRewrite(TNode t);
void ppStaticLearn(TNode in, NodeBuilder<>& learned);
-
+
void presolve();
- bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
+ bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
+
private:
class Statistics {
#include "theory/type_enumerator.h"
#include "theory/valuation.h"
-
using namespace std;
-using namespace CVC4;
using namespace CVC4::kind;
using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::datatypes;
-
-
-TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
- Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo),
- //d_cycle_check(c),
- d_hasSeenCycle(c, false),
- d_infer(c),
- d_infer_exp(c),
- d_notify( *this ),
- d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes", true),
- d_labels( c ),
- d_selector_apps( c ),
- //d_consEqc( c ),
- d_conflict( c, false ),
- d_collectTermsCache( c ),
- d_consTerms( c ),
- d_selTerms( c ),
- d_singleton_eq( u ){
+namespace CVC4 {
+namespace theory {
+namespace datatypes {
+
+TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo,
+ SmtGlobals* globals)
+ : Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo, globals),
+ //d_cycle_check(c),
+ d_hasSeenCycle(c, false),
+ d_infer(c),
+ d_infer_exp(c),
+ d_notify( *this ),
+ d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes", true),
+ d_labels( c ),
+ d_selector_apps( c ),
+ //d_consEqc( c ),
+ d_conflict( c, false ),
+ d_collectTermsCache( c ),
+ d_consTerms( c ),
+ d_selTerms( c ),
+ d_singleton_eq( u )
+{
// The kinds we are treating as function application in congruence
d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR);
d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
}
return false;
}
+
+} /* namepsace CVC4::theory::datatypes */
+} /* namepsace CVC4::theory */
+} /* namepsace CVC4 */
/** sygus utilities */
SygusSplit * d_sygus_split;
SygusSymBreak * d_sygus_sym_break;
+
private:
/** singleton lemmas (for degenerate co-datatype case) */
std::map< TypeNode, Node > d_singleton_lemma[2];
+
/** Cache for singleton equalities processed */
BoolMap d_singleton_eq;
-private:
+
/** assert fact */
void assertFact( Node fact, Node exp );
+
/** flush pending facts */
void flushPendingFacts();
+
/** do pending merged */
void doPendingMerges();
+
/** get or make eqc info */
EqcInfo* getOrMakeEqcInfo( TNode n, bool doMake = false );
+
/** has eqc info */
bool hasEqcInfo( TNode n ) { return d_labels.find( n )!=d_labels.end(); }
+
/** get eqc constructor */
TNode getEqcConstructor( TNode r );
+
protected:
/** compute care graph */
void computeCareGraph();
+
public:
TheoryDatatypes(context::Context* c, context::UserContext* u,
OutputChannel& out, Valuation valuation,
- const LogicInfo& logicInfo);
+ const LogicInfo& logicInfo, SmtGlobals* globals);
~TheoryDatatypes();
void setMasterEqualityEngine(eq::EqualityEngine* eq);
/** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
-TheoryFp::TheoryFp(context::Context* c,
- context::UserContext* u,
- OutputChannel& out,
- Valuation valuation,
- const LogicInfo& logicInfo) :
- Theory(THEORY_FP, c, u, out, valuation, logicInfo) {
-}/* TheoryFp::TheoryFp() */
+TheoryFp::TheoryFp(context::Context* c, context::UserContext* u,
+ OutputChannel& out, Valuation valuation,
+ const LogicInfo& logicInfo, SmtGlobals* globals)
+ : Theory(THEORY_FP, c, u, out, valuation, logicInfo, globals)
+{}/* TheoryFp::TheoryFp() */
Node TheoryFp::expandDefinition(LogicRequest &, Node node) {
/** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
TheoryFp(context::Context* c,
- context::UserContext* u,
- OutputChannel& out,
- Valuation valuation,
- const LogicInfo& logicInfo);
+ context::UserContext* u,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo,
+ SmtGlobals* globals);
Node expandDefinition(LogicRequest &, Node node);
using namespace std;
-using namespace CVC4;
-using namespace theory;
-using namespace idl;
-
-TheoryIdl::TheoryIdl(context::Context* c, context::UserContext* u, OutputChannel& out,
- Valuation valuation, const LogicInfo& logicInfo)
-: Theory(THEORY_ARITH, c, u, out, valuation, logicInfo)
-, d_model(c)
-, d_assertionsDB(c)
+namespace CVC4 {
+namespace theory {
+namespace idl {
+
+TheoryIdl::TheoryIdl(context::Context* c, context::UserContext* u,
+ OutputChannel& out, Valuation valuation,
+ const LogicInfo& logicInfo, SmtGlobals* globals)
+ : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, globals)
+ , d_model(c)
+ , d_assertionsDB(c)
{}
Node TheoryIdl::ppRewrite(TNode atom) {
// Everything fine, no conflict
return true;
}
+
+} /* namepsace CVC4::theory::idl */
+} /* namepsace CVC4::theory */
+} /* namepsace CVC4 */
/** Theory constructor. */
TheoryIdl(context::Context* c, context::UserContext* u, OutputChannel& out,
- Valuation valuation, const LogicInfo& logicInfo);
+ Valuation valuation, const LogicInfo& logicInfo,
+ SmtGlobals* globals);
/** Pre-processing of input atoms */
Node ppRewrite(TNode atom);
* With safePoint(), the theory signals that it is at a safe point
* and can be interrupted.
*/
- virtual void safePoint(uint64_t ammount) throw(Interrupted, UnsafeInterruptException, AssertionException) {
- }
+ virtual void safePoint(uint64_t amount)
+ throw(Interrupted, UnsafeInterruptException, AssertionException)
+ {}
/**
* Indicate a theory conflict has arisen.
using namespace CVC4::theory;
using namespace CVC4::theory::quantifiers;
-TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
- Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo),
+TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, SmtGlobals* globals) :
+ Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, globals),
d_masterEqualityEngine(0)
{
d_numInstantiations = 0;
int d_baseDecLevel;
eq::EqualityEngine* d_masterEqualityEngine;
+
private:
- void computeCareGraph();
+ void computeCareGraph();
+
public:
- TheoryQuantifiers(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
+ TheoryQuantifiers(context::Context* c, context::UserContext* u,
+ OutputChannel& out, Valuation valuation,
+ const LogicInfo& logicInfo, SmtGlobals* globals);
~TheoryQuantifiers();
void setMasterEqualityEngine(eq::EqualityEngine* eq);
context::UserContext* u,
OutputChannel& out,
Valuation valuation,
- const LogicInfo& logicInfo) :
- Theory(THEORY_SETS, c, u, out, valuation, logicInfo),
- d_internal(new TheorySetsPrivate(*this, c, u)) {
-}
+ const LogicInfo& logicInfo,
+ SmtGlobals* globals)
+ : Theory(THEORY_SETS, c, u, out, valuation, logicInfo, globals),
+ d_internal(new TheorySetsPrivate(*this, c, u))
+{}
TheorySets::~TheorySets() {
delete d_internal;
* Constructs a new instance of TheorySets w.r.t. the provided
* contexts.
*/
- TheorySets(context::Context* c,
- context::UserContext* u,
- OutputChannel& out,
- Valuation valuation,
- const LogicInfo& logicInfo);
+ TheorySets(context::Context* c, context::UserContext* u, OutputChannel& out,
+ Valuation valuation, const LogicInfo& logicInfo,
+ SmtGlobals* globals);
~TheorySets();
#include <boost/foreach.hpp>
#include "expr/emptyset.h"
-#include "expr/result.h"
#include "options/sets_options.h"
#include "theory/sets/expr_patterns.h" // ONLY included here
#include "theory/sets/scrutinize.h"
#include "theory/sets/theory_sets.h"
#include "theory/theory_model.h"
+#include "util/result.h"
using namespace std;
using namespace CVC4::expr::pattern;
}
-TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo)
- : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo),
- RMAXINT(LONG_MAX),
- d_notify( *this ),
- d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings", true),
- d_conflict(c, false),
- d_infer(c),
- d_infer_exp(c),
- d_nf_pairs(c),
- d_loop_antec(u),
- d_length_intro_vars(u),
- d_pregistered_terms_cache(u),
- d_registered_terms_cache(u),
- d_preproc(u),
- d_preproc_cache(u),
- d_extf_infer_cache(c),
- d_congruent(c),
- d_proxy_var(u),
- d_proxy_var_to_length(u),
- d_neg_ctn_eqlen(c),
- d_neg_ctn_ulen(c),
- d_neg_ctn_cached(u),
- d_ext_func_terms(c),
- d_regexp_memberships(c),
- d_regexp_ucached(u),
- d_regexp_ccached(c),
- d_pos_memberships(c),
- d_neg_memberships(c),
- d_inter_cache(c),
- d_inter_index(c),
- d_processed_memberships(c),
- d_regexp_ant(c),
- d_input_vars(u),
- d_input_var_lsum(u),
- d_cardinality_lits(u),
- d_curr_cardinality(c, 0)
+TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u,
+ OutputChannel& out, Valuation valuation,
+ const LogicInfo& logicInfo, SmtGlobals* globals)
+ : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo, globals),
+ RMAXINT(LONG_MAX),
+ d_notify( *this ),
+ d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings", true),
+ d_conflict(c, false),
+ d_infer(c),
+ d_infer_exp(c),
+ d_nf_pairs(c),
+ d_loop_antec(u),
+ d_length_intro_vars(u),
+ d_pregistered_terms_cache(u),
+ d_registered_terms_cache(u),
+ d_preproc(u),
+ d_preproc_cache(u),
+ d_extf_infer_cache(c),
+ d_congruent(c),
+ d_proxy_var(u),
+ d_proxy_var_to_length(u),
+ d_neg_ctn_eqlen(c),
+ d_neg_ctn_ulen(c),
+ d_neg_ctn_cached(u),
+ d_ext_func_terms(c),
+ d_regexp_memberships(c),
+ d_regexp_ucached(u),
+ d_regexp_ccached(c),
+ d_pos_memberships(c),
+ d_neg_memberships(c),
+ d_inter_cache(c),
+ d_inter_index(c),
+ d_processed_memberships(c),
+ d_regexp_ant(c),
+ d_input_vars(u),
+ d_input_var_lsum(u),
+ d_cardinality_lits(u),
+ d_curr_cardinality(c, 0)
{
// The kinds we are treating as function application in congruence
d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP);
typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
public:
- TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
+ TheoryStrings(context::Context* c, context::UserContext* u,
+ OutputChannel& out, Valuation valuation,
+ const LogicInfo& logicInfo, SmtGlobals* globals);
~TheoryStrings();
void setMasterEqualityEngine(eq::EqualityEngine* eq);
#include "options/theory_options.h"
#include "options/theoryof_mode.h"
#include "smt/logic_request.h"
+#include "smt/smt_globals.h"
#include "smt_util/command.h"
#include "smt_util/dump.h"
#include "theory/logic_info.h"
* Construct a Theory.
*/
Theory(TheoryId id, context::Context* satContext, context::UserContext* userContext,
- OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) throw()
+ OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo,
+ SmtGlobals* globals) throw()
: d_id(id)
, d_satContext(satContext)
, d_userContext(userContext)
, d_out(&out)
, d_valuation(valuation)
, d_proofEnabled(false)
+ , d_globals(globals)
{
StatisticsRegistry::registerStat(&d_checkTime);
StatisticsRegistry::registerStat(&d_computeCareGraphTime);
*/
bool d_proofEnabled;
+ SmtGlobals* d_globals;
+
public:
/**
*/
virtual std::pair<bool, Node> entailmentCheck(TNode lit, const EntailmentCheckParameters* params = NULL, EntailmentCheckSideEffects* out = NULL);
+
+ /** Returns a pointer to the globals copy the theory is using. */
+ SmtGlobals* globals() { return d_globals; }
+
};/* class Theory */
std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level);
TheoryEngine::TheoryEngine(context::Context* context,
context::UserContext* userContext,
RemoveITE& iteRemover,
- const LogicInfo& logicInfo)
+ const LogicInfo& logicInfo,
+ SmtGlobals* globals)
: d_propEngine(NULL),
d_decisionEngine(NULL),
d_context(context),
d_false(),
d_interrupted(false),
d_resourceManager(NodeManager::currentResourceManager()),
+ d_globals(globals),
d_inPreregister(false),
d_factsAsserted(context, false),
d_preRegistrationVisitor(this, context),
}
// Share with other portfolio threads
- if(options::lemmaOutputChannel() != NULL) {
- options::lemmaOutputChannel()->notifyNewLemma(node.toExpr());
+ if(d_globals->getLemmaOutputChannel() != NULL) {
+ d_globals->getLemmaOutputChannel()->notifyNewLemma(node.toExpr());
}
// Run theory preprocessing, maybe
#include "options/options.h"
#include "options/smt_options.h"
#include "prop/prop_engine.h"
+#include "smt/smt_globals.h"
#include "smt_util/command.h"
#include "theory/atom_requests.h"
#include "theory/bv/bv_to_bool.h"
*/
context::CDHashSet<Node, NodeHashFunction> d_hasPropagated;
+
/**
* Statistics for a particular theory.
*/
bool d_interrupted;
ResourceManager* d_resourceManager;
+ /** Container for misc. globals. */
+ SmtGlobals* d_globals;
+
public:
/** Constructs a theory engine */
- TheoryEngine(context::Context* context, context::UserContext* userContext, RemoveITE& iteRemover, const LogicInfo& logic);
+ TheoryEngine(context::Context* context, context::UserContext* userContext,
+ RemoveITE& iteRemover, const LogicInfo& logic, SmtGlobals* globals);
/** Destroys a theory engine */
~TheoryEngine();
inline void addTheory(theory::TheoryId theoryId) {
Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL);
d_theoryOut[theoryId] = new EngineOutputChannel(this, theoryId);
- d_theoryTable[theoryId] = new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId], theory::Valuation(this), d_logicInfo);
+ d_theoryTable[theoryId] =
+ new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId],
+ theory::Valuation(this), d_logicInfo, d_globals);
}
inline void setPropEngine(prop::PropEngine* propEngine) {
using namespace CVC4::theory::uf;
/** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
-TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
- Theory(THEORY_UF, c, u, out, valuation, logicInfo),
- d_notify(*this),
- /* The strong theory solver can be notified by EqualityEngine::init(),
- * so make sure it's initialized first. */
- d_thss(NULL),
- d_equalityEngine(d_notify, c, "theory::uf::TheoryUF", true),
- d_conflict(c, false),
- d_literalsToPropagate(c),
- d_literalsToPropagateIndex(c, 0),
- d_functionsTerms(c),
- d_symb(u)
+TheoryUF::TheoryUF(context::Context* c, context::UserContext* u,
+ OutputChannel& out, Valuation valuation,
+ const LogicInfo& logicInfo, SmtGlobals* globals)
+ : Theory(THEORY_UF, c, u, out, valuation, logicInfo, globals),
+ d_notify(*this),
+ /* The strong theory solver can be notified by EqualityEngine::init(),
+ * so make sure it's initialized first. */
+ d_thss(NULL),
+ d_equalityEngine(d_notify, c, "theory::uf::TheoryUF", true),
+ d_conflict(c, false),
+ d_literalsToPropagate(c),
+ d_literalsToPropagateIndex(c, 0),
+ d_functionsTerms(c),
+ d_symb(u)
{
// The kinds we are treating as function application in congruence
d_equalityEngine.addFunctionKind(kind::APPLY_UF);
public:
/** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
- TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
+ TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out,
+ Valuation valuation, const LogicInfo& logicInfo,
+ SmtGlobals* globals);
~TheoryUF();
proof.h \
regexp.cpp \
regexp.h \
+ result.cpp \
+ result.h \
smt2_quote_string.cpp \
smt2_quote_string.h \
subrange_bound.cpp \
rational_gmp_imp.cpp \
rational_gmp_imp.h \
regexp.i \
+ result.i \
subrange_bound.i \
tuple.i \
unsafe_interrupt_exception.i
--- /dev/null
+/********************* */
+/*! \file result.cpp
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Encapsulation of the result of a query.
+ **
+ ** Encapsulation of the result of a query.
+ **/
+#include "util/result.h"
+
+#include <algorithm>
+#include <cctype>
+#include <iostream>
+#include <string>
+
+#include "base/cvc4_assert.h"
+#include "options/set_language.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+Result::Result()
+ : d_sat(SAT_UNKNOWN)
+ , d_validity(VALIDITY_UNKNOWN)
+ , d_which(TYPE_NONE)
+ , d_unknownExplanation(UNKNOWN_REASON)
+ , d_inputName("")
+{ }
+
+
+Result::Result(enum Sat s, std::string inputName)
+ : d_sat(s)
+ , d_validity(VALIDITY_UNKNOWN)
+ , d_which(TYPE_SAT)
+ , d_unknownExplanation(UNKNOWN_REASON)
+ , d_inputName(inputName)
+{
+ PrettyCheckArgument(s != SAT_UNKNOWN,
+ "Must provide a reason for satisfiability being unknown");
+}
+
+Result::Result(enum Validity v, std::string inputName)
+ : d_sat(SAT_UNKNOWN)
+ , d_validity(v)
+ , d_which(TYPE_VALIDITY)
+ , d_unknownExplanation(UNKNOWN_REASON)
+ , d_inputName(inputName)
+{
+ PrettyCheckArgument(v != VALIDITY_UNKNOWN,
+ "Must provide a reason for validity being unknown");
+}
+
+
+Result::Result(enum Sat s, enum UnknownExplanation unknownExplanation,
+ std::string inputName)
+ : d_sat(s)
+ , d_validity(VALIDITY_UNKNOWN)
+ , d_which(TYPE_SAT)
+ , d_unknownExplanation(unknownExplanation)
+ , d_inputName(inputName)
+{
+ PrettyCheckArgument(s == SAT_UNKNOWN,
+ "improper use of unknown-result constructor");
+}
+
+Result::Result(enum Validity v, enum UnknownExplanation unknownExplanation,
+ std::string inputName)
+ : d_sat(SAT_UNKNOWN)
+ , d_validity(v)
+ , d_which(TYPE_VALIDITY)
+ , d_unknownExplanation(unknownExplanation)
+ , d_inputName(inputName)
+{
+ PrettyCheckArgument(v == VALIDITY_UNKNOWN,
+ "improper use of unknown-result constructor");
+}
+
+Result::Result(const std::string& instr, std::string inputName) :
+ d_sat(SAT_UNKNOWN),
+ d_validity(VALIDITY_UNKNOWN),
+ d_which(TYPE_NONE),
+ d_unknownExplanation(UNKNOWN_REASON),
+ d_inputName(inputName) {
+ string s = instr;
+ transform(s.begin(), s.end(), s.begin(), ::tolower);
+ if(s == "sat" || s == "satisfiable") {
+ d_which = TYPE_SAT;
+ d_sat = SAT;
+ } else if(s == "unsat" || s == "unsatisfiable") {
+ d_which = TYPE_SAT;
+ d_sat = UNSAT;
+ } else if(s == "valid") {
+ d_which = TYPE_VALIDITY;
+ d_validity = VALID;
+ } else if(s == "invalid") {
+ d_which = TYPE_VALIDITY;
+ d_validity = INVALID;
+ } else if(s == "incomplete") {
+ d_which = TYPE_SAT;
+ d_sat = SAT_UNKNOWN;
+ d_unknownExplanation = INCOMPLETE;
+ } else if(s == "timeout") {
+ d_which = TYPE_SAT;
+ d_sat = SAT_UNKNOWN;
+ d_unknownExplanation = TIMEOUT;
+ } else if(s == "resourceout") {
+ d_which = TYPE_SAT;
+ d_sat = SAT_UNKNOWN;
+ d_unknownExplanation = RESOURCEOUT;
+ } else if(s == "memout") {
+ d_which = TYPE_SAT;
+ d_sat = SAT_UNKNOWN;
+ d_unknownExplanation = MEMOUT;
+ } else if(s == "interrupted") {
+ d_which = TYPE_SAT;
+ d_sat = SAT_UNKNOWN;
+ d_unknownExplanation = INTERRUPTED;
+ } else if(s.size() >= 7 && s.compare(0, 7, "unknown") == 0) {
+ d_which = TYPE_SAT;
+ d_sat = SAT_UNKNOWN;
+ } else {
+ IllegalArgument(s, "expected satisfiability/validity result, "
+ "instead got `%s'", s.c_str());
+ }
+}
+
+Result::UnknownExplanation Result::whyUnknown() const {
+ PrettyCheckArgument( isUnknown(), this,
+ "This result is not unknown, so the reason for "
+ "being unknown cannot be inquired of it" );
+ return d_unknownExplanation;
+}
+
+bool Result::operator==(const Result& r) const throw() {
+ if(d_which != r.d_which) {
+ return false;
+ }
+ if(d_which == TYPE_SAT) {
+ return d_sat == r.d_sat &&
+ ( d_sat != SAT_UNKNOWN ||
+ d_unknownExplanation == r.d_unknownExplanation );
+ }
+ if(d_which == TYPE_VALIDITY) {
+ return d_validity == r.d_validity &&
+ ( d_validity != VALIDITY_UNKNOWN ||
+ d_unknownExplanation == r.d_unknownExplanation );
+ }
+ return false;
+}
+
+bool operator==(enum Result::Sat sr, const Result& r) throw() {
+ return r == sr;
+}
+
+bool operator==(enum Result::Validity vr, const Result& r) throw() {
+ return r == vr;
+}
+bool operator!=(enum Result::Sat s, const Result& r) throw(){
+ return !(s == r);
+}
+bool operator!=(enum Result::Validity v, const Result& r) throw(){
+ return !(v == r);
+}
+
+Result Result::asSatisfiabilityResult() const throw() {
+ if(d_which == TYPE_SAT) {
+ return *this;
+ }
+
+ if(d_which == TYPE_VALIDITY) {
+ switch(d_validity) {
+
+ case INVALID:
+ return Result(SAT, d_inputName);
+
+ case VALID:
+ return Result(UNSAT, d_inputName);
+
+ case VALIDITY_UNKNOWN:
+ return Result(SAT_UNKNOWN, d_unknownExplanation, d_inputName);
+
+ default:
+ Unhandled(d_validity);
+ }
+ }
+
+ // TYPE_NONE
+ return Result(SAT_UNKNOWN, NO_STATUS, d_inputName);
+}
+
+Result Result::asValidityResult() const throw() {
+ if(d_which == TYPE_VALIDITY) {
+ return *this;
+ }
+
+ if(d_which == TYPE_SAT) {
+ switch(d_sat) {
+
+ case SAT:
+ return Result(INVALID, d_inputName);
+
+ case UNSAT:
+ return Result(VALID, d_inputName);
+
+ case SAT_UNKNOWN:
+ return Result(VALIDITY_UNKNOWN, d_unknownExplanation, d_inputName);
+
+ default:
+ Unhandled(d_sat);
+ }
+ }
+
+ // TYPE_NONE
+ return Result(VALIDITY_UNKNOWN, NO_STATUS, d_inputName);
+}
+
+string Result::toString() const {
+ stringstream ss;
+ ss << *this;
+ return ss.str();
+}
+
+ostream& operator<<(ostream& out, enum Result::Sat s) {
+ switch(s) {
+ case Result::UNSAT: out << "UNSAT"; break;
+ case Result::SAT: out << "SAT"; break;
+ case Result::SAT_UNKNOWN: out << "SAT_UNKNOWN"; break;
+ default: Unhandled(s);
+ }
+ return out;
+}
+
+ostream& operator<<(ostream& out, enum Result::Validity v) {
+ switch(v) {
+ case Result::INVALID: out << "INVALID"; break;
+ case Result::VALID: out << "VALID"; break;
+ case Result::VALIDITY_UNKNOWN: out << "VALIDITY_UNKNOWN"; break;
+ default: Unhandled(v);
+ }
+ return out;
+}
+
+ostream& operator<<(ostream& out, enum Result::UnknownExplanation e) {
+ switch(e) {
+ case Result::REQUIRES_FULL_CHECK: out << "REQUIRES_FULL_CHECK"; break;
+ case Result::INCOMPLETE: out << "INCOMPLETE"; break;
+ case Result::TIMEOUT: out << "TIMEOUT"; break;
+ case Result::RESOURCEOUT: out << "RESOURCEOUT"; break;
+ case Result::MEMOUT: out << "MEMOUT"; break;
+ case Result::INTERRUPTED: out << "INTERRUPTED"; break;
+ case Result::NO_STATUS: out << "NO_STATUS"; break;
+ case Result::UNSUPPORTED: out << "UNSUPPORTED"; break;
+ case Result::OTHER: out << "OTHER"; break;
+ case Result::UNKNOWN_REASON: out << "UNKNOWN_REASON"; break;
+ default: Unhandled(e);
+ }
+ return out;
+}
+
+ostream& operator<<(ostream& out, const Result& r) {
+ r.toStream(out, language::SetLanguage::getLanguage(out));
+ return out;
+}/* operator<<(ostream&, const Result&) */
+
+
+void Result::toStreamDefault(std::ostream& out) const throw() {
+ if(getType() == Result::TYPE_SAT) {
+ switch(isSat()) {
+ case Result::UNSAT:
+ out << "unsat";
+ break;
+ case Result::SAT:
+ out << "sat";
+ break;
+ case Result::SAT_UNKNOWN:
+ out << "unknown";
+ if(whyUnknown() != Result::UNKNOWN_REASON) {
+ out << " (" << whyUnknown() << ")";
+ }
+ break;
+ }
+ } else {
+ switch(isValid()) {
+ case Result::INVALID:
+ out << "invalid";
+ break;
+ case Result::VALID:
+ out << "valid";
+ break;
+ case Result::VALIDITY_UNKNOWN:
+ out << "unknown";
+ if(whyUnknown() != Result::UNKNOWN_REASON) {
+ out << " (" << whyUnknown() << ")";
+ }
+ break;
+ }
+ }
+}/* Result::toStreamDefault() */
+
+
+void Result::toStreamSmt2(ostream& out) const throw(){
+ if(getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN) {
+ out << "unknown";
+ } else {
+ toStreamDefault(out);
+ }
+}
+
+void Result::toStreamTptp(std::ostream& out) const throw() {
+ out << "% SZS status ";
+ if(isSat() == Result::SAT) {
+ out << "Satisfiable";
+ } else if(isSat() == Result::UNSAT) {
+ out << "Unsatisfiable";
+ } else if(isValid() == Result::VALID) {
+ out << "Theorem";
+ } else if(isValid() == Result::INVALID) {
+ out << "CounterSatisfiable";
+ } else {
+ out << "GaveUp";
+ }
+ out << " for " << getInputName();
+}
+
+void Result::toStream(std::ostream& out, OutputLanguage language) const throw() {
+ switch(language) {
+ case language::output::LANG_SMTLIB_V2_0:
+ case language::output::LANG_SMTLIB_V2_5:
+ case language::output::LANG_SYGUS:
+ case language::output::LANG_Z3STR:
+ toStreamSmt2(out);
+ break;
+ case language::output::LANG_TPTP:
+ toStreamTptp(out);
+ break;
+ case language::output::LANG_AST:
+ case language::output::LANG_AUTO:
+ case language::output::LANG_CVC3:
+ case language::output::LANG_CVC4:
+ case language::output::LANG_MAX:
+ case language::output::LANG_SMTLIB_V1:
+ default:
+ toStreamDefault(out);
+ break;
+ };
+}
+
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file result.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Encapsulation of the result of a query.
+ **
+ ** Encapsulation of the result of a query.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__RESULT_H
+#define __CVC4__RESULT_H
+
+#include <iostream>
+#include <string>
+
+#include "base/exception.h"
+#include "options/language.h"
+
+namespace CVC4 {
+
+class Result;
+
+std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_PUBLIC;
+
+/**
+ * Three-valued SMT result, with optional explanation.
+ */
+class CVC4_PUBLIC Result {
+public:
+ enum Sat {
+ UNSAT = 0,
+ SAT = 1,
+ SAT_UNKNOWN = 2
+ };
+
+ enum Validity {
+ INVALID = 0,
+ VALID = 1,
+ VALIDITY_UNKNOWN = 2
+ };
+
+ enum Type {
+ TYPE_SAT,
+ TYPE_VALIDITY,
+ TYPE_NONE
+ };
+
+ enum UnknownExplanation {
+ REQUIRES_FULL_CHECK,
+ INCOMPLETE,
+ TIMEOUT,
+ RESOURCEOUT,
+ MEMOUT,
+ INTERRUPTED,
+ NO_STATUS,
+ UNSUPPORTED,
+ OTHER,
+ UNKNOWN_REASON
+ };
+
+private:
+ enum Sat d_sat;
+ enum Validity d_validity;
+ enum Type d_which;
+ enum UnknownExplanation d_unknownExplanation;
+ std::string d_inputName;
+
+public:
+
+ Result();
+
+ Result(enum Sat s, std::string inputName = "");
+
+ Result(enum Validity v, std::string inputName = "");
+
+ Result(enum Sat s,
+ enum UnknownExplanation unknownExplanation,
+ std::string inputName = "");
+
+ Result(enum Validity v, enum UnknownExplanation unknownExplanation,
+ std::string inputName = "");
+
+ Result(const std::string& s, std::string inputName = "");
+
+ Result(const Result& r, std::string inputName) {
+ *this = r;
+ d_inputName = inputName;
+ }
+
+ enum Sat isSat() const {
+ return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN;
+ }
+
+ enum Validity isValid() const {
+ return d_which == TYPE_VALIDITY ? d_validity : VALIDITY_UNKNOWN;
+ }
+
+ bool isUnknown() const {
+ return isSat() == SAT_UNKNOWN && isValid() == VALIDITY_UNKNOWN;
+ }
+
+ Type getType() const {
+ return d_which;
+ }
+
+ bool isNull() const {
+ return d_which == TYPE_NONE;
+ }
+
+ enum UnknownExplanation whyUnknown() const;
+
+ bool operator==(const Result& r) const throw();
+ inline bool operator!=(const Result& r) const throw();
+ Result asSatisfiabilityResult() const throw();
+ Result asValidityResult() const throw();
+
+ std::string toString() const;
+
+ std::string getInputName() const { return d_inputName; }
+
+ /**
+ * Write a Result out to a stream in this language.
+ */
+ void toStream(std::ostream& out, OutputLanguage language) const throw();
+
+ /**
+ * This is mostly the same the default
+ * If getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN,
+ *
+ */
+ void toStreamSmt2(std::ostream& out) const throw();
+
+ /**
+ * Write a Result out to a stream in the Tptp format
+ */
+ void toStreamTptp(std::ostream& out) const throw();
+
+ /**
+ * Write a Result out to a stream.
+ *
+ * The default implementation writes a reasonable string in lowercase
+ * for sat, unsat, valid, invalid, or unknown results. This behavior
+ * is overridable by each Printer, since sometimes an output language
+ * has a particular preference for how results should appear.
+ */
+ void toStreamDefault(std::ostream& out) const throw();
+};/* class Result */
+
+inline bool Result::operator!=(const Result& r) const throw() {
+ return !(*this == r);
+}
+
+std::ostream& operator<<(std::ostream& out,
+ enum Result::Sat s) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out,
+ enum Result::Validity v) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out,
+ enum Result::UnknownExplanation e) CVC4_PUBLIC;
+
+bool operator==(enum Result::Sat s, const Result& r) throw() CVC4_PUBLIC;
+bool operator==(enum Result::Validity v, const Result& r) throw() CVC4_PUBLIC;
+
+bool operator!=(enum Result::Sat s, const Result& r) throw() CVC4_PUBLIC;
+bool operator!=(enum Result::Validity v, const Result& r) throw() CVC4_PUBLIC;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__RESULT_H */
--- /dev/null
+%{
+#include "util/result.h"
+%}
+
+%ignore CVC4::operator<<(std::ostream&, const Result& r);
+
+%rename(equals) CVC4::Result::operator==(const Result& r) const;
+%ignore CVC4::Result::operator!=(const Result& r) const;
+
+%ignore CVC4::operator<<(std::ostream&, enum Result::Sat);
+%ignore CVC4::operator<<(std::ostream&, enum Result::Validity);
+%ignore CVC4::operator<<(std::ostream&, enum Result::UnknownExplanation);
+
+%ignore CVC4::operator==(enum Result::Sat, const Result&);
+%ignore CVC4::operator!=(enum Result::Sat, const Result&);
+
+%ignore CVC4::operator==(enum Result::Validity, const Result&);
+%ignore CVC4::operator!=(enum Result::Validity, const Result&);
+
+%include "util/result.h"
d_theoryEngine = d_smt->d_theoryEngine;
d_satSolver = new FakeSatSolver();
- d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, new theory::TheoryRegistrar(d_theoryEngine), new context::Context());
+ d_cnfStream = new CVC4::prop::TseitinCnfStream(
+ d_satSolver, new theory::TheoryRegistrar(d_theoryEngine),
+ new context::Context(), d_smt->globals());
}
void tearDown() {
d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH] = NULL;
d_smt->d_theoryEngine->d_theoryOut[THEORY_ARITH] = NULL;
- d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), d_logicInfo);
+ d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL),
+ d_logicInfo, d_smt->globals());
preregistered = new std::set<Node>();
// static std::deque<RewriteItem> s_expected;
public:
- FakeTheory(context::Context* ctxt, context::UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
- Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo)
+ FakeTheory(context::Context* ctxt, context::UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, SmtGlobals* globals) :
+ Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo, globals)
{ }
/** Register an expected rewrite call */
- static void expect(RewriteType type, FakeTheory* thy,
- TNode n, bool topLevel) throw() {
+ static void expect(RewriteType type, FakeTheory* thy, TNode n, bool topLevel)
+ throw()
+ {
RewriteItem item = { type, thy, n, topLevel };
//s_expected.push_back(item);
}
void registerTerm(TNode) { Unimplemented(); }
void check(Theory::Effort) { Unimplemented(); }
void propagate(Theory::Effort) { Unimplemented(); }
- void explain(TNode, Theory::Effort) { Unimplemented(); }
+ Node explain(TNode) { Unimplemented(); }
Node getValue(TNode n) { return Node::null(); }
};/* class FakeTheory */
~TestOutputChannel() {}
- void safePoint() throw(Interrupted, AssertionException) {}
+ void safePoint(uint64_t amount)
+ throw(Interrupted, UnsafeInterruptException, AssertionException)
+ {}
void conflict(TNode n)
throw(AssertionException) {
set<Node> d_registered;
vector<Node> d_getSequence;
- DummyTheory(Context* ctxt, UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
- Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo) {
- }
+ DummyTheory(Context* ctxt, UserContext* uctxt, OutputChannel& out,
+ Valuation valuation, const LogicInfo& logicInfo, SmtGlobals* globals)
+ : Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo, globals)
+ {}
void registerTerm(TNode n) {
// check that we registerTerm() a term only once
}
void preRegisterTerm(TNode n) {}
void propagate(Effort level) {}
- void explain(TNode n, Effort level) {}
+ Node explain(TNode n) { return Node::null(); }
Node getValue(TNode n) { return Node::null(); }
string identify() const { return "DummyTheory"; }
};/* class DummyTheory */
d_smt->d_theoryEngine->d_theoryTable[THEORY_BUILTIN] = NULL;
d_smt->d_theoryEngine->d_theoryOut[THEORY_BUILTIN] = NULL;
- d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), *d_logicInfo);
+ d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL),
+ *d_logicInfo, d_smt->globals());
d_outputChannel.clear();
atom0 = d_nm->mkConst(true);
atom1 = d_nm->mkConst(false);
projects / cvc5.git / commitdiff