--drat2er use drat2er (required for eager BV proofs)
--lfsc use the LFSC proof checker
--symfpu use SymFPU for floating point solver
- --portfolio build the multithreaded portfolio version of CVC4
- (pcvc4)
--readline support the readline library
Optional Path to Optional Packages:
lfsc=default
muzzle=default
optimized=default
-portfolio=default
proofs=default
replay=default
shared=default
--optimized) optimized=ON;;
--no-optimized) optimized=OFF;;
- --portfolio) portfolio=ON;;
- --no-portfolio) portfolio=OFF;;
-
--proofs) proofs=ON;;
--no-proofs) proofs=OFF;;
smt/update_ostream.h
smt_util/boolean_simplification.cpp
smt_util/boolean_simplification.h
- smt_util/lemma_channels.cpp
- smt_util/lemma_channels.h
- smt_util/lemma_input_channel.h
- smt_util/lemma_output_channel.h
smt_util/nary_builder.cpp
smt_util/nary_builder.h
smt_util/node_visitor.h
smt/smt_engine.h
DESTINATION
${INCLUDE_INSTALL_DIR}/cvc4/smt)
-install(FILES
- smt_util/lemma_channels.h
- smt_util/lemma_input_channel.h
- smt_util/lemma_output_channel.h
- DESTINATION
- ${INCLUDE_INSTALL_DIR}/cvc4/smt_util)
install(FILES
theory/logic_info.h
theory/theory_id.h
${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__Model.java
${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__Printer.java
${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__options__InstFormatMode.java
- ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_LemmaChannels.java
${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_Listener.java
${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_ListenerCollection__Registration.java
${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_MaybeT_CVC4__Rational_t.java
static void printStatsFilterZeros(std::ostream& out,
const std::string& statsString);
- LemmaChannels* channels() { return d_smtEngine->channels(); }
void flushOutputStreams();
void setReplayStream(ExprStream* replayStream);
read_only = true
help = "do not run destructors at exit; default on except in debug builds"
-[[option]]
- name = "fallbackSequential"
- category = "regular"
- long = "fallback-sequential"
- type = "bool"
- default = "false"
- read_only = true
- help = "Switch to sequential mode (instead of printing an error) if it can't be solved in portfolio mode"
-
-[[option]]
- name = "incrementalParallel"
- category = "regular"
- long = "incremental-parallel"
- type = "bool"
- default = "false"
- links = ["--incremental"]
- read_only = true
- help = "Use parallel solver even in incremental mode (may print 'unknown's at times)"
-
[[option]]
name = "interactive"
category = "regular"
default = "0"
read_only = true
help = "implement PUSH/POP/multi-query by destroying and recreating SmtEngine every N queries"
-
-[[option]]
- name = "waitToJoin"
- category = "expert"
- long = "wait-to-join"
- type = "bool"
- default = "true"
- read_only = true
- help = "wait for other threads to join before quitting"
bool getDumpSynth() const;
bool getDumpUnsatCores() const;
bool getEarlyExit() const;
- bool getFallbackSequential() const;
bool getFilesystemAccess() const;
bool getForceNoLimitCpuWhileDump() const;
bool getHelp() const;
- bool getIncrementalParallel() const;
bool getIncrementalSolving() const;
bool getInteractive() const;
bool getInteractivePrompt() const;
bool getStrictParsing() const;
int getTearDownIncremental() const;
bool getVersion() const;
- bool getWaitToJoin() const;
const std::string& getForceLogicString() const;
int getVerbosity() const;
std::istream* getIn() const;
return (*this)[options::earlyExit];
}
-bool Options::getFallbackSequential() const{
- return (*this)[options::fallbackSequential];
-}
-
bool Options::getFilesystemAccess() const{
return (*this)[options::filesystemAccess];
}
return (*this)[options::help];
}
-bool Options::getIncrementalParallel() const{
- return (*this)[options::incrementalParallel];
-}
-
bool Options::getIncrementalSolving() const{
return (*this)[options::incrementalSolving];
}
return (*this)[options::version];
}
-bool Options::getWaitToJoin() const{
- return (*this)[options::waitToJoin];
-}
-
const std::string& Options::getForceLogicString() const{
return (*this)[options::forceLogicString];
}
#include "proof/proof_manager.h"
#include "prop/registrar.h"
#include "prop/theory_proxy.h"
-#include "smt_util/lemma_channels.h"
namespace CVC4 {
}
};
-PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext,
- Context* userContext, std::ostream* replayLog,
- ExprStream* replayStream, LemmaChannels* channels) :
- d_inCheckSat(false),
- d_theoryEngine(te),
- d_decisionEngine(de),
- d_context(satContext),
- d_theoryProxy(NULL),
- d_satSolver(NULL),
- d_registrar(NULL),
- d_cnfStream(NULL),
- d_interrupted(false),
- d_resourceManager(NodeManager::currentResourceManager())
+PropEngine::PropEngine(TheoryEngine* te,
+ DecisionEngine* de,
+ Context* satContext,
+ Context* userContext,
+ std::ostream* replayLog,
+ ExprStream* replayStream)
+ : d_inCheckSat(false),
+ d_theoryEngine(te),
+ d_decisionEngine(de),
+ d_context(satContext),
+ d_theoryProxy(NULL),
+ d_satSolver(NULL),
+ d_registrar(NULL),
+ d_cnfStream(NULL),
+ d_interrupted(false),
+ d_resourceManager(NodeManager::currentResourceManager())
{
Debug("prop") << "Constructing the PropEngine" << endl;
d_cnfStream = new CVC4::prop::TseitinCnfStream(
d_satSolver, d_registrar, userContext, true);
- d_theoryProxy = new TheoryProxy(
- this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream, replayLog,
- replayStream, channels);
+ d_theoryProxy = new TheoryProxy(this,
+ d_theoryEngine,
+ d_decisionEngine,
+ d_context,
+ d_cnfStream,
+ replayLog,
+ replayStream);
d_satSolver->initialize(d_context, d_theoryProxy);
d_decisionEngine->setSatSolver(d_satSolver);
#include "expr/node.h"
#include "options/options.h"
#include "proof/proof_manager.h"
-#include "smt_util/lemma_channels.h"
#include "util/resource_manager.h"
#include "util/result.h"
#include "util/unsafe_interrupt_exception.h"
/** Dump out the satisfying assignment (after SAT result) */
void printSatisfyingAssignment();
-public:
-
+ public:
/**
* Create a PropEngine with a particular decision and theory engine.
*/
- PropEngine(TheoryEngine*, DecisionEngine*, context::Context* satContext,
- context::Context* userContext, std::ostream* replayLog,
- ExprStream* replayStream, LemmaChannels* channels);
+ PropEngine(TheoryEngine*,
+ DecisionEngine*,
+ context::Context* satContext,
+ context::Context* userContext,
+ std::ostream* replayLog,
+ ExprStream* replayStream);
/**
* Destructor.
* PropEngine and Theory). For now, there's nothing to do here in
* the PropEngine.
*/
- void shutdown() { }
+ void shutdown() {}
/**
* Converts the given formula to CNF and assert the CNF to the SAT solver.
* @param removable whether this lemma can be quietly removed based
* on an activity heuristic (or not)
*/
- void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, TNode from = TNode::null());
+ void assertLemma(TNode node,
+ bool negated,
+ bool removable,
+ ProofRule rule,
+ TNode from = TNode::null());
/**
* If ever n is decided upon, it must be in the given phase. This
*/
bool properExplanation(TNode node, TNode expl) const;
-};/* class PropEngine */
-
+}; /* class PropEngine */
}/* CVC4::prop namespace */
}/* CVC4 namespace */
#include "proof/cnf_proof.h"
#include "smt/command.h"
#include "smt/smt_statistics_registry.h"
-#include "smt_util/lemma_input_channel.h"
-#include "smt_util/lemma_output_channel.h"
#include "theory/rewriter.h"
#include "theory/theory_engine.h"
#include "util/statistics_registry.h"
context::Context* context,
CnfStream* cnfStream,
std::ostream* replayLog,
- ExprStream* replayStream,
- LemmaChannels* channels)
+ ExprStream* replayStream)
: d_propEngine(propEngine),
d_cnfStream(cnfStream),
d_decisionEngine(decisionEngine),
d_theoryEngine(theoryEngine),
- d_channels(channels),
d_replayLog(replayLog),
d_replayStream(replayStream),
d_queue(context),
smtStatisticsRegistry()->unregisterStat(&d_replayedDecisions);
}
-/** The lemma input channel we are using. */
-LemmaInputChannel* TheoryProxy::inputChannel() {
- return d_channels->getLemmaInputChannel();
-}
-
-/** The lemma output channel we are using. */
-LemmaOutputChannel* TheoryProxy::outputChannel() {
- return d_channels->getLemmaOutputChannel();
-}
-
-
void TheoryProxy::variableNotify(SatVariable var) {
d_theoryEngine->preRegister(getNode(SatLiteral(var)));
}
void TheoryProxy::notifyRestart() {
d_propEngine->spendResource(ResourceManager::Resource::RestartStep);
d_theoryEngine->notifyRestart();
-
- static uint32_t lemmaCount = 0;
-
- if(inputChannel() != NULL) {
- while(inputChannel()->hasNewLemma()) {
- Debug("shared") << "shared" << std::endl;
- Expr lemma = inputChannel()->getNewLemma();
- Node asNode = lemma.getNode();
- asNode = theory::Rewriter::rewrite(asNode);
-
- if(d_shared.find(asNode) == d_shared.end()) {
- d_shared.insert(asNode);
- if(asNode.getKind() == kind::OR) {
- ++lemmaCount;
- if(lemmaCount % 1 == 0) {
- Debug("shared") << "=) " << asNode << std::endl;
- }
-
- d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID);
- } else {
- Debug("shared") << "=(" << asNode << std::endl;
- }
- } else {
- Debug("shared") <<"drop shared " << asNode << std::endl;
- }
- }
- }
-}
-
-void TheoryProxy::notifyNewLemma(SatClause& lemma) {
- Assert(lemma.size() > 0);
- if(outputChannel() != NULL) {
- if(lemma.size() == 1) {
- // cannot share units yet
- //options::lemmaOutputChannel()->notifyNewLemma(d_cnfStream->getNode(lemma[0]).toExpr());
- } else {
- NodeBuilder<> b(kind::OR);
- for(unsigned i = 0, i_end = lemma.size(); i < i_end; ++i) {
- b << d_cnfStream->getNode(lemma[i]);
- }
- Node n = b;
-
- if(d_shared.find(n) == d_shared.end()) {
- d_shared.insert(n);
- outputChannel()->notifyNewLemma(n.toExpr());
- } else {
- Debug("shared") <<"drop new " << n << std::endl;
- }
- }
- }
}
SatLiteral TheoryProxy::getNextReplayDecision() {
#include "expr/expr_stream.h"
#include "expr/node.h"
#include "prop/sat_solver.h"
-#include "smt_util/lemma_channels.h"
-#include "smt_util/lemma_input_channel.h"
-#include "smt_util/lemma_output_channel.h"
#include "theory/theory.h"
#include "util/resource_manager.h"
#include "util/statistics_registry.h"
/**
* The proxy class that allows the SatSolver to communicate with the theories
*/
-class TheoryProxy {
-public:
+class TheoryProxy
+{
+ public:
TheoryProxy(PropEngine* propEngine,
TheoryEngine* theoryEngine,
DecisionEngine* decisionEngine,
context::Context* context,
CnfStream* cnfStream,
std::ostream* replayLog,
- ExprStream* replayStream,
- LemmaChannels* globals);
+ ExprStream* replayStream);
~TheoryProxy();
-
void theoryCheck(theory::Theory::Effort effort);
void explainPropagation(SatLiteral l, SatClause& explanation);
void notifyRestart();
- void notifyNewLemma(SatClause& lemma);
-
SatLiteral getNextReplayDecision();
void logDecision(SatLiteral lit);
/** The theory engine we are using. */
TheoryEngine* d_theoryEngine;
-
- /** Container for inputChannel() and outputChannel(). */
- LemmaChannels* d_channels;
-
/** Stream on which to log replay events. */
std::ostream* d_replayLog;
/** Stream for replaying decisions. */
ExprStream* d_replayStream;
- /** The lemma input channel we are using. */
- LemmaInputChannel* inputChannel();
-
- /** The lemma output channel we are using. */
- LemmaOutputChannel* outputChannel();
-
/** Queue of asserted facts */
context::CDQueue<TNode> d_queue;
*/
IntStat d_replayedDecisions;
-};/* class SatSolver */
+}; /* class SatSolver */
}/* CVC4::prop namespace */
d_replayStream(NULL),
d_private(NULL),
d_statisticsRegistry(NULL),
- d_stats(NULL),
- d_channels(new LemmaChannels())
+ d_stats(NULL)
{
SmtScope smts(this);
d_originalOptions.copyValues(em->getOptions());
d_theoryEngine = new TheoryEngine(d_context,
d_userContext,
d_private->d_iteRemover,
- const_cast<const LogicInfo&>(d_logic),
- d_channels);
+ const_cast<const LogicInfo&>(d_logic));
// Add the theories
for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
d_decisionEngine->init(); // enable appropriate strategies
Trace("smt-debug") << "Making prop engine..." << std::endl;
- d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context,
- d_userContext, d_private->getReplayLog(),
- d_replayStream, d_channels);
+ d_propEngine = new PropEngine(d_theoryEngine,
+ d_decisionEngine,
+ d_context,
+ d_userContext,
+ d_private->getReplayLog(),
+ d_replayStream);
Trace("smt-debug") << "Setting up theory engine..." << std::endl;
d_theoryEngine->setPropEngine(d_propEngine);
delete d_context;
d_context = NULL;
- delete d_channels;
- d_channels = NULL;
-
} catch(Exception& e) {
Warning() << "CVC4 threw an exception during cleanup." << endl
<< e << endl;
#include "options/options.h"
#include "proof/unsat_core.h"
#include "smt/logic_exception.h"
-#include "smt_util/lemma_channels.h"
#include "theory/logic_info.h"
#include "util/hash.h"
#include "util/proof.h"
*/
void beforeSearch();
- LemmaChannels* channels() { return d_channels; }
-
/**
* Expermintal feature: Sets the sequence of decisions.
* This currently requires very fine grained knowledge about literal
smt::SmtEngineStatistics* d_stats;
- /** Container for the lemma input and output channels for this SmtEngine.*/
- LemmaChannels* d_channels;
-
/*---------------------------- sygus commands ---------------------------*/
/**
+++ /dev/null
-/********************* */
-/*! \file lemma_channels.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief This class is a light container for globals that used to live
- ** in options. This is NOT a good long term solution, but is a reasonable
- ** stop gap.
- **
- ** This class is a light container for globals that used to live
- ** in options. This is NOT a good long term solution, but is a reasonable
- ** stop gap.
- **/
-
-#include "smt_util/lemma_channels.h"
-
-#include <cerrno>
-#include <iostream>
-#include <string>
-#include <utility>
-
-#include "cvc4autoconfig.h" // Needed for CVC4_REPLAY
-#include "expr/expr_stream.h"
-#include "options/open_ostream.h"
-#include "options/option_exception.h"
-#include "options/parser_options.h"
-#include "smt_util/lemma_input_channel.h"
-#include "smt_util/lemma_output_channel.h"
-
-namespace CVC4 {
-
-LemmaChannels::LemmaChannels()
- : d_lemmaInputChannel(NULL)
- , d_lemmaOutputChannel(NULL)
-{}
-
-LemmaChannels::~LemmaChannels(){}
-
-void LemmaChannels::setLemmaInputChannel(LemmaInputChannel* in) {
- d_lemmaInputChannel = in;
-}
-
-void LemmaChannels::setLemmaOutputChannel(LemmaOutputChannel* out) {
- d_lemmaOutputChannel = out;
-}
-
-
-} /* namespace CVC4 */
+++ /dev/null
-/********************* */
-/*! \file lemma_channels.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Tim King, Andres Noetzli
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief LemmaChannels is a light container for a pair of input and output
- ** lemma channels.
- **
- ** LemmaChannels is a light container for a pair of input and output
- ** lemma channels. These contain paramaters for the infrequently
- ** used Portfolio mode. There should be exactly one of these per SmtEngine
- ** with the same lifetime as the SmtEngine. The user directly passes these as
- ** pointers and is resonsible for cleaning up the memory.
- **
- ** Basically, the problem this class is solving is that previously these were
- ** using smt_options.h and the Options class as globals for these same
- ** datastructures.
- **/
-
-#include "cvc4_public.h"
-
-#ifndef CVC4__SMT_UTIL__LEMMA_CHANNELS_H
-#define CVC4__SMT_UTIL__LEMMA_CHANNELS_H
-
-#include <iosfwd>
-#include <string>
-#include <utility>
-
-#include "options/option_exception.h"
-#include "smt_util/lemma_input_channel.h"
-#include "smt_util/lemma_output_channel.h"
-
-namespace CVC4 {
-
-/**
- * LemmaChannels is a wrapper around two pointers:
- * - getLemmaInputChannel()
- * - getLemmaOutputChannel()
- *
- * The user can directly set these and is responsible for handling the
- * memory for these. These datastructures are used for Portfolio mode.
- */
-class CVC4_PUBLIC LemmaChannels {
- public:
- /** Creates an empty LemmaChannels with all 4 pointers initially NULL. */
- LemmaChannels();
- ~LemmaChannels();
-
- void setLemmaInputChannel(LemmaInputChannel* in);
- LemmaInputChannel* getLemmaInputChannel() { return d_lemmaInputChannel; }
-
- void setLemmaOutputChannel(LemmaOutputChannel* out);
- LemmaOutputChannel* getLemmaOutputChannel() { return d_lemmaOutputChannel; }
-
- private:
- // Disable copy constructor.
- LemmaChannels(const LemmaChannels&) = delete;
-
- // Disable assignment operator.
- LemmaChannels& operator=(const LemmaChannels&) = delete;
-
- /** This captures the old options::lemmaInputChannel .*/
- LemmaInputChannel* d_lemmaInputChannel;
-
- /** This captures the old options::lemmaOutputChannel .*/
- LemmaOutputChannel* d_lemmaOutputChannel;
-}; /* class LemmaChannels */
-
-} /* namespace CVC4 */
-
-#endif /* CVC4__SMT_UTIL__LEMMA_CHANNELS_H */
+++ /dev/null
-/********************* */
-/*! \file lemma_input_channel.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Morgan Deters, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_public.h"
-
-#ifndef CVC4__LEMMA_INPUT_CHANNEL_H
-#define CVC4__LEMMA_INPUT_CHANNEL_H
-
-#include "expr/expr.h"
-
-namespace CVC4 {
-
-class CVC4_PUBLIC LemmaInputChannel {
-public:
- virtual ~LemmaInputChannel() {}
-
- virtual bool hasNewLemma() = 0;
- virtual Expr getNewLemma() = 0;
-
-};/* class LemmaOutputChannel */
-
-}/* CVC4 namespace */
-
-#endif /* CVC4__LEMMA_INPUT_CHANNEL_H */
+++ /dev/null
-/********************* */
-/*! \file lemma_output_channel.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Morgan Deters, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Mechanism for communication about new lemmas
- **
- ** This file defines an interface for use by the theory and propositional
- ** engines to communicate new lemmas to the "outside world".
- **/
-
-#include "cvc4_public.h"
-
-#ifndef CVC4__LEMMA_OUTPUT_CHANNEL_H
-#define CVC4__LEMMA_OUTPUT_CHANNEL_H
-
-#include "expr/expr.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 {
-public:
- virtual ~LemmaOutputChannel() {}
-
- /**
- * Notifies this output channel that there's a new lemma.
- * The lemma may or may not be in CNF.
- */
- virtual void notifyNewLemma(Expr lemma) = 0;
-};/* class LemmaOutputChannel */
-
-}/* CVC4 namespace */
-
-#endif /* CVC4__LEMMA_OUTPUT_CHANNEL_H */
#include "proof/theory_proof.h"
#include "smt/logic_exception.h"
#include "smt/term_formula_removal.h"
-#include "smt_util/lemma_output_channel.h"
#include "smt_util/node_visitor.h"
#include "theory/arith/arith_ite_utils.h"
#include "theory/bv/theory_bv_utils.h"
TheoryEngine::TheoryEngine(context::Context* context,
context::UserContext* userContext,
RemoveTermFormulas& iteRemover,
- const LogicInfo& logicInfo,
- LemmaChannels* channels)
+ const LogicInfo& logicInfo)
: d_propEngine(nullptr),
d_decisionEngine(nullptr),
d_context(context),
d_false(),
d_interrupted(false),
d_resourceManager(NodeManager::currentResourceManager()),
- d_channels(channels),
d_inPreregister(false),
d_factsAsserted(context, false),
d_preRegistrationVisitor(this, context),
<< CheckSatCommand(n.toExpr());
}
- // Share with other portfolio threads
- if(d_channels->getLemmaOutputChannel() != NULL) {
- d_channels->getLemmaOutputChannel()->notifyNewLemma(node.toExpr());
- }
-
AssertionPipeline additionalLemmas;
// Run theory preprocessing, maybe
#include "options/theory_options.h"
#include "prop/prop_engine.h"
#include "smt/command.h"
-#include "smt_util/lemma_channels.h"
#include "theory/atom_requests.h"
#include "theory/decision_manager.h"
#include "theory/interrupted.h"
bool d_interrupted;
ResourceManager* d_resourceManager;
- /** Container for lemma input and output channels. */
- LemmaChannels* d_channels;
-
-public:
-
+ public:
/** Constructs a theory engine */
- TheoryEngine(context::Context* context, context::UserContext* userContext,
- RemoveTermFormulas& iteRemover, const LogicInfo& logic,
- LemmaChannels* channels);
+ TheoryEngine(context::Context* context,
+ context::UserContext* userContext,
+ RemoveTermFormulas& iteRemover,
+ const LogicInfo& logic);
/** Destroys a theory engine */
~TheoryEngine();
* there is another theory it will be deleted.
*/
template <class TheoryClass>
- inline void addTheory(theory::TheoryId theoryId) {
+ 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);
}
inline void setPropEngine(prop::PropEngine* propEngine) {
d_cnfContext = new context::Context();
d_cnfRegistrar = new theory::TheoryRegistrar(d_theoryEngine);
d_cnfStream = new CVC4::prop::TseitinCnfStream(
- d_satSolver, d_cnfRegistrar, d_cnfContext, d_smt->channels());
+ d_satSolver, d_cnfRegistrar, d_cnfContext);
}
void tearDown() override
projects / cvc5.git / commitdiff