diff options
Diffstat (limited to 'src/smt/command.cpp')
-rw-r--r-- | src/smt/command.cpp | 247 |
1 files changed, 0 insertions, 247 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 17d8cbed5..ce8d4fa88 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -2841,251 +2841,4 @@ std::string DatatypeDeclarationCommand::getCommandName() const return "declare-datatypes"; } -/* -------------------------------------------------------------------------- */ -/* class RewriteRuleCommand */ -/* -------------------------------------------------------------------------- */ - -RewriteRuleCommand::RewriteRuleCommand(const std::vector<Expr>& vars, - const std::vector<Expr>& guards, - Expr head, - Expr body, - const Triggers& triggers) - : d_vars(vars), - d_guards(guards), - d_head(head), - d_body(body), - d_triggers(triggers) -{ -} - -RewriteRuleCommand::RewriteRuleCommand(const std::vector<Expr>& vars, - Expr head, - Expr body) - : d_vars(vars), d_head(head), d_body(body) -{ -} - -const std::vector<Expr>& RewriteRuleCommand::getVars() const { return d_vars; } -const std::vector<Expr>& RewriteRuleCommand::getGuards() const -{ - return d_guards; -} - -Expr RewriteRuleCommand::getHead() const { return d_head; } -Expr RewriteRuleCommand::getBody() const { return d_body; } -const RewriteRuleCommand::Triggers& RewriteRuleCommand::getTriggers() const -{ - return d_triggers; -} - -void RewriteRuleCommand::invoke(SmtEngine* smtEngine) -{ - try - { - ExprManager* em = smtEngine->getExprManager(); - /** build vars list */ - Expr vars = em->mkExpr(kind::BOUND_VAR_LIST, d_vars); - /** build guards list */ - Expr guards; - if (d_guards.size() == 0) - guards = em->mkConst<bool>(true); - else if (d_guards.size() == 1) - guards = d_guards[0]; - else - guards = em->mkExpr(kind::AND, d_guards); - /** build expression */ - Expr expr; - if (d_triggers.empty()) - { - expr = em->mkExpr(kind::RR_REWRITE, vars, guards, d_head, d_body); - } - else - { - /** build triggers list */ - std::vector<Expr> vtriggers; - vtriggers.reserve(d_triggers.size()); - for (Triggers::const_iterator i = d_triggers.begin(), - end = d_triggers.end(); - i != end; - ++i) - { - vtriggers.push_back(em->mkExpr(kind::INST_PATTERN, *i)); - } - Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST, vtriggers); - expr = - em->mkExpr(kind::RR_REWRITE, vars, guards, d_head, d_body, triggers); - } - smtEngine->assertFormula(expr); - d_commandStatus = CommandSuccess::instance(); - } - catch (exception& e) - { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* RewriteRuleCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - /** Convert variables */ - VExpr vars = ExportTo(exprManager, variableMap, d_vars); - /** Convert guards */ - VExpr guards = ExportTo(exprManager, variableMap, d_guards); - /** Convert triggers */ - Triggers triggers; - triggers.reserve(d_triggers.size()); - for (const std::vector<Expr>& trigger_list : d_triggers) - { - triggers.push_back(ExportTo(exprManager, variableMap, trigger_list)); - } - /** Convert head and body */ - Expr head = d_head.exportTo(exprManager, variableMap); - Expr body = d_body.exportTo(exprManager, variableMap); - /** Create the converted rules */ - return new RewriteRuleCommand(vars, guards, head, body, triggers); -} - -Command* RewriteRuleCommand::clone() const -{ - return new RewriteRuleCommand(d_vars, d_guards, d_head, d_body, d_triggers); -} - -std::string RewriteRuleCommand::getCommandName() const -{ - return "rewrite-rule"; -} - -/* -------------------------------------------------------------------------- */ -/* class PropagateRuleCommand */ -/* -------------------------------------------------------------------------- */ - -PropagateRuleCommand::PropagateRuleCommand(const std::vector<Expr>& vars, - const std::vector<Expr>& guards, - const std::vector<Expr>& heads, - Expr body, - const Triggers& triggers, - bool deduction) - : d_vars(vars), - d_guards(guards), - d_heads(heads), - d_body(body), - d_triggers(triggers), - d_deduction(deduction) -{ -} - -PropagateRuleCommand::PropagateRuleCommand(const std::vector<Expr>& vars, - const std::vector<Expr>& heads, - Expr body, - bool deduction) - : d_vars(vars), d_heads(heads), d_body(body), d_deduction(deduction) -{ -} - -const std::vector<Expr>& PropagateRuleCommand::getVars() const -{ - return d_vars; -} - -const std::vector<Expr>& PropagateRuleCommand::getGuards() const -{ - return d_guards; -} - -const std::vector<Expr>& PropagateRuleCommand::getHeads() const -{ - return d_heads; -} - -Expr PropagateRuleCommand::getBody() const { return d_body; } -const PropagateRuleCommand::Triggers& PropagateRuleCommand::getTriggers() const -{ - return d_triggers; -} - -bool PropagateRuleCommand::isDeduction() const { return d_deduction; } -void PropagateRuleCommand::invoke(SmtEngine* smtEngine) -{ - try - { - ExprManager* em = smtEngine->getExprManager(); - /** build vars list */ - Expr vars = em->mkExpr(kind::BOUND_VAR_LIST, d_vars); - /** build guards list */ - Expr guards; - if (d_guards.size() == 0) - guards = em->mkConst<bool>(true); - else if (d_guards.size() == 1) - guards = d_guards[0]; - else - guards = em->mkExpr(kind::AND, d_guards); - /** build heads list */ - Expr heads; - if (d_heads.size() == 1) - heads = d_heads[0]; - else - heads = em->mkExpr(kind::AND, d_heads); - /** build expression */ - Expr expr; - if (d_triggers.empty()) - { - expr = em->mkExpr(kind::RR_REWRITE, vars, guards, heads, d_body); - } - else - { - /** build triggers list */ - std::vector<Expr> vtriggers; - vtriggers.reserve(d_triggers.size()); - for (Triggers::const_iterator i = d_triggers.begin(), - end = d_triggers.end(); - i != end; - ++i) - { - vtriggers.push_back(em->mkExpr(kind::INST_PATTERN, *i)); - } - Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST, vtriggers); - expr = - em->mkExpr(kind::RR_REWRITE, vars, guards, heads, d_body, triggers); - } - smtEngine->assertFormula(expr); - d_commandStatus = CommandSuccess::instance(); - } - catch (exception& e) - { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* PropagateRuleCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - /** Convert variables */ - VExpr vars = ExportTo(exprManager, variableMap, d_vars); - /** Convert guards */ - VExpr guards = ExportTo(exprManager, variableMap, d_guards); - /** Convert heads */ - VExpr heads = ExportTo(exprManager, variableMap, d_heads); - /** Convert triggers */ - Triggers triggers; - triggers.reserve(d_triggers.size()); - for (const std::vector<Expr>& trigger_list : d_triggers) - { - triggers.push_back(ExportTo(exprManager, variableMap, trigger_list)); - } - /** Convert head and body */ - Expr body = d_body.exportTo(exprManager, variableMap); - /** Create the converted rules */ - return new PropagateRuleCommand(vars, guards, heads, body, triggers); -} - -Command* PropagateRuleCommand::clone() const -{ - return new PropagateRuleCommand( - d_vars, d_guards, d_heads, d_body, d_triggers); -} - -std::string PropagateRuleCommand::getCommandName() const -{ - return "propagate-rule"; -} } // namespace CVC4 |