diff options
Diffstat (limited to 'src/expr/command.cpp')
-rw-r--r-- | src/expr/command.cpp | 73 |
1 files changed, 40 insertions, 33 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 69bdd704b..4d9ca9f30 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -189,8 +189,8 @@ std::string EchoCommand::getCommandName() const throw() { /* class AssertCommand */ -AssertCommand::AssertCommand(const Expr& e) throw() : - d_expr(e) { +AssertCommand::AssertCommand(const Expr& e, bool inUnsatCore) throw() : + d_expr(e), d_inUnsatCore(inUnsatCore) { } Expr AssertCommand::getExpr() const throw() { @@ -199,7 +199,7 @@ Expr AssertCommand::getExpr() const throw() { void AssertCommand::invoke(SmtEngine* smtEngine) throw() { try { - smtEngine->assertFormula(d_expr); + smtEngine->assertFormula(d_expr, d_inUnsatCore); d_commandStatus = CommandSuccess::instance(); } catch(exception& e) { d_commandStatus = new CommandFailure(e.what()); @@ -207,18 +207,17 @@ void AssertCommand::invoke(SmtEngine* smtEngine) throw() { } Command* AssertCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new AssertCommand(d_expr.exportTo(exprManager, variableMap)); + return new AssertCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore); } Command* AssertCommand::clone() const { - return new AssertCommand(d_expr); + return new AssertCommand(d_expr, d_inUnsatCore); } std::string AssertCommand::getCommandName() const throw() { return "assert"; } - /* class PushCommand */ void PushCommand::invoke(SmtEngine* smtEngine) throw() { @@ -271,8 +270,8 @@ CheckSatCommand::CheckSatCommand() throw() : d_expr() { } -CheckSatCommand::CheckSatCommand(const Expr& expr) throw() : - d_expr(expr) { +CheckSatCommand::CheckSatCommand(const Expr& expr, bool inUnsatCore) throw() : + d_expr(expr), d_inUnsatCore(inUnsatCore) { } Expr CheckSatCommand::getExpr() const throw() { @@ -301,13 +300,13 @@ void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const t } Command* CheckSatCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - CheckSatCommand* c = new CheckSatCommand(d_expr.exportTo(exprManager, variableMap)); + CheckSatCommand* c = new CheckSatCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore); c->d_result = d_result; return c; } Command* CheckSatCommand::clone() const { - CheckSatCommand* c = new CheckSatCommand(d_expr); + CheckSatCommand* c = new CheckSatCommand(d_expr, d_inUnsatCore); c->d_result = d_result; return c; } @@ -318,8 +317,8 @@ std::string CheckSatCommand::getCommandName() const throw() { /* class QueryCommand */ -QueryCommand::QueryCommand(const Expr& e) throw() : - d_expr(e) { +QueryCommand::QueryCommand(const Expr& e, bool inUnsatCore) throw() : + d_expr(e), d_inUnsatCore(inUnsatCore) { } Expr QueryCommand::getExpr() const throw() { @@ -348,13 +347,13 @@ void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const thro } Command* QueryCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - QueryCommand* c = new QueryCommand(d_expr.exportTo(exprManager, variableMap)); + QueryCommand* c = new QueryCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore); c->d_result = d_result; return c; } Command* QueryCommand::clone() const { - QueryCommand* c = new QueryCommand(d_expr); + QueryCommand* c = new QueryCommand(d_expr, d_inUnsatCore); c->d_result = d_result; return c; } @@ -744,22 +743,22 @@ Command* DefineNamedFunctionCommand::clone() const { SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr ) throw() : d_attr( attr ), d_expr( expr ){ } -/* -SetUserAttributeCommand::SetUserAttributeCommand( const std::string& id, Expr expr, + +SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr, std::vector<Expr>& values ) throw() : - d_id( id ), d_expr( expr ){ + d_attr( attr ), d_expr( expr ){ d_expr_values.insert( d_expr_values.begin(), values.begin(), values.end() ); } -SetUserAttributeCommand::SetUserAttributeCommand( const std::string& id, Expr expr, - std::string& value ) throw() : - d_id( id ), d_expr( expr ), d_str_value( value ){ +SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr, + const std::string& value ) throw() : + d_attr( attr ), d_expr( expr ), d_str_value( value ){ } -*/ + void SetUserAttributeCommand::invoke(SmtEngine* smtEngine) throw(){ try { if(!d_expr.isNull()) { - smtEngine->setUserAttribute( d_attr, d_expr ); + smtEngine->setUserAttribute( d_attr, d_expr, d_expr_values, d_str_value ); } d_commandStatus = CommandSuccess::instance(); } catch(exception& e) { @@ -769,11 +768,15 @@ void SetUserAttributeCommand::invoke(SmtEngine* smtEngine) throw(){ Command* SetUserAttributeCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap){ Expr expr = d_expr.exportTo(exprManager, variableMap); - return new SetUserAttributeCommand( d_attr, expr ); + SetUserAttributeCommand * c = new SetUserAttributeCommand( d_attr, expr, d_str_value ); + c->d_expr_values.insert( c->d_expr_values.end(), d_expr_values.begin(), d_expr_values.end() ); + return c; } Command* SetUserAttributeCommand::clone() const{ - return new SetUserAttributeCommand( d_attr, d_expr ); + SetUserAttributeCommand * c = new SetUserAttributeCommand( d_attr, d_expr, d_str_value ); + c->d_expr_values.insert( c->d_expr_values.end(), d_expr_values.begin(), d_expr_values.end() ); + return c; } std::string SetUserAttributeCommand::getCommandName() const throw() { @@ -1125,36 +1128,40 @@ std::string GetInstantiationsCommand::getCommandName() const throw() { GetUnsatCoreCommand::GetUnsatCoreCommand() throw() { } +GetUnsatCoreCommand::GetUnsatCoreCommand(const std::map<Expr, std::string>& names) throw() : d_names(names) { +} + void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) throw() { - /* try { d_result = smtEngine->getUnsatCore(); d_commandStatus = CommandSuccess::instance(); } catch(exception& e) { d_commandStatus = new CommandFailure(e.what()); } - */ - d_commandStatus = new CommandUnsupported(); } void GetUnsatCoreCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { if(! ok()) { this->Command::printResult(out, verbosity); } else { - //do nothing -- unsat cores not yet supported - // d_result->toStream(out); + d_result.toStream(out, d_names); } } +const UnsatCore& GetUnsatCoreCommand::getUnsatCore() const throw() { + // of course, this will be empty if the command hasn't been invoked yet + return d_result; +} + Command* GetUnsatCoreCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetUnsatCoreCommand* c = new GetUnsatCoreCommand(); - //c->d_result = d_result; + GetUnsatCoreCommand* c = new GetUnsatCoreCommand(d_names); + c->d_result = d_result; return c; } Command* GetUnsatCoreCommand::clone() const { - GetUnsatCoreCommand* c = new GetUnsatCoreCommand(); - //c->d_result = d_result; + GetUnsatCoreCommand* c = new GetUnsatCoreCommand(d_names); + c->d_result = d_result; return c; } |