Now, SMT models do not store an internal list of commands, and are not dependent on a reference to SmtEngine.
The next cleanup step will be to merge OutputManager, DumpManager, and SmtEngineNodeListener.
/* substituteUnderQuantifiers = */ false);
Trace("check-model") << "checkModel: Collect substitution..." << std::endl;
- for (size_t k = 0, ncmd = m->getNumCommands(); k < ncmd; ++k)
+ const std::vector<Node>& decTerms = m->getDeclaredTerms();
+ for (const Node& func : decTerms)
{
- const DeclareFunctionNodeCommand* c =
- dynamic_cast<const DeclareFunctionNodeCommand*>(m->getCommand(k));
- Notice() << "SmtEngine::checkModel(): model command " << k << " : "
- << m->getCommand(k)->toString() << std::endl;
- if (c == nullptr)
- {
- // we don't care about DECLARE-DATATYPES, DECLARE-SORT, ...
- Notice() << "SmtEngine::checkModel(): skipping..." << std::endl;
- continue;
- }
// We have a DECLARE-FUN:
//
// We'll first do some checks, then add to our substitution map
// the mapping: function symbol |-> value
- Node func = c->getFunction();
Node val = m->getValue(func);
Notice() << "SmtEngine::checkModel(): adding substitution: " << func
api::Sort sort)
: DeclarationDefinitionCommand(id),
d_func(func),
- d_sort(sort),
- d_printInModel(true),
- d_printInModelSetByUser(false)
+ d_sort(sort)
{
}
api::Term DeclareFunctionCommand::getFunction() const { return d_func; }
api::Sort DeclareFunctionCommand::getSort() const { return d_sort; }
-bool DeclareFunctionCommand::getPrintInModel() const { return d_printInModel; }
-bool DeclareFunctionCommand::getPrintInModelSetByUser() const
-{
- return d_printInModelSetByUser;
-}
-
-void DeclareFunctionCommand::setPrintInModel(bool p)
-{
- d_printInModel = p;
- d_printInModelSetByUser = true;
-}
void DeclareFunctionCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
{
DeclareFunctionCommand* dfc =
new DeclareFunctionCommand(d_symbol, d_func, d_sort);
- dfc->d_printInModel = d_printInModel;
- dfc->d_printInModelSetByUser = d_printInModelSetByUser;
return dfc;
}
protected:
api::Term d_func;
api::Sort d_sort;
- bool d_printInModel;
- bool d_printInModelSetByUser;
public:
DeclareFunctionCommand(const std::string& id, api::Term func, api::Sort sort);
api::Term getFunction() const;
api::Sort getSort() const;
- bool getPrintInModel() const;
- bool getPrintInModelSetByUser() const;
- void setPrintInModel(bool p);
void invoke(api::Solver* solver, SymbolManager* sm) override;
Command* clone() const override;
DumpManager::DumpManager(context::UserContext* u)
: d_fullyInited(false),
- d_modelGlobalCommands(),
- d_modelCommands(u),
d_dumpCommands()
{
}
DumpManager::~DumpManager()
{
d_dumpCommands.clear();
- d_modelCommandsAlloc.clear();
- d_modelGlobalCommands.clear();
}
void DumpManager::finishInit()
d_fullyInited = true;
}
-
-void DumpManager::resetAssertions() { d_modelGlobalCommands.clear(); }
+void DumpManager::resetAssertions()
+{
+ // currently, do nothing
+}
void DumpManager::addToModelCommandAndDump(const NodeCommand& c,
uint32_t flags,
const char* dumpTag)
{
Trace("smt") << "SMT addToModelCommandAndDump(" << c << ")" << std::endl;
- // If we aren't yet fully inited, the user might still turn on
- // produce-models. So let's keep any commands around just in
- // case. This is useful in two cases: (1) SMT-LIBv1 auto-declares
- // sort "U" in QF_UF before setLogic() is run and we still want to
- // support finding card(U) with --finite-model-find, and (2) to
- // decouple SmtEngine and ExprManager if the user does a few
- // ExprManager::mkSort() before SmtEngine::setOption("produce-models")
- // and expects to find their cardinalities in the model.
- if ((!d_fullyInited || options::produceModels())
- && (flags & ExprManager::VAR_FLAG_DEFINED) == 0)
- {
- if (flags & ExprManager::VAR_FLAG_GLOBAL)
- {
- d_modelGlobalCommands.push_back(std::unique_ptr<NodeCommand>(c.clone()));
- }
- else
- {
- NodeCommand* cc = c.clone();
- d_modelCommands.push_back(cc);
- // also remember for memory management purposes
- d_modelCommandsAlloc.push_back(std::unique_ptr<NodeCommand>(cc));
- }
- }
if (Dump.isOn(dumpTag))
{
if (d_fullyInited)
void DumpManager::setPrintFuncInModel(Node f, bool p)
{
Trace("setp-model") << "Set printInModel " << f << " to " << p << std::endl;
- for (std::unique_ptr<NodeCommand>& c : d_modelGlobalCommands)
- {
- DeclareFunctionNodeCommand* dfc =
- dynamic_cast<DeclareFunctionNodeCommand*>(c.get());
- if (dfc != NULL)
- {
- Node df = dfc->getFunction();
- if (df == f)
- {
- dfc->setPrintInModel(p);
- }
- }
- }
- for (NodeCommand* c : d_modelCommands)
- {
- DeclareFunctionNodeCommand* dfc =
- dynamic_cast<DeclareFunctionNodeCommand*>(c);
- if (dfc != NULL)
- {
- Node df = dfc->getFunction();
- if (df == f)
- {
- dfc->setPrintInModel(p);
- }
- }
- }
-}
-
-size_t DumpManager::getNumModelCommands() const
-{
- return d_modelCommands.size() + d_modelGlobalCommands.size();
-}
-
-const NodeCommand* DumpManager::getModelCommand(size_t i) const
-{
- Assert(i < getNumModelCommands());
- // index the global commands first, then the locals
- if (i < d_modelGlobalCommands.size())
- {
- return d_modelGlobalCommands[i].get();
- }
- return d_modelCommands[i - d_modelGlobalCommands.size()];
+ // TODO (cvc4-wishues/issues/75): implement
}
} // namespace smt
/**
* This utility is responsible for:
- * (1) storing information required for SMT-LIB queries such as get-model,
- * which requires knowing what symbols are declared and should be printed in
- * the model.
- * (2) implementing some dumping traces e.g. --dump=declarations.
+ * implementing some dumping traces e.g. --dump=declarations.
*/
class DumpManager
{
- typedef context::CDList<NodeCommand*> CommandList;
public:
DumpManager(context::UserContext* u);
* Set that function f should print in the model if and only if p is true.
*/
void setPrintFuncInModel(Node f, bool p);
- /** get number of commands to report in a model */
- size_t getNumModelCommands() const;
- /** get model command at index i */
- const NodeCommand* getModelCommand(size_t i) const;
private:
/** Fully inited */
bool d_fullyInited;
-
- /**
- * A list of commands that should be in the Model globally (i.e.,
- * regardless of push/pop). Only maintained if produce-models option
- * is on.
- */
- std::vector<std::unique_ptr<NodeCommand>> d_modelGlobalCommands;
-
- /**
- * A list of commands that should be in the Model locally (i.e.,
- * it is context-dependent on push/pop). Only maintained if
- * produce-models option is on.
- */
- CommandList d_modelCommands;
- /**
- * A list of model commands allocated to d_modelCommands at any time. This
- * is maintained for memory management purposes.
- */
- std::vector<std::unique_ptr<NodeCommand>> d_modelCommandsAlloc;
-
/**
* A vector of declaration commands waiting to be dumped out.
* Once the SmtEngine is fully initialized, we'll dump them.
namespace CVC4 {
namespace smt {
-Model::Model(SmtEngine& smt, theory::TheoryModel* tm)
- : d_smt(smt), d_isKnownSat(false), d_tmodel(tm)
+Model::Model(theory::TheoryModel* tm) : d_isKnownSat(false), d_tmodel(tm)
{
Assert(d_tmodel != nullptr);
}
std::ostream& operator<<(std::ostream& out, const Model& m) {
- smt::SmtScope smts(&m.d_smt);
expr::ExprDag::Scope scope(out, false);
Printer::getPrinter(options::outputLanguage())->toStream(out, m);
return out;
}
-size_t Model::getNumCommands() const
-{
- return d_smt.getDumpManager()->getNumModelCommands();
-}
-
-const NodeCommand* Model::getCommand(size_t i) const
-{
- return d_smt.getDumpManager()->getModelCommand(i);
-}
-
theory::TheoryModel* Model::getTheoryModel() { return d_tmodel; }
const theory::TheoryModel* Model::getTheoryModel() const { return d_tmodel; }
namespace CVC4 {
class SmtEngine;
-class NodeCommand;
namespace smt {
public:
/** construct */
- Model(SmtEngine& smt, theory::TheoryModel* tm);
+ Model(theory::TheoryModel* tm);
/** virtual destructor */
~Model() {}
- /** get the smt engine that this model is hooked up to */
- SmtEngine* getSmtEngine() { return &d_smt; }
- /** get the smt engine (as a pointer-to-const) that this model is hooked up to */
- const SmtEngine* getSmtEngine() const { return &d_smt; }
/** get the input name (file name, etc.) this model is associated to */
std::string getInputName() const { return d_inputName; }
/**
/** Does this model have approximations? */
bool hasApproximations() const;
//----------------------- end helper methods
- /** get number of commands to report */
- size_t getNumCommands() const;
- /** get command */
- const NodeCommand* getCommand(size_t i) const;
//----------------------- model declarations
/** Clear the current model declarations. */
void clearModelDeclarations();
const std::vector<Node>& getDeclaredTerms() const;
//----------------------- end model declarations
protected:
- /** The SmtEngine we're associated with */
- SmtEngine& d_smt;
/** the input name (file name, etc.) this model is associated to */
std::string d_inputName;
/**
TypeNode type)
: d_id(id),
d_fun(expr),
- d_type(type),
- d_printInModel(true),
- d_printInModelSetByUser(false)
+ d_type(type)
{
}
const Node& DeclareFunctionNodeCommand::getFunction() const { return d_fun; }
-bool DeclareFunctionNodeCommand::getPrintInModel() const
-{
- return d_printInModel;
-}
-
-bool DeclareFunctionNodeCommand::getPrintInModelSetByUser() const
-{
- return d_printInModelSetByUser;
-}
-
-void DeclareFunctionNodeCommand::setPrintInModel(bool p)
-{
- d_printInModel = p;
- d_printInModelSetByUser = true;
-}
-
/* -------------------------------------------------------------------------- */
/* class DeclareTypeNodeCommand */
/* -------------------------------------------------------------------------- */
OutputLanguage language = language::output::LANG_AUTO) const override;
NodeCommand* clone() const override;
const Node& getFunction() const;
- bool getPrintInModel() const;
- bool getPrintInModelSetByUser() const;
- void setPrintInModel(bool p);
private:
std::string d_id;
Node d_fun;
TypeNode d_type;
- bool d_printInModel;
- bool d_printInModelSetByUser;
};
/**
TheoryModel* tm = te->getModel();
if (tm != nullptr)
{
- d_model.reset(new Model(*this, tm));
+ d_model.reset(new Model(tm));
// make the check models utility
d_checkModels.reset(new CheckModels(*d_smtSolver.get()));
}
projects / cvc5.git / commitdiff