summaryrefslogtreecommitdiff
path: root/src/expr/command.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/command.cpp')
-rw-r--r--src/expr/command.cpp73
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;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback