This PR decouples Options from NodeManager. Instead, options now live in SmtEngine.
The changes that were required for this PR include:
The main internal options object is now owned by SmtEngine instead of ExprManager.
The ownership resource manager is moved from NodeManager to SmtEngine.
Node manager listeners are deleted, timeouts and resource limits are set during SmtEngine::finishInit.
A temporary hack was added to make the last constructed SmtEngine to be the one in scope. This ensures that options are in scope whenever an SmtEngine is created.
The methods for invoking "subsolvers" (theory/smt_engine_subsolver.h,cpp) was simplified, as versions of these calls that change options do not have to clone a new copy of the ExprManager anymore.
Resource manager was removed from the smt2 parser.
Minor refactoring was done in SmtEngine to copy "original options" so that options are restored to their state after parsing command line options on reset.
Updates to unit tests to ensure conformance to new options scoping.
Solver::Solver(Options* opts)
{
- Options* o = opts == nullptr ? new Options() : opts;
- d_exprMgr.reset(new ExprManager(*o));
- d_smtEngine.reset(new SmtEngine(d_exprMgr.get()));
+ d_exprMgr.reset(new ExprManager);
+ d_smtEngine.reset(new SmtEngine(d_exprMgr.get(), opts));
d_smtEngine->setSolver(this);
- d_rng.reset(new Random((*o)[options::seed]));
- if (opts == nullptr) delete o;
+ Options& o = d_smtEngine->getOptions();
+ d_rng.reset(new Random(o[options::seed]));
}
Solver::~Solver() {}
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
CVC4_API_CHECK(!d_smtEngine->isQueryMade()
- || CVC4::options::incrementalSolving())
+ || d_smtEngine->getOptions()[options::incrementalSolving])
<< "Cannot make multiple queries unless incremental solving is enabled "
"(try --incremental)";
CVC4_API_ARG_CHECK_NOT_NULL(term);
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
CVC4_API_CHECK(!d_smtEngine->isQueryMade()
- || CVC4::options::incrementalSolving())
+ || d_smtEngine->getOptions()[options::incrementalSolving])
<< "Cannot make multiple queries unless incremental solving is enabled "
"(try --incremental)";
for (const Term& term : terms)
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
CVC4_API_CHECK(!d_smtEngine->isQueryMade()
- || CVC4::options::incrementalSolving())
+ || d_smtEngine->getOptions()[options::incrementalSolving])
<< "Cannot make multiple queries unless incremental solving is enabled "
"(try --incremental)";
CVC4::Result r = d_smtEngine->checkSat();
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
CVC4_API_CHECK(!d_smtEngine->isQueryMade()
- || CVC4::options::incrementalSolving())
+ || d_smtEngine->getOptions()[options::incrementalSolving])
<< "Cannot make multiple queries unless incremental solving is enabled "
"(try --incremental)";
CVC4_API_SOLVER_CHECK_TERM(assumption);
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
CVC4_API_CHECK(!d_smtEngine->isQueryMade() || assumptions.size() == 0
- || CVC4::options::incrementalSolving())
+ || d_smtEngine->getOptions()[options::incrementalSolving])
<< "Cannot make multiple queries unless incremental solving is enabled "
"(try --incremental)";
for (const Term& term : assumptions)
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
- CVC4_API_CHECK(CVC4::options::produceAssignments())
+ CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceAssignments])
<< "Cannot get assignment unless assignment generation is enabled "
"(try --produce-assignments)";
std::vector<std::pair<Expr, Expr>> assignment = d_smtEngine->getAssignment();
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
- CVC4_API_CHECK(CVC4::options::incrementalSolving())
+ CVC4_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving])
<< "Cannot get unsat assumptions unless incremental solving is enabled "
"(try --incremental)";
- CVC4_API_CHECK(CVC4::options::unsatAssumptions())
+ CVC4_API_CHECK(d_smtEngine->getOptions()[options::unsatAssumptions])
<< "Cannot get unsat assumptions unless explicitly enabled "
"(try --produce-unsat-assumptions)";
CVC4_API_CHECK(d_smtEngine->getSmtMode()
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
- CVC4_API_CHECK(CVC4::options::unsatCores())
+ CVC4_API_CHECK(d_smtEngine->getOptions()[options::unsatCores])
<< "Cannot get unsat core unless explicitly enabled "
"(try --produce-unsat-cores)";
CVC4_API_CHECK(d_smtEngine->getSmtMode()
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
- CVC4_API_CHECK(CVC4::options::produceModels())
+ CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
<< "Cannot get value unless model generation is enabled "
"(try --produce-models)";
CVC4_API_CHECK(d_smtEngine->getSmtMode()
<< "Cannot obtain separation logic expressions if not using the "
"separation logic theory.";
CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
- CVC4_API_CHECK(CVC4::options::produceModels())
+ CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
<< "Cannot get separation heap term unless model generation is enabled "
"(try --produce-models)";
CVC4_API_CHECK(d_smtEngine->getSmtMode()
<< "Cannot obtain separation logic expressions if not using the "
"separation logic theory.";
CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
- CVC4_API_CHECK(CVC4::options::produceModels())
+ CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
<< "Cannot get separation nil term unless model generation is enabled "
"(try --produce-models)";
CVC4_API_CHECK(d_smtEngine->getSmtMode()
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
- CVC4_API_CHECK(CVC4::options::incrementalSolving())
+ CVC4_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving])
<< "Cannot pop when not solving incrementally (use --incremental)";
CVC4_API_CHECK(nscopes <= d_smtEngine->getNumUserLevels())
<< "Cannot pop beyond first pushed context";
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
- CVC4_API_CHECK(CVC4::options::produceModels())
+ CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
<< "Cannot get value unless model generation is enabled "
"(try --produce-models)";
CVC4_API_CHECK(d_smtEngine->getSmtMode()
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
- CVC4_API_CHECK(CVC4::options::incrementalSolving())
+ CVC4_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving])
<< "Cannot push when not solving incrementally (use --incremental)";
for (uint32_t n = 0; n < nscopes; ++n)
*/
SmtEngine* Solver::getSmtEngine(void) const { return d_smtEngine.get(); }
+/**
+ * !!! This is only temporarily available until the parser is fully migrated to
+ * the new API. !!!
+ */
+Options& Solver::getOptions(void) { return d_smtEngine->getOptions(); }
+
/* -------------------------------------------------------------------------- */
/* Conversions */
/* -------------------------------------------------------------------------- */
/**
* Constructor.
- * @param opts a pointer to a solver options object (for parser only)
+ * @param opts an optional pointer to a solver options object
* @return the Solver
*/
Solver(Options* opts = nullptr);
// to the new API. !!!
SmtEngine* getSmtEngine(void) const;
+ // !!! This is only temporarily available until options are refactored at
+ // the driver level. !!!
+ Options& getOptions(void);
+
private:
/* Helper to convert a vector of internal types to sorts. */
std::vector<Type> sortVectorToTypes(const std::vector<Sort>& vector) const;
node_manager.cpp
node_manager.h
node_manager_attributes.h
- node_manager_listeners.cpp
- node_manager_listeners.h
node_self_iterator.h
node_trie.cpp
node_trie.h
#endif
}
-ExprManager::ExprManager(const Options& options) :
- d_nodeManager(new NodeManager(this, options)) {
-#ifdef CVC4_STATISTICS_ON
- for (unsigned i = 0; i <= LAST_TYPE; ++ i) {
- d_exprStatisticsVars[i] = NULL;
- }
- for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
- d_exprStatistics[i] = NULL;
- }
-#endif
-}
-
ExprManager::~ExprManager()
{
NodeManagerScope nms(d_nodeManager);
}
}
-const Options& ExprManager::getOptions() const {
- return d_nodeManager->getOptions();
-}
-
-ResourceManager* ExprManager::getResourceManager()
-{
- return d_nodeManager->getResourceManager();
-}
-
BooleanType ExprManager::booleanType() const {
NodeManagerScope nms(d_nodeManager);
return BooleanType(Type(d_nodeManager, new TypeNode(d_nodeManager->booleanType())));
}
Expr ExprManager::mkVar(const std::string& name, Type type, uint32_t flags) {
- Assert(NodeManager::currentNM() == NULL)
- << "ExprManager::mkVar() should only be called externally, not from "
- "within CVC4 code. Please use mkSkolem().";
NodeManagerScope nms(d_nodeManager);
Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode, flags);
Debug("nm") << "set " << name << " on " << *n << std::endl;
}
Expr ExprManager::mkVar(Type type, uint32_t flags) {
- Assert(NodeManager::currentNM() == NULL)
- << "ExprManager::mkVar() should only be called externally, not from "
- "within CVC4 code. Please use mkSkolem().";
NodeManagerScope nms(d_nodeManager);
INC_STAT_VAR(type, false);
return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode, flags));
/** A list of datatypes owned by this expr manager. */
std::vector<std::unique_ptr<Datatype> > d_ownedDatatypes;
- /**
- * Creates an expression manager with default options.
- */
+ /** Creates an expression manager. */
ExprManager();
-
- /**
- * Creates an expression manager.
- *
- * @param options the earlyTypeChecking field is used to configure
- * whether to do at Expr creation time.
- */
- explicit ExprManager(const Options& options);
-
public:
/**
* Destroys the expression manager. No will be deallocated at this point, so
*/
~ExprManager();
- /** Get this expr manager's options */
- const Options& getOptions() const;
-
- /** Get this expr manager's resource manager */
- ResourceManager* getResourceManager();
-
/** Get the type for booleans */
BooleanType booleanType() const;
#include "expr/attribute.h"
#include "expr/dtype.h"
#include "expr/node_manager_attributes.h"
-#include "expr/node_manager_listeners.h"
#include "expr/skolem_manager.h"
#include "expr/type_checker.h"
#include "options/options.h"
typedef expr::Attribute<attr::LambdaBoundVarListTag, Node> LambdaBoundVarListAttr;
NodeManager::NodeManager(ExprManager* exprManager)
- : d_options(new Options()),
- d_statisticsRegistry(new StatisticsRegistry()),
- d_resourceManager(new ResourceManager(*d_statisticsRegistry, *d_options)),
+ : d_statisticsRegistry(new StatisticsRegistry()),
d_skManager(new SkolemManager),
- d_registrations(new ListenerRegistrationList()),
next_id(0),
d_attrManager(new expr::attr::AttributeManager()),
d_exprManager(exprManager),
init();
}
-NodeManager::NodeManager(ExprManager* exprManager, const Options& options)
- : d_options(new Options()),
- d_statisticsRegistry(new StatisticsRegistry()),
- d_resourceManager(new ResourceManager(*d_statisticsRegistry, *d_options)),
- d_skManager(new SkolemManager),
- d_registrations(new ListenerRegistrationList()),
- next_id(0),
- d_attrManager(new expr::attr::AttributeManager()),
- d_exprManager(exprManager),
- d_nodeUnderDeletion(NULL),
- d_inReclaimZombies(false),
- d_abstractValueCount(0),
- d_skolemCounter(0)
-{
- d_options->copyValues(options);
- init();
-}
-
void NodeManager::init() {
poolInsert( &expr::NodeValue::null() );
d_operators[i] = mkConst(Kind(k));
}
}
- d_resourceManager->setHardLimit((*d_options)[options::hardLimit]);
- if((*d_options)[options::perCallResourceLimit] != 0) {
- d_resourceManager->setResourceLimit((*d_options)[options::perCallResourceLimit], false);
- }
- if((*d_options)[options::cumulativeResourceLimit] != 0) {
- d_resourceManager->setResourceLimit((*d_options)[options::cumulativeResourceLimit], true);
- }
- if((*d_options)[options::perCallMillisecondLimit] != 0) {
- d_resourceManager->setTimeLimit((*d_options)[options::perCallMillisecondLimit], false);
- }
- if((*d_options)[options::cumulativeMillisecondLimit] != 0) {
- d_resourceManager->setTimeLimit((*d_options)[options::cumulativeMillisecondLimit], true);
- }
- if((*d_options)[options::cpuTime]) {
- d_resourceManager->useCPUTime(true);
- }
-
- // Do not notify() upon registration as these were handled manually above.
- d_registrations->add(d_options->registerTlimitListener(
- new TlimitListener(d_resourceManager), false));
- d_registrations->add(d_options->registerTlimitPerListener(
- new TlimitPerListener(d_resourceManager), false));
- d_registrations->add(d_options->registerRlimitListener(
- new RlimitListener(d_resourceManager), false));
- d_registrations->add(d_options->registerRlimitPerListener(
- new RlimitPerListener(d_resourceManager), false));
}
NodeManager::~NodeManager() {
}
// defensive coding, in case destruction-order issues pop up (they often do)
- delete d_resourceManager;
- d_resourceManager = NULL;
delete d_statisticsRegistry;
d_statisticsRegistry = NULL;
- delete d_registrations;
- d_registrations = NULL;
delete d_attrManager;
d_attrManager = NULL;
- delete d_options;
- d_options = NULL;
}
size_t NodeManager::registerDatatype(std::shared_ptr<DType> dt)
static thread_local NodeManager* s_current;
- Options* d_options;
StatisticsRegistry* d_statisticsRegistry;
- ResourceManager* d_resourceManager;
-
/** The skolem manager */
std::shared_ptr<SkolemManager> d_skManager;
- /**
- * A list of registrations on d_options to that call into d_resourceManager.
- * These must be garbage collected before d_options and d_resourceManager.
- */
- ListenerRegistrationList* d_registrations;
-
NodeValuePool d_nodeValuePool;
size_t next_id;
public:
explicit NodeManager(ExprManager* exprManager);
- explicit NodeManager(ExprManager* exprManager, const Options& options);
~NodeManager();
/** The node manager in the current public-facing CVC4 library context */
static NodeManager* currentNM() { return s_current; }
- /** The resource manager associated with the current node manager */
- static ResourceManager* currentResourceManager() { return s_current->d_resourceManager; }
-
- /** Get this node manager's options (const version) */
- const Options& getOptions() const {
- return *d_options;
- }
-
- /** Get this node manager's options (non-const version) */
- Options& getOptions() {
- return *d_options;
- }
-
- /** Get this node manager's resource manager */
- ResourceManager* getResourceManager() { return d_resourceManager; }
/** Get this node manager's skolem manager */
SkolemManager* getSkolemManager() { return d_skManager.get(); }
class NodeManagerScope {
/** The old NodeManager, to be restored on destruction. */
NodeManager* d_oldNodeManager;
- Options::OptionsScope d_optionsScope;
public:
-
- NodeManagerScope(NodeManager* nm)
- : d_oldNodeManager(NodeManager::s_current)
- , d_optionsScope(nm ? nm->d_options : NULL) {
- // There are corner cases where nm can be NULL and it's ok.
- // For example, if you write { Expr e; }, then when the null
- // Expr is destructed, there's no active node manager.
- //Assert(nm != NULL);
- NodeManager::s_current = nm;
- //Options::s_current = nm ? nm->d_options : NULL;
- Debug("current") << "node manager scope: "
- << NodeManager::s_current << "\n";
+ NodeManagerScope(NodeManager* nm) : d_oldNodeManager(NodeManager::s_current)
+ {
+ // There are corner cases where nm can be NULL and it's ok.
+ // For example, if you write { Expr e; }, then when the null
+ // Expr is destructed, there's no active node manager.
+ // Assert(nm != NULL);
+ NodeManager::s_current = nm;
+ Debug("current") << "node manager scope: " << NodeManager::s_current << "\n";
}
~NodeManagerScope() {
NodeManager::s_current = d_oldNodeManager;
- //Options::s_current = d_oldNodeManager ? d_oldNodeManager->d_options : NULL;
Debug("current") << "node manager scope: "
<< "returning to " << NodeManager::s_current << "\n";
}
+++ /dev/null
-/********************* */
-/*! \file node_manager_listeners.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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 Listeners that NodeManager registers to its Options object.
- **
- ** Listeners that NodeManager registers to its Options object.
- **/
-
-#include "node_manager_listeners.h"
-
-#include "base/listener.h"
-#include "options/smt_options.h"
-#include "util/resource_manager.h"
-
-namespace CVC4 {
-namespace expr {
-
-
-void TlimitListener::notify() {
- d_rm->setTimeLimit(options::cumulativeMillisecondLimit(), true);
-}
-
-void TlimitPerListener::notify() {
- d_rm->setTimeLimit(options::perCallMillisecondLimit(), false);
-}
-
-void RlimitListener::notify() {
- d_rm->setTimeLimit(options::cumulativeResourceLimit(), true);
-}
-
-void RlimitPerListener::notify() {
- d_rm->setTimeLimit(options::perCallResourceLimit(), false);
-}
-
-}/* CVC4::expr namespace */
-}/* CVC4 namespace */
+++ /dev/null
-/********************* */
-/*! \file node_manager_listeners.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Tim King, Mathias Preiner
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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 Listeners that NodeManager registers to its Options object.
- **
- ** Listeners that NodeManager registers to its Options object.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4__EXPR__NODE_MANAGER_LISTENERS_H
-#define CVC4__EXPR__NODE_MANAGER_LISTENERS_H
-
-#include "base/listener.h"
-#include "util/resource_manager.h"
-
-namespace CVC4 {
-namespace expr {
-
-class TlimitListener : public Listener {
- public:
- TlimitListener(ResourceManager* rm) : d_rm(rm) {}
- void notify() override;
-
- private:
- ResourceManager* d_rm;
-};
-
-class TlimitPerListener : public Listener {
- public:
- TlimitPerListener(ResourceManager* rm) : d_rm(rm) {}
- void notify() override;
-
- private:
- ResourceManager* d_rm;
-};
-
-class RlimitListener : public Listener {
- public:
- RlimitListener(ResourceManager* rm) : d_rm(rm) {}
- void notify() override;
-
- private:
- ResourceManager* d_rm;
-};
-
-class RlimitPerListener : public Listener {
- public:
- RlimitPerListener(ResourceManager* rm) : d_rm(rm) {}
- void notify() override;
-
- private:
- ResourceManager* d_rm;
-};
-
-}/* CVC4::expr namespace */
-}/* CVC4 namespace */
-
-#endif /* CVC4__EXPR__NODE_MANAGER_LISTENERS_H */
ReferenceStat<std::string> s_statFilename("filename", filenameStr);
RegisterStatistic statFilenameReg(&pExecutor->getStatisticsRegistry(),
&s_statFilename);
- // set filename in smt engine
- pExecutor->getSmtEngine()->setFilename(filenameStr);
+ // notify SmtEngine that we are starting to parse
+ pExecutor->getSmtEngine()->notifyStartParsing(filenameStr);
// Parse and execute commands until we are done
Command* cmd;
#endif /* HAVE_LIBREADLINE */
InteractiveShell::InteractiveShell(api::Solver* solver)
- : d_options(solver->getExprManager()->getOptions()),
+ : d_options(solver->getOptions()),
d_in(*d_options.getIn()),
d_out(*d_options.getOutConst()),
d_quit(false)
/** Listeners for notifyBeforeSearch. */
ListenerCollection d_beforeSearchListeners;
- /** Listeners for options::tlimit. */
- ListenerCollection d_tlimitListeners;
-
- /** Listeners for options::tlimit-per. */
- ListenerCollection d_tlimitPerListeners;
-
- /** Listeners for options::rlimit. */
- ListenerCollection d_rlimitListeners;
-
- /** Listeners for options::tlimit-per. */
- ListenerCollection d_rlimitPerListeners;
-
/** Listeners for options::defaultExprDepth. */
ListenerCollection d_setDefaultExprDepthListeners;
ListenerCollection::Registration* registerBeforeSearchListener(
Listener* listener);
- /**
- * Registers a listener for options::tlimit being set.
- *
- * If notifyIfSet is true, this calls notify on the listener
- * if the option was set by the user.
- *
- * The memory for the Registration is controlled by the user and must
- * be destroyed before the Options object is.
- */
- ListenerCollection::Registration* registerTlimitListener(
- Listener* listener, bool notifyIfSet);
-
- /**
- * Registers a listener for options::tlimit-per being set.
- *
- * If notifyIfSet is true, this calls notify on the listener
- * if the option was set by the user.
- *
- * The memory for the Registration is controlled by the user and must
- * be destroyed before the Options object is.
- */
- ListenerCollection::Registration* registerTlimitPerListener(
- Listener* listener, bool notifyIfSet);
-
-
- /**
- * Registers a listener for options::rlimit being set.
- *
- * If notifyIfSet is true, this calls notify on the listener
- * if the option was set by the user.
- *
- * The memory for the Registration is controlled by the user and must
- * be destroyed before the Options object is.
- */
- ListenerCollection::Registration* registerRlimitListener(
- Listener* listener, bool notifyIfSet);
-
- /**
- * Registers a listener for options::rlimit-per being set.
- *
- * If notifyIfSet is true, this calls notify on the listener
- * if the option was set by the user.
- *
- * The memory for the Registration is controlled by the user and must
- * be destroyed before the Options object is.
- */
- ListenerCollection::Registration* registerRlimitPerListener(
- Listener* listener, bool notifyIfSet);
-
/**
* Registers a listener for options::defaultExprDepth being set.
*
}
}
-
-void OptionsHandler::notifyTlimit(const std::string& option) {
- d_options->d_tlimitListeners.notify();
-}
-
-void OptionsHandler::notifyTlimitPer(const std::string& option) {
- d_options->d_tlimitPerListeners.notify();
-}
-
-void OptionsHandler::notifyRlimit(const std::string& option) {
- d_options->d_rlimitListeners.notify();
-}
-
-void OptionsHandler::notifyRlimitPer(const std::string& option) {
- d_options->d_rlimitPerListeners.notify();
-}
-
unsigned long OptionsHandler::limitHandler(std::string option,
std::string optarg)
{
unsigned long limitHandler(std::string option, std::string optarg);
- void notifyTlimit(const std::string& option);
- void notifyTlimitPer(const std::string& option);
- void notifyRlimit(const std::string& option);
- void notifyRlimitPer(const std::string& option);
-
-
/* expr/options_handlers.h */
void setDefaultExprDepthPredicate(std::string option, int depth);
void setDefaultDagThreshPredicate(std::string option, int dag);
: d_holder(new options::OptionsHolder())
, d_handler(new options::OptionsHandler(this))
, d_beforeSearchListeners()
- , d_tlimitListeners()
- , d_tlimitPerListeners()
- , d_rlimitListeners()
- , d_rlimitPerListeners()
{}
Options::~Options() {
return d_beforeSearchListeners.registerListener(listener);
}
-ListenerCollection::Registration* Options::registerTlimitListener(
- Listener* listener, bool notifyIfSet)
-{
- bool notify = notifyIfSet &&
- wasSetByUser(options::cumulativeMillisecondLimit);
- return registerAndNotify(d_tlimitListeners, listener, notify);
-}
-
-ListenerCollection::Registration* Options::registerTlimitPerListener(
- Listener* listener, bool notifyIfSet)
-{
- bool notify = notifyIfSet && wasSetByUser(options::perCallMillisecondLimit);
- return registerAndNotify(d_tlimitPerListeners, listener, notify);
-}
-
-ListenerCollection::Registration* Options::registerRlimitListener(
- Listener* listener, bool notifyIfSet)
-{
- bool notify = notifyIfSet && wasSetByUser(options::cumulativeResourceLimit);
- return registerAndNotify(d_rlimitListeners, listener, notify);
-}
-
-ListenerCollection::Registration* Options::registerRlimitPerListener(
- Listener* listener, bool notifyIfSet)
-{
- bool notify = notifyIfSet && wasSetByUser(options::perCallResourceLimit);
- return registerAndNotify(d_rlimitPerListeners, listener, notify);
-}
-
ListenerCollection::Registration* Options::registerSetDefaultExprDepthListener(
Listener* listener, bool notifyIfSet)
{
${custom_handlers}$
-
-#ifdef CVC4_DEBUG
-# define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true
-#else /* CVC4_DEBUG */
-# define USE_EARLY_TYPE_CHECKING_BY_DEFAULT false
-#endif /* CVC4_DEBUG */
-
#if defined(CVC4_MUZZLED) || defined(CVC4_COMPETITION_MODE)
# define DO_SEMANTIC_CHECKS_BY_DEFAULT false
#else /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */
void Options::setOption(const std::string& key, const std::string& optionarg)
{
options::OptionsHandler* handler = d_handler;
- Options *options = Options::current();
+ Options* options = this;
Trace("options") << "SMT setOption(" << key << ", " << optionarg << ")"
<< std::endl;
default = "false"
help = "compute backwards filtering to compute whether previous solutions are filtered based on later ones"
-
-[[option]]
- name = "sygusExprMinerCheckUseExport"
- category = "expert"
- long = "sygus-expr-miner-check-use-export"
- type = "bool"
- default = "true"
- help = "export expressions to a different ExprManager with different options for satisfiability checks in expression miners"
-
# CEGQI applied to general quantified formulas
[[option]]
long = "check-synth-sol"
type = "bool"
default = "false"
- read_only = true
help = "checks whether produced solutions to functions-to-synthesize satisfy the conjecture"
[[option]]
long = "tlimit=MS"
type = "unsigned long"
handler = "limitHandler"
- notifies = ["notifyTlimit"]
read_only = true
help = "enable time limiting (give milliseconds)"
long = "tlimit-per=MS"
type = "unsigned long"
handler = "limitHandler"
- notifies = ["notifyTlimitPer"]
read_only = true
help = "enable time limiting per query (give milliseconds)"
long = "rlimit=N"
type = "unsigned long"
handler = "limitHandler"
- notifies = ["notifyRlimit"]
read_only = true
help = "enable resource limiting (currently, roughly the number of SAT conflicts)"
long = "rlimit-per=N"
type = "unsigned long"
handler = "limitHandler"
- notifies = ["notifyRlimitPer"]
read_only = true
help = "enable resource limiting per query"
#include "parser/input.h"
#include "parser/parser_exception.h"
#include "smt/command.h"
-#include "util/resource_manager.h"
using namespace std;
using namespace CVC4::kind;
Input* input,
bool strictMode,
bool parseOnly)
- : d_resourceManager(solver->getExprManager()->getResourceManager()),
- d_input(input),
+ : d_input(input),
d_symtabAllocated(),
d_symtab(&d_symtabAllocated),
d_assertionLevel(0),
}
}
Debug("parser") << "nextCommand() => " << cmd << std::endl;
- if (cmd != NULL && dynamic_cast<SetOptionCommand*>(cmd) == NULL &&
- dynamic_cast<QuitCommand*>(cmd) == NULL) {
- // don't count set-option commands as to not get stuck in an infinite
- // loop of resourcing out
- d_resourceManager->spendResource(ResourceManager::Resource::ParseStep);
- }
return cmd;
}
api::Term Parser::nextExpression()
{
Debug("parser") << "nextExpression()" << std::endl;
- d_resourceManager->spendResource(ResourceManager::Resource::ParseStep);
api::Term result;
if (!done()) {
try {
api::Term Parser::mkStringConstant(const std::string& s)
{
- ExprManager* em = d_solver->getExprManager();
- if (language::isInputLang_smt2_6(em->getOptions().getInputLanguage()))
+ if (language::isInputLang_smt2_6(d_solver->getOptions().getInputLanguage()))
{
return api::Term(d_solver, d_solver->mkString(s, true).getExpr());
}
class CVC4_PUBLIC Parser {
friend class ParserBuilder;
private:
- /** The resource manager associated with this expr manager */
- ResourceManager* d_resourceManager;
/** The input that we're parsing. */
Input* d_input;
bool Smt2::isHoEnabled() const
{
- return getLogic().isHigherOrder()
- && d_solver->getExprManager()->getOptions().getUfHo();
+ return getLogic().isHigherOrder() && d_solver->getOptions().getUfHo();
}
bool Smt2::logicIsSet() {
InputLanguage Smt2::getLanguage() const
{
- return d_solver->getExprManager()->getOptions().getInputLanguage();
+ return d_solver->getOptions().getInputLanguage();
}
void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type)
}
}
// Second phase: apply the arguments to the parse op
- const Options& opts = d_solver->getExprManager()->getOptions();
+ const Options& opts = d_solver->getOptions();
// handle special cases
if (p.d_kind == api::CONST_ARRAY && !p.d_type.isNull())
{
isBuiltinKind = true;
}
assert(kind != api::NULL_EXPR);
- const Options& opts = d_solver->getExprManager()->getOptions();
+ const Options& opts = d_solver->getOptions();
// Second phase: apply parse op to the arguments
if (isBuiltinKind)
{
PreprocessingPassResult StaticLearning::applyInternal(
AssertionPipeline* assertionsToPreprocess)
{
- NodeManager::currentResourceManager()->spendResource(
- ResourceManager::Resource::PreprocessStep);
+ d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
{
Trace("sygus-infer") << "*** Return sygus inference : " << body << std::endl;
// make a separate smt call
- SmtEngine rrSygus(nm->toExprManager());
- rrSygus.setLogic(smt::currentSmtEngine()->getLogicInfo());
+ SmtEngine* currSmt = smt::currentSmtEngine();
+ SmtEngine rrSygus(nm->toExprManager(), &currSmt->getOptions());
+ rrSygus.setLogic(currSmt->getLogicInfo());
rrSygus.assertFormula(body.toExpr());
Trace("sygus-infer") << "*** Check sat..." << std::endl;
Result r = rrSygus.checkSat();
PreprocessingPassContext::PreprocessingPassContext(
SmtEngine* smt,
- ResourceManager* resourceManager,
RemoveTermFormulas* iteRemover,
theory::booleans::CircuitPropagator* circuitPropagator)
: d_smt(smt),
- d_resourceManager(resourceManager),
+ d_resourceManager(smt->getResourceManager()),
d_iteRemover(iteRemover),
d_topLevelSubstitutions(smt->getUserContext()),
d_circuitPropagator(circuitPropagator),
public:
PreprocessingPassContext(
SmtEngine* smt,
- ResourceManager* resourceManager,
RemoveTermFormulas* iteRemover,
theory::booleans::CircuitPropagator* circuitPropagator);
options::bvLazyRewriteExtf.set(false);
}
- if (!options::sygusExprMinerCheckUseExport())
- {
- if (options::sygusExprMinerCheckTimeout.wasSetByUser())
- {
- throw OptionException(
- "--sygus-expr-miner-check-timeout=N requires "
- "--sygus-expr-miner-check-use-export");
- }
- if (options::sygusRewSynthInput() || options::produceAbducts())
- {
- std::stringstream ss;
- ss << (options::sygusRewSynthInput() ? "--sygus-rr-synth-input"
- : "--produce-abducts");
- ss << "requires --sygus-expr-miner-check-use-export";
- throw OptionException(ss.str());
- }
- }
-
if (options::stringFMF() && !options::stringProcessLoopMode.wasSetByUser())
{
Trace("smt") << "settting stringProcessLoopMode to 'simple' since "
typedef unordered_map<Node, Node, NodeHashFunction> NodeToNodeHashMap;
typedef unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
- /**
- * Manager for limiting time and abstract resource usage.
- */
- ResourceManager* d_resourceManager;
-
/** Manager for the memory of regular-output-channel. */
ManagedRegularOutputChannel d_managedRegularChannel;
public:
SmtEnginePrivate(SmtEngine& smt)
: d_smt(smt),
- d_resourceManager(NodeManager::currentResourceManager()),
d_managedRegularChannel(),
d_managedDiagnosticChannel(),
d_managedDumpChannel(),
d_fakeContext(),
d_abstractValueMap(&d_fakeContext),
d_abstractValues(),
- d_processor(smt, *d_resourceManager),
+ d_processor(smt, *smt.getResourceManager()),
// d_needsExpandDefs(true), //TODO?
d_exprNames(smt.getUserContext()),
d_iteRemover(smt.getUserContext()),
{
d_smt.d_nodeManager->subscribeEvents(this);
d_true = NodeManager::currentNM()->mkConst(true);
+ ResourceManager* rm = d_smt.getResourceManager();
- d_listenerRegistrations->add(d_resourceManager->registerSoftListener(
- new SoftResourceOutListener(d_smt)));
+ d_listenerRegistrations->add(
+ rm->registerSoftListener(new SoftResourceOutListener(d_smt)));
- d_listenerRegistrations->add(d_resourceManager->registerHardListener(
- new HardResourceOutListener(d_smt)));
+ d_listenerRegistrations->add(
+ rm->registerHardListener(new HardResourceOutListener(d_smt)));
try
{
- Options& nodeManagerOptions = NodeManager::currentNM()->getOptions();
-
+ Options& opts = d_smt.getOptions();
// Multiple options reuse BeforeSearchListener so registration requires an
// extra bit of care.
// We can safely not call notify on this before search listener at
// time. Therefore the BeforeSearchListener is a no-op. Therefore it does
// not have to be called.
d_listenerRegistrations->add(
- nodeManagerOptions.registerBeforeSearchListener(
- new BeforeSearchListener(d_smt)));
+ opts.registerBeforeSearchListener(new BeforeSearchListener(d_smt)));
// These do need registration calls.
+ d_listenerRegistrations->add(opts.registerSetDefaultExprDepthListener(
+ new SetDefaultExprDepthListener(), true));
+ d_listenerRegistrations->add(opts.registerSetDefaultExprDagListener(
+ new SetDefaultExprDagListener(), true));
+ d_listenerRegistrations->add(opts.registerSetPrintExprTypesListener(
+ new SetPrintExprTypesListener(), true));
d_listenerRegistrations->add(
- nodeManagerOptions.registerSetDefaultExprDepthListener(
- new SetDefaultExprDepthListener(), true));
- d_listenerRegistrations->add(
- nodeManagerOptions.registerSetDefaultExprDagListener(
- new SetDefaultExprDagListener(), true));
- d_listenerRegistrations->add(
- nodeManagerOptions.registerSetPrintExprTypesListener(
- new SetPrintExprTypesListener(), true));
+ opts.registerSetDumpModeListener(new DumpModeListener(), true));
+ d_listenerRegistrations->add(opts.registerSetPrintSuccessListener(
+ new PrintSuccessListener(), true));
+ d_listenerRegistrations->add(opts.registerSetRegularOutputChannelListener(
+ new SetToDefaultSourceListener(&d_managedRegularChannel), true));
d_listenerRegistrations->add(
- nodeManagerOptions.registerSetDumpModeListener(new DumpModeListener(),
- true));
- d_listenerRegistrations->add(
- nodeManagerOptions.registerSetPrintSuccessListener(
- new PrintSuccessListener(), true));
- d_listenerRegistrations->add(
- nodeManagerOptions.registerSetRegularOutputChannelListener(
- new SetToDefaultSourceListener(&d_managedRegularChannel), true));
- d_listenerRegistrations->add(
- nodeManagerOptions.registerSetDiagnosticOutputChannelListener(
+ opts.registerSetDiagnosticOutputChannelListener(
new SetToDefaultSourceListener(&d_managedDiagnosticChannel),
true));
- d_listenerRegistrations->add(
- nodeManagerOptions.registerDumpToFileNameListener(
- new SetToDefaultSourceListener(&d_managedDumpChannel), true));
+ d_listenerRegistrations->add(opts.registerDumpToFileNameListener(
+ new SetToDefaultSourceListener(&d_managedDumpChannel), true));
}
catch (OptionException& e)
{
d_smt.d_nodeManager->unsubscribeEvents(this);
}
- ResourceManager* getResourceManager() { return d_resourceManager; }
-
void spendResource(ResourceManager::Resource r)
{
- d_resourceManager->spendResource(r);
+ d_smt.getResourceManager()->spendResource(r);
}
ProcessAssertions* getProcessAssertions() { return &d_processor; }
}/* namespace CVC4::smt */
-SmtEngine::SmtEngine(ExprManager* em)
+SmtEngine::SmtEngine(ExprManager* em, Options* optr)
: d_context(new Context()),
d_userContext(new UserContext()),
d_userLevels(),
d_smtMode(SMT_MODE_START),
d_private(nullptr),
d_statisticsRegistry(nullptr),
- d_stats(nullptr)
-{
- SmtScope smts(this);
- d_originalOptions.copyValues(em->getOptions());
- d_private.reset(new smt::SmtEnginePrivate(*this));
+ d_stats(nullptr),
+ d_resourceManager(nullptr),
+ d_scope(nullptr)
+{
+ // !!!!!!!!!!!!!!!!!!!!!! temporary hack: this makes the current SmtEngine
+ // we are constructing the current SmtEngine in scope for the lifetime of
+ // this SmtEngine, or until another SmtEngine is constructed (that SmtEngine
+ // is then in scope during its lifetime). This is mostly to ensure that
+ // options are always in scope, for e.g. printing expressions, which rely
+ // on knowing the output language.
+ // Notice that the SmtEngine may spawn new SmtEngine "subsolvers" internally.
+ // These are created, used, and deleted in a modular fashion while not
+ // interleaving calls to the master SmtEngine. Thus the hack here does not
+ // break this use case.
+ // On the other hand, this hack breaks use cases where multiple SmtEngine
+ // objects are created by the user.
+ d_scope.reset(new SmtScope(this));
+ if (optr != nullptr)
+ {
+ // if we provided a set of options, copy their values to the options
+ // owned by this SmtEngine.
+ d_options.copyValues(*optr);
+ }
d_statisticsRegistry.reset(new StatisticsRegistry());
+ d_resourceManager.reset(
+ new ResourceManager(*d_statisticsRegistry.get(), d_options));
+ d_private.reset(new smt::SmtEnginePrivate(*this));
d_stats.reset(new SmtEngineStatistics());
- d_stats->d_resourceUnitsUsed.setData(
- d_private->getResourceManager()->getResourceUsage());
+ d_stats->d_resourceUnitsUsed.setData(d_resourceManager->getResourceUsage());
// The ProofManager is constructed before any other proof objects such as
// SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are
void SmtEngine::finishInit()
{
+ // Notice that finishInit is called when options are finalized. If we are
+ // parsing smt2, this occurs at the moment we enter "Assert mode", page 52
+ // of SMT-LIB 2.6 standard.
+
+ // Inialize the resource manager based on the options.
+ d_resourceManager->setHardLimit(options::hardLimit());
+ if (options::perCallResourceLimit() != 0)
+ {
+ d_resourceManager->setResourceLimit(options::perCallResourceLimit(), false);
+ }
+ if (options::cumulativeResourceLimit() != 0)
+ {
+ d_resourceManager->setResourceLimit(options::cumulativeResourceLimit(),
+ true);
+ }
+ if (options::perCallMillisecondLimit() != 0)
+ {
+ d_resourceManager->setTimeLimit(options::perCallMillisecondLimit(), false);
+ }
+ if (options::cumulativeMillisecondLimit() != 0)
+ {
+ d_resourceManager->setTimeLimit(options::cumulativeMillisecondLimit(),
+ true);
+ }
+ if (options::cpuTime())
+ {
+ d_resourceManager->useCPUTime(true);
+ }
+
// set the random seed
Random::getRandom().setSeed(options::seed());
// engine later (it is non-essential there)
d_theoryEngine.reset(new TheoryEngine(getContext(),
getUserContext(),
+ getResourceManager(),
d_private->d_iteRemover,
const_cast<const LogicInfo&>(d_logic)));
* are unregistered by the obsolete PropEngine object before registered
* again by the new PropEngine object */
d_propEngine.reset(nullptr);
- d_propEngine.reset(new PropEngine(getTheoryEngine(),
- getContext(),
- getUserContext(),
- d_private->getResourceManager()));
+ d_propEngine.reset(new PropEngine(
+ getTheoryEngine(), getContext(), getUserContext(), getResourceManager()));
Trace("smt-debug") << "Setting up theory engine..." << std::endl;
d_theoryEngine->setPropEngine(getPropEngine());
d_propEngine.reset(nullptr);
d_stats.reset(nullptr);
+ d_private.reset(nullptr);
+ // d_resourceManager must be destroyed before d_statisticsRegistry
+ d_resourceManager.reset(nullptr);
d_statisticsRegistry.reset(nullptr);
- d_private.reset(nullptr);
d_userContext.reset(nullptr);
d_context.reset(nullptr);
LogicInfo SmtEngine::getLogicInfo() const {
return d_logic;
}
+
LogicInfo SmtEngine::getUserLogicInfo() const
{
// Lock the logic to make sure that this logic can be queried. We create a
res.lock();
return res;
}
-void SmtEngine::setFilename(std::string filename) { d_filename = filename; }
+
+void SmtEngine::notifyStartParsing(std::string filename)
+{
+ d_filename = filename;
+
+ // Copy the original options. This is called prior to beginning parsing.
+ // Hence reset should revert to these options, which note is after reading
+ // the command line.
+ d_originalOptions.copyValues(d_options);
+}
+
std::string SmtEngine::getFilename() const { return d_filename; }
void SmtEngine::setLogicInternal()
{
void SmtEnginePrivate::finishInit()
{
- d_preprocessingPassContext.reset(new PreprocessingPassContext(
- &d_smt, d_resourceManager, &d_iteRemover, &d_propagator));
+ d_preprocessingPassContext.reset(
+ new PreprocessingPassContext(&d_smt, &d_iteRemover, &d_propagator));
// initialize the preprocessing passes
d_processor.finishInit(d_preprocessingPassContext.get());
Trace("smt") << "SmtEngine::check()" << endl;
- ResourceManager* resourceManager = d_private->getResourceManager();
-
- resourceManager->beginCall();
+ d_resourceManager->beginCall();
// Only way we can be out of resource is if cumulative budget is on
- if (resourceManager->cumulativeLimitOn() &&
- resourceManager->out()) {
- Result::UnknownExplanation why = resourceManager->outOfResources() ?
- Result::RESOURCEOUT : Result::TIMEOUT;
+ if (d_resourceManager->cumulativeLimitOn() && d_resourceManager->out())
+ {
+ Result::UnknownExplanation why = d_resourceManager->outOfResources()
+ ? Result::RESOURCEOUT
+ : Result::TIMEOUT;
return Result(Result::ENTAILMENT_UNKNOWN, why, d_filename);
}
Trace("smt") << "SmtEngine::check(): running check" << endl;
Result result = d_propEngine->checkSat();
- resourceManager->endCall();
- Trace("limit") << "SmtEngine::check(): cumulative millis " << resourceManager->getTimeUsage()
- << ", resources " << resourceManager->getResourceUsage() << endl;
-
+ d_resourceManager->endCall();
+ Trace("limit") << "SmtEngine::check(): cumulative millis "
+ << d_resourceManager->getTimeUsage() << ", resources "
+ << d_resourceManager->getResourceUsage() << endl;
return Result(result, d_filename);
}
return r;
} catch (UnsafeInterruptException& e) {
- AlwaysAssert(d_private->getResourceManager()->out());
- Result::UnknownExplanation why = d_private->getResourceManager()->outOfResources() ?
- Result::RESOURCEOUT : Result::TIMEOUT;
+ AlwaysAssert(d_resourceManager->out());
+ Result::UnknownExplanation why = d_resourceManager->outOfResources()
+ ? Result::RESOURCEOUT
+ : Result::TIMEOUT;
return Result(Result::SAT_UNKNOWN, why, d_filename);
}
}
Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl;
UnsatCore core = getUnsatCore();
- SmtEngine coreChecker(d_exprManager);
+ SmtEngine coreChecker(d_exprManager, &d_options);
+ coreChecker.setIsInternalSubsolver();
coreChecker.setLogic(getLogicInfo());
+ coreChecker.getOptions().set(options::checkUnsatCores, false);
+ coreChecker.getOptions().set(options::checkProofs, false);
PROOF(
std::vector<Command*>::const_iterator itg = d_defineCommands.begin();
Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i << endl;
coreChecker.assertFormula(*i);
}
- const bool checkUnsatCores = options::checkUnsatCores();
Result r;
try {
- options::checkUnsatCores.set(false);
- options::checkProofs.set(false);
r = coreChecker.checkSat();
} catch(...) {
- options::checkUnsatCores.set(checkUnsatCores);
throw;
}
Notice() << "SmtEngine::checkUnsatCore(): result is " << r << endl;
}
Trace("check-synth-sol") << "Starting new SMT Engine\n";
/* Start new SMT engine to check solutions */
- SmtEngine solChecker(d_exprManager);
+ SmtEngine solChecker(d_exprManager, &d_options);
+ solChecker.setIsInternalSubsolver();
solChecker.setLogic(getLogicInfo());
- setOption("check-synth-sol", SExpr("false"));
- setOption("sygus-rec-fun", SExpr("false"));
+ solChecker.getOptions().set(options::checkSynthSol, false);
+ solChecker.getOptions().set(options::sygusRecFun, false);
Trace("check-synth-sol") << "Retrieving assertions\n";
// Build conjecture from original assertions
Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j
<< ": make new SMT engine" << std::endl;
// Start new SMT engine to check solution
- SmtEngine abdChecker(d_exprManager);
+ SmtEngine abdChecker(d_exprManager, &d_options);
+ abdChecker.setIsInternalSubsolver();
abdChecker.setLogic(getLogicInfo());
Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j
<< ": asserting formulas" << std::endl;
Trace("sygus-abduct") << "SmtEngine::getAbduct: made conjecture : " << aconj
<< ", solving for " << d_sssf << std::endl;
// we generate a new smt engine to do the abduction query
- d_subsolver.reset(new SmtEngine(NodeManager::currentNM()->toExprManager()));
+ d_subsolver.reset(
+ new SmtEngine(NodeManager::currentNM()->toExprManager(), &d_options));
d_subsolver->setIsInternalSubsolver();
// get the logic
LogicInfo l = d_logic.getUnlockedCopy();
Options opts;
opts.copyValues(d_originalOptions);
this->~SmtEngine();
- NodeManager::fromExprManager(em)->getOptions().copyValues(opts);
- new(this) SmtEngine(em);
+ new (this) SmtEngine(em, &opts);
}
void SmtEngine::resetAssertions()
* statistics are unregistered by the obsolete PropEngine object before
* registered again by the new PropEngine object */
d_propEngine.reset(nullptr);
- d_propEngine.reset(new PropEngine(getTheoryEngine(),
- getContext(),
- getUserContext(),
- d_private->getResourceManager()));
+ d_propEngine.reset(new PropEngine(
+ getTheoryEngine(), getContext(), getUserContext(), getResourceManager()));
d_theoryEngine->setPropEngine(getPropEngine());
}
}
void SmtEngine::setResourceLimit(unsigned long units, bool cumulative) {
- d_private->getResourceManager()->setResourceLimit(units, cumulative);
+ d_resourceManager->setResourceLimit(units, cumulative);
}
void SmtEngine::setTimeLimit(unsigned long milis, bool cumulative) {
- d_private->getResourceManager()->setTimeLimit(milis, cumulative);
+ d_resourceManager->setTimeLimit(milis, cumulative);
}
unsigned long SmtEngine::getResourceUsage() const {
- return d_private->getResourceManager()->getResourceUsage();
+ return d_resourceManager->getResourceUsage();
}
unsigned long SmtEngine::getTimeUsage() const {
- return d_private->getResourceManager()->getTimeUsage();
+ return d_resourceManager->getTimeUsage();
}
unsigned long SmtEngine::getResourceRemaining() const
{
- return d_private->getResourceManager()->getResourceRemaining();
+ return d_resourceManager->getResourceRemaining();
}
unsigned long SmtEngine::getTimeRemaining() const
{
- return d_private->getResourceManager()->getTimeRemaining();
+ return d_resourceManager->getTimeRemaining();
+}
+
+NodeManager* SmtEngine::getNodeManager() const
+{
+ return d_exprManager->getNodeManager();
}
Statistics SmtEngine::getStatistics() const
}
string optionarg = value.getValue();
- Options& nodeManagerOptions = NodeManager::currentNM()->getOptions();
- nodeManagerOptions.setOption(key, optionarg);
+ d_options.setOption(key, optionarg);
}
void SmtEngine::setIsInternalSubsolver() { d_isInternalSubsolver = true; }
return SExpr(result);
}
- Options& nodeManagerOptions = NodeManager::currentNM()->getOptions();
- return SExpr::parseAtom(nodeManagerOptions.getOption(key));
+ return SExpr::parseAtom(d_options.getOption(key));
}
bool SmtEngine::getExpressionName(Expr e, std::string& name) const {
d_private->setExpressionName(e,name);
}
+Options& SmtEngine::getOptions() { return d_options; }
+
+const Options& SmtEngine::getOptions() const { return d_options; }
+
+ResourceManager* SmtEngine::getResourceManager()
+{
+ return d_resourceManager.get();
+}
+
void SmtEngine::setSygusConjectureStale()
{
if (d_private->d_sygusConjectureStale)
SMT_MODE_INTERPOL
};
- /** Construct an SmtEngine with the given expression manager. */
- SmtEngine(ExprManager* em);
+ /**
+ * Construct an SmtEngine with the given expression manager.
+ * If provided, optr is a pointer to a set of options that should initialize the values
+ * of the options object owned by this class.
+ */
+ SmtEngine(ExprManager* em, Options* optr = nullptr);
/** Destruct the SMT engine. */
~SmtEngine();
/** Is this an internal subsolver? */
bool isInternalSubsolver() const;
- /** set the input name */
- void setFilename(std::string filename);
+ /**
+ * Notify that we are now parsing the input with the given filename.
+ * This call sets the filename maintained by this SmtEngine for bookkeeping
+ * and also makes a copy of the current options of this SmtEngine. This
+ * is required so that the SMT-LIB command (reset) returns the SmtEngine
+ * to a state where its options were prior to parsing but after e.g.
+ * reading command line options.
+ */
+ void notifyStartParsing(std::string filename);
/** return the input name (if any) */
std::string getFilename() const;
/** Permit access to the underlying ExprManager. */
ExprManager* getExprManager() const { return d_exprManager; }
+ /** Permit access to the underlying NodeManager. */
+ NodeManager* getNodeManager() const;
+
/** Export statistics from this SmtEngine. */
Statistics getStatistics() const;
*/
void setExpressionName(Expr e, const std::string& name);
+ /** Get the options object (const and non-const versions) */
+ Options& getOptions();
+ const Options& getOptions() const;
+
+ /** Get the resource manager of this SMT engine */
+ ResourceManager* getResourceManager();
/* ....................................................................... */
private:
/* ....................................................................... */
std::unique_ptr<smt::SmtEngineStatistics> d_stats;
+ /** The options object */
+ Options d_options;
+ /**
+ * Manager for limiting time and abstract resource usage.
+ */
+ std::unique_ptr<ResourceManager> d_resourceManager;
+ /**
+ * The global scope object. Upon creation of this SmtEngine, it becomes the
+ * SmtEngine in scope. It says the SmtEngine in scope until it is destructed,
+ * or another SmtEngine is created.
+ */
+ std::unique_ptr<smt::SmtScope> d_scope;
/*---------------------------- sygus commands ---------------------------*/
/**
#endif /* IS_PROOFS_BUILD */
}
+ResourceManager* currentResourceManager()
+{
+ return s_smtEngine_current->getResourceManager();
+}
+
SmtScope::SmtScope(const SmtEngine* smt)
: NodeManagerScope(smt->d_nodeManager),
- d_oldSmtEngine(s_smtEngine_current) {
+ d_oldSmtEngine(s_smtEngine_current),
+ d_optionsScope(smt ? &const_cast<SmtEngine*>(smt)->getOptions() : nullptr)
+{
Assert(smt != NULL);
s_smtEngine_current = const_cast<SmtEngine*>(smt);
Debug("current") << "smt scope: " << s_smtEngine_current << std::endl;
#include "expr/node_manager.h"
+#include "options/options.h"
+
namespace CVC4 {
class ProofManager;
// FIXME: Maybe move into SmtScope?
ProofManager* currentProofManager();
-class SmtScope : public NodeManagerScope {
- /** The old NodeManager, to be restored on destruction. */
- SmtEngine* d_oldSmtEngine;
-
-public:
- SmtScope(const SmtEngine* smt);
- ~SmtScope();
+/** get the current resource manager */
+ResourceManager* currentResourceManager();
- /**
- * This returns the StatisticsRegistry attached to the currently in scope
- * SmtEngine.
- */
- static StatisticsRegistry* currentStatisticsRegistry();
+class SmtScope : public NodeManagerScope
+{
+ public:
+ SmtScope(const SmtEngine* smt);
+ ~SmtScope();
+ /**
+ * This returns the StatisticsRegistry attached to the currently in scope
+ * SmtEngine.
+ */
+ static StatisticsRegistry* currentStatisticsRegistry();
+ private:
+ /** The old SmtEngine, to be restored on destruction. */
+ SmtEngine* d_oldSmtEngine;
+ /** Options scope */
+ Options::OptionsScope d_optionsScope;
};/* class SmtScope */
#include "proof/bitvector_proof.h"
#include "prop/bv_sat_solver_notify.h"
#include "prop/sat_solver_types.h"
+#include "smt/smt_engine_scope.h"
#include "theory/bv/bitblast/bitblast_strategies_template.h"
#include "theory/theory_registrar.h"
#include "theory/valuation.h"
#include "util/resource_manager.h"
-
namespace CVC4 {
namespace theory {
namespace bv {
void notify(prop::SatClause& clause) override {}
void spendResource(ResourceManager::Resource r) override
{
- NodeManager::currentResourceManager()->spendResource(r);
+ smt::currentResourceManager()->spendResource(r);
}
void safePoint(ResourceManager::Resource r) override {}
default: Unreachable() << "Unknown SAT solver type";
}
d_satSolver.reset(solver);
- ResourceManager* rm = NodeManager::currentResourceManager();
+ ResourceManager* rm = smt::currentResourceManager();
d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(),
d_bitblastingRegistrar.get(),
d_nullContext.get(),
d_satSolver.reset(
prop::SatSolverFactory::createMinisat(c, smtStatisticsRegistry(), name));
- ResourceManager* rm = NodeManager::currentResourceManager();
+ ResourceManager* rm = smt::currentResourceManager();
d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(),
d_nullRegistrar.get(),
d_nullContext.get(),
// recreate sat solver
d_satSolver.reset(
prop::SatSolverFactory::createMinisat(d_ctx, smtStatisticsRegistry()));
- ResourceManager* rm = NodeManager::currentResourceManager();
+ ResourceManager* rm = smt::currentResourceManager();
d_cnfStream.reset(new prop::TseitinCnfStream(
d_satSolver.get(), d_nullRegistrar.get(), d_nullContext.get(), rm));
d_satSolverNotify.reset(
// verify it if applicable
if (options::sygusRewSynthCheck())
{
- NodeManager* nm = NodeManager::currentNM();
-
Node crr = solbr.eqNode(eq_solr).negate();
Trace("rr-check") << "Check candidate rewrite : " << crr << std::endl;
// Notice we don't set produce-models. rrChecker takes the same
// options as the SmtEngine we belong to, where we ensure that
// produce-models is set.
- bool needExport = false;
-
- // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
- // This is only temporarily until we have separate options for each
- // SmtEngine instance. We should reuse the same ExprManager with
- // a different SmtEngine (and different options) here, eventually.
- // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
- api::Solver slv(&nm->getOptions());
- ExprManager* em = slv.getExprManager();
- SmtEngine* rrChecker = slv.getSmtEngine();
- ExprManagerMapCollection varMap;
- initializeChecker(rrChecker, em, varMap, crr, needExport);
+ std::unique_ptr<SmtEngine> rrChecker;
+ initializeChecker(rrChecker, crr);
Result r = rrChecker->checkSat();
Trace("rr-check") << "...result : " << r << std::endl;
if (r.asSatisfiabilityResult().isSat() == Result::SAT)
if (val.isNull())
{
Assert(!refv.isNull() && refv.getKind() != BOUND_VARIABLE);
- if (needExport)
- {
- Expr erefv = refv.toExpr().exportTo(em, varMap);
- val = Node::fromExpr(rrChecker->getValue(erefv).exportTo(
- nm->toExprManager(), varMap));
- }
- else
- {
- val = Node::fromExpr(rrChecker->getValue(refv.toExpr()));
- }
+ val = Node::fromExpr(rrChecker->getValue(refv.toExpr()));
}
Trace("rr-check") << " " << v << " -> " << val << std::endl;
pt.push_back(val);
return n.substitute(sfvs.begin(), sfvs.end(), sks.begin(), sks.end());
}
-void ExprMiner::initializeChecker(SmtEngine* checker,
- ExprManager* em,
- ExprManagerMapCollection& varMap,
- Node query,
- bool& needExport)
+void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
+ Node query)
{
// Convert bound variables to skolems. This ensures the satisfiability
// check is ground.
Node squery = convertToSkolem(query);
- if (options::sygusExprMinerCheckUseExport())
- {
- initializeSubsolverWithExport(checker,
- em,
- varMap,
- squery.toExpr(),
- true,
- options::sygusExprMinerCheckTimeout());
- checker->setOption("sygus-rr-synth-input", false);
- checker->setOption("input-language", "smt2");
- needExport = true;
- }
- else
- {
- initializeSubsolver(checker, squery.toExpr());
- needExport = false;
- }
+ initializeSubsolver(checker, squery.toExpr());
+ // also set the options
+ checker->setOption("sygus-rr-synth-input", false);
+ checker->setOption("input-language", "smt2");
}
Result ExprMiner::doCheck(Node query)
return Result(Result::SAT);
}
}
- // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
- // This is only temporarily until we have separate options for each
- // SmtEngine instance. We should reuse the same ExprManager with
- // a different SmtEngine (and different options) here, eventually.
- // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
- NodeManager* nm = NodeManager::currentNM();
- bool needExport = false;
- api::Solver slv(&nm->getOptions());
- ExprManager* em = slv.getExprManager();
- SmtEngine* smte = slv.getSmtEngine();
- ExprManagerMapCollection varMap;
- initializeChecker(smte, em, varMap, queryr, needExport);
+ std::unique_ptr<SmtEngine> smte;
+ initializeChecker(smte, query);
return smte->checkSat();
}
* This function initializes the smt engine smte to check the satisfiability
* of the argument "query", which is a formula whose free variables (of
* kind BOUND_VARIABLE) are a subset of d_vars.
- *
- * The arguments em and varMap are used for supporting cases where we
- * want smte to use a different expression manager instead of the current
- * expression manager. The motivation for this so that different options can
- * be set for the subcall.
- *
- * We update the flag needExport to true if smte is using the expression
- * manager em. In this case, subsequent expressions extracted from smte
- * (for instance, model values) must be exported to the current expression
- * manager.
*/
- void initializeChecker(SmtEngine* smte,
- ExprManager* em,
- ExprManagerMapCollection& varMap,
- Node query,
- bool& needExport);
+ void initializeChecker(std::unique_ptr<SmtEngine>& smte, Node query);
/**
* Run the satisfiability check on query and return the result
* (sat/unsat/unknown).
if (options::sygusQueryGenCheck())
{
Trace("sygus-qgen-check") << " query: check " << qy << "..." << std::endl;
- NodeManager* nm = NodeManager::currentNM();
// make the satisfiability query
- //
- // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
- // This is only temporarily until we have separate options for each
- // SmtEngine instance. We should reuse the same ExprManager with
- // a different SmtEngine (and different options) here, eventually.
- // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
- bool needExport = false;
- api::Solver slv(&nm->getOptions());
- ExprManager* em = slv.getExprManager();
- SmtEngine* queryChecker = slv.getSmtEngine();
- ExprManagerMapCollection varMap;
- initializeChecker(queryChecker, em, varMap, qy, needExport);
+ std::unique_ptr<SmtEngine> queryChecker;
+ initializeChecker(queryChecker, qy);
Result r = queryChecker->checkSat();
Trace("sygus-qgen-check") << " query: ...got : " << r << std::endl;
if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
}
else
{
- Options& nodeManagerOptions = nm->getOptions();
- std::ostream* nodeManagerOut = nodeManagerOptions.getOut();
- (*nodeManagerOut) << "; (filtered " << (d_isStrong ? s : s.negate())
- << ")" << std::endl;
+ Options& opts = smt::currentSmtEngine()->getOptions();
+ std::ostream* smtOut = opts.getOut();
+ (*smtOut) << "; (filtered " << (d_isStrong ? s : s.negate()) << ")"
+ << std::endl;
}
}
d_curr_sols.clear();
#include "theory/quantifiers/term_enumeration.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
+#include "theory/smt_engine_subsolver.h"
using namespace CVC4::kind;
siq = nm->mkNode(FORALL, siq[0], siq[1], n_attr);
}
// solve the single invocation conjecture using a fresh copy of SMT engine
- SmtEngine siSmt(nm->toExprManager());
- siSmt.setLogic(smt::currentSmtEngine()->getLogicInfo());
- siSmt.assertFormula(siq.toExpr());
- Result r = siSmt.checkSat();
+ std::unique_ptr<SmtEngine> siSmt;
+ initializeSubsolver(siSmt, siq);
+ Result r = siSmt->checkSat();
Trace("sygus-si") << "Result: " << r << std::endl;
if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
{
}
// now, get the instantiations
std::vector<Expr> qs;
- siSmt.getInstantiatedQuantifiedFormulas(qs);
+ siSmt->getInstantiatedQuantifiedFormulas(qs);
Assert(qs.size() <= 1);
// track the instantiations, as solution construction is based on this
Trace("sygus-si") << "#instantiated quantified formulas=" << qs.size()
TNode qn = Node::fromExpr(q);
Assert(qn.getKind() == FORALL);
std::vector<std::vector<Expr> > tvecs;
- siSmt.getInstantiationTermVectors(q, tvecs);
+ siSmt->getInstantiationTermVectors(q, tvecs);
Trace("sygus-si") << "#instantiations of " << q << "=" << tvecs.size()
<< std::endl;
std::vector<Node> vars;
{
addSuccess = false;
// try a new core
- std::unique_ptr<SmtEngine> checkSol(
- new SmtEngine(NodeManager::currentNM()->toExprManager()));
- initializeSubsolver(checkSol.get());
+ std::unique_ptr<SmtEngine> checkSol;
+ initializeSubsolver(checkSol);
Trace("sygus-ccore") << "----- Check candidate " << an << std::endl;
std::vector<Node> rasserts = asserts;
rasserts.push_back(d_sc);
{
// In terms of Variant #2, this is the check "if S ^ U is unsat"
Trace("sygus-ccore") << "----- Check side condition" << std::endl;
- std::unique_ptr<SmtEngine> checkSc(
- new SmtEngine(NodeManager::currentNM()->toExprManager()));
- initializeSubsolver(checkSc.get());
+ std::unique_ptr<SmtEngine> checkSc;
+ initializeSubsolver(checkSc);
std::vector<Node> scasserts;
scasserts.insert(scasserts.end(), uasserts.begin(), uasserts.end());
scasserts.push_back(d_sc);
return false;
}
- NodeManager* nm = NodeManager::currentNM();
Trace("sygus-repair-const") << "Get first-order query..." << std::endl;
Node fo_body =
getFoQuery(sygusBody, candidates, candidate_skeletons, sk_vars);
Trace("sygus-engine") << "Repairing previous solution..." << std::endl;
// make the satisfiability query
- //
- // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
- // This is only temporarily until we have separate options for each
- // SmtEngine instance. We should reuse the same ExprManager with
- // a different SmtEngine (and different options) here, eventually.
- // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
- bool needExport = true;
- std::unique_ptr<SmtEngine> simpleSmte;
- std::unique_ptr<api::Solver> slv;
- ExprManager* em = nullptr;
- SmtEngine* repcChecker = nullptr;
- ExprManagerMapCollection varMap;
-
- if (options::sygusRepairConstTimeout.wasSetByUser())
- {
- // To support a separate timeout for the subsolver, we need to create
- // a separate ExprManager with its own options. This requires that
- // the expressions sent to the subsolver can be exported from on
- // ExprManager to another.
- slv.reset(new api::Solver(&nm->getOptions()));
- em = slv->getExprManager();
- repcChecker = slv->getSmtEngine();
- initializeSubsolverWithExport(repcChecker,
- em,
- varMap,
- fo_body.toExpr(),
- true,
- options::sygusRepairConstTimeout());
- // renable options disabled by sygus
- repcChecker->setOption("miniscope-quant", true);
- repcChecker->setOption("miniscope-quant-fv", true);
- repcChecker->setOption("quant-split", true);
- }
- else
- {
- needExport = false;
- em = nm->toExprManager();
- simpleSmte.reset(new SmtEngine(em));
- repcChecker = simpleSmte.get();
- initializeSubsolver(repcChecker, fo_body.toExpr());
- }
-
+ std::unique_ptr<SmtEngine> repcChecker;
+ // initialize the subsolver using the standard method
+ initializeSubsolver(repcChecker,
+ fo_body.toExpr(),
+ options::sygusRepairConstTimeout.wasSetByUser(),
+ options::sygusRepairConstTimeout());
+ // renable options disabled by sygus
+ repcChecker->setOption("miniscope-quant", true);
+ repcChecker->setOption("miniscope-quant-fv", true);
+ repcChecker->setOption("quant-split", true);
+ // check satisfiability
Result r = repcChecker->checkSat();
Trace("sygus-repair-const") << "...got : " << r << std::endl;
if (r.asSatisfiabilityResult().isSat() == Result::UNSAT
{
Assert(d_sk_to_fo.find(v) != d_sk_to_fo.end());
Node fov = d_sk_to_fo[v];
- Node fov_m;
- if (needExport)
- {
- Expr e_fov = fov.toExpr().exportTo(em, varMap);
- fov_m = Node::fromExpr(
- repcChecker->getValue(e_fov).exportTo(nm->toExprManager(), varMap));
- }
- else
- {
- fov_m = Node::fromExpr(repcChecker->getValue(fov.toExpr()));
- }
+ Node fov_m = Node::fromExpr(repcChecker->getValue(fov.toExpr()));
Trace("sygus-repair-const") << " " << fov << " = " << fov_m << std::endl;
// convert to sygus
Node fov_m_to_sygus = d_tds->getProxyVariable(v.getType(), fov_m);
#include "options/quantifiers_options.h"
#include "printer/printer.h"
#include "prop/prop_engine.h"
+#include "smt/smt_engine_scope.h"
#include "smt/smt_statistics_registry.h"
#include "theory/datatypes/sygus_datatype_utils.h"
#include "theory/quantifiers/first_order_model.h"
// we have generated a solution, print it
// get the current output stream
// this output stream should coincide with wherever --dump-synth is output on
- Options& nodeManagerOptions = NodeManager::currentNM()->getOptions();
- printSynthSolution(*nodeManagerOptions.getOut());
+ Options& sopts = smt::currentSmtEngine()->getOptions();
+ printSynthSolution(*sopts.getOut());
excludeCurrentSolution(enums, values);
}
if (!sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation())
{
// create new smt engine to do quantifier elimination
- std::unique_ptr<SmtEngine> smt_qe(
- new SmtEngine(NodeManager::currentNM()->toExprManager()));
- initializeSubsolver(smt_qe.get());
+ std::unique_ptr<SmtEngine> smt_qe;
+ initializeSubsolver(smt_qe);
Trace("cegqi-qep") << "Property is non-ground single invocation, run "
"QE to obtain single invocation."
<< std::endl;
#include "options/base_options.h"
#include "options/quantifiers_options.h"
#include "printer/printer.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
#include "theory/quantifiers/lazy_trie.h"
#include "util/bitvector.h"
#include "util/random.h"
return;
}
// we have detected unsoundness in the rewriter
- Options& nodeManagerOptions = NodeManager::currentNM()->getOptions();
- std::ostream* out = nodeManagerOptions.getOut();
+ Options& sopts = smt::currentSmtEngine()->getOptions();
+ std::ostream* out = sopts.getOut();
(*out) << "(unsound-rewrite " << bv << " " << bvr << ")" << std::endl;
// debugging information
(*out) << "Terms are not equivalent for : " << std::endl;
ResourceManager* rm = NULL;
bool hasSmtEngine = smt::smtEngineInScope();
if (hasSmtEngine) {
- rm = NodeManager::currentResourceManager();
+ rm = smt::currentResourceManager();
}
// Rewrite until the stack is empty
for (;;){
return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK);
}
-void initializeSubsolver(SmtEngine* smte)
+void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
+ Node query,
+ bool needsTimeout,
+ unsigned long timeout)
{
+ NodeManager* nm = NodeManager::currentNM();
+ SmtEngine* smtCurr = smt::currentSmtEngine();
+ // must copy the options
+ smte.reset(new SmtEngine(nm->toExprManager(), &smtCurr->getOptions()));
smte->setIsInternalSubsolver();
- smte->setLogic(smt::currentSmtEngine()->getLogicInfo());
-}
-
-void initializeSubsolverWithExport(SmtEngine* smte,
- ExprManager* em,
- ExprManagerMapCollection& varMap,
- Node query,
- bool needsTimeout,
- unsigned long timeout)
-{
- // To support a separate timeout for the subsolver, we need to use
- // a separate ExprManager with its own options. This requires that
- // the expressions sent to the subsolver can be exported from on
- // ExprManager to another. If the export fails, we throw an
- // OptionException.
- try
+ smte->setLogic(smtCurr->getLogicInfo());
+ if (needsTimeout)
{
- smte->setIsInternalSubsolver();
- if (needsTimeout)
- {
- smte->setTimeLimit(timeout, true);
- }
- smte->setLogic(smt::currentSmtEngine()->getLogicInfo());
- Expr equery = query.toExpr().exportTo(em, varMap);
- smte->assertFormula(equery);
+ smte->setTimeLimit(timeout, true);
}
- catch (const CVC4::ExportUnsupportedException& e)
+ smte->setLogic(smt::currentSmtEngine()->getLogicInfo());
+ if (!query.isNull())
{
- std::stringstream msg;
- msg << "Unable to export " << query
- << " but exporting expressions is "
- "required for a subsolver.";
- throw OptionException(msg.str());
+ smte->assertFormula(query.toExpr());
}
}
-void initializeSubsolver(SmtEngine* smte, Node query)
-{
- initializeSubsolver(smte);
- smte->assertFormula(query.toExpr());
-}
-
-Result checkWithSubsolver(SmtEngine* smte, Node query)
+Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte,
+ Node query,
+ bool needsTimeout,
+ unsigned long timeout)
{
Assert(query.getType().isBoolean());
Result r = quickCheck(query);
{
return r;
}
- initializeSubsolver(smte, query);
+ initializeSubsolver(smte, query, needsTimeout, timeout);
return smte->checkSat();
}
}
return r;
}
-
- // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
- // This is only temporarily until we have separate options for each
- // SmtEngine instance. We should reuse the same ExprManager with
- // a different SmtEngine (and different options) here, eventually.
- // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
- std::unique_ptr<SmtEngine> simpleSmte;
- std::unique_ptr<api::Solver> slv;
- ExprManager* em = nullptr;
- SmtEngine* smte = nullptr;
- ExprManagerMapCollection varMap;
- NodeManager* nm = NodeManager::currentNM();
- bool needsExport = false;
- if (needsTimeout)
- {
- slv.reset(new api::Solver(&nm->getOptions()));
- em = slv->getExprManager();
- smte = slv->getSmtEngine();
- needsExport = true;
- initializeSubsolverWithExport(
- smte, em, varMap, query, needsTimeout, timeout);
- }
- else
- {
- em = nm->toExprManager();
- simpleSmte.reset(new SmtEngine(em));
- smte = simpleSmte.get();
- initializeSubsolver(smte, query);
- }
+ std::unique_ptr<SmtEngine> smte;
+ initializeSubsolver(smte, query, needsTimeout, timeout);
r = smte->checkSat();
if (r.asSatisfiabilityResult().isSat() == Result::SAT)
{
for (const Node& v : vars)
{
- Expr val;
- if (needsExport)
- {
- Expr ev = v.toExpr().exportTo(em, varMap);
- val = smte->getValue(ev).exportTo(nm->toExprManager(), varMap);
- }
- else
- {
- val = smte->getValue(v.toExpr());
- }
+ Expr val = smte->getValue(v.toExpr());
modelVals.push_back(Node::fromExpr(val));
}
}
namespace theory {
/**
- * This function initializes the smt engine smte as a subsolver, e.g. it
- * creates a new SMT engine and sets the options of the current SMT engine.
- */
-void initializeSubsolver(SmtEngine* smte);
-
-/**
- * Initialize Smt subsolver with exporting
- *
* This function initializes the smt engine smte to check the satisfiability
* of the argument "query".
*
- * The arguments em and varMap are used for supporting cases where we
- * want smte to use a different expression manager instead of the current
- * expression manager. The motivation for this so that different options can
- * be set for the subcall.
- *
- * Notice that subsequent expressions extracted from smte (for instance, model
- * values) must be exported to the current expression
- * manager.
- *
* @param smte The smt engine pointer to initialize
- * @param em Reference to the expression manager used by smte
- * @param varMap Map used for exporting expressions
- * @param query The query to check
+ * @param query The query to check (if provided)
* @param needsTimeout Whether we would like to set a timeout
* @param timeout The timeout (in milliseconds)
*/
-void initializeSubsolverWithExport(SmtEngine* smte,
- ExprManager* em,
- ExprManagerMapCollection& varMap,
- Node query,
- bool needsTimeout = false,
- unsigned long timeout = 0);
-
-/**
- * This function initializes the smt engine smte to check the satisfiability
- * of the argument "query", without exporting expressions.
- *
- * Notice that is not possible to set a timeout value currently without
- * exporting since the Options and ExprManager are tied together.
- * TODO: eliminate this dependency (cvc4-projects #120).
- */
-void initializeSubsolver(SmtEngine* smte, Node query);
+void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
+ Node query = Node::null(),
+ bool needsTimeout = false,
+ unsigned long timeout = 0);
/**
* This returns the result of checking the satisfiability of formula query.
* If necessary, smte is initialized to the SMT engine that checked its
* satisfiability.
*/
-Result checkWithSubsolver(SmtEngine* smte, Node query);
+Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte,
+ Node query,
+ bool needsTimeout = false,
+ unsigned long timeout = 0);
/**
* This returns the result of checking the satisfiability of formula query.
TheoryEngine::TheoryEngine(context::Context* context,
context::UserContext* userContext,
+ ResourceManager* rm,
RemoveTermFormulas& iteRemover,
const LogicInfo& logicInfo)
: d_propEngine(nullptr),
d_true(),
d_false(),
d_interrupted(false),
- d_resourceManager(NodeManager::currentResourceManager()),
+ d_resourceManager(rm),
d_inPreregister(false),
d_factsAsserted(context, false),
d_preRegistrationVisitor(this, context),
/** Constructs a theory engine */
TheoryEngine(context::Context* context,
context::UserContext* userContext,
+ ResourceManager* rm,
RemoveTermFormulas& iteRemover,
const LogicInfo& logic);
; EXPECT: unsat
-; COMMAND-LINE: --sygus-inference --sygus-qe-preproc
+; COMMAND-LINE: --sygus-inference --sygus-qe-preproc --no-check-unsat-cores
(set-logic ALL)
(declare-fun a () Real)
(declare-fun b () Real)
void testGetInfo(api::Solver* solver, const char* s)
{
- ParserBuilder pb(
- solver, "<internal>", solver->getExprManager()->getOptions());
+ ParserBuilder pb(solver, "<internal>", solver->getOptions());
Parser* p = pb.withStringInput(string("(get-info ") + s + ")").build();
assert(p != NULL);
Command* c = p->nextCommand();
void GrammarBlack::setUp() { d_solver.reset(new Solver()); }
-void GrammarBlack::tearDown() {}
+void GrammarBlack::tearDown() { d_solver.reset(nullptr); }
void GrammarBlack::testAddRule()
{
{
public:
void setUp() { d_solver.reset(new Solver()); }
- void tearDown() override {}
+ void tearDown() override { d_solver.reset(nullptr); }
void testIsNull();
void testEq();
void SolverBlack::setUp() { d_solver.reset(new Solver()); }
-void SolverBlack::tearDown() {}
+void SolverBlack::tearDown() { d_solver.reset(nullptr); }
void SolverBlack::testGetBooleanSort()
{
#include <string>
#include <vector>
+#include "api/cvc4cpp.h"
+#include "smt/smt_engine.h"
#include "expr/expr_manager.h"
#include "expr/node.h"
#include "expr/node_builder.h"
class NodeBlack : public CxxTest::TestSuite {
private:
- Options opts;
NodeManager* d_nodeManager;
- NodeManagerScope* d_scope;
- TypeNode* d_booleanType;
- TypeNode* d_realType;
-
+ api::Solver* d_slv;
public:
void setUp() override
{
+ // setup a SMT engine so that options are in scope
+ Options opts;
char* argv[2];
argv[0] = strdup("");
argv[1] = strdup("--output-lang=ast");
free(argv[0]);
free(argv[1]);
- d_nodeManager = new NodeManager(NULL, opts);
- d_scope = new NodeManagerScope(d_nodeManager);
- d_booleanType = new TypeNode(d_nodeManager->booleanType());
- d_realType = new TypeNode(d_nodeManager->realType());
+ d_slv = new api::Solver(&opts);
+ d_nodeManager = d_slv->getSmtEngine()->getNodeManager();
}
- void tearDown() override
- {
- delete d_realType;
- delete d_booleanType;
- delete d_scope;
- delete d_nodeManager;
+ void tearDown() override {
+ delete d_slv;
}
bool imp(bool a, bool b) const { return (!a) || (b); }
void testOperatorEquals() {
Node a, b, c;
- b = d_nodeManager->mkSkolem("b", *d_booleanType);
+ b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
a = b;
c = a;
- Node d = d_nodeManager->mkSkolem("d", *d_booleanType);
+ Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType());
TS_ASSERT(a == a);
TS_ASSERT(a == b);
void testOperatorNotEquals() {
Node a, b, c;
- b = d_nodeManager->mkSkolem("b", *d_booleanType);
+ b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
a = b;
c = a;
- Node d = d_nodeManager->mkSkolem("d", *d_booleanType);
+ Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType());
/*structed assuming operator == works */
TS_ASSERT(iff(a != a, !(a == a)));
void testOperatorAssign() {
Node a, b;
Node c = d_nodeManager->mkNode(
- NOT, d_nodeManager->mkSkolem("c", *d_booleanType));
+ NOT, d_nodeManager->mkSkolem("c", d_nodeManager->booleanType()));
b = c;
TS_ASSERT(b == c);
void testIteNode() {
/*Node iteNode(const Node& thenpart, const Node& elsepart) const;*/
- Node a = d_nodeManager->mkSkolem("a", *d_booleanType);
- Node b = d_nodeManager->mkSkolem("b", *d_booleanType);
+ Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
+ Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
Node cnd = d_nodeManager->mkNode(OR, a, b);
Node thenBranch = d_nodeManager->mkConst(true);
void testGetKind() {
/*inline Kind getKind() const; */
- Node a = d_nodeManager->mkSkolem("a", *d_booleanType);
- Node b = d_nodeManager->mkSkolem("b", *d_booleanType);
+ Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
+ Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
Node n = d_nodeManager->mkNode(NOT, a);
TS_ASSERT(NOT == n.getKind());
n = d_nodeManager->mkNode(EQUAL, a, b);
TS_ASSERT(EQUAL == n.getKind());
- Node x = d_nodeManager->mkSkolem("x", *d_realType);
- Node y = d_nodeManager->mkSkolem("y", *d_realType);
+ Node x = d_nodeManager->mkSkolem("x", d_nodeManager->realType());
+ Node y = d_nodeManager->mkSkolem("y", d_nodeManager->realType());
n = d_nodeManager->mkNode(PLUS, x, y);
TS_ASSERT(PLUS == n.getKind());
// test iterators
void testIterator() {
NodeBuilder<> b;
- Node x = d_nodeManager->mkSkolem("x", *d_booleanType);
- Node y = d_nodeManager->mkSkolem("y", *d_booleanType);
- Node z = d_nodeManager->mkSkolem("z", *d_booleanType);
+ Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
+ Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType());
+ Node z = d_nodeManager->mkSkolem("z", d_nodeManager->booleanType());
Node n = b << x << y << z << kind::AND;
{ // iterator
// This is for demonstrating what a certain type of user error looks like.
// Node level0(){
// NodeBuilder<> nb(kind::AND);
- // Node x = d_nodeManager->mkSkolem("x", *d_booleanType);
+ // Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
// nb << x;
// nb << x;
// return Node(nb.constructNode());
d_solver.reset(new api::Solver(&d_options));
}
- void tearDown() {
- }
+ void tearDown() { d_solver.reset(nullptr); }
private:
InputLanguage d_lang;
d_satSolver = new FakeSatSolver();
d_cnfContext = new context::Context();
d_cnfRegistrar = new theory::TheoryRegistrar(d_theoryEngine);
- ResourceManager * rm = d_nodeManager->getResourceManager();
+ ResourceManager* rm = d_smt->getResourceManager();
d_cnfStream = new CVC4::prop::TseitinCnfStream(
d_satSolver, d_cnfRegistrar, d_cnfContext, rm);
}
{
Options opts;
opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
- d_em = new ExprManager(opts);
+ d_em = new ExprManager;
d_nm = NodeManager::fromExprManager(d_em);
- d_smt = new SmtEngine(d_em);
+ d_smt = new SmtEngine(d_em, &opts);
d_scope = new SmtScope(d_smt);
d_smt->finalOptionsAreSet();
}
{
Options opts;
opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
- d_em = new ExprManager(opts);
- d_smt = new SmtEngine(d_em);
+ d_em = new ExprManager;
+ d_smt = new SmtEngine(d_em, &opts);
d_scope = new SmtScope(d_smt);
d_smt->finalOptionsAreSet();
d_rewriter = new ExtendedRewriter(true);
{
Options opts;
opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
- d_em = new ExprManager(opts);
- d_smt = new SmtEngine(d_em);
+ d_em = new ExprManager;
+ d_smt = new SmtEngine(d_em, &opts);
d_scope = new SmtScope(d_smt);
d_smt->finalOptionsAreSet();
{
Options opts;
opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
- d_em = new ExprManager(opts);
- d_smt = new SmtEngine(d_em);
+ d_em = new ExprManager;
+ d_smt = new SmtEngine(d_em, &opts);
d_scope = new SmtScope(d_smt);
d_nm = NodeManager::currentNM();
projects / cvc5.git / commitdiff