* Move unsat core names to SmtEnginePrivate. Adds a SetExpressionNameCommand to do this. Removes the names field from GetUnsatCoreCommand.
* Comment
* Pass expression names by reference.
* Update throw specifiers.
* Minor
* Switch expression names to CDMap, simplify interface for printing unsat core names.
* Revert throw specifier change.
* Minor simplifcations
{ bool inUnsatCore = PARSER_STATE->lastNamedTerm().first == expr;
cmd->reset(new AssertCommand(expr, inUnsatCore));
if(inUnsatCore) {
- PARSER_STATE->registerUnsatCoreName(PARSER_STATE->lastNamedTerm());
+ // set the expression name, if there was a named term
+ std::pair<Expr, std::string> namedTerm = PARSER_STATE->lastNamedTerm();
+ Command* csen = new SetExpressionNameCommand(namedTerm.first, namedTerm.second);
+ csen->setMuted(true);
+ PARSER_STATE->preemptCommand(csen);
}
}
| /* check-sat */
{ cmd->reset(new GetProofCommand()); }
| /* get-unsat-core */
GET_UNSAT_CORE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
- { cmd->reset(new GetUnsatCoreCommand(PARSER_STATE->getUnsatCoreNames())); }
+ { cmd->reset(new GetUnsatCoreCommand); }
| /* push */
PUSH_TOK { PARSER_STATE->checkThatLogicIsSet(); }
{ if( PARSER_STATE->sygus() ){
cmd->reset(new EmptyCommand());
} else if(n == 1) {
PARSER_STATE->pushScope();
- PARSER_STATE->pushUnsatCoreNameScope();
cmd->reset(new PushCommand());
} else {
std::unique_ptr<CommandSequence> seq(new CommandSequence());
do {
PARSER_STATE->pushScope();
- PARSER_STATE->pushUnsatCoreNameScope();
Command* push_cmd = new PushCommand();
push_cmd->setMuted(n > 1);
seq->addCommand(push_cmd);
"PUSH. Maybe you want (push 1)?");
} else {
PARSER_STATE->pushScope();
- PARSER_STATE->pushUnsatCoreNameScope();
cmd->reset(new PushCommand());
}
} )
if(n == 0) {
cmd->reset(new EmptyCommand());
} else if(n == 1) {
- PARSER_STATE->popUnsatCoreNameScope();
PARSER_STATE->popScope();
cmd->reset(new PopCommand());
} else {
std::unique_ptr<CommandSequence> seq(new CommandSequence());
do {
- PARSER_STATE->popUnsatCoreNameScope();
PARSER_STATE->popScope();
Command* pop_command = new PopCommand();
pop_command->setMuted(n > 1);
"Strict compliance mode demands an integer to be provided to POP."
"Maybe you want (pop 1)?");
} else {
- PARSER_STATE->popUnsatCoreNameScope();
PARSER_STATE->popScope();
cmd->reset(new PopCommand());
}
Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
Parser(exprManager,input,strictMode,parseOnly),
d_logicSet(false) {
- d_unsatCoreNames.push(std::map<Expr, std::string>());
if( !strictModeEnabled() ) {
addTheory(Smt2::THEORY_CORE);
}
d_logic = LogicInfo();
operatorKindMap.clear();
d_lastNamedTerm = std::pair<Expr, std::string>();
- d_unsatCoreNames = std::stack< std::map<Expr, std::string> >();
this->Parser::reset();
- d_unsatCoreNames.push(std::map<Expr, std::string>());
if( !strictModeEnabled() ) {
addTheory(Smt2::THEORY_CORE);
}
LogicInfo d_logic;
std::unordered_map<std::string, Kind> operatorKindMap;
std::pair<Expr, std::string> d_lastNamedTerm;
- // this is a user-context stack
- std::stack< std::map<Expr, std::string> > d_unsatCoreNames;
// for sygus
std::vector<Expr> d_sygusVars, d_sygusConstraints, d_sygusFunSymbols;
std::map< Expr, bool > d_sygusVarPrimed;
return d_lastNamedTerm;
}
- void pushUnsatCoreNameScope() {
- d_unsatCoreNames.push(d_unsatCoreNames.top());
- }
-
- void popUnsatCoreNameScope() {
- d_unsatCoreNames.pop();
- }
-
- void registerUnsatCoreName(std::pair<Expr, std::string> name) {
- d_unsatCoreNames.top().insert(name);
- }
-
- std::map<Expr, std::string> getUnsatCoreNames() {
- return d_unsatCoreNames.top();
- }
-
bool isAbstractValue(const std::string& name) {
return name.length() >= 2 && name[0] == '@' && name[1] != '0' &&
name.find_first_not_of("0123456789", 1) == std::string::npos;
}/* Printer::toStream(Model) */
void Printer::toStream(std::ostream& out, const UnsatCore& core) const throw() {
- std::map<Expr, std::string> names;
- toStream(out, core, names);
-}/* Printer::toStream(UnsatCore) */
-
-void Printer::toStream(std::ostream& out, const UnsatCore& core, const std::map<Expr, std::string>& names) const throw() {
for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
AssertCommand cmd(*i);
toStream(out, &cmd, -1, false, -1);
out << std::endl;
}
-}/* Printer::toStream(UnsatCore, std::map<Expr, std::string>) */
+}/* Printer::toStream(UnsatCore) */
Printer* Printer::getPrinter(OutputLanguage lang) throw() {
if(lang == language::output::LANG_AUTO) {
/** Write an UnsatCore out to a stream with this Printer. */
virtual void toStream(std::ostream& out, const UnsatCore& core) const throw();
- /** Write an UnsatCore out to a stream with this Printer. */
- virtual void toStream(std::ostream& out, const UnsatCore& core, const std::map<Expr, std::string>& names) const throw();
-
};/* class Printer */
}/* CVC4 namespace */
}/* Smt2Printer::toStream(CommandStatus*) */
-void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core, const std::map<Expr, std::string>& names) const throw() {
+void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core) const throw() {
out << "(" << std::endl;
+ SmtEngine * smt = core.getSmtEngine();
+ Assert( smt!=NULL );
for(UnsatCore::const_iterator i = core.begin(); i != core.end(); ++i) {
- map<Expr, string>::const_iterator j = names.find(*i);
- if (j != names.end()) {
+ std::string name;
+ if (smt->getExpressionName(*i,name)) {
// Named assertions always get printed
- out << maybeQuoteSymbol((*j).second) << endl;
+ out << maybeQuoteSymbol(name) << endl;
} else if (options::dumpUnsatCoresFull()) {
// Unnamed assertions only get printed if the option is set
out << *i << endl;
void toStream(std::ostream& out, const CommandStatus* s) const throw();
void toStream(std::ostream& out, const SExpr& sexpr) const throw();
void toStream(std::ostream& out, const Model& m) const throw();
- void toStream(std::ostream& out, const UnsatCore& core, const std::map<Expr, std::string>& names) const throw();
+ /** print the unsat core to the stream out.
+ * We use the expression names that are stored in the SMT engine associated
+ * with the core (UnsatCore::getSmtEngine) for printing named assertions.
+ */
+ void toStream(std::ostream& out, const UnsatCore& core) const throw();
};/* class Smt2Printer */
}/* CVC4::printer::smt2 namespace */
Printer::getPrinter(options::outputLanguage())->toStream(out, *this);
}
-void UnsatCore::toStream(std::ostream& out, const std::map<Expr, std::string>& names) const {
- Assert(d_smt != NULL);
- smt::SmtScope smts(d_smt);
- expr::ExprDag::Scope scope(out, false);
- Printer::getPrinter(options::outputLanguage())->toStream(out, *this, names);
-}
-
std::ostream& operator<<(std::ostream& out, const UnsatCore& core) {
core.toStream(out);
return out;
~UnsatCore() {}
/** get the smt engine that this unsat core is hooked up to */
- SmtEngine* getSmtEngine() { return d_smt; }
+ SmtEngine* getSmtEngine() const { return d_smt; }
size_t size() const { return d_core.size(); }
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
+ */
void toStream(std::ostream& out) const;
- void toStream(std::ostream& out, const std::map<Expr, std::string>& names) const;
};/* class UnsatCore */
GetUnsatCoreCommand::GetUnsatCoreCommand() throw() {
}
-GetUnsatCoreCommand::GetUnsatCoreCommand(const std::map<Expr, std::string>& names) throw() : d_names(names) {
-}
-
void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) {
try {
d_result = smtEngine->getUnsatCore();
if(! ok()) {
this->Command::printResult(out, verbosity);
} else {
- d_result.toStream(out, d_names);
+ d_result.toStream(out);
}
}
}
Command* GetUnsatCoreCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- GetUnsatCoreCommand* c = new GetUnsatCoreCommand(d_names);
+ GetUnsatCoreCommand* c = new GetUnsatCoreCommand;
c->d_result = d_result;
return c;
}
Command* GetUnsatCoreCommand::clone() const {
- GetUnsatCoreCommand* c = new GetUnsatCoreCommand(d_names);
+ GetUnsatCoreCommand* c = new GetUnsatCoreCommand;
c->d_result = d_result;
return c;
}
return "get-option";
}
+
+/* class SetExpressionNameCommand */
+
+SetExpressionNameCommand::SetExpressionNameCommand(Expr expr, std::string name) throw() :
+d_expr(expr), d_name(name) {
+
+}
+
+void SetExpressionNameCommand::invoke(SmtEngine* smtEngine) {
+ smtEngine->setExpressionName(d_expr, d_name);
+ d_commandStatus = CommandSuccess::instance();
+}
+
+Command* SetExpressionNameCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ SetExpressionNameCommand* c = new SetExpressionNameCommand(d_expr.exportTo(exprManager, variableMap), d_name);
+ return c;
+}
+
+Command* SetExpressionNameCommand::clone() const {
+ SetExpressionNameCommand* c = new SetExpressionNameCommand(d_expr, d_name);
+ return c;
+}
+
+std::string SetExpressionNameCommand::getCommandName() const throw() {
+ return "set-expr-name";
+}
+
/* class DatatypeDeclarationCommand */
DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) throw() :
};/* class GetQuantifierEliminationCommand */
class CVC4_PUBLIC GetUnsatCoreCommand : public Command {
-protected:
- UnsatCore d_result;
- std::map<Expr, std::string> d_names;
public:
GetUnsatCoreCommand() throw();
- GetUnsatCoreCommand(const std::map<Expr, std::string>& names) throw();
~GetUnsatCoreCommand() throw() {}
void invoke(SmtEngine* smtEngine);
void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
+
+protected:
+ // the result of the unsat core call
+ UnsatCore d_result;
};/* class GetUnsatCoreCommand */
class CVC4_PUBLIC GetAssertionsCommand : public Command {
std::string getCommandName() const throw();
};/* 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:
+ Expr d_expr;
+ std::string d_name;
+public:
+ SetExpressionNameCommand(Expr expr, std::string name) throw();
+ ~SetExpressionNameCommand() throw() {}
+ void invoke(SmtEngine* smtEngine);
+ Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+ Command* clone() const;
+ std::string getCommandName() const throw();
+};/* class SetExpressionNameCommand */
+
+
class CVC4_PUBLIC DatatypeDeclarationCommand : public Command {
private:
std::vector<DatatypeType> d_datatypes;
#include "base/listener.h"
#include "base/modal_exception.h"
#include "base/output.h"
+#include "context/cdhashmap.h"
#include "context/cdhashset.h"
#include "context/cdlist.h"
#include "context/context.h"
/** TODO: whether certain preprocess steps are necessary */
//bool d_needsExpandDefs;
-
+
+ //------------------------------- expression names
+ /** mapping from expressions to name */
+ context::CDHashMap< Node, std::string, NodeHashFunction > d_exprNames;
+ //------------------------------- end expression names
public:
/**
* Map from skolem variables to index in d_assertions containing
d_abstractValues(),
d_simplifyAssertionsDepth(0),
//d_needsExpandDefs(true), //TODO?
+ d_exprNames(smt.d_userContext),
d_iteSkolemMap(),
d_iteRemover(smt.d_userContext),
d_pbsProcessor(smt.d_userContext),
*/
void processAssertions();
+ /** Process a user push.
+ */
+ void notifyPush() {
+
+ }
+
/**
* Process a user pop. Clears out the non-context-dependent stuff in this
* SmtEnginePrivate. Necessary to clear out our assertion vectors in case
- * someone does a push-assert-pop without a check-sat.
+ * someone does a push-assert-pop without a check-sat. It also pops the
+ * last map of expression names from notifyPush.
*/
void notifyPop() {
d_assertions.clear();
std::ostream* getReplayLog() const {
return d_managedReplayLog.getReplayLog();
}
+
+ //------------------------------- expression names
+ // implements setExpressionName, as described in smt_engine.h
+ void setExpressionName(Expr e, std::string name) {
+ d_exprNames[Node::fromExpr(e)] = name;
+ }
+
+ // implements getExpressionName, as described in smt_engine.h
+ bool getExpressionName(Expr e, std::string& name) const {
+ context::CDHashMap< Node, std::string, NodeHashFunction >::const_iterator it = d_exprNames.find(e);
+ if(it!=d_exprNames.end()) {
+ name = (*it).second;
+ return true;
+ }else{
+ return false;
+ }
+ }
+ //------------------------------- end expression names
};/* class SmtEnginePrivate */
finalOptionsAreSet();
doPendingPops();
Trace("smt") << "SMT push()" << endl;
+ d_private->notifyPush();
d_private->processAssertions();
if(Dump.isOn("benchmark")) {
Dump("benchmark") << PushCommand();
AlwaysAssert(!d_fullyInited,
"Cannot set replay stream once fully initialized");
d_replayStream = replayStream;
+}
+
+bool SmtEngine::getExpressionName(Expr e, std::string& name) const {
+ return d_private->getExpressionName(e, name);
+}
+
+void SmtEngine::setExpressionName(Expr e, const std::string& name) {
+ Trace("smt-debug") << "Set expression name " << e << " to " << name << std::endl;
+ d_private->setExpressionName(e,name);
}
}/* CVC4 namespace */
* Verbosity of various commands.
*/
std::map<std::string, Integer> d_commandVerbosity;
+
/** ReplayStream for the solver. */
ExprStream* d_replayStream;
* translation.
*/
void setReplayStream(ExprStream* exprStream);
+
+ /** get expression name
+ * Returns true if e has an expression name in the current context.
+ * If it returns true, the name of e is stored in name.
+ */
+ bool getExpressionName(Expr e, std::string& name) const;
+
+ /** set expression name
+ * Sets the expression name of e to name.
+ * This information is user-context-dependent.
+ * If e already has a name, it is overwritten.
+ */
+ void setExpressionName(Expr e, const std::string& name);
};/* class SmtEngine */
projects / cvc5.git / commitdiff