This PR uses the symbol manager for handling names for unsat cores.
This replaces interfaces in SmtEngine for managing expression names. It removes the SetExpressionName command.
smt/dump.h
smt/dump_manager.cpp
smt/dump_manager.h
- smt/expr_names.cpp
- smt/expr_names.h
smt/listeners.cpp
smt/listeners.h
smt/logic_exception.h
const std::string& name,
bool isAssertion)
{
+ Trace("sym-manager") << "set expression name: " << t << " -> " << name
+ << ", isAssertion=" << isAssertion << std::endl;
// cannot name subexpressions under quantifiers
PrettyCheckArgument(
!d_hasPushedScope.get(), name, "cannot name function in a scope");
+ if (isAssertion)
+ {
+ d_namedAsserts.insert(t);
+ }
if (d_names.find(t) != d_names.end())
{
// already named assertion
return false;
}
- if (isAssertion)
- {
- d_namedAsserts.insert(t);
- }
d_names[t] = name;
return true;
}
// set the expression name, if there was a named term
std::pair<api::Term, std::string> namedTerm =
PARSER_STATE->lastNamedTerm();
- // TODO (projects-248)
- // SYM_MAN->setExpressionName(namedTerm.first, namedTerm.second, true);
- Command* csen =
- new SetExpressionNameCommand(namedTerm.first, namedTerm.second);
- csen->setMuted(true);
- PARSER_STATE->preemptCommand(csen);
+ SYM_MAN->setExpressionName(namedTerm.first, namedTerm.second, true);
}
}
| /* check-sat */
#define PARSER_STATE ((Tptp*)PARSER->super)
#undef SOLVER
#define SOLVER PARSER_STATE->getSolver()
+#undef SYM_MAN
+#define SYM_MAN PARSER_STATE->getSymbolManager()
#undef MK_TERM
#define MK_TERM SOLVER->mkTerm
#define UNSUPPORTED PARSER_STATE->unimplementedFeature
CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr, expr);
if( !aexpr.isNull() ){
// set the expression name (e.g. used with unsat core printing)
- Command* csen = new SetExpressionNameCommand(aexpr, name);
- csen->setMuted(true);
- PARSER_STATE->preemptCommand(csen);
+ SYM_MAN->setExpressionName(aexpr, name, true);
}
// make the command to assert the formula
cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, /* cnf == */ true, true);
CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr,expr);
if( !aexpr.isNull() ){
// set the expression name (e.g. used with unsat core printing)
- Command* csen = new SetExpressionNameCommand(aexpr, name);
- csen->setMuted(true);
- PARSER_STATE->preemptCommand(csen);
+ SYM_MAN->setExpressionName(aexpr, name, true);
}
// make the command to assert the formula
cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, /* cnf == */ false, true);
CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr,expr);
if( !aexpr.isNull() ){
// set the expression name (e.g. used with unsat core printing)
- Command* csen = new SetExpressionNameCommand(aexpr, name);
- csen->setMuted(true);
- PARSER_STATE->preemptCommand(csen);
+ SYM_MAN->setExpressionName(aexpr, name, true);
}
// make the command to assert the formula
cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, /* cnf == */ false, true);
if (!aexpr.isNull())
{
// set the expression name (e.g. used with unsat core printing)
- Command* csen = new SetExpressionNameCommand(aexpr, name);
- csen->setMuted(true);
- PARSER_STATE->preemptCommand(csen);
+ SYM_MAN->setExpressionName(aexpr, name, true);
}
// make the command to assert the formula
cmd = PARSER_STATE->makeAssertCommand(
void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core) const
{
out << "(" << std::endl;
- SmtEngine * smt = core.getSmtEngine();
- Assert(smt != NULL);
- for(UnsatCore::const_iterator i = core.begin(); i != core.end(); ++i) {
- std::string name;
- if (smt->getExpressionName(*i,name)) {
- // Named assertions always get printed
- out << CVC4::quoteSymbol(name) << endl;
- } else if (options::dumpUnsatCoresFull()) {
- // Unnamed assertions only get printed if the option is set
+ if (core.useNames())
+ {
+ // use the names
+ const std::vector<std::string>& cnames = core.getCoreNames();
+ for (const std::string& cn : cnames)
+ {
+ out << CVC4::quoteSymbol(cn) << std::endl;
+ }
+ }
+ else
+ {
+ // otherwise, use the formulas
+ for (UnsatCore::const_iterator i = core.begin(); i != core.end(); ++i)
+ {
out << *i << endl;
}
}
void TptpPrinter::toStream(std::ostream& out, const UnsatCore& core) const
{
out << "% SZS output start UnsatCore " << std::endl;
- SmtEngine * smt = core.getSmtEngine();
- Assert(smt != NULL);
- for(UnsatCore::const_iterator i = core.begin(); i != core.end(); ++i) {
- std::string name;
- if (smt->getExpressionName(*i, name)) {
- // Named assertions always get printed
- out << name << endl;
- } else if (options::dumpUnsatCoresFull()) {
- // Unnamed assertions only get printed if the option is set
+ if (core.useNames())
+ {
+ // use the names
+ const std::vector<std::string>& cnames = core.getCoreNames();
+ for (const std::string& cn : cnames)
+ {
+ out << cn << std::endl;
+ }
+ }
+ else
+ {
+ // otherwise, use the formulas
+ for (UnsatCore::const_iterator i = core.begin(); i != core.end(); ++i)
+ {
out << *i << endl;
}
}
** directory for licensing information.\endverbatim
**
** \brief Representation of unsat cores
- **
- ** Representation of unsat cores.
**/
#include "proof/unsat_core.h"
namespace CVC4 {
-void UnsatCore::initMessage() const {
+UnsatCore::UnsatCore(const std::vector<Node>& core)
+ : d_useNames(false), d_core(core), d_names()
+{
Debug("core") << "UnsatCore size " << d_core.size() << std::endl;
}
+UnsatCore::UnsatCore(std::vector<std::string>& names)
+ : d_useNames(true), d_core(), d_names(names)
+{
+ Debug("core") << "UnsatCore (names) size " << d_names.size() << std::endl;
+}
+
+const std::vector<Node>& UnsatCore::getCore() const { return d_core; }
+const std::vector<std::string>& UnsatCore::getCoreNames() const
+{
+ return d_names;
+}
+
UnsatCore::const_iterator UnsatCore::begin() const {
return d_core.begin();
}
}
void UnsatCore::toStream(std::ostream& out) const {
- Assert(d_smt != NULL);
- smt::SmtScope smts(d_smt);
expr::ExprDag::Scope scope(out, false);
Printer::getPrinter(options::outputLanguage())->toStream(out, *this);
}
** 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
+ ** \brief Representation of unsat cores.
**/
#include "cvc4_private.h"
namespace CVC4 {
-class SmtEngine;
-
+/**
+ * An unsat core, which can optionally be initialized as a list of names
+ * or as a list of formulas.
+ */
class UnsatCore
{
- /** The SmtEngine we're associated with */
- SmtEngine* d_smt;
-
- std::vector<Node> d_core;
-
- void initMessage() const;
-
-public:
- UnsatCore() : d_smt(NULL) {}
-
- UnsatCore(SmtEngine* smt, const std::vector<Node>& core)
- : d_smt(smt), d_core(core)
- {
- initMessage();
- }
-
+ public:
+ UnsatCore() {}
+ /** Initialize using assertions */
+ UnsatCore(const std::vector<Node>& core);
+ /** Initialize using assertion names */
+ UnsatCore(std::vector<std::string>& names);
~UnsatCore() {}
- /** get the smt engine that this unsat core is hooked up to */
- SmtEngine* getSmtEngine() const { return d_smt; }
-
- size_t size() const { return d_core.size(); }
+ /** Whether we are using names for this unsat core */
+ bool useNames() const { return d_useNames; }
+ /** Get the assertions in the unsat core */
+ const std::vector<Node>& getCore() const;
+ /** Get their names */
+ const std::vector<std::string>& getCoreNames() const;
typedef std::vector<Node>::const_iterator iterator;
typedef std::vector<Node>::const_iterator const_iterator;
const_iterator begin() const;
const_iterator end() const;
-
- /** prints this UnsatCore object to the stream out.
- * We use the expression names stored in the SmtEngine d_smt
- */
+
+ /**
+ * prints this UnsatCore object to the stream out.
+ */
void toStream(std::ostream& out) const;
+ private:
+ /** Whether we are using names for this unsat core */
+ bool d_useNames;
+ /** The unsat core */
+ std::vector<Node> d_core;
+ /** The names of assertions in the above core */
+ std::vector<std::string> d_names;
};/* class UnsatCore */
/** Print the unsat core to stream out */
/* class GetUnsatCoreCommand */
/* -------------------------------------------------------------------------- */
-GetUnsatCoreCommand::GetUnsatCoreCommand() {}
+GetUnsatCoreCommand::GetUnsatCoreCommand() : d_sm(nullptr) {}
void GetUnsatCoreCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
- d_solver = solver;
+ d_sm = sm;
d_result = solver->getUnsatCore();
d_commandStatus = CommandSuccess::instance();
}
else
{
- UnsatCore ucr(d_solver->getSmtEngine(), api::termVectorToNodes(d_result));
- ucr.toStream(out);
+ if (options::dumpUnsatCoresFull())
+ {
+ // use the assertions
+ UnsatCore ucr(api::termVectorToNodes(d_result));
+ ucr.toStream(out);
+ }
+ else
+ {
+ // otherwise, use the names
+ std::vector<std::string> names;
+ d_sm->getExpressionNames(d_result, names, true);
+ UnsatCore ucr(names);
+ ucr.toStream(out);
+ }
}
}
Command* GetUnsatCoreCommand::clone() const
{
GetUnsatCoreCommand* c = new GetUnsatCoreCommand;
- c->d_solver = d_solver;
+ c->d_sm = d_sm;
c->d_result = d_result;
return c;
}
Printer::getPrinter(language)->toStreamCmdGetOption(out, d_flag);
}
-/* -------------------------------------------------------------------------- */
-/* class SetExpressionNameCommand */
-/* -------------------------------------------------------------------------- */
-
-SetExpressionNameCommand::SetExpressionNameCommand(api::Term term,
- std::string name)
- : d_term(term), d_name(name)
-{
-}
-
-void SetExpressionNameCommand::invoke(api::Solver* solver, SymbolManager* sm)
-{
- solver->getSmtEngine()->setExpressionName(d_term.getExpr(), d_name);
- d_commandStatus = CommandSuccess::instance();
-}
-
-Command* SetExpressionNameCommand::clone() const
-{
- SetExpressionNameCommand* c = new SetExpressionNameCommand(d_term, d_name);
- return c;
-}
-
-std::string SetExpressionNameCommand::getCommandName() const
-{
- return "set-expr-name";
-}
-
-void SetExpressionNameCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- OutputLanguage language) const
-{
- Printer::getPrinter(language)->toStreamCmdSetExpressionName(
- out, d_term.getNode(), d_name);
-}
-
/* -------------------------------------------------------------------------- */
/* class DatatypeDeclarationCommand */
/* -------------------------------------------------------------------------- */
OutputLanguage language = language::output::LANG_AUTO) const override;
protected:
- /** The solver we were invoked with */
- api::Solver* d_solver;
+ /** The symbol manager we were invoked with */
+ SymbolManager* d_sm;
/** the result of the unsat core call */
std::vector<api::Term> d_result;
}; /* class GetUnsatCoreCommand */
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class GetOptionCommand */
-// Set expression name command
-// Note this is not an official smt2 command
-// Conceptually:
-// (assert (! expr :named name))
-// is converted to
-// (assert expr)
-// (set-expr-name expr name)
-class CVC4_PUBLIC SetExpressionNameCommand : public Command
-{
- protected:
- api::Term d_term;
- std::string d_name;
-
- public:
- SetExpressionNameCommand(api::Term term, std::string name);
-
- void invoke(api::Solver* solver, SymbolManager* sm) override;
- Command* clone() const override;
- std::string getCommandName() const override;
- void toStream(
- std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- OutputLanguage language = language::output::LANG_AUTO) const override;
-}; /* class SetExpressionNameCommand */
-
class CVC4_PUBLIC DatatypeDeclarationCommand : public Command
{
private:
+++ /dev/null
-/********************* */
-/*! \file expr_names.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Andrew Reynolds
- ** 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 Utility for maintaining expression names.
- **/
-
-#include "smt/expr_names.h"
-
-namespace CVC4 {
-namespace smt {
-
-ExprNames::ExprNames(context::UserContext* u)
- : d_exprNames(u)
-{
-}
-
-void ExprNames::setExpressionName(const Node& e, const std::string& name) {
- d_exprNames[e] = name;
-}
-
-bool ExprNames::getExpressionName(const Node& e, std::string& name) const {
- auto it = d_exprNames.find(e);
- if(it!=d_exprNames.end()) {
- name = (*it).second;
- return true;
- }
- return false;
-}
-
-} // namespace smt
-} // namespace CVC4
+++ /dev/null
-/********************* */
-/*! \file expr_names.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Andrew Reynolds, Aina Niemetz, Kshitij Bansal
- ** 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 Utility for maintaining expression names.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4__SMT__EXPR_NAMES_H
-#define CVC4__SMT__EXPR_NAMES_H
-
-#include <string>
-
-#include "context/cdhashmap.h"
-#include "expr/node.h"
-
-namespace CVC4 {
-namespace smt {
-
-/**
- * This utility is responsible for maintaining names for expressions.
- */
-class ExprNames
-{
- public:
- ExprNames(context::UserContext* u);
- /**
- * Get expression name.
- *
- * Return true if given expression has a name in the current context.
- * If it returns true, the name of expression 'e' is stored in 'name'.
- */
- bool getExpressionName(const Node& e, std::string& name) const;
-
- /**
- * Set name of given expression 'e' to 'name'.
- *
- * This information is user-context-dependent.
- * If 'e' already has a name, it is overwritten.
- */
- void setExpressionName(const Node& e, const std::string& name);
-
- private:
- /** mapping from expressions to name */
- context::CDHashMap< Node, std::string, NodeHashFunction > d_exprNames;
-};
-
-} // namespace smt
-} // namespace CVC4
-
-#endif
#include "smt/check_models.h"
#include "smt/defined_function.h"
#include "smt/dump_manager.h"
-#include "smt/expr_names.h"
#include "smt/interpolation_solver.h"
#include "smt/listeners.h"
#include "smt/logic_request.h"
d_nodeManager(d_exprManager->getNodeManager()),
d_absValues(new AbstractValues(d_nodeManager)),
d_asserts(new Assertions(getUserContext(), *d_absValues.get())),
- d_exprNames(new ExprNames(getUserContext())),
d_dumpm(new DumpManager(getUserContext())),
d_routListener(new ResourceOutListener(*this)),
d_snmListener(new SmtNodeManagerListener(*d_dumpm.get(), d_outMgr)),
d_absValues.reset(nullptr);
d_asserts.reset(nullptr);
- d_exprNames.reset(nullptr);
d_dumpm.reset(nullptr);
d_sygusSolver.reset(nullptr);
}
d_proofManager->traceUnsatCore(); // just to trigger core creation
- return UnsatCore(this, d_proofManager->extractUnsatCore());
+ return UnsatCore(d_proofManager->extractUnsatCore());
#else /* IS_PROOFS_BUILD */
throw ModalException(
"This build of CVC4 doesn't have proof support (required for unsat "
coreChecker->declareSepHeap(sepLocType, sepDataType);
}
- Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core.size() << ")" << endl;
+ Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions"
+ << std::endl;
for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
Node assertionAfterExpansion = expandDefinitions(*i);
Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i
return SExpr::parseAtom(d_options.getOption(key));
}
-bool SmtEngine::getExpressionName(const Node& e, std::string& name) const {
- return d_exprNames->getExpressionName(e, name);
-}
-
-void SmtEngine::setExpressionName(const Node& e, const std::string& name) {
- Trace("smt-debug") << "Set expression name " << e << " to " << name << std::endl;
- d_exprNames->setExpressionName(e,name);
-}
-
Options& SmtEngine::getOptions() { return d_options; }
const Options& SmtEngine::getOptions() const { return d_options; }
const std::vector<Expr>& expr_values,
const std::string& str_value);
- /**
- * Get expression name.
- *
- * Return true if given expressoion has a name in the current context.
- * If it returns true, the name of expression 'e' is stored in 'name'.
- */
- bool getExpressionName(const Node& e, std::string& name) const;
-
- /**
- * Set name of given expression 'e' to 'name'.
- *
- * This information is user-context-dependent.
- * If 'e' already has a name, it is overwritten.
- */
- void setExpressionName(const Node& e, const std::string& name);
-
/** Get the options object (const and non-const versions) */
Options& getOptions();
const Options& getOptions() const;
std::unique_ptr<smt::AbstractValues> d_absValues;
/** Assertions manager */
std::unique_ptr<smt::Assertions> d_asserts;
- /** Expression names */
- std::unique_ptr<smt::ExprNames> d_exprNames;
/** The dump manager */
std::unique_ptr<smt::DumpManager> d_dumpm;
/** Resource out listener */
projects / cvc5.git / commitdiff