From: Tim King Date: Tue, 2 Feb 2016 17:47:34 +0000 (-0800) Subject: Moving dump.*, command.*, model.*, and ite_removal.* from smt_util/ to smt/. Breaking... X-Git-Tag: cvc5-1.0.0~6089 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e21e99b7dfe45f042260db7eb754e25e7108f288;p=cvc5.git Moving dump.*, command.*, model.*, and ite_removal.* from smt_util/ to smt/. Breaking an edge between the sat solver and command.h. --- diff --git a/examples/hashsmt/sha1_collision.cpp b/examples/hashsmt/sha1_collision.cpp index 984cbde13..106369468 100644 --- a/examples/hashsmt/sha1_collision.cpp +++ b/examples/hashsmt/sha1_collision.cpp @@ -32,7 +32,7 @@ #include "options/language.h" #include "options/set_language.h" #include "sha1.hpp" -#include "smt_util/command.h" +#include "smt/command.h" #include "word.h" using namespace std; diff --git a/examples/hashsmt/sha1_inversion.cpp b/examples/hashsmt/sha1_inversion.cpp index 9aac7bbe0..c79bd5b61 100644 --- a/examples/hashsmt/sha1_inversion.cpp +++ b/examples/hashsmt/sha1_inversion.cpp @@ -32,7 +32,7 @@ #include "options/language.h" #include "options/set_language.h" #include "sha1.hpp" -#include "smt_util/command.h" +#include "smt/command.h" #include "word.h" using namespace std; diff --git a/examples/nra-translate/normalize.cpp b/examples/nra-translate/normalize.cpp index 38329fba6..e917fa43d 100644 --- a/examples/nra-translate/normalize.cpp +++ b/examples/nra-translate/normalize.cpp @@ -30,7 +30,7 @@ #include "parser/parser.h" #include "parser/parser_builder.h" #include "smt/smt_engine.h" -#include "smt_util/command.h" +#include "smt/command.h" using namespace std; using namespace CVC4; diff --git a/examples/nra-translate/smt2info.cpp b/examples/nra-translate/smt2info.cpp index 7efb5c855..bb9260572 100644 --- a/examples/nra-translate/smt2info.cpp +++ b/examples/nra-translate/smt2info.cpp @@ -25,7 +25,7 @@ #include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.h" -#include "smt_util/command.h" +#include "smt/command.h" using namespace std; using namespace CVC4; diff --git a/examples/nra-translate/smt2todreal.cpp b/examples/nra-translate/smt2todreal.cpp index 331cf894f..332763280 100644 --- a/examples/nra-translate/smt2todreal.cpp +++ b/examples/nra-translate/smt2todreal.cpp @@ -28,7 +28,7 @@ #include "parser/parser.h" #include "parser/parser_builder.h" #include "smt/smt_engine.h" -#include "smt_util/command.h" +#include "smt/command.h" using namespace std; using namespace CVC4; diff --git a/examples/nra-translate/smt2toisat.cpp b/examples/nra-translate/smt2toisat.cpp index bcfb4a180..9c93ac39a 100644 --- a/examples/nra-translate/smt2toisat.cpp +++ b/examples/nra-translate/smt2toisat.cpp @@ -26,8 +26,8 @@ #include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.h" +#include "smt/command.h" #include "smt/smt_engine.h" -#include "smt_util/command.h" using namespace std; using namespace CVC4; diff --git a/examples/nra-translate/smt2tomathematica.cpp b/examples/nra-translate/smt2tomathematica.cpp index ec1da2d7c..d2ff9b05d 100644 --- a/examples/nra-translate/smt2tomathematica.cpp +++ b/examples/nra-translate/smt2tomathematica.cpp @@ -26,7 +26,7 @@ #include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.h" -#include "smt_util/command.h" +#include "smt/command.h" using namespace std; using namespace CVC4; diff --git a/examples/nra-translate/smt2toqepcad.cpp b/examples/nra-translate/smt2toqepcad.cpp index ea9f2a4e6..d2e613dae 100644 --- a/examples/nra-translate/smt2toqepcad.cpp +++ b/examples/nra-translate/smt2toqepcad.cpp @@ -26,7 +26,7 @@ #include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.h" -#include "smt_util/command.h" +#include "smt/command.h" using namespace std; using namespace CVC4; diff --git a/examples/nra-translate/smt2toredlog.cpp b/examples/nra-translate/smt2toredlog.cpp index 934906b74..25eabfbad 100644 --- a/examples/nra-translate/smt2toredlog.cpp +++ b/examples/nra-translate/smt2toredlog.cpp @@ -26,8 +26,8 @@ #include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.h" +#include "smt/command.h" #include "smt/smt_engine.h" -#include "smt_util/command.h" using namespace std; using namespace CVC4; diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp index c07369661..18773af7b 100644 --- a/examples/sets-translate/sets_translate.cpp +++ b/examples/sets-translate/sets_translate.cpp @@ -28,7 +28,7 @@ #include "options/set_language.h" #include "parser/parser.h" #include "parser/parser_builder.h" -#include "smt_util/command.h" +#include "smt/command.h" #include "theory/logic_info.h" using namespace std; diff --git a/examples/translator.cpp b/examples/translator.cpp index 94f5ad1b8..3169c7308 100644 --- a/examples/translator.cpp +++ b/examples/translator.cpp @@ -29,8 +29,8 @@ #include "options/set_language.h" #include "parser/parser.h" #include "parser/parser_builder.h" +#include "smt/command.h" #include "smt/smt_engine.h" -#include "smt_util/command.h" using namespace std; using namespace CVC4; diff --git a/src/Makefile.am b/src/Makefile.am index fc346ded5..4f2998e7a 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -107,13 +107,21 @@ libcvc4_la_SOURCES = \ prop/sat_solver_factory.cpp \ smt/boolean_terms.cpp \ smt/boolean_terms.h \ + smt/command.cpp \ + smt/command.h \ smt/command_list.cpp \ smt/command_list.h \ + smt/dump.cpp \ + smt/dump.h \ + smt/ite_removal.cpp \ + smt/ite_removal.h \ smt/logic_exception.h \ smt/logic_request.cpp \ smt/logic_request.h \ smt/managed_ostreams.cpp \ smt/managed_ostreams.h \ + smt/model.cpp \ + smt/model.h \ smt/model_postprocessor.cpp \ smt/model_postprocessor.h \ smt/smt_engine.cpp \ @@ -478,6 +486,7 @@ EXTRA_DIST = \ include/cvc4parser_private.h \ include/cvc4parser_public.h \ mksubdirs \ + smt/command.i \ smt/logic_exception.i \ smt/smt_engine.i \ proof/unsat_core.i \ diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index a62776c80..ed8478ee8 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -32,7 +32,7 @@ #include "options/set_language.h" #include "parser/parser.h" #include "parser/parser_builder.h" -#include "smt_util/command.h" +#include "smt/command.h" #include "util/bitvector.h" #include "util/hash.h" #include "util/integer.h" diff --git a/src/cvc4.i b/src/cvc4.i index f4525203e..c950bb4c4 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -54,7 +54,7 @@ using namespace CVC4; #include "expr/expr.h" #include "expr/type.h" #include "options/option_exception.h" -#include "smt_util/command.h" +#include "smt/command.h" #include "util/bitvector.h" #include "util/integer.h" #include "util/sexpr.h" @@ -356,8 +356,8 @@ std::set CVC4::JavaInputStreamAdapter::s_adapters; %include "options/option_exception.i" %include "options/options.i" %include "parser/cvc4parser.i" +%include "smt/command.i" %include "smt/logic_exception.i" -%include "smt_util/command.i" %include "theory/logic_info.i" // Tim: This should come after "theory/logic_info.i". diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index 7f1b7fbe2..de8a67413 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -27,8 +27,8 @@ #include "prop/cnf_stream.h" #include "prop/prop_engine.h" #include "prop/sat_solver_types.h" +#include "smt/ite_removal.h" #include "smt/smt_engine_scope.h" -#include "smt_util/ite_removal.h" using namespace std; using namespace CVC4::prop; diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h index 210628afc..fca48ced1 100644 --- a/src/decision/decision_strategy.h +++ b/src/decision/decision_strategy.h @@ -20,7 +20,7 @@ #define __CVC4__DECISION__DECISION_STRATEGY_H #include "prop/sat_solver_types.h" -#include "smt_util/ite_removal.h" +#include "smt/ite_removal.h" namespace CVC4 { diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index e9f4997b7..bdde41b52 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -22,7 +22,7 @@ #include "expr/node_manager.h" #include "options/decision_options.h" #include "theory/rewriter.h" -#include "smt_util/ite_removal.h" +#include "smt/ite_removal.h" #include "smt/smt_statistics_registry.h" namespace CVC4 { diff --git a/src/include/cvc4.h b/src/include/cvc4.h index 09be6ff4c..90088de40 100644 --- a/src/include/cvc4.h +++ b/src/include/cvc4.h @@ -26,8 +26,8 @@ #include #include #include +#include #include -#include #include #include diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index b2dbaf39b..672dedc50 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -22,7 +22,7 @@ #include #include "main/main.h" -#include "smt_util/command.h" +#include "smt/command.h" namespace CVC4 { diff --git a/src/main/command_executor.h b/src/main/command_executor.h index 03bbe661b..d8294212a 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -20,8 +20,8 @@ #include "expr/expr_manager.h" #include "options/options.h" +#include "smt/command.h" #include "smt/smt_engine.h" -#include "smt_util/command.h" #include "util/statistics_registry.h" namespace CVC4 { diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index bf1143647..15165e82c 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -33,7 +33,7 @@ #include "main/portfolio.h" #include "options/options.h" #include "options/set_language.h" -#include "smt_util/command.h" +#include "smt/command.h" using namespace std; diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 83b85c170..b83907bd3 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -42,7 +42,7 @@ #include "parser/parser.h" #include "parser/parser_builder.h" #include "parser/parser_exception.h" -#include "smt_util/command.h" +#include "smt/command.h" #include "util/result.h" #include "util/statistics_registry.h" diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 19e4859b0..4982cb2bb 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -44,8 +44,8 @@ #include "parser/input.h" #include "parser/parser.h" #include "parser/parser_builder.h" +#include "smt/command.h" #include "theory/logic_info.h" -#include "smt_util/command.h" using namespace std; diff --git a/src/main/main.cpp b/src/main/main.cpp index 9151d8bf7..56fc3ef40 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -32,8 +32,8 @@ #include "parser/parser.h" #include "parser/parser_builder.h" #include "parser/parser_exception.h" +#include "smt/command.h" #include "smt/smt_engine.h" -#include "smt_util/command.h" #include "util/result.h" #include "util/statistics.h" diff --git a/src/main/portfolio.h b/src/main/portfolio.h index cab8bda3c..a7f15a04d 100644 --- a/src/main/portfolio.h +++ b/src/main/portfolio.h @@ -20,8 +20,8 @@ #include #include "options/options.h" +#include "smt/command.h" #include "smt/smt_engine.h" -#include "smt_util/command.h" #include "util/statistics_registry.h" namespace CVC4 { diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index 6428017f5..a1f74d694 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -37,7 +37,7 @@ #include "parser/smt2/smt2_input.h" #include "parser/smt2/sygus_input.h" #include "parser/tptp/tptp_input.h" -#include "smt_util/command.h" +#include "smt/command.h" using namespace std; using namespace CVC4; diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 08fba893e..d57aea93c 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -500,7 +500,7 @@ Expr addNots(ExprManager* em, size_t n, Expr e) { #include "options/set_language.h" #include "parser/antlr_tracing.h" #include "parser/parser.h" -#include "smt_util/command.h" +#include "smt/command.h" #include "util/subrange_bound.h" namespace CVC4 { diff --git a/src/parser/input.cpp b/src/parser/input.cpp index 7cc5ac0ca..896e8bc74 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -23,7 +23,7 @@ #include "expr/type.h" #include "parser/parser.h" #include "parser/parser_exception.h" -#include "smt_util/command.h" +#include "smt/command.h" using namespace std; diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 3cfe78145..b9531e8d9 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -32,7 +32,7 @@ #include "options/options.h" #include "parser/input.h" #include "parser/parser_exception.h" -#include "smt_util/command.h" +#include "smt/command.h" #include "util/resource_manager.h" using namespace std; diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g index e8b7d5b9b..a8e797470 100644 --- a/src/parser/smt1/Smt1.g +++ b/src/parser/smt1/Smt1.g @@ -72,7 +72,7 @@ options { #include -#include "smt_util/command.h" +#include "smt/command.h" #include "parser/parser.h" #include "parser/antlr_tracing.h" diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp index 01bc8901e..a2abee2e7 100644 --- a/src/parser/smt1/smt1.cpp +++ b/src/parser/smt1/smt1.cpp @@ -18,7 +18,7 @@ namespace std { } #include "expr/type.h" -#include "smt_util/command.h" +#include "smt/command.h" #include "parser/parser.h" #include "parser/smt1/smt1.h" diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 8be9ad2dd..fb3b5ec5e 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -86,7 +86,7 @@ using namespace CVC4::parser; #include "parser/parser.h" #include "parser/antlr_tracing.h" -#include "smt_util/command.h" +#include "smt/command.h" namespace CVC4 { class Expr; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 3b1467b5e..e3fbe36f2 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -21,7 +21,7 @@ #include "parser/parser.h" #include "parser/smt1/smt1.h" #include "parser/smt2/smt2_input.h" -#include "smt_util/command.h" +#include "smt/command.h" #include "util/bitvector.h" // ANTLR defines these, which is really bad! diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 52951dd38..d57aea376 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -92,7 +92,7 @@ using namespace CVC4::parser; // files. See the documentation in "parser/antlr_undefines.h" for more details. #include "parser/antlr_undefines.h" -#include "smt_util/command.h" +#include "smt/command.h" #include "parser/parser.h" #include "parser/tptp/tptp.h" #include "parser/antlr_tracing.h" diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index 5e00ea1ce..0937a11bf 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -25,7 +25,7 @@ #include #include "parser/parser.h" -#include "smt_util/command.h" +#include "smt/command.h" #include "util/hash.h" namespace CVC4 { diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index b26a983be..d05309ef7 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -24,7 +24,7 @@ #include "expr/node_manager_attributes.h" // for VarNameAttr #include "options/language.h" // for LANG_AST #include "printer/dagification_visitor.h" -#include "smt_util/command.h" +#include "smt/command.h" #include "smt_util/node_visitor.h" #include "theory/substitutions.h" diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index db4558af6..25f958963 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -29,8 +29,8 @@ #include "options/language.h" // for LANG_AST #include "printer/dagification_visitor.h" #include "options/smt_options.h" +#include "smt/command.h" #include "smt/smt_engine.h" -#include "smt_util/command.h" #include "smt_util/node_visitor.h" #include "theory/arrays/theory_arrays_rewriter.h" #include "theory/substitutions.h" diff --git a/src/printer/printer.h b/src/printer/printer.h index aa6bf0470..f4cd4635c 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -24,8 +24,8 @@ #include "expr/node.h" #include "options/language.h" -#include "smt_util/command.h" -#include "smt_util/model.h" +#include "smt/command.h" +#include "smt/model.h" #include "util/sexpr.h" namespace CVC4 { diff --git a/src/printer/smt1/smt1_printer.cpp b/src/printer/smt1/smt1_printer.cpp index 87880d3bc..bcd6faa83 100644 --- a/src/printer/smt1/smt1_printer.cpp +++ b/src/printer/smt1/smt1_printer.cpp @@ -23,7 +23,7 @@ #include "expr/expr.h" // for ExprSetDepth etc.. #include "expr/node_manager.h" // for VarNameAttr #include "options/language.h" // for LANG_AST -#include "smt_util/command.h" +#include "smt/command.h" using namespace std; diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp index 923a7b3aa..46ae47ba4 100644 --- a/src/printer/tptp/tptp_printer.cpp +++ b/src/printer/tptp/tptp_printer.cpp @@ -23,7 +23,7 @@ #include "expr/expr.h" // for ExprSetDepth etc.. #include "expr/node_manager.h" // for VarNameAttr #include "options/language.h" // for LANG_AST -#include "smt_util/command.h" +#include "smt/command.h" using namespace std; diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp index 37cc62aa0..2b559d117 100644 --- a/src/proof/unsat_core.cpp +++ b/src/proof/unsat_core.cpp @@ -19,8 +19,8 @@ #include "expr/expr_iomanip.h" #include "options/base_options.h" #include "printer/printer.h" +#include "smt/command.h" #include "smt/smt_engine_scope.h" -#include "smt_util/command.h" namespace CVC4 { diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 1cd32bee8..d54848d26 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -29,8 +29,8 @@ #include "prop/minisat/minisat.h" #include "prop/prop_engine.h" #include "prop/theory_proxy.h" +#include "smt/command.h" #include "smt/smt_engine_scope.h" -#include "smt_util/command.h" #include "theory/theory.h" #include "theory/theory_engine.h" diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index f4489c4be..b7fb1603d 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -31,7 +31,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/minisat.h" #include "prop/minisat/mtl/Sort.h" #include "prop/theory_proxy.h" -#include "smt_util/command.h" using namespace CVC4::prop; @@ -479,15 +478,18 @@ void Solver::cancelUntil(int level) { for (int l = trail_lim.size() - level; l > 0; --l) { context->pop(); if(Dump.isOn("state")) { - Dump("state") << PopCommand(); + proxy->dumpStatePop(); } } for (int c = trail.size()-1; c >= trail_lim[level]; c--){ Var x = var(trail[c]); assigns [x] = l_Undef; vardata[x].trail_index = -1; - if ((phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last()) && (polarity[x] & 0x2) == 0) + if ((phase_saving > 1 || + ((phase_saving == 1) && c > trail_lim.last()) + ) && ((polarity[x] & 0x2) == 0)) { polarity[x] = sign(trail[c]); + } insertVarOrder(x); } qhead = trail_lim[level]; diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index a239eba72..777fb1093 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -32,7 +32,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/mtl/Heap.h" #include "prop/minisat/mtl/Vec.h" #include "prop/minisat/utils/Options.h" -#include "smt_util/command.h" #include "theory/theory.h" diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 36d6408b5..583e9da18 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -36,7 +36,7 @@ #include "prop/sat_solver_factory.h" #include "prop/theory_proxy.h" #include "smt/smt_statistics_registry.h" -#include "smt_util/command.h" +#include "smt/command.h" #include "theory/theory_engine.h" #include "theory/theory_registrar.h" #include "util/resource_manager.h" diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 5de97d0d8..63a09169f 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -23,9 +23,10 @@ #include "prop/cnf_stream.h" #include "prop/prop_engine.h" #include "proof/cnf_proof.h" +#include "smt/command.h" +#include "smt/smt_statistics_registry.h" #include "smt_util/lemma_input_channel.h" #include "smt_util/lemma_output_channel.h" -#include "smt/smt_statistics_registry.h" #include "theory/rewriter.h" #include "theory/theory_engine.h" #include "util/statistics_registry.h" @@ -236,5 +237,11 @@ SatValue TheoryProxy::getDecisionPolarity(SatVariable var) { return d_decisionEngine->getPolarity(var); } +void TheoryProxy::dumpStatePop() { + if(Dump.isOn("state")) { + Dump("state") << PopCommand(); + } +} + }/* CVC4::prop namespace */ }/* CVC4 namespace */ diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index acc242ab6..0e2b885d9 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -99,6 +99,9 @@ public: SatValue getDecisionPolarity(SatVariable var); + /** Shorthand for Dump("state") << PopCommand() */ + void dumpStatePop(); + private: /** The prop engine we are using. */ PropEngine* d_propEngine; diff --git a/src/smt/command.cpp b/src/smt/command.cpp new file mode 100644 index 000000000..d6ec0769a --- /dev/null +++ b/src/smt/command.cpp @@ -0,0 +1,1855 @@ +/********************* */ +/*! \file command.cpp + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): Kshitij Bansal, Dejan Jovanovic, Andrew Reynolds, Francois Bobot + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of command objects. + ** + ** Implementation of command objects. + **/ + +#include "smt/command.h" + +#include +#include +#include +#include +#include +#include + +#include "base/cvc4_assert.h" +#include "base/output.h" +#include "expr/expr_iomanip.h" +#include "expr/node.h" +#include "options/options.h" +#include "options/smt_options.h" +#include "printer/printer.h" +#include "smt/dump.h" +#include "smt/model.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" +#include "util/sexpr.h" + +using namespace std; + +namespace CVC4 { + +const int CommandPrintSuccess::s_iosIndex = std::ios_base::xalloc(); +const CommandSuccess* CommandSuccess::s_instance = new CommandSuccess(); +const CommandInterrupted* CommandInterrupted::s_instance = new CommandInterrupted(); + +std::ostream& operator<<(std::ostream& out, const Command& c) throw() { + c.toStream(out, + Node::setdepth::getDepth(out), + Node::printtypes::getPrintTypes(out), + Node::dag::getDag(out), + Node::setlanguage::getLanguage(out)); + return out; +} + +ostream& operator<<(ostream& out, const Command* c) throw() { + if(c == NULL) { + out << "null"; + } else { + out << *c; + } + return out; +} + +std::ostream& operator<<(std::ostream& out, const CommandStatus& s) throw() { + s.toStream(out, Node::setlanguage::getLanguage(out)); + return out; +} + +ostream& operator<<(ostream& out, const CommandStatus* s) throw() { + if(s == NULL) { + out << "null"; + } else { + out << *s; + } + return out; +} + +/* class Command */ + +Command::Command() throw() : d_commandStatus(NULL), d_muted(false) { +} + +Command::Command(const Command& cmd) { + d_commandStatus = (cmd.d_commandStatus == NULL) ? NULL : &cmd.d_commandStatus->clone(); + d_muted = cmd.d_muted; +} + +Command::~Command() throw() { + if(d_commandStatus != NULL && d_commandStatus != CommandSuccess::instance()) { + delete d_commandStatus; + } +} + +bool Command::ok() const throw() { + // either we haven't run the command yet, or it ran successfully + return d_commandStatus == NULL || dynamic_cast(d_commandStatus) != NULL; +} + +bool Command::fail() const throw() { + return d_commandStatus != NULL && dynamic_cast(d_commandStatus) != NULL; +} + +bool Command::interrupted() const throw() { + return d_commandStatus != NULL && dynamic_cast(d_commandStatus) != NULL; +} + +void Command::invoke(SmtEngine* smtEngine, std::ostream& out) throw() { + invoke(smtEngine); + if(!(isMuted() && ok())) { + printResult(out, smtEngine->getOption("command-verbosity:" + getCommandName()).getIntegerValue().toUnsignedInt()); + } +} + +std::string Command::toString() const throw() { + std::stringstream ss; + toStream(ss); + return ss.str(); +} + +void Command::toStream(std::ostream& out, int toDepth, bool types, size_t dag, + OutputLanguage language) const throw() { + Printer::getPrinter(language)->toStream(out, this, toDepth, types, dag); +} + +void CommandStatus::toStream(std::ostream& out, OutputLanguage language) const throw() { + Printer::getPrinter(language)->toStream(out, this); +} + +void Command::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(d_commandStatus != NULL) { + if((!ok() && verbosity >= 1) || verbosity >= 2) { + out << *d_commandStatus; + } + } +} + +/* class EmptyCommand */ + +EmptyCommand::EmptyCommand(std::string name) throw() : + d_name(name) { +} + +std::string EmptyCommand::getName() const throw() { + return d_name; +} + +void EmptyCommand::invoke(SmtEngine* smtEngine) throw() { + /* empty commands have no implementation */ + d_commandStatus = CommandSuccess::instance(); +} + +Command* EmptyCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new EmptyCommand(d_name); +} + +Command* EmptyCommand::clone() const { + return new EmptyCommand(d_name); +} + +std::string EmptyCommand::getCommandName() const throw() { + return "empty"; +} + +/* class EchoCommand */ + +EchoCommand::EchoCommand(std::string output) throw() : + d_output(output) { +} + +std::string EchoCommand::getOutput() const throw() { + return d_output; +} + +void EchoCommand::invoke(SmtEngine* smtEngine) throw() { + /* we don't have an output stream here, nothing to do */ + d_commandStatus = CommandSuccess::instance(); +} + +void EchoCommand::invoke(SmtEngine* smtEngine, std::ostream& out) throw() { + out << d_output << std::endl; + d_commandStatus = CommandSuccess::instance(); + printResult(out, smtEngine->getOption("command-verbosity:" + getCommandName()).getIntegerValue().toUnsignedInt()); +} + +Command* EchoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new EchoCommand(d_output); +} + +Command* EchoCommand::clone() const { + return new EchoCommand(d_output); +} + +std::string EchoCommand::getCommandName() const throw() { + return "echo"; +} + +/* class AssertCommand */ + +AssertCommand::AssertCommand(const Expr& e, bool inUnsatCore) throw() : + d_expr(e), d_inUnsatCore(inUnsatCore) { +} + +Expr AssertCommand::getExpr() const throw() { + return d_expr; +} + +void AssertCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->assertFormula(d_expr, d_inUnsatCore); + d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* AssertCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new AssertCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore); +} + +Command* AssertCommand::clone() const { + return new AssertCommand(d_expr, d_inUnsatCore); +} + +std::string AssertCommand::getCommandName() const throw() { + return "assert"; +} + +/* class PushCommand */ + +void PushCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->push(); + d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* PushCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new PushCommand(); +} + +Command* PushCommand::clone() const { + return new PushCommand(); +} + +std::string PushCommand::getCommandName() const throw() { + return "push"; +} + +/* class PopCommand */ + +void PopCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->pop(); + d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* PopCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new PopCommand(); +} + +Command* PopCommand::clone() const { + return new PopCommand(); +} + +std::string PopCommand::getCommandName() const throw() { + return "pop"; +} + +/* class CheckSatCommand */ + +CheckSatCommand::CheckSatCommand() throw() : + d_expr() { +} + +CheckSatCommand::CheckSatCommand(const Expr& expr, bool inUnsatCore) throw() : + d_expr(expr), d_inUnsatCore(inUnsatCore) { +} + +Expr CheckSatCommand::getExpr() const throw() { + return d_expr; +} + +void CheckSatCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_result = smtEngine->checkSat(d_expr); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Result CheckSatCommand::getResult() const throw() { + return d_result; +} + +void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + out << d_result << endl; + } +} + +Command* CheckSatCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& 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, d_inUnsatCore); + c->d_result = d_result; + return c; +} + +std::string CheckSatCommand::getCommandName() const throw() { + return "check-sat"; +} + +/* class QueryCommand */ + +QueryCommand::QueryCommand(const Expr& e, bool inUnsatCore) throw() : + d_expr(e), d_inUnsatCore(inUnsatCore) { +} + +Expr QueryCommand::getExpr() const throw() { + return d_expr; +} + +void QueryCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_result = smtEngine->query(d_expr); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Result QueryCommand::getResult() const throw() { + return d_result; +} + +void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + out << d_result << endl; + } +} + +Command* QueryCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& 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, d_inUnsatCore); + c->d_result = d_result; + return c; +} + +std::string QueryCommand::getCommandName() const throw() { + return "query"; +} + +/* class ResetCommand */ + +void ResetCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->reset(); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* ResetCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new ResetCommand(); +} + +Command* ResetCommand::clone() const { + return new ResetCommand(); +} + +std::string ResetCommand::getCommandName() const throw() { + return "reset"; +} + +/* class ResetAssertionsCommand */ + +void ResetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->resetAssertions(); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* ResetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new ResetAssertionsCommand(); +} + +Command* ResetAssertionsCommand::clone() const { + return new ResetAssertionsCommand(); +} + +std::string ResetAssertionsCommand::getCommandName() const throw() { + return "reset-assertions"; +} + +/* class QuitCommand */ + +void QuitCommand::invoke(SmtEngine* smtEngine) throw() { + Dump("benchmark") << *this; + d_commandStatus = CommandSuccess::instance(); +} + +Command* QuitCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new QuitCommand(); +} + +Command* QuitCommand::clone() const { + return new QuitCommand(); +} + +std::string QuitCommand::getCommandName() const throw() { + return "exit"; +} + +/* class CommentCommand */ + +CommentCommand::CommentCommand(std::string comment) throw() : d_comment(comment) { +} + +std::string CommentCommand::getComment() const throw() { + return d_comment; +} + +void CommentCommand::invoke(SmtEngine* smtEngine) throw() { + Dump("benchmark") << *this; + d_commandStatus = CommandSuccess::instance(); +} + +Command* CommentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new CommentCommand(d_comment); +} + +Command* CommentCommand::clone() const { + return new CommentCommand(d_comment); +} + +std::string CommentCommand::getCommandName() const throw() { + return "comment"; +} + +/* class CommandSequence */ + +CommandSequence::CommandSequence() throw() : + d_index(0) { +} + +CommandSequence::~CommandSequence() throw() { + for(unsigned i = d_index; i < d_commandSequence.size(); ++i) { + delete d_commandSequence[i]; + } +} + +void CommandSequence::addCommand(Command* cmd) throw() { + d_commandSequence.push_back(cmd); +} + +void CommandSequence::clear() throw() { + d_commandSequence.clear(); +} + +void CommandSequence::invoke(SmtEngine* smtEngine) throw() { + for(; d_index < d_commandSequence.size(); ++d_index) { + d_commandSequence[d_index]->invoke(smtEngine); + if(! d_commandSequence[d_index]->ok()) { + // abort execution + d_commandStatus = d_commandSequence[d_index]->getCommandStatus(); + return; + } + delete d_commandSequence[d_index]; + } + + AlwaysAssert(d_commandStatus == NULL); + d_commandStatus = CommandSuccess::instance(); +} + +void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) throw() { + for(; d_index < d_commandSequence.size(); ++d_index) { + d_commandSequence[d_index]->invoke(smtEngine, out); + if(! d_commandSequence[d_index]->ok()) { + // abort execution + d_commandStatus = d_commandSequence[d_index]->getCommandStatus(); + return; + } + delete d_commandSequence[d_index]; + } + + AlwaysAssert(d_commandStatus == NULL); + d_commandStatus = CommandSuccess::instance(); +} + +Command* CommandSequence::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + CommandSequence* seq = new CommandSequence(); + for(iterator i = begin(); i != end(); ++i) { + Command* cmd_to_export = *i; + Command* cmd = cmd_to_export->exportTo(exprManager, variableMap); + seq->addCommand(cmd); + Debug("export") << "[export] so far converted: " << seq << endl; + } + seq->d_index = d_index; + return seq; +} + +Command* CommandSequence::clone() const { + CommandSequence* seq = new CommandSequence(); + for(const_iterator i = begin(); i != end(); ++i) { + seq->addCommand((*i)->clone()); + } + seq->d_index = d_index; + return seq; +} + +CommandSequence::const_iterator CommandSequence::begin() const throw() { + return d_commandSequence.begin(); +} + +CommandSequence::const_iterator CommandSequence::end() const throw() { + return d_commandSequence.end(); +} + +CommandSequence::iterator CommandSequence::begin() throw() { + return d_commandSequence.begin(); +} + +CommandSequence::iterator CommandSequence::end() throw() { + return d_commandSequence.end(); +} + +std::string CommandSequence::getCommandName() const throw() { + return "sequence"; +} + +/* class DeclarationSequenceCommand */ + +/* class DeclarationDefinitionCommand */ + +DeclarationDefinitionCommand::DeclarationDefinitionCommand(const std::string& id) throw() : + d_symbol(id) { +} + +std::string DeclarationDefinitionCommand::getSymbol() const throw() { + return d_symbol; +} + +/* class DeclareFunctionCommand */ + +DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id, Expr func, Type t) throw() : + DeclarationDefinitionCommand(id), + d_func(func), + d_type(t), + d_printInModel(true), + d_printInModelSetByUser(false){ +} + +Expr DeclareFunctionCommand::getFunction() const throw() { + return d_func; +} + +Type DeclareFunctionCommand::getType() const throw() { + return d_type; +} + +bool DeclareFunctionCommand::getPrintInModel() const throw() { + return d_printInModel; +} + +bool DeclareFunctionCommand::getPrintInModelSetByUser() const throw() { + return d_printInModelSetByUser; +} + +void DeclareFunctionCommand::setPrintInModel( bool p ) { + d_printInModel = p; + d_printInModelSetByUser = true; +} + +void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() { + d_commandStatus = CommandSuccess::instance(); +} + +Command* DeclareFunctionCommand::exportTo(ExprManager* exprManager, + ExprManagerMapCollection& variableMap) { + DeclareFunctionCommand * dfc = new DeclareFunctionCommand(d_symbol, d_func.exportTo(exprManager, variableMap), + d_type.exportTo(exprManager, variableMap)); + dfc->d_printInModel = d_printInModel; + dfc->d_printInModelSetByUser = d_printInModelSetByUser; + return dfc; +} + +Command* DeclareFunctionCommand::clone() const { + DeclareFunctionCommand * dfc = new DeclareFunctionCommand(d_symbol, d_func, d_type); + dfc->d_printInModel = d_printInModel; + dfc->d_printInModelSetByUser = d_printInModelSetByUser; + return dfc; +} + +std::string DeclareFunctionCommand::getCommandName() const throw() { + return "declare-fun"; +} + +/* class DeclareTypeCommand */ + +DeclareTypeCommand::DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw() : + DeclarationDefinitionCommand(id), + d_arity(arity), + d_type(t) { +} + +size_t DeclareTypeCommand::getArity() const throw() { + return d_arity; +} + +Type DeclareTypeCommand::getType() const throw() { + return d_type; +} + +void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() { + d_commandStatus = CommandSuccess::instance(); +} + +Command* DeclareTypeCommand::exportTo(ExprManager* exprManager, + ExprManagerMapCollection& variableMap) { + return new DeclareTypeCommand(d_symbol, d_arity, + d_type.exportTo(exprManager, variableMap)); +} + +Command* DeclareTypeCommand::clone() const { + return new DeclareTypeCommand(d_symbol, d_arity, d_type); +} + +std::string DeclareTypeCommand::getCommandName() const throw() { + return "declare-sort"; +} + +/* class DefineTypeCommand */ + +DefineTypeCommand::DefineTypeCommand(const std::string& id, + Type t) throw() : + DeclarationDefinitionCommand(id), + d_params(), + d_type(t) { +} + +DefineTypeCommand::DefineTypeCommand(const std::string& id, + const std::vector& params, + Type t) throw() : + DeclarationDefinitionCommand(id), + d_params(params), + d_type(t) { +} + +const std::vector& DefineTypeCommand::getParameters() const throw() { + return d_params; +} + +Type DefineTypeCommand::getType() const throw() { + return d_type; +} + +void DefineTypeCommand::invoke(SmtEngine* smtEngine) throw() { + d_commandStatus = CommandSuccess::instance(); +} + +Command* DefineTypeCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + vector params; + transform(d_params.begin(), d_params.end(), back_inserter(params), + ExportTransformer(exprManager, variableMap)); + Type type = d_type.exportTo(exprManager, variableMap); + return new DefineTypeCommand(d_symbol, params, type); +} + +Command* DefineTypeCommand::clone() const { + return new DefineTypeCommand(d_symbol, d_params, d_type); +} + +std::string DefineTypeCommand::getCommandName() const throw() { + return "define-sort"; +} + +/* class DefineFunctionCommand */ + +DefineFunctionCommand::DefineFunctionCommand(const std::string& id, + Expr func, + Expr formula) throw() : + DeclarationDefinitionCommand(id), + d_func(func), + d_formals(), + d_formula(formula) { +} + +DefineFunctionCommand::DefineFunctionCommand(const std::string& id, + Expr func, + const std::vector& formals, + Expr formula) throw() : + DeclarationDefinitionCommand(id), + d_func(func), + d_formals(formals), + d_formula(formula) { +} + +Expr DefineFunctionCommand::getFunction() const throw() { + return d_func; +} + +const std::vector& DefineFunctionCommand::getFormals() const throw() { + return d_formals; +} + +Expr DefineFunctionCommand::getFormula() const throw() { + return d_formula; +} + +void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() { + try { + if(!d_func.isNull()) { + smtEngine->defineFunction(d_func, d_formals, d_formula); + } + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* DefineFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + Expr func = d_func.exportTo(exprManager, variableMap, /* flags = */ ExprManager::VAR_FLAG_DEFINED); + vector formals; + transform(d_formals.begin(), d_formals.end(), back_inserter(formals), + ExportTransformer(exprManager, variableMap)); + Expr formula = d_formula.exportTo(exprManager, variableMap); + return new DefineFunctionCommand(d_symbol, func, formals, formula); +} + +Command* DefineFunctionCommand::clone() const { + return new DefineFunctionCommand(d_symbol, d_func, d_formals, d_formula); +} + +std::string DefineFunctionCommand::getCommandName() const throw() { + return "define-fun"; +} + +/* class DefineNamedFunctionCommand */ + +DefineNamedFunctionCommand::DefineNamedFunctionCommand(const std::string& id, + Expr func, + const std::vector& formals, + Expr formula) throw() : + DefineFunctionCommand(id, func, formals, formula) { +} + +void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) throw() { + this->DefineFunctionCommand::invoke(smtEngine); + if(!d_func.isNull() && d_func.getType().isBoolean()) { + smtEngine->addToAssignment(d_func.getExprManager()->mkExpr(kind::APPLY, d_func)); + } + d_commandStatus = CommandSuccess::instance(); +} + +Command* DefineNamedFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + Expr func = d_func.exportTo(exprManager, variableMap); + vector formals; + transform(d_formals.begin(), d_formals.end(), back_inserter(formals), + ExportTransformer(exprManager, variableMap)); + Expr formula = d_formula.exportTo(exprManager, variableMap); + return new DefineNamedFunctionCommand(d_symbol, func, formals, formula); +} + +Command* DefineNamedFunctionCommand::clone() const { + return new DefineNamedFunctionCommand(d_symbol, d_func, d_formals, d_formula); +} + +/* class SetUserAttribute */ + +SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr ) throw() : + d_attr( attr ), d_expr( expr ){ +} + +SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr, + std::vector& values ) throw() : + d_attr( attr ), d_expr( expr ){ + d_expr_values.insert( d_expr_values.begin(), values.begin(), values.end() ); +} + +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, d_expr_values, d_str_value ); + } + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* SetUserAttributeCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap){ + Expr expr = d_expr.exportTo(exprManager, variableMap); + 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{ + 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() { + return "set-user-attribute"; +} + +/* class SimplifyCommand */ + +SimplifyCommand::SimplifyCommand(Expr term) throw() : + d_term(term) { +} + +Expr SimplifyCommand::getTerm() const throw() { + return d_term; +} + +void SimplifyCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_result = smtEngine->simplify(d_term); + d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Expr SimplifyCommand::getResult() const throw() { + return d_result; +} + +void SimplifyCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + out << d_result << endl; + } +} + +Command* SimplifyCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + SimplifyCommand* c = new SimplifyCommand(d_term.exportTo(exprManager, variableMap)); + c->d_result = d_result.exportTo(exprManager, variableMap); + return c; +} + +Command* SimplifyCommand::clone() const { + SimplifyCommand* c = new SimplifyCommand(d_term); + c->d_result = d_result; + return c; +} + +std::string SimplifyCommand::getCommandName() const throw() { + return "simplify"; +} + +/* class ExpandDefinitionsCommand */ + +ExpandDefinitionsCommand::ExpandDefinitionsCommand(Expr term) throw() : + d_term(term) { +} + +Expr ExpandDefinitionsCommand::getTerm() const throw() { + return d_term; +} + +void ExpandDefinitionsCommand::invoke(SmtEngine* smtEngine) throw() { + d_result = smtEngine->expandDefinitions(d_term); + d_commandStatus = CommandSuccess::instance(); +} + +Expr ExpandDefinitionsCommand::getResult() const throw() { + return d_result; +} + +void ExpandDefinitionsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + out << d_result << endl; + } +} + +Command* ExpandDefinitionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term.exportTo(exprManager, variableMap)); + c->d_result = d_result.exportTo(exprManager, variableMap); + return c; +} + +Command* ExpandDefinitionsCommand::clone() const { + ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term); + c->d_result = d_result; + return c; +} + +std::string ExpandDefinitionsCommand::getCommandName() const throw() { + return "expand-definitions"; +} + +/* class GetValueCommand */ + +GetValueCommand::GetValueCommand(Expr term) throw() : + d_terms() { + d_terms.push_back(term); +} + +GetValueCommand::GetValueCommand(const std::vector& terms) throw() : + d_terms(terms) { + PrettyCheckArgument(terms.size() >= 1, terms, + "cannot get-value of an empty set of terms"); +} + +const std::vector& GetValueCommand::getTerms() const throw() { + return d_terms; +} + +void GetValueCommand::invoke(SmtEngine* smtEngine) throw() { + try { + vector result; + ExprManager* em = smtEngine->getExprManager(); + NodeManager* nm = NodeManager::fromExprManager(em); + for(std::vector::const_iterator i = d_terms.begin(); i != d_terms.end(); ++i) { + Assert(nm == NodeManager::fromExprManager((*i).getExprManager())); + smt::SmtScope scope(smtEngine); + Node request = Node::fromExpr(options::expandDefinitions() ? smtEngine->expandDefinitions(*i) : *i); + Node value = Node::fromExpr(smtEngine->getValue(*i)); + if(value.getType().isInteger() && request.getType() == nm->realType()) { + // Need to wrap in special marker so that output printers know this + // is an integer-looking constant that really should be output as + // a rational. Necessary for SMT-LIB standards compliance, but ugly. + value = nm->mkNode(kind::APPLY_TYPE_ASCRIPTION, + nm->mkConst(AscriptionType(em->realType())), value); + } + result.push_back(nm->mkNode(kind::SEXPR, request, value).toExpr()); + } + d_result = em->mkExpr(kind::SEXPR, result); + d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Expr GetValueCommand::getResult() const throw() { + return d_result; +} + +void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + expr::ExprDag::Scope scope(out, false); + out << d_result << endl; + } +} + +Command* GetValueCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + vector exportedTerms; + for(std::vector::const_iterator i = d_terms.begin(); i != d_terms.end(); ++i) { + exportedTerms.push_back((*i).exportTo(exprManager, variableMap)); + } + GetValueCommand* c = new GetValueCommand(exportedTerms); + c->d_result = d_result.exportTo(exprManager, variableMap); + return c; +} + +Command* GetValueCommand::clone() const { + GetValueCommand* c = new GetValueCommand(d_terms); + c->d_result = d_result; + return c; +} + +std::string GetValueCommand::getCommandName() const throw() { + return "get-value"; +} + +/* class GetAssignmentCommand */ + +GetAssignmentCommand::GetAssignmentCommand() throw() { +} + +void GetAssignmentCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_result = smtEngine->getAssignment(); + d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +SExpr GetAssignmentCommand::getResult() const throw() { + return d_result; +} + +void GetAssignmentCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + out << d_result << endl; + } +} + +Command* GetAssignmentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetAssignmentCommand* c = new GetAssignmentCommand(); + c->d_result = d_result; + return c; +} + +Command* GetAssignmentCommand::clone() const { + GetAssignmentCommand* c = new GetAssignmentCommand(); + c->d_result = d_result; + return c; +} + +std::string GetAssignmentCommand::getCommandName() const throw() { + return "get-assignment"; +} + +/* class GetModelCommand */ + +GetModelCommand::GetModelCommand() throw() { +} + +void GetModelCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_result = smtEngine->getModel(); + d_smtEngine = smtEngine; + d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +/* Model is private to the library -- for now +Model* GetModelCommand::getResult() const throw() { + return d_result; +} +*/ + +void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + out << *d_result; + } +} + +Command* GetModelCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetModelCommand* c = new GetModelCommand(); + c->d_result = d_result; + c->d_smtEngine = d_smtEngine; + return c; +} + +Command* GetModelCommand::clone() const { + GetModelCommand* c = new GetModelCommand(); + c->d_result = d_result; + c->d_smtEngine = d_smtEngine; + return c; +} + +std::string GetModelCommand::getCommandName() const throw() { + return "get-model"; +} + +/* class GetProofCommand */ + +GetProofCommand::GetProofCommand() throw() { +} + +void GetProofCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_smtEngine = smtEngine; + d_result = smtEngine->getProof(); + d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Proof* GetProofCommand::getResult() const throw() { + return d_result; +} + +void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + smt::SmtScope scope(d_smtEngine); + d_result->toStream(out); + } +} + +Command* GetProofCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetProofCommand* c = new GetProofCommand(); + c->d_result = d_result; + c->d_smtEngine = d_smtEngine; + return c; +} + +Command* GetProofCommand::clone() const { + GetProofCommand* c = new GetProofCommand(); + c->d_result = d_result; + c->d_smtEngine = d_smtEngine; + return c; +} + +std::string GetProofCommand::getCommandName() const throw() { + return "get-proof"; +} + +/* class GetInstantiationsCommand */ + +GetInstantiationsCommand::GetInstantiationsCommand() throw() { +} + +void GetInstantiationsCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_smtEngine = smtEngine; + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +//Instantiations* GetInstantiationsCommand::getResult() const throw() { +// return d_result; +//} + +void GetInstantiationsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + d_smtEngine->printInstantiations(out); + } +} + +Command* GetInstantiationsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetInstantiationsCommand* c = new GetInstantiationsCommand(); + //c->d_result = d_result; + c->d_smtEngine = d_smtEngine; + return c; +} + +Command* GetInstantiationsCommand::clone() const { + GetInstantiationsCommand* c = new GetInstantiationsCommand(); + //c->d_result = d_result; + c->d_smtEngine = d_smtEngine; + return c; +} + +std::string GetInstantiationsCommand::getCommandName() const throw() { + return "get-instantiations"; +} + +/* class GetSynthSolutionCommand */ + +GetSynthSolutionCommand::GetSynthSolutionCommand() throw() { +} + +void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_smtEngine = smtEngine; + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +void GetSynthSolutionCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + d_smtEngine->printSynthSolution(out); + } +} + +Command* GetSynthSolutionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetSynthSolutionCommand* c = new GetSynthSolutionCommand(); + c->d_smtEngine = d_smtEngine; + return c; +} + +Command* GetSynthSolutionCommand::clone() const { + GetSynthSolutionCommand* c = new GetSynthSolutionCommand(); + c->d_smtEngine = d_smtEngine; + return c; +} + +std::string GetSynthSolutionCommand::getCommandName() const throw() { + return "get-instantiations"; +} + +/* class GetUnsatCoreCommand */ + +GetUnsatCoreCommand::GetUnsatCoreCommand() throw() { +} + +GetUnsatCoreCommand::GetUnsatCoreCommand(const std::map& 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()); + } +} + +void GetUnsatCoreCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + 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(d_names); + c->d_result = d_result; + return c; +} + +Command* GetUnsatCoreCommand::clone() const { + GetUnsatCoreCommand* c = new GetUnsatCoreCommand(d_names); + c->d_result = d_result; + return c; +} + +std::string GetUnsatCoreCommand::getCommandName() const throw() { + return "get-unsat-core"; +} + +/* class GetAssertionsCommand */ + +GetAssertionsCommand::GetAssertionsCommand() throw() { +} + +void GetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() { + try { + stringstream ss; + const vector v = smtEngine->getAssertions(); + ss << "(\n"; + copy( v.begin(), v.end(), ostream_iterator(ss, "\n") ); + ss << ")\n"; + d_result = ss.str(); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +std::string GetAssertionsCommand::getResult() const throw() { + return d_result; +} + +void GetAssertionsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + out << d_result; + } +} + +Command* GetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetAssertionsCommand* c = new GetAssertionsCommand(); + c->d_result = d_result; + return c; +} + +Command* GetAssertionsCommand::clone() const { + GetAssertionsCommand* c = new GetAssertionsCommand(); + c->d_result = d_result; + return c; +} + +std::string GetAssertionsCommand::getCommandName() const throw() { + return "get-assertions"; +} + +/* class SetBenchmarkStatusCommand */ + +SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) throw() : + d_status(status) { +} + +BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const throw() { + return d_status; +} + +void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) throw() { + try { + stringstream ss; + ss << d_status; + SExpr status = SExpr(ss.str()); + smtEngine->setInfo("status", status); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* SetBenchmarkStatusCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new SetBenchmarkStatusCommand(d_status); +} + +Command* SetBenchmarkStatusCommand::clone() const { + return new SetBenchmarkStatusCommand(d_status); +} + +std::string SetBenchmarkStatusCommand::getCommandName() const throw() { + return "set-info"; +} + +/* class SetBenchmarkLogicCommand */ + +SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) throw() : + d_logic(logic) { +} + +std::string SetBenchmarkLogicCommand::getLogic() const throw() { + return d_logic; +} + +void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->setLogic(d_logic); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* SetBenchmarkLogicCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new SetBenchmarkLogicCommand(d_logic); +} + +Command* SetBenchmarkLogicCommand::clone() const { + return new SetBenchmarkLogicCommand(d_logic); +} + +std::string SetBenchmarkLogicCommand::getCommandName() const throw() { + return "set-logic"; +} + +/* class SetInfoCommand */ + +SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) throw() : + d_flag(flag), + d_sexpr(sexpr) { +} + +std::string SetInfoCommand::getFlag() const throw() { + return d_flag; +} + +SExpr SetInfoCommand::getSExpr() const throw() { + return d_sexpr; +} + +void SetInfoCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->setInfo(d_flag, d_sexpr); + d_commandStatus = CommandSuccess::instance(); + } catch(UnrecognizedOptionException&) { + // As per SMT-LIB spec, silently accept unknown set-info keys + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* SetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new SetInfoCommand(d_flag, d_sexpr); +} + +Command* SetInfoCommand::clone() const { + return new SetInfoCommand(d_flag, d_sexpr); +} + +std::string SetInfoCommand::getCommandName() const throw() { + return "set-info"; +} + +/* class GetInfoCommand */ + +GetInfoCommand::GetInfoCommand(std::string flag) throw() : + d_flag(flag) { +} + +std::string GetInfoCommand::getFlag() const throw() { + return d_flag; +} + +void GetInfoCommand::invoke(SmtEngine* smtEngine) throw() { + try { + vector v; + v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag))); + v.push_back(smtEngine->getInfo(d_flag)); + stringstream ss; + if(d_flag == "all-options" || d_flag == "all-statistics") { + ss << PrettySExprs(true); + } + ss << SExpr(v); + d_result = ss.str(); + d_commandStatus = CommandSuccess::instance(); + } catch(UnrecognizedOptionException&) { + d_commandStatus = new CommandUnsupported(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +std::string GetInfoCommand::getResult() const throw() { + return d_result; +} + +void GetInfoCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else if(d_result != "") { + out << d_result << endl; + } +} + +Command* GetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetInfoCommand* c = new GetInfoCommand(d_flag); + c->d_result = d_result; + return c; +} + +Command* GetInfoCommand::clone() const { + GetInfoCommand* c = new GetInfoCommand(d_flag); + c->d_result = d_result; + return c; +} + +std::string GetInfoCommand::getCommandName() const throw() { + return "get-info"; +} + +/* class SetOptionCommand */ + +SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) throw() : + d_flag(flag), + d_sexpr(sexpr) { +} + +std::string SetOptionCommand::getFlag() const throw() { + return d_flag; +} + +SExpr SetOptionCommand::getSExpr() const throw() { + return d_sexpr; +} + +void SetOptionCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->setOption(d_flag, d_sexpr); + d_commandStatus = CommandSuccess::instance(); + } catch(UnrecognizedOptionException&) { + d_commandStatus = new CommandUnsupported(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* SetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new SetOptionCommand(d_flag, d_sexpr); +} + +Command* SetOptionCommand::clone() const { + return new SetOptionCommand(d_flag, d_sexpr); +} + +std::string SetOptionCommand::getCommandName() const throw() { + return "set-option"; +} + +/* class GetOptionCommand */ + +GetOptionCommand::GetOptionCommand(std::string flag) throw() : + d_flag(flag) { +} + +std::string GetOptionCommand::getFlag() const throw() { + return d_flag; +} + +void GetOptionCommand::invoke(SmtEngine* smtEngine) throw() { + try { + SExpr res = smtEngine->getOption(d_flag); + d_result = res.toString(); + d_commandStatus = CommandSuccess::instance(); + } catch(UnrecognizedOptionException&) { + d_commandStatus = new CommandUnsupported(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +std::string GetOptionCommand::getResult() const throw() { + return d_result; +} + +void GetOptionCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else if(d_result != "") { + out << d_result << endl; + } +} + +Command* GetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetOptionCommand* c = new GetOptionCommand(d_flag); + c->d_result = d_result; + return c; +} + +Command* GetOptionCommand::clone() const { + GetOptionCommand* c = new GetOptionCommand(d_flag); + c->d_result = d_result; + return c; +} + +std::string GetOptionCommand::getCommandName() const throw() { + return "get-option"; +} + +/* class DatatypeDeclarationCommand */ + +DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) throw() : + d_datatypes() { + d_datatypes.push_back(datatype); +} + +DatatypeDeclarationCommand::DatatypeDeclarationCommand(const std::vector& datatypes) throw() : + d_datatypes(datatypes) { +} + +const std::vector& +DatatypeDeclarationCommand::getDatatypes() const throw() { + return d_datatypes; +} + +void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() { + d_commandStatus = CommandSuccess::instance(); +} + +Command* DatatypeDeclarationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + throw ExportUnsupportedException + ("export of DatatypeDeclarationCommand unsupported"); +} + +Command* DatatypeDeclarationCommand::clone() const { + return new DatatypeDeclarationCommand(d_datatypes); +} + +std::string DatatypeDeclarationCommand::getCommandName() const throw() { + return "declare-datatypes"; +} + +/* class RewriteRuleCommand */ + +RewriteRuleCommand::RewriteRuleCommand(const std::vector& vars, + const std::vector& guards, + Expr head, Expr body, + const Triggers& triggers) throw() : + d_vars(vars), d_guards(guards), d_head(head), d_body(body), d_triggers(triggers) { +} + +RewriteRuleCommand::RewriteRuleCommand(const std::vector& vars, + Expr head, Expr body) throw() : + d_vars(vars), d_head(head), d_body(body) { +} + +const std::vector& RewriteRuleCommand::getVars() const throw() { + return d_vars; +} + +const std::vector& RewriteRuleCommand::getGuards() const throw() { + return d_guards; +} + +Expr RewriteRuleCommand::getHead() const throw() { + return d_head; +} + +Expr RewriteRuleCommand::getBody() const throw() { + return d_body; +} + +const RewriteRuleCommand::Triggers& RewriteRuleCommand::getTriggers() const throw() { + return d_triggers; +} + +void RewriteRuleCommand::invoke(SmtEngine* smtEngine) throw() { + 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(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 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; vars.reserve(d_vars.size()); + for(VExpr::iterator i = d_vars.begin(), end = d_vars.end(); + i == end; ++i){ + vars.push_back(i->exportTo(exprManager, variableMap)); + }; + /** Convert guards */ + VExpr guards; guards.reserve(d_guards.size()); + for(VExpr::iterator i = d_guards.begin(), end = d_guards.end(); + i == end; ++i){ + guards.push_back(i->exportTo(exprManager, variableMap)); + }; + /** Convert triggers */ + Triggers triggers; triggers.resize(d_triggers.size()); + for(size_t i = 0, end = d_triggers.size(); + i < end; ++i){ + triggers[i].reserve(d_triggers[i].size()); + for(VExpr::iterator j = d_triggers[i].begin(), jend = d_triggers[i].end(); + j == jend; ++i){ + triggers[i].push_back(j->exportTo(exprManager, variableMap)); + }; + }; + /** 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 throw() { + return "rewrite-rule"; +} + +/* class PropagateRuleCommand */ + +PropagateRuleCommand::PropagateRuleCommand(const std::vector& vars, + const std::vector& guards, + const std::vector& heads, + Expr body, + const Triggers& triggers, + bool deduction) throw() : + d_vars(vars), d_guards(guards), d_heads(heads), d_body(body), d_triggers(triggers), d_deduction(deduction) { +} + +PropagateRuleCommand::PropagateRuleCommand(const std::vector& vars, + const std::vector& heads, + Expr body, + bool deduction) throw() : + d_vars(vars), d_heads(heads), d_body(body), d_deduction(deduction) { +} + +const std::vector& PropagateRuleCommand::getVars() const throw() { + return d_vars; +} + +const std::vector& PropagateRuleCommand::getGuards() const throw() { + return d_guards; +} + +const std::vector& PropagateRuleCommand::getHeads() const throw() { + return d_heads; +} + +Expr PropagateRuleCommand::getBody() const throw() { + return d_body; +} + +const PropagateRuleCommand::Triggers& PropagateRuleCommand::getTriggers() const throw() { + return d_triggers; +} + +bool PropagateRuleCommand::isDeduction() const throw() { + return d_deduction; +} + +void PropagateRuleCommand::invoke(SmtEngine* smtEngine) throw() { + 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(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 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; vars.reserve(d_vars.size()); + for(VExpr::iterator i = d_vars.begin(), end = d_vars.end(); + i == end; ++i){ + vars.push_back(i->exportTo(exprManager, variableMap)); + }; + /** Convert guards */ + VExpr guards; guards.reserve(d_guards.size()); + for(VExpr::iterator i = d_guards.begin(), end = d_guards.end(); + i == end; ++i){ + guards.push_back(i->exportTo(exprManager, variableMap)); + }; + /** Convert heads */ + VExpr heads; heads.reserve(d_heads.size()); + for(VExpr::iterator i = d_heads.begin(), end = d_heads.end(); + i == end; ++i){ + heads.push_back(i->exportTo(exprManager, variableMap)); + }; + /** Convert triggers */ + Triggers triggers; triggers.resize(d_triggers.size()); + for(size_t i = 0, end = d_triggers.size(); + i < end; ++i){ + triggers[i].reserve(d_triggers[i].size()); + for(VExpr::iterator j = d_triggers[i].begin(), jend = d_triggers[i].end(); + j == jend; ++i){ + triggers[i].push_back(j->exportTo(exprManager, variableMap)); + }; + }; + /** 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 throw() { + return "propagate-rule"; +} + +/* output stream insertion operator for benchmark statuses */ +std::ostream& operator<<(std::ostream& out, + BenchmarkStatus status) throw() { + switch(status) { + + case SMT_SATISFIABLE: + return out << "sat"; + + case SMT_UNSATISFIABLE: + return out << "unsat"; + + case SMT_UNKNOWN: + return out << "unknown"; + + default: + return out << "BenchmarkStatus::[UNKNOWNSTATUS!]"; + } +} + +}/* CVC4 namespace */ diff --git a/src/smt/command.h b/src/smt/command.h new file mode 100644 index 000000000..248e69b0e --- /dev/null +++ b/src/smt/command.h @@ -0,0 +1,905 @@ +/********************* */ +/*! \file command.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): Kshitij Bansal, Christopher L. Conway, Dejan Jovanovic, Francois Bobot, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of the command pattern on SmtEngines. + ** + ** Implementation of the command pattern on SmtEngines. Command + ** objects are generated by the parser (typically) to implement the + ** commands in parsed input (see Parser::parseNextCommand()), or by + ** client code. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__COMMAND_H +#define __CVC4__COMMAND_H + +#include +#include +#include +#include +#include + +#include "expr/datatype.h" +#include "expr/expr.h" +#include "expr/type.h" +#include "expr/variable_type_map.h" +#include "proof/unsat_core.h" +#include "util/proof.h" +#include "util/result.h" +#include "util/sexpr.h" + +namespace CVC4 { + +class SmtEngine; +class Command; +class CommandStatus; +class Model; + +std::ostream& operator<<(std::ostream&, const Command&) throw() CVC4_PUBLIC; +std::ostream& operator<<(std::ostream&, const Command*) throw() CVC4_PUBLIC; +std::ostream& operator<<(std::ostream&, const CommandStatus&) throw() CVC4_PUBLIC; +std::ostream& operator<<(std::ostream&, const CommandStatus*) throw() CVC4_PUBLIC; + +/** The status an SMT benchmark can have */ +enum BenchmarkStatus { + /** Benchmark is satisfiable */ + SMT_SATISFIABLE, + /** Benchmark is unsatisfiable */ + SMT_UNSATISFIABLE, + /** The status of the benchmark is unknown */ + SMT_UNKNOWN +};/* enum BenchmarkStatus */ + +std::ostream& operator<<(std::ostream& out, + BenchmarkStatus status) throw() CVC4_PUBLIC; + +/** + * IOStream manipulator to print success messages or not. + * + * out << Command::printsuccess(false) << CommandSuccess(); + * + * prints nothing, but + * + * out << Command::printsuccess(true) << CommandSuccess(); + * + * prints a success message (in a manner appropriate for the current + * output language). + */ +class CVC4_PUBLIC CommandPrintSuccess { + /** + * The allocated index in ios_base for our depth setting. + */ + static const int s_iosIndex; + + /** + * The default setting, for ostreams that haven't yet had a + * setdepth() applied to them. + */ + static const int s_defaultPrintSuccess = false; + + /** + * When this manipulator is used, the setting is stored here. + */ + bool d_printSuccess; + +public: + /** + * Construct a CommandPrintSuccess with the given setting. + */ + CommandPrintSuccess(bool printSuccess) throw() : d_printSuccess(printSuccess) {} + + inline void applyPrintSuccess(std::ostream& out) throw() { + out.iword(s_iosIndex) = d_printSuccess; + } + + static inline bool getPrintSuccess(std::ostream& out) throw() { + return out.iword(s_iosIndex); + } + + static inline void setPrintSuccess(std::ostream& out, bool printSuccess) throw() { + out.iword(s_iosIndex) = printSuccess; + } + + /** + * Set the print-success state on the output stream for the current + * stack scope. This makes sure the old state is reset on the + * stream after normal OR exceptional exit from the scope, using the + * RAII C++ idiom. + */ + class Scope { + std::ostream& d_out; + bool d_oldPrintSuccess; + + public: + + inline Scope(std::ostream& out, bool printSuccess) throw() : + d_out(out), + d_oldPrintSuccess(CommandPrintSuccess::getPrintSuccess(out)) { + CommandPrintSuccess::setPrintSuccess(out, printSuccess); + } + + inline ~Scope() throw() { + CommandPrintSuccess::setPrintSuccess(d_out, d_oldPrintSuccess); + } + + };/* class CommandPrintSuccess::Scope */ + +};/* class CommandPrintSuccess */ + +/** + * Sets the default print-success setting when pretty-printing an Expr + * to an ostream. Use like this: + * + * // let out be an ostream, e an Expr + * out << Expr::setdepth(n) << e << endl; + * + * The depth stays permanently (until set again) with the stream. + */ +inline std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) throw() CVC4_PUBLIC; +inline std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) throw() { + cps.applyPrintSuccess(out); + return out; +} + +class CVC4_PUBLIC CommandStatus { +protected: + // shouldn't construct a CommandStatus (use a derived class) + CommandStatus() throw() {} +public: + virtual ~CommandStatus() throw() {} + void toStream(std::ostream& out, + OutputLanguage language = language::output::LANG_AUTO) const throw(); + virtual CommandStatus& clone() const = 0; +};/* class CommandStatus */ + +class CVC4_PUBLIC CommandSuccess : public CommandStatus { + static const CommandSuccess* s_instance; +public: + static const CommandSuccess* instance() throw() { return s_instance; } + CommandStatus& clone() const { return const_cast(*this); } +};/* class CommandSuccess */ + +class CVC4_PUBLIC CommandInterrupted : public CommandStatus { + static const CommandInterrupted* s_instance; +public: + static const CommandInterrupted* instance() throw() { return s_instance; } + CommandStatus& clone() const { return const_cast(*this); } +};/* class CommandInterrupted */ + +class CVC4_PUBLIC CommandUnsupported : public CommandStatus { +public: + CommandStatus& clone() const { return *new CommandUnsupported(*this); } +};/* class CommandSuccess */ + +class CVC4_PUBLIC CommandFailure : public CommandStatus { + std::string d_message; +public: + CommandFailure(std::string message) throw() : d_message(message) {} + CommandFailure& clone() const { return *new CommandFailure(*this); } + ~CommandFailure() throw() {} + std::string getMessage() const throw() { return d_message; } +};/* class CommandFailure */ + +class CVC4_PUBLIC Command { +protected: + /** + * This field contains a command status if the command has been + * invoked, or NULL if it has not. This field is either a + * dynamically-allocated pointer, or it's a pointer to the singleton + * CommandSuccess instance. Doing so is somewhat asymmetric, but + * it avoids the need to dynamically allocate memory in the common + * case of a successful command. + */ + const CommandStatus* d_commandStatus; + + /** + * True if this command is "muted"---i.e., don't print "success" on + * successful execution. + */ + bool d_muted; + +public: + typedef CommandPrintSuccess printsuccess; + + Command() throw(); + Command(const Command& cmd); + + virtual ~Command() throw(); + + virtual void invoke(SmtEngine* smtEngine) throw() = 0; + virtual void invoke(SmtEngine* smtEngine, std::ostream& out) throw(); + + virtual void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1, + OutputLanguage language = language::output::LANG_AUTO) const throw(); + + std::string toString() const throw(); + + virtual std::string getCommandName() const throw() = 0; + + /** + * If false, instruct this Command not to print a success message. + */ + void setMuted(bool muted) throw() { d_muted = muted; } + + /** + * Determine whether this Command will print a success message. + */ + bool isMuted() throw() { return d_muted; } + + /** + * Either the command hasn't run yet, or it completed successfully + * (CommandSuccess, not CommandUnsupported or CommandFailure). + */ + bool ok() const throw(); + + /** + * The command completed in a failure state (CommandFailure, not + * CommandSuccess or CommandUnsupported). + */ + bool fail() const throw(); + + /** + * The command was ran but was interrupted due to resource limiting. + */ + bool interrupted() const throw(); + + /** Get the command status (it's NULL if we haven't run yet). */ + const CommandStatus* getCommandStatus() const throw() { return d_commandStatus; } + + virtual void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + + /** + * Maps this Command into one for a different ExprManager, using + * variableMap for the translation and extending it with any new + * mappings. + */ + virtual Command* exportTo(ExprManager* exprManager, + ExprManagerMapCollection& variableMap) = 0; + + /** + * Clone this Command (make a shallow copy). + */ + virtual Command* clone() const = 0; + +protected: + class ExportTransformer { + ExprManager* d_exprManager; + ExprManagerMapCollection& d_variableMap; + public: + ExportTransformer(ExprManager* exprManager, ExprManagerMapCollection& variableMap) : + d_exprManager(exprManager), + d_variableMap(variableMap) { + } + Expr operator()(Expr e) { + return e.exportTo(d_exprManager, d_variableMap); + } + Type operator()(Type t) { + return t.exportTo(d_exprManager, d_variableMap); + } + };/* class Command::ExportTransformer */ +};/* class Command */ + +/** + * EmptyCommands are the residue of a command after the parser handles + * them (and there's nothing left to do). + */ +class CVC4_PUBLIC EmptyCommand : public Command { +protected: + std::string d_name; +public: + EmptyCommand(std::string name = "") throw(); + ~EmptyCommand() throw() {} + std::string getName() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class EmptyCommand */ + +class CVC4_PUBLIC EchoCommand : public Command { +protected: + std::string d_output; +public: + EchoCommand(std::string output = "") throw(); + ~EchoCommand() throw() {} + std::string getOutput() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + void invoke(SmtEngine* smtEngine, std::ostream& out) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class EchoCommand */ + +class CVC4_PUBLIC AssertCommand : public Command { +protected: + Expr d_expr; + bool d_inUnsatCore; +public: + AssertCommand(const Expr& e, bool inUnsatCore = true) throw(); + ~AssertCommand() throw() {} + Expr getExpr() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class AssertCommand */ + +class CVC4_PUBLIC PushCommand : public Command { +public: + ~PushCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class PushCommand */ + +class CVC4_PUBLIC PopCommand : public Command { +public: + ~PopCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class PopCommand */ + +class CVC4_PUBLIC DeclarationDefinitionCommand : public Command { +protected: + std::string d_symbol; +public: + DeclarationDefinitionCommand(const std::string& id) throw(); + ~DeclarationDefinitionCommand() throw() {} + virtual void invoke(SmtEngine* smtEngine) throw() = 0; + std::string getSymbol() const throw(); +};/* class DeclarationDefinitionCommand */ + +class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand { +protected: + Expr d_func; + Type d_type; + bool d_printInModel; + bool d_printInModelSetByUser; +public: + DeclareFunctionCommand(const std::string& id, Expr func, Type type) throw(); + ~DeclareFunctionCommand() throw() {} + Expr getFunction() const throw(); + Type getType() const throw(); + bool getPrintInModel() const throw(); + bool getPrintInModelSetByUser() const throw(); + void setPrintInModel( bool p ); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class DeclareFunctionCommand */ + +class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand { +protected: + size_t d_arity; + Type d_type; +public: + DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw(); + ~DeclareTypeCommand() throw() {} + size_t getArity() const throw(); + Type getType() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class DeclareTypeCommand */ + +class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand { +protected: + std::vector d_params; + Type d_type; +public: + DefineTypeCommand(const std::string& id, Type t) throw(); + DefineTypeCommand(const std::string& id, const std::vector& params, Type t) throw(); + ~DefineTypeCommand() throw() {} + const std::vector& getParameters() const throw(); + Type getType() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class DefineTypeCommand */ + +class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand { +protected: + Expr d_func; + std::vector d_formals; + Expr d_formula; +public: + DefineFunctionCommand(const std::string& id, Expr func, Expr formula) throw(); + DefineFunctionCommand(const std::string& id, Expr func, + const std::vector& formals, Expr formula) throw(); + ~DefineFunctionCommand() throw() {} + Expr getFunction() const throw(); + const std::vector& getFormals() const throw(); + Expr getFormula() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class DefineFunctionCommand */ + +/** + * This differs from DefineFunctionCommand only in that it instructs + * the SmtEngine to "remember" this function for later retrieval with + * getAssignment(). Used for :named attributes in SMT-LIBv2. + */ +class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand { +public: + DefineNamedFunctionCommand(const std::string& id, Expr func, + const std::vector& formals, Expr formula) throw(); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; +};/* class DefineNamedFunctionCommand */ + +/** + * The command when an attribute is set by a user. In SMT-LIBv2 this is done + * via the syntax (! expr :attr) + */ +class CVC4_PUBLIC SetUserAttributeCommand : public Command { +protected: + std::string d_attr; + Expr d_expr; + std::vector d_expr_values; + std::string d_str_value; +public: + SetUserAttributeCommand( const std::string& attr, Expr expr ) throw(); + SetUserAttributeCommand( const std::string& attr, Expr expr, std::vector& values ) throw(); + SetUserAttributeCommand( const std::string& attr, Expr expr, const std::string& value ) throw(); + ~SetUserAttributeCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class SetUserAttributeCommand */ + +class CVC4_PUBLIC CheckSatCommand : public Command { +protected: + Expr d_expr; + Result d_result; + bool d_inUnsatCore; +public: + CheckSatCommand() throw(); + CheckSatCommand(const Expr& expr, bool inUnsatCore = true) throw(); + ~CheckSatCommand() throw() {} + Expr getExpr() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Result getResult() const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class CheckSatCommand */ + +class CVC4_PUBLIC QueryCommand : public Command { +protected: + Expr d_expr; + Result d_result; + bool d_inUnsatCore; +public: + QueryCommand(const Expr& e, bool inUnsatCore = true) throw(); + ~QueryCommand() throw() {} + Expr getExpr() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Result getResult() const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class QueryCommand */ + +// this is TRANSFORM in the CVC presentation language +class CVC4_PUBLIC SimplifyCommand : public Command { +protected: + Expr d_term; + Expr d_result; +public: + SimplifyCommand(Expr term) throw(); + ~SimplifyCommand() throw() {} + Expr getTerm() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Expr getResult() const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class SimplifyCommand */ + +class CVC4_PUBLIC ExpandDefinitionsCommand : public Command { +protected: + Expr d_term; + Expr d_result; +public: + ExpandDefinitionsCommand(Expr term) throw(); + ~ExpandDefinitionsCommand() throw() {} + Expr getTerm() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Expr getResult() const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class ExpandDefinitionsCommand */ + +class CVC4_PUBLIC GetValueCommand : public Command { +protected: + std::vector d_terms; + Expr d_result; +public: + GetValueCommand(Expr term) throw(); + GetValueCommand(const std::vector& terms) throw(); + ~GetValueCommand() throw() {} + const std::vector& getTerms() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Expr getResult() const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class GetValueCommand */ + +class CVC4_PUBLIC GetAssignmentCommand : public Command { +protected: + SExpr d_result; +public: + GetAssignmentCommand() throw(); + ~GetAssignmentCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + SExpr getResult() const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class GetAssignmentCommand */ + +class CVC4_PUBLIC GetModelCommand : public Command { +protected: + Model* d_result; + SmtEngine* d_smtEngine; +public: + GetModelCommand() throw(); + ~GetModelCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + // Model is private to the library -- for now + //Model* getResult() const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class GetModelCommand */ + +class CVC4_PUBLIC GetProofCommand : public Command { +protected: + Proof* d_result; + SmtEngine* d_smtEngine; +public: + GetProofCommand() throw(); + ~GetProofCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + Proof* getResult() const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class GetProofCommand */ + +class CVC4_PUBLIC GetInstantiationsCommand : public Command { +protected: + //Instantiations* d_result; + SmtEngine* d_smtEngine; +public: + GetInstantiationsCommand() throw(); + ~GetInstantiationsCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + //Instantiations* getResult() const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class GetInstantiationsCommand */ + +class CVC4_PUBLIC GetSynthSolutionCommand : public Command { +protected: + SmtEngine* d_smtEngine; +public: + GetSynthSolutionCommand() throw(); + ~GetSynthSolutionCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class GetSynthSolutionCommand */ + +class CVC4_PUBLIC GetUnsatCoreCommand : public Command { +protected: + UnsatCore d_result; + std::map d_names; +public: + GetUnsatCoreCommand() throw(); + GetUnsatCoreCommand(const std::map& names) throw(); + ~GetUnsatCoreCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + const UnsatCore& getUnsatCore() const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class GetUnsatCoreCommand */ + +class CVC4_PUBLIC GetAssertionsCommand : public Command { +protected: + std::string d_result; +public: + GetAssertionsCommand() throw(); + ~GetAssertionsCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + std::string getResult() const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class GetAssertionsCommand */ + +class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command { +protected: + BenchmarkStatus d_status; +public: + SetBenchmarkStatusCommand(BenchmarkStatus status) throw(); + ~SetBenchmarkStatusCommand() throw() {} + BenchmarkStatus getStatus() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class SetBenchmarkStatusCommand */ + +class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command { +protected: + std::string d_logic; +public: + SetBenchmarkLogicCommand(std::string logic) throw(); + ~SetBenchmarkLogicCommand() throw() {} + std::string getLogic() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class SetBenchmarkLogicCommand */ + +class CVC4_PUBLIC SetInfoCommand : public Command { +protected: + std::string d_flag; + SExpr d_sexpr; +public: + SetInfoCommand(std::string flag, const SExpr& sexpr) throw(); + ~SetInfoCommand() throw() {} + std::string getFlag() const throw(); + SExpr getSExpr() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class SetInfoCommand */ + +class CVC4_PUBLIC GetInfoCommand : public Command { +protected: + std::string d_flag; + std::string d_result; +public: + GetInfoCommand(std::string flag) throw(); + ~GetInfoCommand() throw() {} + std::string getFlag() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + std::string getResult() const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class GetInfoCommand */ + +class CVC4_PUBLIC SetOptionCommand : public Command { +protected: + std::string d_flag; + SExpr d_sexpr; +public: + SetOptionCommand(std::string flag, const SExpr& sexpr) throw(); + ~SetOptionCommand() throw() {} + std::string getFlag() const throw(); + SExpr getSExpr() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class SetOptionCommand */ + +class CVC4_PUBLIC GetOptionCommand : public Command { +protected: + std::string d_flag; + std::string d_result; +public: + GetOptionCommand(std::string flag) throw(); + ~GetOptionCommand() throw() {} + std::string getFlag() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + std::string getResult() const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class GetOptionCommand */ + +class CVC4_PUBLIC DatatypeDeclarationCommand : public Command { +private: + std::vector d_datatypes; +public: + DatatypeDeclarationCommand(const DatatypeType& datatype) throw(); + ~DatatypeDeclarationCommand() throw() {} + DatatypeDeclarationCommand(const std::vector& datatypes) throw(); + const std::vector& getDatatypes() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class DatatypeDeclarationCommand */ + +class CVC4_PUBLIC RewriteRuleCommand : public Command { +public: + typedef std::vector< std::vector< Expr > > Triggers; +protected: + typedef std::vector< Expr > VExpr; + VExpr d_vars; + VExpr d_guards; + Expr d_head; + Expr d_body; + Triggers d_triggers; +public: + RewriteRuleCommand(const std::vector& vars, + const std::vector& guards, + Expr head, + Expr body, + const Triggers& d_triggers) throw(); + RewriteRuleCommand(const std::vector& vars, + Expr head, + Expr body) throw(); + ~RewriteRuleCommand() throw() {} + const std::vector& getVars() const throw(); + const std::vector& getGuards() const throw(); + Expr getHead() const throw(); + Expr getBody() const throw(); + const Triggers& getTriggers() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class RewriteRuleCommand */ + +class CVC4_PUBLIC PropagateRuleCommand : public Command { +public: + typedef std::vector< std::vector< Expr > > Triggers; +protected: + typedef std::vector< Expr > VExpr; + VExpr d_vars; + VExpr d_guards; + VExpr d_heads; + Expr d_body; + Triggers d_triggers; + bool d_deduction; +public: + PropagateRuleCommand(const std::vector& vars, + const std::vector& guards, + const std::vector& heads, + Expr body, + const Triggers& d_triggers, + /* true if we want a deduction rule */ + bool d_deduction = false) throw(); + PropagateRuleCommand(const std::vector& vars, + const std::vector& heads, + Expr body, + bool d_deduction = false) throw(); + ~PropagateRuleCommand() throw() {} + const std::vector& getVars() const throw(); + const std::vector& getGuards() const throw(); + const std::vector& getHeads() const throw(); + Expr getBody() const throw(); + const Triggers& getTriggers() const throw(); + bool isDeduction() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class PropagateRuleCommand */ + +class CVC4_PUBLIC ResetCommand : public Command { +public: + ResetCommand() throw() {} + ~ResetCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class ResetCommand */ + +class CVC4_PUBLIC ResetAssertionsCommand : public Command { +public: + ResetAssertionsCommand() throw() {} + ~ResetAssertionsCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class ResetAssertionsCommand */ + +class CVC4_PUBLIC QuitCommand : public Command { +public: + QuitCommand() throw() {} + ~QuitCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class QuitCommand */ + +class CVC4_PUBLIC CommentCommand : public Command { + std::string d_comment; +public: + CommentCommand(std::string comment) throw(); + ~CommentCommand() throw() {} + std::string getComment() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class CommentCommand */ + +class CVC4_PUBLIC CommandSequence : public Command { +private: + /** All the commands to be executed (in sequence) */ + std::vector d_commandSequence; + /** Next command to be executed */ + unsigned int d_index; +public: + CommandSequence() throw(); + ~CommandSequence() throw(); + + void addCommand(Command* cmd) throw(); + void clear() throw(); + + void invoke(SmtEngine* smtEngine) throw(); + void invoke(SmtEngine* smtEngine, std::ostream& out) throw(); + + typedef std::vector::iterator iterator; + typedef std::vector::const_iterator const_iterator; + + const_iterator begin() const throw(); + const_iterator end() const throw(); + + iterator begin() throw(); + iterator end() throw(); + + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class CommandSequence */ + +class CVC4_PUBLIC DeclarationSequence : public CommandSequence { +public: + ~DeclarationSequence() throw() {} +};/* class DeclarationSequence */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__COMMAND_H */ diff --git a/src/smt/command.i b/src/smt/command.i new file mode 100644 index 000000000..0c050201d --- /dev/null +++ b/src/smt/command.i @@ -0,0 +1,77 @@ +%{ +#include "smt/command.h" + +#ifdef SWIGJAVA + +#include "bindings/java_iterator_adapter.h" +#include "bindings/java_stream_adapters.h" + +#endif /* SWIGJAVA */ +%} + +%ignore CVC4::operator<<(std::ostream&, const Command&) throw(); +%ignore CVC4::operator<<(std::ostream&, const Command*) throw(); +%ignore CVC4::operator<<(std::ostream&, const CommandStatus&) throw(); +%ignore CVC4::operator<<(std::ostream&, const CommandStatus*) throw(); +%ignore CVC4::operator<<(std::ostream&, BenchmarkStatus status) throw(); +%ignore CVC4::operator<<(std::ostream&, CommandPrintSuccess) throw(); + +%ignore CVC4::GetProofCommand; +%ignore CVC4::CommandPrintSuccess::Scope; + +#ifdef SWIGJAVA + +// Instead of CommandSequence::begin() and end(), create an +// iterator() method on the Java side that returns a Java-style +// Iterator. +%ignore CVC4::CommandSequence::begin(); +%ignore CVC4::CommandSequence::end(); +%ignore CVC4::CommandSequence::begin() const; +%ignore CVC4::CommandSequence::end() const; +%extend CVC4::CommandSequence { + CVC4::JavaIteratorAdapter iterator() { + return CVC4::JavaIteratorAdapter(*$self); + } +} + +// CommandSequence is "iterable" on the Java side +%typemap(javainterfaces) CVC4::CommandSequence "java.lang.Iterable"; + +// the JavaIteratorAdapter should not be public, and implements Iterator +%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter "class"; +%typemap(javainterfaces) CVC4::JavaIteratorAdapter "java.util.Iterator"; +// add some functions to the Java side (do it here because there's no way to do these in C++) +%typemap(javacode) CVC4::JavaIteratorAdapter " + public void remove() { + throw new java.lang.UnsupportedOperationException(); + } + + public edu.nyu.acsys.CVC4.Command next() { + if(hasNext()) { + return getNext(); + } else { + throw new java.util.NoSuchElementException(); + } + } +" +// getNext() just allows C++ iterator access from Java-side next(), make it private +%javamethodmodifiers CVC4::JavaIteratorAdapter::getNext() "private"; + +// map the types appropriately +%typemap(jni) CVC4::CommandSequence::const_iterator::value_type "jobject"; +%typemap(jtype) CVC4::CommandSequence::const_iterator::value_type "edu.nyu.acsys.CVC4.Command"; +%typemap(jstype) CVC4::CommandSequence::const_iterator::value_type "edu.nyu.acsys.CVC4.Command"; +%typemap(javaout) CVC4::CommandSequence::const_iterator::value_type { return $jnicall; } + +#endif /* SWIGJAVA */ + +%include "smt/command.h" + +#ifdef SWIGJAVA + +%include "bindings/java_iterator_adapter.h" +%include "bindings/java_stream_adapters.h" + +%template(JavaIteratorAdapter_CommandSequence) CVC4::JavaIteratorAdapter; + +#endif /* SWIGJAVA */ diff --git a/src/smt/command_list.cpp b/src/smt/command_list.cpp index 3e912d338..2319d9539 100644 --- a/src/smt/command_list.cpp +++ b/src/smt/command_list.cpp @@ -15,9 +15,9 @@ **/ // we include both of these to make sure they agree on the typedef +#include "smt/command.h" #include "smt/command_list.h" #include "smt/smt_engine.h" -#include "smt_util/command.h" namespace CVC4 { namespace smt { diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp new file mode 100644 index 000000000..3b9ec3273 --- /dev/null +++ b/src/smt/dump.cpp @@ -0,0 +1,221 @@ +/********************* */ +/*! \file dump.cpp + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Dump utility classes and functions + ** + ** Dump utility classes and functions. + **/ +#include "smt/dump.h" + +#include "base/output.h" + +namespace CVC4 { + +DumpC DumpChannel CVC4_PUBLIC; + +std::ostream& DumpC::setStream(std::ostream* os) { + ::CVC4::DumpOutChannel.setStream(os); + return *os; +} +std::ostream& DumpC::getStream() { return ::CVC4::DumpOutChannel.getStream(); } +std::ostream* DumpC::getStreamPointer() { return ::CVC4::DumpOutChannel.getStreamPointer(); } + + +void DumpC::setDumpFromString(const std::string& optarg) { +#ifdef CVC4_DUMPING + char* optargPtr = strdup(optarg.c_str()); + char* tokstr = optargPtr; + char* toksave; + while((optargPtr = strtok_r(tokstr, ",", &toksave)) != NULL) { + tokstr = NULL; + if(!strcmp(optargPtr, "benchmark")) { + } else if(!strcmp(optargPtr, "declarations")) { + } else if(!strcmp(optargPtr, "assertions")) { + Dump.on("assertions:post-everything"); + } else if(!strncmp(optargPtr, "assertions:", 11)) { + const char* p = optargPtr + 11; + if(!strncmp(p, "pre-", 4)) { + p += 4; + } else if(!strncmp(p, "post-", 5)) { + p += 5; + } else { + throw OptionException(std::string("don't know how to dump `") + + optargPtr + "'. Please consult --dump help."); + } + if(!strcmp(p, "everything")) { + } else if(!strcmp(p, "definition-expansion")) { + } else if(!strcmp(p, "boolean-terms")) { + } else if(!strcmp(p, "constrain-subtypes")) { + } else if(!strcmp(p, "substitution")) { + } else if(!strcmp(p, "strings-pp")) { + } else if(!strcmp(p, "skolem-quant")) { + } else if(!strcmp(p, "simplify")) { + } else if(!strcmp(p, "static-learning")) { + } else if(!strcmp(p, "ite-removal")) { + } else if(!strcmp(p, "repeat-simplify")) { + } else if(!strcmp(p, "rewrite-apply-to-const")) { + } else if(!strcmp(p, "theory-preprocessing")) { + } else if(!strcmp(p, "nonclausal")) { + } else if(!strcmp(p, "theorypp")) { + } else if(!strcmp(p, "itesimp")) { + } else if(!strcmp(p, "unconstrained")) { + } else if(!strcmp(p, "repeatsimp")) { + } else { + throw OptionException(std::string("don't know how to dump `") + + optargPtr + "'. Please consult --dump help."); + } + Dump.on("assertions"); + } else if(!strcmp(optargPtr, "skolems")) { + } else if(!strcmp(optargPtr, "clauses")) { + } else if(!strcmp(optargPtr, "t-conflicts") || + !strcmp(optargPtr, "t-lemmas") || + !strcmp(optargPtr, "t-explanations") || + !strcmp(optargPtr, "bv-rewrites") || + !strcmp(optargPtr, "theory::fullcheck")) { + // These are "non-state-dumping" modes. If state (SAT decisions, + // propagations, etc.) is dumped, it will interfere with the validity + // of these generated queries. + if(Dump.isOn("state")) { + throw OptionException(std::string("dump option `") + optargPtr + + "' conflicts with a previous, " + "state-dumping dump option. You cannot " + "mix stateful and non-stateful dumping modes; " + "see --dump help."); + } else { + Dump.on("no-permit-state"); + } + } else if(!strcmp(optargPtr, "state") || + !strcmp(optargPtr, "missed-t-conflicts") || + !strcmp(optargPtr, "t-propagations") || + !strcmp(optargPtr, "missed-t-propagations")) { + // These are "state-dumping" modes. If state (SAT decisions, + // propagations, etc.) is not dumped, it will interfere with the + // validity of these generated queries. + if(Dump.isOn("no-permit-state")) { + throw OptionException(std::string("dump option `") + optargPtr + + "' conflicts with a previous, " + "non-state-dumping dump option. You cannot " + "mix stateful and non-stateful dumping modes; " + "see --dump help."); + } else { + Dump.on("state"); + } + } else if(!strcmp(optargPtr, "help")) { + puts(s_dumpHelp.c_str()); + exit(1); + } else if(!strcmp(optargPtr, "bv-abstraction")) { + Dump.on("bv-abstraction"); + } else if(!strcmp(optargPtr, "bv-algebraic")) { + Dump.on("bv-algebraic"); + } else { + throw OptionException(std::string("unknown option for --dump: `") + + optargPtr + "'. Try --dump help."); + } + + Dump.on(optargPtr); + Dump.on("benchmark"); + if(strcmp(optargPtr, "benchmark")) { + Dump.on("declarations"); + if(strcmp(optargPtr, "declarations")) { + Dump.on("skolems"); + } + } + } + free(optargPtr); +#else /* CVC4_DUMPING */ + throw OptionException("The dumping feature was disabled in this build of CVC4."); +#endif /* CVC4_DUMPING */ +} + + +const std::string DumpC::s_dumpHelp = "\ +Dump modes currently supported by the --dump option:\n\ +\n\ +benchmark\n\ ++ Dump the benchmark structure (set-logic, push/pop, queries, etc.), but\n\ + does not include any declarations or assertions. Implied by all following\n\ + modes.\n\ +\n\ +declarations\n\ ++ Dump user declarations. Implied by all following modes.\n\ +\n\ +skolems\n\ ++ Dump internally-created skolem variable declarations. These can\n\ + arise from preprocessing simplifications, existential elimination,\n\ + and a number of other things. Implied by all following modes.\n\ +\n\ +assertions\n\ ++ Output the assertions after preprocessing and before clausification.\n\ + Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\ + where PASS is one of the preprocessing passes: definition-expansion\n\ + boolean-terms constrain-subtypes substitution strings-pp skolem-quant\n\ + simplify static-learning ite-removal repeat-simplify\n\ + rewrite-apply-to-const theory-preprocessing.\n\ + PASS can also be the special value \"everything\", in which case the\n\ + assertions are printed before any preprocessing (with\n\ + \"assertions:pre-everything\") or after all preprocessing completes\n\ + (with \"assertions:post-everything\").\n\ +\n\ +clauses\n\ ++ Do all the preprocessing outlined above, and dump the CNF-converted\n\ + output\n\ +\n\ +state\n\ ++ Dump all contextual assertions (e.g., SAT decisions, propagations..).\n\ + Implied by all \"stateful\" modes below and conflicts with all\n\ + non-stateful modes below.\n\ +\n\ +t-conflicts [non-stateful]\n\ ++ Output correctness queries for all theory conflicts\n\ +\n\ +missed-t-conflicts [stateful]\n\ ++ Output completeness queries for theory conflicts\n\ +\n\ +t-propagations [stateful]\n\ ++ Output correctness queries for all theory propagations\n\ +\n\ +missed-t-propagations [stateful]\n\ ++ Output completeness queries for theory propagations (LARGE and EXPENSIVE)\n\ +\n\ +t-lemmas [non-stateful]\n\ ++ Output correctness queries for all theory lemmas\n\ +\n\ +t-explanations [non-stateful]\n\ ++ Output correctness queries for all theory explanations\n\ +\n\ +bv-rewrites [non-stateful]\n\ ++ Output correctness queries for all bitvector rewrites\n\ +\n\ +bv-abstraction [non-stateful]\n\ ++ Output correctness queries for all bv abstraction \n\ +\n\ +bv-algebraic [non-stateful]\n\ ++ Output correctness queries for bv algebraic solver. \n\ +\n\ +theory::fullcheck [non-stateful]\n \ ++ Output completeness queries for all full-check effort-level theory checks\n\ +\n\ +Dump modes can be combined with multiple uses of --dump. Generally you want\n\ +one from the assertions category (either assertions or clauses), and\n\ +perhaps one or more stateful or non-stateful modes for checking correctness\n\ +and completeness of decision procedure implementations. Stateful modes dump\n\ +the contextual assertions made by the core solver (all decisions and\n\ +propagations as assertions; that affects the validity of the resulting\n\ +correctness and completeness queries, so of course stateful and non-stateful\n\ +modes cannot be mixed in the same run.\n\ +\n\ +The --output-language option controls the language used for dumping, and\n\ +this allows you to connect CVC4 to another solver implementation via a UNIX\n\ +pipe to perform on-line checking. The --dump-to option can be used to dump\n\ +to a file.\n\ +"; + +}/* CVC4 namespace */ diff --git a/src/smt/dump.h b/src/smt/dump.h new file mode 100644 index 000000000..a6fa899da --- /dev/null +++ b/src/smt/dump.h @@ -0,0 +1,123 @@ +/********************* */ +/*! \file dump.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Dump utility classes and functions + ** + ** Dump utility classes and functions. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__DUMP_H +#define __CVC4__DUMP_H + +#include "base/output.h" +#include "smt/command.h" + +namespace CVC4 { + +class CVC4_PUBLIC CVC4dumpstream { + +#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) + std::ostream* d_os; +#endif /* CVC4_DUMPING && !CVC4_MUZZLE */ + +#ifdef CVC4_PORTFOLIO + CommandSequence* d_commands; +#endif /* CVC4_PORTFOLIO */ + +public: + CVC4dumpstream() throw() +#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && defined(CVC4_PORTFOLIO) + : d_os(NULL), d_commands(NULL) +#elif defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) + : d_os(NULL) +#elif defined(CVC4_PORTFOLIO) + : d_commands(NULL) +#endif /* CVC4_PORTFOLIO */ + { } + + CVC4dumpstream(std::ostream& os, CommandSequence& commands) throw() +#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && defined(CVC4_PORTFOLIO) + : d_os(&os), d_commands(&commands) +#elif defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) + : d_os(&os) +#elif defined(CVC4_PORTFOLIO) + : d_commands(&commands) +#endif /* CVC4_PORTFOLIO */ + { } + + CVC4dumpstream& operator<<(const Command& c) { +#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) + if(d_os != NULL) { + (*d_os) << c << std::endl; + } +#endif +#if defined(CVC4_PORTFOLIO) + if(d_commands != NULL) { + d_commands->addCommand(c.clone()); + } +#endif + return *this; + } +};/* class CVC4dumpstream */ + +/** The dump class */ +class CVC4_PUBLIC DumpC { + std::set d_tags; + CommandSequence d_commands; + + static const std::string s_dumpHelp; + +public: + CVC4dumpstream operator()(const char* tag) { + if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) { + return CVC4dumpstream(getStream(), d_commands); + } else { + return CVC4dumpstream(); + } + } + + CVC4dumpstream operator()(std::string tag) { + if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) { + return CVC4dumpstream(getStream(), d_commands); + } else { + return CVC4dumpstream(); + } + } + + void clear() { d_commands.clear(); } + const CommandSequence& getCommands() const { return d_commands; } + + bool on (const char* tag) { d_tags.insert(std::string(tag)); return true; } + bool on (std::string tag) { d_tags.insert(tag); return true; } + bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; } + bool off(std::string tag) { d_tags.erase (tag); return false; } + bool off() { d_tags.clear(); return false; } + + bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); } + bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); } + + std::ostream& setStream(std::ostream* os); + std::ostream& getStream(); + std::ostream* getStreamPointer(); + + void setDumpFromString(const std::string& optarg); +};/* class DumpC */ + +/** The dump singleton */ +extern DumpC DumpChannel CVC4_PUBLIC; + +#define Dump ::CVC4::DumpChannel + +}/* CVC4 namespace */ + +#endif /* __CVC4__DUMP_H */ diff --git a/src/smt/ite_removal.cpp b/src/smt/ite_removal.cpp new file mode 100644 index 000000000..c0c6ed02b --- /dev/null +++ b/src/smt/ite_removal.cpp @@ -0,0 +1,190 @@ +/********************* */ +/*! \file ite_removal.cpp + ** \verbatim + ** Original author: Dejan Jovanovic + ** Major contributors: Tim King, Morgan Deters + ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds, Clark Barrett + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Removal of term ITEs + ** + ** Removal of term ITEs. + **/ +#include "smt/ite_removal.h" + +#include + +#include "proof/proof_manager.h" +#include "theory/ite_utilities.h" + +using namespace std; + +namespace CVC4 { + +RemoveITE::RemoveITE(context::UserContext* u) + : d_iteCache(u) +{ + d_containsVisitor = new theory::ContainsTermITEVisitor(); +} + +RemoveITE::~RemoveITE(){ + delete d_containsVisitor; +} + +void RemoveITE::garbageCollect(){ + d_containsVisitor->garbageCollect(); +} + +theory::ContainsTermITEVisitor* RemoveITE::getContainsVisitor() { + return d_containsVisitor; +} + +size_t RemoveITE::collectedCacheSizes() const{ + return d_containsVisitor->cache_size() + d_iteCache.size(); +} + +void RemoveITE::run(std::vector& output, IteSkolemMap& iteSkolemMap, bool reportDeps) +{ + size_t n = output.size(); + for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) { + // Do this in two steps to avoid Node problems(?) + // Appears related to bug 512, splitting this into two lines + // fixes the bug on clang on Mac OS + Node itesRemoved = run(output[i], output, iteSkolemMap, false); + // In some calling contexts, not necessary to report dependence information. + if(reportDeps && options::unsatCores()) { + // new assertions have a dependence on the node + PROOF( ProofManager::currentPM()->addDependence(itesRemoved, output[i]); ) + while(n < output.size()) { + PROOF( ProofManager::currentPM()->addDependence(output[n], output[i]); ) + ++n; + } + } + output[i] = itesRemoved; + } +} + +bool RemoveITE::containsTermITE(TNode e) const { + return d_containsVisitor->containsTermITE(e); +} + +Node RemoveITE::run(TNode node, std::vector& output, + IteSkolemMap& iteSkolemMap, bool inQuant) { + // Current node + Debug("ite") << "removeITEs(" << node << ")" << endl; + + if(node.isVar() || node.isConst() || + (options::biasedITERemoval() && !containsTermITE(node))){ + return Node(node); + } + + // The result may be cached already + std::pair cacheKey(node, inQuant); + NodeManager *nodeManager = NodeManager::currentNM(); + ITECache::const_iterator i = d_iteCache.find(cacheKey); + if(i != d_iteCache.end()) { + Node cached = (*i).second; + Debug("ite") << "removeITEs: in-cache: " << cached << endl; + return cached.isNull() ? Node(node) : cached; + } + + // Remember that we're inside a quantifier + if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) { + inQuant = true; + } + + // If an ITE replace it + if(node.getKind() == kind::ITE) { + TypeNode nodeType = node.getType(); + if(!nodeType.isBoolean() && (!inQuant || !node.hasBoundVar())) { + Node skolem; + // Make the skolem to represent the ITE + skolem = nodeManager->mkSkolem("termITE", nodeType, "a variable introduced due to term-level ITE removal"); + + // The new assertion + Node newAssertion = + nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]), + skolem.eqNode(node[2])); + Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl; + + // Attach the skolem + d_iteCache.insert(cacheKey, skolem); + + // Remove ITEs from the new assertion, rewrite it and push it to the output + newAssertion = run(newAssertion, output, iteSkolemMap, inQuant); + + iteSkolemMap[skolem] = output.size(); + output.push_back(newAssertion); + + // The representation is now the skolem + return skolem; + } + } + + // If not an ITE, go deep + vector newChildren; + bool somethingChanged = false; + if(node.getMetaKind() == kind::metakind::PARAMETERIZED) { + newChildren.push_back(node.getOperator()); + } + // Remove the ITEs from the children + for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) { + Node newChild = run(*it, output, iteSkolemMap, inQuant); + somethingChanged |= (newChild != *it); + newChildren.push_back(newChild); + } + + // If changes, we rewrite + if(somethingChanged) { + Node cached = nodeManager->mkNode(node.getKind(), newChildren); + d_iteCache.insert(cacheKey, cached); + return cached; + } else { + d_iteCache.insert(cacheKey, Node::null()); + return node; + } +} + +Node RemoveITE::replace(TNode node, bool inQuant) const { + if(node.isVar() || node.isConst() || + (options::biasedITERemoval() && !containsTermITE(node))){ + return Node(node); + } + + // Check the cache + NodeManager *nodeManager = NodeManager::currentNM(); + ITECache::const_iterator i = d_iteCache.find(make_pair(node, inQuant)); + if(i != d_iteCache.end()) { + Node cached = (*i).second; + return cached.isNull() ? Node(node) : cached; + } + + // Remember that we're inside a quantifier + if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) { + inQuant = true; + } + + vector newChildren; + bool somethingChanged = false; + if(node.getMetaKind() == kind::metakind::PARAMETERIZED) { + newChildren.push_back(node.getOperator()); + } + // Replace in children + for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) { + Node newChild = replace(*it, inQuant); + somethingChanged |= (newChild != *it); + newChildren.push_back(newChild); + } + + // If changes, we rewrite + if(somethingChanged) { + return nodeManager->mkNode(node.getKind(), newChildren); + } else { + return node; + } +} + +}/* CVC4 namespace */ diff --git a/src/smt/ite_removal.h b/src/smt/ite_removal.h new file mode 100644 index 000000000..d6d820f89 --- /dev/null +++ b/src/smt/ite_removal.h @@ -0,0 +1,93 @@ +/********************* */ +/*! \file ite_removal.h + ** \verbatim + ** Original author: Dejan Jovanovic + ** Major contributors: Kshitij Bansal, Tim King, Morgan Deters + ** Minor contributors (to current version): Clark Barrett + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Removal of term ITEs + ** + ** Removal of term ITEs. + **/ + +#include "cvc4_private.h" + +#pragma once + +#include + +#include "context/cdinsert_hashmap.h" +#include "context/context.h" +#include "expr/node.h" +#include "smt/dump.h" +#include "util/bool.h" +#include "util/hash.h" + +namespace CVC4 { + +namespace theory { + class ContainsTermITEVisitor; +}/* CVC4::theory namespace */ + +typedef std::hash_map IteSkolemMap; + +class RemoveITE { + typedef context::CDInsertHashMap< std::pair, Node, PairHashFunction > ITECache; + ITECache d_iteCache; + + +public: + + RemoveITE(context::UserContext* u); + ~RemoveITE(); + + /** + * Removes the ITE nodes by introducing skolem variables. All + * additional assertions are pushed into assertions. iteSkolemMap + * contains a map from introduced skolem variables to the index in + * assertions containing the new Boolean ite created in conjunction + * with that skolem variable. + * + * With reportDeps true, report reasoning dependences to the proof + * manager (for unsat cores). + */ + void run(std::vector& assertions, IteSkolemMap& iteSkolemMap, bool reportDeps = false); + + /** + * Removes the ITE from the node by introducing skolem + * variables. All additional assertions are pushed into + * assertions. iteSkolemMap contains a map from introduced skolem + * variables to the index in assertions containing the new Boolean + * ite created in conjunction with that skolem variable. + */ + Node run(TNode node, std::vector& additionalAssertions, + IteSkolemMap& iteSkolemMap, bool inQuant); + + /** + * Substitute under node using pre-existing cache. Do not remove + * any ITEs not seen during previous runs. + */ + Node replace(TNode node, bool inQuant = false) const; + + /** Returns true if e contains a term ite. */ + bool containsTermITE(TNode e) const; + + /** Returns the collected size of the caches. */ + size_t collectedCacheSizes() const; + + /** Garbage collects non-context dependent data-structures. */ + void garbageCollect(); + + /** Return the RemoveITE's containsVisitor. */ + theory::ContainsTermITEVisitor* getContainsVisitor(); + +private: + theory::ContainsTermITEVisitor* d_containsVisitor; + +};/* class RemoveTTE */ + +}/* CVC4 namespace */ diff --git a/src/smt/model.cpp b/src/smt/model.cpp new file mode 100644 index 000000000..15ecbadfb --- /dev/null +++ b/src/smt/model.cpp @@ -0,0 +1,55 @@ +/********************* */ +/*! \file model.cpp + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: Morgan Deters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief implementation of Model class + **/ + +#include "smt/model.h" + +#include + +#include "expr/expr_iomanip.h" +#include "options/base_options.h" +#include "printer/printer.h" +#include "smt/command.h" +#include "smt/command_list.h" +#include "smt/smt_engine_scope.h" + +using namespace std; + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, const Model& m) { + smt::SmtScope smts(&m.d_smt); + expr::ExprDag::Scope scope(out, false); + Printer::getPrinter(options::outputLanguage())->toStream(out, m); + return out; +} + +Model::Model() : + d_smt(*smt::currentSmtEngine()) { +} + +size_t Model::getNumCommands() const { + return d_smt.d_modelCommands->size() + d_smt.d_modelGlobalCommands.size(); +} + +const Command* Model::getCommand(size_t i) const { + Assert(i < getNumCommands()); + // index the global commands first, then the locals + if(i < d_smt.d_modelGlobalCommands.size()) { + return d_smt.d_modelGlobalCommands[i]; + } else { + return (*d_smt.d_modelCommands)[i - d_smt.d_modelGlobalCommands.size()]; + } +} + +}/* CVC4 namespace */ diff --git a/src/smt/model.h b/src/smt/model.h new file mode 100644 index 000000000..33a9312a6 --- /dev/null +++ b/src/smt/model.h @@ -0,0 +1,78 @@ +/********************* */ +/*! \file model.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: Andrew Reynolds + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Model class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__MODEL_H +#define __CVC4__MODEL_H + +#include +#include + +#include "expr/expr.h" +#include "util/cardinality.h" + +namespace CVC4 { + +class Command; +class SmtEngine; +class Model; + +std::ostream& operator<<(std::ostream&, const Model&); + +class Model { + friend std::ostream& operator<<(std::ostream&, const Model&); + friend class SmtEngine; + + /** the input name (file name, etc.) this model is associated to */ + std::string d_inputName; + +protected: + /** The SmtEngine we're associated with */ + SmtEngine& d_smt; + + /** construct the base class; users cannot do this, only CVC4 internals */ + Model(); + +public: + /** virtual destructor */ + virtual ~Model() { } + /** get number of commands to report */ + size_t getNumCommands() const; + /** get command */ + const Command* getCommand(size_t i) const; + /** get the smt engine that this model is hooked up to */ + SmtEngine* getSmtEngine() { return &d_smt; } + /** get the smt engine (as a pointer-to-const) that this model is hooked up to */ + const SmtEngine* getSmtEngine() const { return &d_smt; } + /** get the input name (file name, etc.) this model is associated to */ + std::string getInputName() const { return d_inputName; } + +public: + /** get value for expression */ + virtual Expr getValue(Expr expr) const = 0; + /** get cardinality for sort */ + virtual Cardinality getCardinality(Type t) const = 0; +};/* class Model */ + +class ModelBuilder { +public: + ModelBuilder() { } + virtual ~ModelBuilder() { } + virtual void buildModel(Model* m, bool fullModel) = 0; +};/* class ModelBuilder */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__MODEL_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index df3466d92..850b37fe0 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -72,15 +72,15 @@ #include "proof/unsat_core.h" #include "prop/prop_engine.h" #include "smt/boolean_terms.h" +#include "smt/command.h" #include "smt/command_list.h" +#include "smt/ite_removal.h" #include "smt/logic_request.h" #include "smt/managed_ostreams.h" #include "smt/model_postprocessor.h" #include "smt/smt_engine_scope.h" #include "smt/update_ostream.h" #include "smt_util/boolean_simplification.h" -#include "smt_util/command.h" -#include "smt_util/ite_removal.h" #include "smt_util/nary_builder.h" #include "smt_util/node_visitor.h" #include "theory/arith/pseudoboolean_proc.h" diff --git a/src/smt/update_ostream.h b/src/smt/update_ostream.h index c5f09a2a9..b87ed69d2 100644 --- a/src/smt/update_ostream.h +++ b/src/smt/update_ostream.h @@ -28,7 +28,7 @@ #include "options/language.h" #include "options/set_language.h" #include "options/base_options.h" -#include "smt_util/dump.h" +#include "smt/dump.h" namespace CVC4 { diff --git a/src/smt_util/Makefile.am b/src/smt_util/Makefile.am index ae1ea1f70..46f6493a9 100644 --- a/src/smt_util/Makefile.am +++ b/src/smt_util/Makefile.am @@ -10,23 +10,11 @@ libsmtutil_la_SOURCES = \ Makefile.in \ boolean_simplification.cpp \ boolean_simplification.h \ - command.cpp \ - command.h \ - dump.cpp \ - dump.h \ - ite_removal.cpp \ - ite_removal.h \ lemma_channels.cpp \ lemma_channels.h \ lemma_input_channel.h \ lemma_output_channel.h \ - model.cpp \ - model.h \ nary_builder.cpp \ nary_builder.h \ node_visitor.h - -EXTRA_DIST = \ - command.i - diff --git a/src/smt_util/command.cpp b/src/smt_util/command.cpp deleted file mode 100644 index 83298836f..000000000 --- a/src/smt_util/command.cpp +++ /dev/null @@ -1,1855 +0,0 @@ -/********************* */ -/*! \file command.cpp - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Kshitij Bansal, Dejan Jovanovic, Andrew Reynolds, Francois Bobot - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Implementation of command objects. - ** - ** Implementation of command objects. - **/ - -#include "smt_util/command.h" - -#include -#include -#include -#include -#include -#include - -#include "base/cvc4_assert.h" -#include "base/output.h" -#include "expr/expr_iomanip.h" -#include "expr/node.h" -#include "options/options.h" -#include "options/smt_options.h" -#include "printer/printer.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" -#include "smt_util/dump.h" -#include "smt_util/model.h" -#include "util/sexpr.h" - -using namespace std; - -namespace CVC4 { - -const int CommandPrintSuccess::s_iosIndex = std::ios_base::xalloc(); -const CommandSuccess* CommandSuccess::s_instance = new CommandSuccess(); -const CommandInterrupted* CommandInterrupted::s_instance = new CommandInterrupted(); - -std::ostream& operator<<(std::ostream& out, const Command& c) throw() { - c.toStream(out, - Node::setdepth::getDepth(out), - Node::printtypes::getPrintTypes(out), - Node::dag::getDag(out), - Node::setlanguage::getLanguage(out)); - return out; -} - -ostream& operator<<(ostream& out, const Command* c) throw() { - if(c == NULL) { - out << "null"; - } else { - out << *c; - } - return out; -} - -std::ostream& operator<<(std::ostream& out, const CommandStatus& s) throw() { - s.toStream(out, Node::setlanguage::getLanguage(out)); - return out; -} - -ostream& operator<<(ostream& out, const CommandStatus* s) throw() { - if(s == NULL) { - out << "null"; - } else { - out << *s; - } - return out; -} - -/* class Command */ - -Command::Command() throw() : d_commandStatus(NULL), d_muted(false) { -} - -Command::Command(const Command& cmd) { - d_commandStatus = (cmd.d_commandStatus == NULL) ? NULL : &cmd.d_commandStatus->clone(); - d_muted = cmd.d_muted; -} - -Command::~Command() throw() { - if(d_commandStatus != NULL && d_commandStatus != CommandSuccess::instance()) { - delete d_commandStatus; - } -} - -bool Command::ok() const throw() { - // either we haven't run the command yet, or it ran successfully - return d_commandStatus == NULL || dynamic_cast(d_commandStatus) != NULL; -} - -bool Command::fail() const throw() { - return d_commandStatus != NULL && dynamic_cast(d_commandStatus) != NULL; -} - -bool Command::interrupted() const throw() { - return d_commandStatus != NULL && dynamic_cast(d_commandStatus) != NULL; -} - -void Command::invoke(SmtEngine* smtEngine, std::ostream& out) throw() { - invoke(smtEngine); - if(!(isMuted() && ok())) { - printResult(out, smtEngine->getOption("command-verbosity:" + getCommandName()).getIntegerValue().toUnsignedInt()); - } -} - -std::string Command::toString() const throw() { - std::stringstream ss; - toStream(ss); - return ss.str(); -} - -void Command::toStream(std::ostream& out, int toDepth, bool types, size_t dag, - OutputLanguage language) const throw() { - Printer::getPrinter(language)->toStream(out, this, toDepth, types, dag); -} - -void CommandStatus::toStream(std::ostream& out, OutputLanguage language) const throw() { - Printer::getPrinter(language)->toStream(out, this); -} - -void Command::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(d_commandStatus != NULL) { - if((!ok() && verbosity >= 1) || verbosity >= 2) { - out << *d_commandStatus; - } - } -} - -/* class EmptyCommand */ - -EmptyCommand::EmptyCommand(std::string name) throw() : - d_name(name) { -} - -std::string EmptyCommand::getName() const throw() { - return d_name; -} - -void EmptyCommand::invoke(SmtEngine* smtEngine) throw() { - /* empty commands have no implementation */ - d_commandStatus = CommandSuccess::instance(); -} - -Command* EmptyCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new EmptyCommand(d_name); -} - -Command* EmptyCommand::clone() const { - return new EmptyCommand(d_name); -} - -std::string EmptyCommand::getCommandName() const throw() { - return "empty"; -} - -/* class EchoCommand */ - -EchoCommand::EchoCommand(std::string output) throw() : - d_output(output) { -} - -std::string EchoCommand::getOutput() const throw() { - return d_output; -} - -void EchoCommand::invoke(SmtEngine* smtEngine) throw() { - /* we don't have an output stream here, nothing to do */ - d_commandStatus = CommandSuccess::instance(); -} - -void EchoCommand::invoke(SmtEngine* smtEngine, std::ostream& out) throw() { - out << d_output << std::endl; - d_commandStatus = CommandSuccess::instance(); - printResult(out, smtEngine->getOption("command-verbosity:" + getCommandName()).getIntegerValue().toUnsignedInt()); -} - -Command* EchoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new EchoCommand(d_output); -} - -Command* EchoCommand::clone() const { - return new EchoCommand(d_output); -} - -std::string EchoCommand::getCommandName() const throw() { - return "echo"; -} - -/* class AssertCommand */ - -AssertCommand::AssertCommand(const Expr& e, bool inUnsatCore) throw() : - d_expr(e), d_inUnsatCore(inUnsatCore) { -} - -Expr AssertCommand::getExpr() const throw() { - return d_expr; -} - -void AssertCommand::invoke(SmtEngine* smtEngine) throw() { - try { - smtEngine->assertFormula(d_expr, d_inUnsatCore); - d_commandStatus = CommandSuccess::instance(); - } catch(UnsafeInterruptException& e) { - d_commandStatus = new CommandInterrupted(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* AssertCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new AssertCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore); -} - -Command* AssertCommand::clone() const { - return new AssertCommand(d_expr, d_inUnsatCore); -} - -std::string AssertCommand::getCommandName() const throw() { - return "assert"; -} - -/* class PushCommand */ - -void PushCommand::invoke(SmtEngine* smtEngine) throw() { - try { - smtEngine->push(); - d_commandStatus = CommandSuccess::instance(); - } catch(UnsafeInterruptException& e) { - d_commandStatus = new CommandInterrupted(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* PushCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new PushCommand(); -} - -Command* PushCommand::clone() const { - return new PushCommand(); -} - -std::string PushCommand::getCommandName() const throw() { - return "push"; -} - -/* class PopCommand */ - -void PopCommand::invoke(SmtEngine* smtEngine) throw() { - try { - smtEngine->pop(); - d_commandStatus = CommandSuccess::instance(); - } catch(UnsafeInterruptException& e) { - d_commandStatus = new CommandInterrupted(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* PopCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new PopCommand(); -} - -Command* PopCommand::clone() const { - return new PopCommand(); -} - -std::string PopCommand::getCommandName() const throw() { - return "pop"; -} - -/* class CheckSatCommand */ - -CheckSatCommand::CheckSatCommand() throw() : - d_expr() { -} - -CheckSatCommand::CheckSatCommand(const Expr& expr, bool inUnsatCore) throw() : - d_expr(expr), d_inUnsatCore(inUnsatCore) { -} - -Expr CheckSatCommand::getExpr() const throw() { - return d_expr; -} - -void CheckSatCommand::invoke(SmtEngine* smtEngine) throw() { - try { - d_result = smtEngine->checkSat(d_expr); - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Result CheckSatCommand::getResult() const throw() { - return d_result; -} - -void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - out << d_result << endl; - } -} - -Command* CheckSatCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& 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, d_inUnsatCore); - c->d_result = d_result; - return c; -} - -std::string CheckSatCommand::getCommandName() const throw() { - return "check-sat"; -} - -/* class QueryCommand */ - -QueryCommand::QueryCommand(const Expr& e, bool inUnsatCore) throw() : - d_expr(e), d_inUnsatCore(inUnsatCore) { -} - -Expr QueryCommand::getExpr() const throw() { - return d_expr; -} - -void QueryCommand::invoke(SmtEngine* smtEngine) throw() { - try { - d_result = smtEngine->query(d_expr); - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Result QueryCommand::getResult() const throw() { - return d_result; -} - -void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - out << d_result << endl; - } -} - -Command* QueryCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& 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, d_inUnsatCore); - c->d_result = d_result; - return c; -} - -std::string QueryCommand::getCommandName() const throw() { - return "query"; -} - -/* class ResetCommand */ - -void ResetCommand::invoke(SmtEngine* smtEngine) throw() { - try { - smtEngine->reset(); - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* ResetCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new ResetCommand(); -} - -Command* ResetCommand::clone() const { - return new ResetCommand(); -} - -std::string ResetCommand::getCommandName() const throw() { - return "reset"; -} - -/* class ResetAssertionsCommand */ - -void ResetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() { - try { - smtEngine->resetAssertions(); - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* ResetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new ResetAssertionsCommand(); -} - -Command* ResetAssertionsCommand::clone() const { - return new ResetAssertionsCommand(); -} - -std::string ResetAssertionsCommand::getCommandName() const throw() { - return "reset-assertions"; -} - -/* class QuitCommand */ - -void QuitCommand::invoke(SmtEngine* smtEngine) throw() { - Dump("benchmark") << *this; - d_commandStatus = CommandSuccess::instance(); -} - -Command* QuitCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new QuitCommand(); -} - -Command* QuitCommand::clone() const { - return new QuitCommand(); -} - -std::string QuitCommand::getCommandName() const throw() { - return "exit"; -} - -/* class CommentCommand */ - -CommentCommand::CommentCommand(std::string comment) throw() : d_comment(comment) { -} - -std::string CommentCommand::getComment() const throw() { - return d_comment; -} - -void CommentCommand::invoke(SmtEngine* smtEngine) throw() { - Dump("benchmark") << *this; - d_commandStatus = CommandSuccess::instance(); -} - -Command* CommentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new CommentCommand(d_comment); -} - -Command* CommentCommand::clone() const { - return new CommentCommand(d_comment); -} - -std::string CommentCommand::getCommandName() const throw() { - return "comment"; -} - -/* class CommandSequence */ - -CommandSequence::CommandSequence() throw() : - d_index(0) { -} - -CommandSequence::~CommandSequence() throw() { - for(unsigned i = d_index; i < d_commandSequence.size(); ++i) { - delete d_commandSequence[i]; - } -} - -void CommandSequence::addCommand(Command* cmd) throw() { - d_commandSequence.push_back(cmd); -} - -void CommandSequence::clear() throw() { - d_commandSequence.clear(); -} - -void CommandSequence::invoke(SmtEngine* smtEngine) throw() { - for(; d_index < d_commandSequence.size(); ++d_index) { - d_commandSequence[d_index]->invoke(smtEngine); - if(! d_commandSequence[d_index]->ok()) { - // abort execution - d_commandStatus = d_commandSequence[d_index]->getCommandStatus(); - return; - } - delete d_commandSequence[d_index]; - } - - AlwaysAssert(d_commandStatus == NULL); - d_commandStatus = CommandSuccess::instance(); -} - -void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) throw() { - for(; d_index < d_commandSequence.size(); ++d_index) { - d_commandSequence[d_index]->invoke(smtEngine, out); - if(! d_commandSequence[d_index]->ok()) { - // abort execution - d_commandStatus = d_commandSequence[d_index]->getCommandStatus(); - return; - } - delete d_commandSequence[d_index]; - } - - AlwaysAssert(d_commandStatus == NULL); - d_commandStatus = CommandSuccess::instance(); -} - -Command* CommandSequence::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - CommandSequence* seq = new CommandSequence(); - for(iterator i = begin(); i != end(); ++i) { - Command* cmd_to_export = *i; - Command* cmd = cmd_to_export->exportTo(exprManager, variableMap); - seq->addCommand(cmd); - Debug("export") << "[export] so far converted: " << seq << endl; - } - seq->d_index = d_index; - return seq; -} - -Command* CommandSequence::clone() const { - CommandSequence* seq = new CommandSequence(); - for(const_iterator i = begin(); i != end(); ++i) { - seq->addCommand((*i)->clone()); - } - seq->d_index = d_index; - return seq; -} - -CommandSequence::const_iterator CommandSequence::begin() const throw() { - return d_commandSequence.begin(); -} - -CommandSequence::const_iterator CommandSequence::end() const throw() { - return d_commandSequence.end(); -} - -CommandSequence::iterator CommandSequence::begin() throw() { - return d_commandSequence.begin(); -} - -CommandSequence::iterator CommandSequence::end() throw() { - return d_commandSequence.end(); -} - -std::string CommandSequence::getCommandName() const throw() { - return "sequence"; -} - -/* class DeclarationSequenceCommand */ - -/* class DeclarationDefinitionCommand */ - -DeclarationDefinitionCommand::DeclarationDefinitionCommand(const std::string& id) throw() : - d_symbol(id) { -} - -std::string DeclarationDefinitionCommand::getSymbol() const throw() { - return d_symbol; -} - -/* class DeclareFunctionCommand */ - -DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id, Expr func, Type t) throw() : - DeclarationDefinitionCommand(id), - d_func(func), - d_type(t), - d_printInModel(true), - d_printInModelSetByUser(false){ -} - -Expr DeclareFunctionCommand::getFunction() const throw() { - return d_func; -} - -Type DeclareFunctionCommand::getType() const throw() { - return d_type; -} - -bool DeclareFunctionCommand::getPrintInModel() const throw() { - return d_printInModel; -} - -bool DeclareFunctionCommand::getPrintInModelSetByUser() const throw() { - return d_printInModelSetByUser; -} - -void DeclareFunctionCommand::setPrintInModel( bool p ) { - d_printInModel = p; - d_printInModelSetByUser = true; -} - -void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() { - d_commandStatus = CommandSuccess::instance(); -} - -Command* DeclareFunctionCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) { - DeclareFunctionCommand * dfc = new DeclareFunctionCommand(d_symbol, d_func.exportTo(exprManager, variableMap), - d_type.exportTo(exprManager, variableMap)); - dfc->d_printInModel = d_printInModel; - dfc->d_printInModelSetByUser = d_printInModelSetByUser; - return dfc; -} - -Command* DeclareFunctionCommand::clone() const { - DeclareFunctionCommand * dfc = new DeclareFunctionCommand(d_symbol, d_func, d_type); - dfc->d_printInModel = d_printInModel; - dfc->d_printInModelSetByUser = d_printInModelSetByUser; - return dfc; -} - -std::string DeclareFunctionCommand::getCommandName() const throw() { - return "declare-fun"; -} - -/* class DeclareTypeCommand */ - -DeclareTypeCommand::DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw() : - DeclarationDefinitionCommand(id), - d_arity(arity), - d_type(t) { -} - -size_t DeclareTypeCommand::getArity() const throw() { - return d_arity; -} - -Type DeclareTypeCommand::getType() const throw() { - return d_type; -} - -void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() { - d_commandStatus = CommandSuccess::instance(); -} - -Command* DeclareTypeCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) { - return new DeclareTypeCommand(d_symbol, d_arity, - d_type.exportTo(exprManager, variableMap)); -} - -Command* DeclareTypeCommand::clone() const { - return new DeclareTypeCommand(d_symbol, d_arity, d_type); -} - -std::string DeclareTypeCommand::getCommandName() const throw() { - return "declare-sort"; -} - -/* class DefineTypeCommand */ - -DefineTypeCommand::DefineTypeCommand(const std::string& id, - Type t) throw() : - DeclarationDefinitionCommand(id), - d_params(), - d_type(t) { -} - -DefineTypeCommand::DefineTypeCommand(const std::string& id, - const std::vector& params, - Type t) throw() : - DeclarationDefinitionCommand(id), - d_params(params), - d_type(t) { -} - -const std::vector& DefineTypeCommand::getParameters() const throw() { - return d_params; -} - -Type DefineTypeCommand::getType() const throw() { - return d_type; -} - -void DefineTypeCommand::invoke(SmtEngine* smtEngine) throw() { - d_commandStatus = CommandSuccess::instance(); -} - -Command* DefineTypeCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - vector params; - transform(d_params.begin(), d_params.end(), back_inserter(params), - ExportTransformer(exprManager, variableMap)); - Type type = d_type.exportTo(exprManager, variableMap); - return new DefineTypeCommand(d_symbol, params, type); -} - -Command* DefineTypeCommand::clone() const { - return new DefineTypeCommand(d_symbol, d_params, d_type); -} - -std::string DefineTypeCommand::getCommandName() const throw() { - return "define-sort"; -} - -/* class DefineFunctionCommand */ - -DefineFunctionCommand::DefineFunctionCommand(const std::string& id, - Expr func, - Expr formula) throw() : - DeclarationDefinitionCommand(id), - d_func(func), - d_formals(), - d_formula(formula) { -} - -DefineFunctionCommand::DefineFunctionCommand(const std::string& id, - Expr func, - const std::vector& formals, - Expr formula) throw() : - DeclarationDefinitionCommand(id), - d_func(func), - d_formals(formals), - d_formula(formula) { -} - -Expr DefineFunctionCommand::getFunction() const throw() { - return d_func; -} - -const std::vector& DefineFunctionCommand::getFormals() const throw() { - return d_formals; -} - -Expr DefineFunctionCommand::getFormula() const throw() { - return d_formula; -} - -void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() { - try { - if(!d_func.isNull()) { - smtEngine->defineFunction(d_func, d_formals, d_formula); - } - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* DefineFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - Expr func = d_func.exportTo(exprManager, variableMap, /* flags = */ ExprManager::VAR_FLAG_DEFINED); - vector formals; - transform(d_formals.begin(), d_formals.end(), back_inserter(formals), - ExportTransformer(exprManager, variableMap)); - Expr formula = d_formula.exportTo(exprManager, variableMap); - return new DefineFunctionCommand(d_symbol, func, formals, formula); -} - -Command* DefineFunctionCommand::clone() const { - return new DefineFunctionCommand(d_symbol, d_func, d_formals, d_formula); -} - -std::string DefineFunctionCommand::getCommandName() const throw() { - return "define-fun"; -} - -/* class DefineNamedFunctionCommand */ - -DefineNamedFunctionCommand::DefineNamedFunctionCommand(const std::string& id, - Expr func, - const std::vector& formals, - Expr formula) throw() : - DefineFunctionCommand(id, func, formals, formula) { -} - -void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) throw() { - this->DefineFunctionCommand::invoke(smtEngine); - if(!d_func.isNull() && d_func.getType().isBoolean()) { - smtEngine->addToAssignment(d_func.getExprManager()->mkExpr(kind::APPLY, d_func)); - } - d_commandStatus = CommandSuccess::instance(); -} - -Command* DefineNamedFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - Expr func = d_func.exportTo(exprManager, variableMap); - vector formals; - transform(d_formals.begin(), d_formals.end(), back_inserter(formals), - ExportTransformer(exprManager, variableMap)); - Expr formula = d_formula.exportTo(exprManager, variableMap); - return new DefineNamedFunctionCommand(d_symbol, func, formals, formula); -} - -Command* DefineNamedFunctionCommand::clone() const { - return new DefineNamedFunctionCommand(d_symbol, d_func, d_formals, d_formula); -} - -/* class SetUserAttribute */ - -SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr ) throw() : - d_attr( attr ), d_expr( expr ){ -} - -SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr, - std::vector& values ) throw() : - d_attr( attr ), d_expr( expr ){ - d_expr_values.insert( d_expr_values.begin(), values.begin(), values.end() ); -} - -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, d_expr_values, d_str_value ); - } - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* SetUserAttributeCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap){ - Expr expr = d_expr.exportTo(exprManager, variableMap); - 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{ - 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() { - return "set-user-attribute"; -} - -/* class SimplifyCommand */ - -SimplifyCommand::SimplifyCommand(Expr term) throw() : - d_term(term) { -} - -Expr SimplifyCommand::getTerm() const throw() { - return d_term; -} - -void SimplifyCommand::invoke(SmtEngine* smtEngine) throw() { - try { - d_result = smtEngine->simplify(d_term); - d_commandStatus = CommandSuccess::instance(); - } catch(UnsafeInterruptException& e) { - d_commandStatus = new CommandInterrupted(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Expr SimplifyCommand::getResult() const throw() { - return d_result; -} - -void SimplifyCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - out << d_result << endl; - } -} - -Command* SimplifyCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - SimplifyCommand* c = new SimplifyCommand(d_term.exportTo(exprManager, variableMap)); - c->d_result = d_result.exportTo(exprManager, variableMap); - return c; -} - -Command* SimplifyCommand::clone() const { - SimplifyCommand* c = new SimplifyCommand(d_term); - c->d_result = d_result; - return c; -} - -std::string SimplifyCommand::getCommandName() const throw() { - return "simplify"; -} - -/* class ExpandDefinitionsCommand */ - -ExpandDefinitionsCommand::ExpandDefinitionsCommand(Expr term) throw() : - d_term(term) { -} - -Expr ExpandDefinitionsCommand::getTerm() const throw() { - return d_term; -} - -void ExpandDefinitionsCommand::invoke(SmtEngine* smtEngine) throw() { - d_result = smtEngine->expandDefinitions(d_term); - d_commandStatus = CommandSuccess::instance(); -} - -Expr ExpandDefinitionsCommand::getResult() const throw() { - return d_result; -} - -void ExpandDefinitionsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - out << d_result << endl; - } -} - -Command* ExpandDefinitionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term.exportTo(exprManager, variableMap)); - c->d_result = d_result.exportTo(exprManager, variableMap); - return c; -} - -Command* ExpandDefinitionsCommand::clone() const { - ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term); - c->d_result = d_result; - return c; -} - -std::string ExpandDefinitionsCommand::getCommandName() const throw() { - return "expand-definitions"; -} - -/* class GetValueCommand */ - -GetValueCommand::GetValueCommand(Expr term) throw() : - d_terms() { - d_terms.push_back(term); -} - -GetValueCommand::GetValueCommand(const std::vector& terms) throw() : - d_terms(terms) { - PrettyCheckArgument(terms.size() >= 1, terms, - "cannot get-value of an empty set of terms"); -} - -const std::vector& GetValueCommand::getTerms() const throw() { - return d_terms; -} - -void GetValueCommand::invoke(SmtEngine* smtEngine) throw() { - try { - vector result; - ExprManager* em = smtEngine->getExprManager(); - NodeManager* nm = NodeManager::fromExprManager(em); - for(std::vector::const_iterator i = d_terms.begin(); i != d_terms.end(); ++i) { - Assert(nm == NodeManager::fromExprManager((*i).getExprManager())); - smt::SmtScope scope(smtEngine); - Node request = Node::fromExpr(options::expandDefinitions() ? smtEngine->expandDefinitions(*i) : *i); - Node value = Node::fromExpr(smtEngine->getValue(*i)); - if(value.getType().isInteger() && request.getType() == nm->realType()) { - // Need to wrap in special marker so that output printers know this - // is an integer-looking constant that really should be output as - // a rational. Necessary for SMT-LIB standards compliance, but ugly. - value = nm->mkNode(kind::APPLY_TYPE_ASCRIPTION, - nm->mkConst(AscriptionType(em->realType())), value); - } - result.push_back(nm->mkNode(kind::SEXPR, request, value).toExpr()); - } - d_result = em->mkExpr(kind::SEXPR, result); - d_commandStatus = CommandSuccess::instance(); - } catch(UnsafeInterruptException& e) { - d_commandStatus = new CommandInterrupted(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Expr GetValueCommand::getResult() const throw() { - return d_result; -} - -void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - expr::ExprDag::Scope scope(out, false); - out << d_result << endl; - } -} - -Command* GetValueCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - vector exportedTerms; - for(std::vector::const_iterator i = d_terms.begin(); i != d_terms.end(); ++i) { - exportedTerms.push_back((*i).exportTo(exprManager, variableMap)); - } - GetValueCommand* c = new GetValueCommand(exportedTerms); - c->d_result = d_result.exportTo(exprManager, variableMap); - return c; -} - -Command* GetValueCommand::clone() const { - GetValueCommand* c = new GetValueCommand(d_terms); - c->d_result = d_result; - return c; -} - -std::string GetValueCommand::getCommandName() const throw() { - return "get-value"; -} - -/* class GetAssignmentCommand */ - -GetAssignmentCommand::GetAssignmentCommand() throw() { -} - -void GetAssignmentCommand::invoke(SmtEngine* smtEngine) throw() { - try { - d_result = smtEngine->getAssignment(); - d_commandStatus = CommandSuccess::instance(); - } catch(UnsafeInterruptException& e) { - d_commandStatus = new CommandInterrupted(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -SExpr GetAssignmentCommand::getResult() const throw() { - return d_result; -} - -void GetAssignmentCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - out << d_result << endl; - } -} - -Command* GetAssignmentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetAssignmentCommand* c = new GetAssignmentCommand(); - c->d_result = d_result; - return c; -} - -Command* GetAssignmentCommand::clone() const { - GetAssignmentCommand* c = new GetAssignmentCommand(); - c->d_result = d_result; - return c; -} - -std::string GetAssignmentCommand::getCommandName() const throw() { - return "get-assignment"; -} - -/* class GetModelCommand */ - -GetModelCommand::GetModelCommand() throw() { -} - -void GetModelCommand::invoke(SmtEngine* smtEngine) throw() { - try { - d_result = smtEngine->getModel(); - d_smtEngine = smtEngine; - d_commandStatus = CommandSuccess::instance(); - } catch(UnsafeInterruptException& e) { - d_commandStatus = new CommandInterrupted(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -/* Model is private to the library -- for now -Model* GetModelCommand::getResult() const throw() { - return d_result; -} -*/ - -void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - out << *d_result; - } -} - -Command* GetModelCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetModelCommand* c = new GetModelCommand(); - c->d_result = d_result; - c->d_smtEngine = d_smtEngine; - return c; -} - -Command* GetModelCommand::clone() const { - GetModelCommand* c = new GetModelCommand(); - c->d_result = d_result; - c->d_smtEngine = d_smtEngine; - return c; -} - -std::string GetModelCommand::getCommandName() const throw() { - return "get-model"; -} - -/* class GetProofCommand */ - -GetProofCommand::GetProofCommand() throw() { -} - -void GetProofCommand::invoke(SmtEngine* smtEngine) throw() { - try { - d_smtEngine = smtEngine; - d_result = smtEngine->getProof(); - d_commandStatus = CommandSuccess::instance(); - } catch(UnsafeInterruptException& e) { - d_commandStatus = new CommandInterrupted(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Proof* GetProofCommand::getResult() const throw() { - return d_result; -} - -void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - smt::SmtScope scope(d_smtEngine); - d_result->toStream(out); - } -} - -Command* GetProofCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetProofCommand* c = new GetProofCommand(); - c->d_result = d_result; - c->d_smtEngine = d_smtEngine; - return c; -} - -Command* GetProofCommand::clone() const { - GetProofCommand* c = new GetProofCommand(); - c->d_result = d_result; - c->d_smtEngine = d_smtEngine; - return c; -} - -std::string GetProofCommand::getCommandName() const throw() { - return "get-proof"; -} - -/* class GetInstantiationsCommand */ - -GetInstantiationsCommand::GetInstantiationsCommand() throw() { -} - -void GetInstantiationsCommand::invoke(SmtEngine* smtEngine) throw() { - try { - d_smtEngine = smtEngine; - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -//Instantiations* GetInstantiationsCommand::getResult() const throw() { -// return d_result; -//} - -void GetInstantiationsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - d_smtEngine->printInstantiations(out); - } -} - -Command* GetInstantiationsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetInstantiationsCommand* c = new GetInstantiationsCommand(); - //c->d_result = d_result; - c->d_smtEngine = d_smtEngine; - return c; -} - -Command* GetInstantiationsCommand::clone() const { - GetInstantiationsCommand* c = new GetInstantiationsCommand(); - //c->d_result = d_result; - c->d_smtEngine = d_smtEngine; - return c; -} - -std::string GetInstantiationsCommand::getCommandName() const throw() { - return "get-instantiations"; -} - -/* class GetSynthSolutionCommand */ - -GetSynthSolutionCommand::GetSynthSolutionCommand() throw() { -} - -void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine) throw() { - try { - d_smtEngine = smtEngine; - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -void GetSynthSolutionCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - d_smtEngine->printSynthSolution(out); - } -} - -Command* GetSynthSolutionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetSynthSolutionCommand* c = new GetSynthSolutionCommand(); - c->d_smtEngine = d_smtEngine; - return c; -} - -Command* GetSynthSolutionCommand::clone() const { - GetSynthSolutionCommand* c = new GetSynthSolutionCommand(); - c->d_smtEngine = d_smtEngine; - return c; -} - -std::string GetSynthSolutionCommand::getCommandName() const throw() { - return "get-instantiations"; -} - -/* class GetUnsatCoreCommand */ - -GetUnsatCoreCommand::GetUnsatCoreCommand() throw() { -} - -GetUnsatCoreCommand::GetUnsatCoreCommand(const std::map& 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()); - } -} - -void GetUnsatCoreCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - 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(d_names); - c->d_result = d_result; - return c; -} - -Command* GetUnsatCoreCommand::clone() const { - GetUnsatCoreCommand* c = new GetUnsatCoreCommand(d_names); - c->d_result = d_result; - return c; -} - -std::string GetUnsatCoreCommand::getCommandName() const throw() { - return "get-unsat-core"; -} - -/* class GetAssertionsCommand */ - -GetAssertionsCommand::GetAssertionsCommand() throw() { -} - -void GetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() { - try { - stringstream ss; - const vector v = smtEngine->getAssertions(); - ss << "(\n"; - copy( v.begin(), v.end(), ostream_iterator(ss, "\n") ); - ss << ")\n"; - d_result = ss.str(); - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -std::string GetAssertionsCommand::getResult() const throw() { - return d_result; -} - -void GetAssertionsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - out << d_result; - } -} - -Command* GetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetAssertionsCommand* c = new GetAssertionsCommand(); - c->d_result = d_result; - return c; -} - -Command* GetAssertionsCommand::clone() const { - GetAssertionsCommand* c = new GetAssertionsCommand(); - c->d_result = d_result; - return c; -} - -std::string GetAssertionsCommand::getCommandName() const throw() { - return "get-assertions"; -} - -/* class SetBenchmarkStatusCommand */ - -SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) throw() : - d_status(status) { -} - -BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const throw() { - return d_status; -} - -void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) throw() { - try { - stringstream ss; - ss << d_status; - SExpr status = SExpr(ss.str()); - smtEngine->setInfo("status", status); - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* SetBenchmarkStatusCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new SetBenchmarkStatusCommand(d_status); -} - -Command* SetBenchmarkStatusCommand::clone() const { - return new SetBenchmarkStatusCommand(d_status); -} - -std::string SetBenchmarkStatusCommand::getCommandName() const throw() { - return "set-info"; -} - -/* class SetBenchmarkLogicCommand */ - -SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) throw() : - d_logic(logic) { -} - -std::string SetBenchmarkLogicCommand::getLogic() const throw() { - return d_logic; -} - -void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) throw() { - try { - smtEngine->setLogic(d_logic); - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* SetBenchmarkLogicCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new SetBenchmarkLogicCommand(d_logic); -} - -Command* SetBenchmarkLogicCommand::clone() const { - return new SetBenchmarkLogicCommand(d_logic); -} - -std::string SetBenchmarkLogicCommand::getCommandName() const throw() { - return "set-logic"; -} - -/* class SetInfoCommand */ - -SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) throw() : - d_flag(flag), - d_sexpr(sexpr) { -} - -std::string SetInfoCommand::getFlag() const throw() { - return d_flag; -} - -SExpr SetInfoCommand::getSExpr() const throw() { - return d_sexpr; -} - -void SetInfoCommand::invoke(SmtEngine* smtEngine) throw() { - try { - smtEngine->setInfo(d_flag, d_sexpr); - d_commandStatus = CommandSuccess::instance(); - } catch(UnrecognizedOptionException&) { - // As per SMT-LIB spec, silently accept unknown set-info keys - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* SetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new SetInfoCommand(d_flag, d_sexpr); -} - -Command* SetInfoCommand::clone() const { - return new SetInfoCommand(d_flag, d_sexpr); -} - -std::string SetInfoCommand::getCommandName() const throw() { - return "set-info"; -} - -/* class GetInfoCommand */ - -GetInfoCommand::GetInfoCommand(std::string flag) throw() : - d_flag(flag) { -} - -std::string GetInfoCommand::getFlag() const throw() { - return d_flag; -} - -void GetInfoCommand::invoke(SmtEngine* smtEngine) throw() { - try { - vector v; - v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag))); - v.push_back(smtEngine->getInfo(d_flag)); - stringstream ss; - if(d_flag == "all-options" || d_flag == "all-statistics") { - ss << PrettySExprs(true); - } - ss << SExpr(v); - d_result = ss.str(); - d_commandStatus = CommandSuccess::instance(); - } catch(UnrecognizedOptionException&) { - d_commandStatus = new CommandUnsupported(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -std::string GetInfoCommand::getResult() const throw() { - return d_result; -} - -void GetInfoCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else if(d_result != "") { - out << d_result << endl; - } -} - -Command* GetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetInfoCommand* c = new GetInfoCommand(d_flag); - c->d_result = d_result; - return c; -} - -Command* GetInfoCommand::clone() const { - GetInfoCommand* c = new GetInfoCommand(d_flag); - c->d_result = d_result; - return c; -} - -std::string GetInfoCommand::getCommandName() const throw() { - return "get-info"; -} - -/* class SetOptionCommand */ - -SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) throw() : - d_flag(flag), - d_sexpr(sexpr) { -} - -std::string SetOptionCommand::getFlag() const throw() { - return d_flag; -} - -SExpr SetOptionCommand::getSExpr() const throw() { - return d_sexpr; -} - -void SetOptionCommand::invoke(SmtEngine* smtEngine) throw() { - try { - smtEngine->setOption(d_flag, d_sexpr); - d_commandStatus = CommandSuccess::instance(); - } catch(UnrecognizedOptionException&) { - d_commandStatus = new CommandUnsupported(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* SetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new SetOptionCommand(d_flag, d_sexpr); -} - -Command* SetOptionCommand::clone() const { - return new SetOptionCommand(d_flag, d_sexpr); -} - -std::string SetOptionCommand::getCommandName() const throw() { - return "set-option"; -} - -/* class GetOptionCommand */ - -GetOptionCommand::GetOptionCommand(std::string flag) throw() : - d_flag(flag) { -} - -std::string GetOptionCommand::getFlag() const throw() { - return d_flag; -} - -void GetOptionCommand::invoke(SmtEngine* smtEngine) throw() { - try { - SExpr res = smtEngine->getOption(d_flag); - d_result = res.toString(); - d_commandStatus = CommandSuccess::instance(); - } catch(UnrecognizedOptionException&) { - d_commandStatus = new CommandUnsupported(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -std::string GetOptionCommand::getResult() const throw() { - return d_result; -} - -void GetOptionCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else if(d_result != "") { - out << d_result << endl; - } -} - -Command* GetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetOptionCommand* c = new GetOptionCommand(d_flag); - c->d_result = d_result; - return c; -} - -Command* GetOptionCommand::clone() const { - GetOptionCommand* c = new GetOptionCommand(d_flag); - c->d_result = d_result; - return c; -} - -std::string GetOptionCommand::getCommandName() const throw() { - return "get-option"; -} - -/* class DatatypeDeclarationCommand */ - -DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) throw() : - d_datatypes() { - d_datatypes.push_back(datatype); -} - -DatatypeDeclarationCommand::DatatypeDeclarationCommand(const std::vector& datatypes) throw() : - d_datatypes(datatypes) { -} - -const std::vector& -DatatypeDeclarationCommand::getDatatypes() const throw() { - return d_datatypes; -} - -void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() { - d_commandStatus = CommandSuccess::instance(); -} - -Command* DatatypeDeclarationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - throw ExportUnsupportedException - ("export of DatatypeDeclarationCommand unsupported"); -} - -Command* DatatypeDeclarationCommand::clone() const { - return new DatatypeDeclarationCommand(d_datatypes); -} - -std::string DatatypeDeclarationCommand::getCommandName() const throw() { - return "declare-datatypes"; -} - -/* class RewriteRuleCommand */ - -RewriteRuleCommand::RewriteRuleCommand(const std::vector& vars, - const std::vector& guards, - Expr head, Expr body, - const Triggers& triggers) throw() : - d_vars(vars), d_guards(guards), d_head(head), d_body(body), d_triggers(triggers) { -} - -RewriteRuleCommand::RewriteRuleCommand(const std::vector& vars, - Expr head, Expr body) throw() : - d_vars(vars), d_head(head), d_body(body) { -} - -const std::vector& RewriteRuleCommand::getVars() const throw() { - return d_vars; -} - -const std::vector& RewriteRuleCommand::getGuards() const throw() { - return d_guards; -} - -Expr RewriteRuleCommand::getHead() const throw() { - return d_head; -} - -Expr RewriteRuleCommand::getBody() const throw() { - return d_body; -} - -const RewriteRuleCommand::Triggers& RewriteRuleCommand::getTriggers() const throw() { - return d_triggers; -} - -void RewriteRuleCommand::invoke(SmtEngine* smtEngine) throw() { - 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(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 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; vars.reserve(d_vars.size()); - for(VExpr::iterator i = d_vars.begin(), end = d_vars.end(); - i == end; ++i){ - vars.push_back(i->exportTo(exprManager, variableMap)); - }; - /** Convert guards */ - VExpr guards; guards.reserve(d_guards.size()); - for(VExpr::iterator i = d_guards.begin(), end = d_guards.end(); - i == end; ++i){ - guards.push_back(i->exportTo(exprManager, variableMap)); - }; - /** Convert triggers */ - Triggers triggers; triggers.resize(d_triggers.size()); - for(size_t i = 0, end = d_triggers.size(); - i < end; ++i){ - triggers[i].reserve(d_triggers[i].size()); - for(VExpr::iterator j = d_triggers[i].begin(), jend = d_triggers[i].end(); - j == jend; ++i){ - triggers[i].push_back(j->exportTo(exprManager, variableMap)); - }; - }; - /** 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 throw() { - return "rewrite-rule"; -} - -/* class PropagateRuleCommand */ - -PropagateRuleCommand::PropagateRuleCommand(const std::vector& vars, - const std::vector& guards, - const std::vector& heads, - Expr body, - const Triggers& triggers, - bool deduction) throw() : - d_vars(vars), d_guards(guards), d_heads(heads), d_body(body), d_triggers(triggers), d_deduction(deduction) { -} - -PropagateRuleCommand::PropagateRuleCommand(const std::vector& vars, - const std::vector& heads, - Expr body, - bool deduction) throw() : - d_vars(vars), d_heads(heads), d_body(body), d_deduction(deduction) { -} - -const std::vector& PropagateRuleCommand::getVars() const throw() { - return d_vars; -} - -const std::vector& PropagateRuleCommand::getGuards() const throw() { - return d_guards; -} - -const std::vector& PropagateRuleCommand::getHeads() const throw() { - return d_heads; -} - -Expr PropagateRuleCommand::getBody() const throw() { - return d_body; -} - -const PropagateRuleCommand::Triggers& PropagateRuleCommand::getTriggers() const throw() { - return d_triggers; -} - -bool PropagateRuleCommand::isDeduction() const throw() { - return d_deduction; -} - -void PropagateRuleCommand::invoke(SmtEngine* smtEngine) throw() { - 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(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 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; vars.reserve(d_vars.size()); - for(VExpr::iterator i = d_vars.begin(), end = d_vars.end(); - i == end; ++i){ - vars.push_back(i->exportTo(exprManager, variableMap)); - }; - /** Convert guards */ - VExpr guards; guards.reserve(d_guards.size()); - for(VExpr::iterator i = d_guards.begin(), end = d_guards.end(); - i == end; ++i){ - guards.push_back(i->exportTo(exprManager, variableMap)); - }; - /** Convert heads */ - VExpr heads; heads.reserve(d_heads.size()); - for(VExpr::iterator i = d_heads.begin(), end = d_heads.end(); - i == end; ++i){ - heads.push_back(i->exportTo(exprManager, variableMap)); - }; - /** Convert triggers */ - Triggers triggers; triggers.resize(d_triggers.size()); - for(size_t i = 0, end = d_triggers.size(); - i < end; ++i){ - triggers[i].reserve(d_triggers[i].size()); - for(VExpr::iterator j = d_triggers[i].begin(), jend = d_triggers[i].end(); - j == jend; ++i){ - triggers[i].push_back(j->exportTo(exprManager, variableMap)); - }; - }; - /** 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 throw() { - return "propagate-rule"; -} - -/* output stream insertion operator for benchmark statuses */ -std::ostream& operator<<(std::ostream& out, - BenchmarkStatus status) throw() { - switch(status) { - - case SMT_SATISFIABLE: - return out << "sat"; - - case SMT_UNSATISFIABLE: - return out << "unsat"; - - case SMT_UNKNOWN: - return out << "unknown"; - - default: - return out << "BenchmarkStatus::[UNKNOWNSTATUS!]"; - } -} - -}/* CVC4 namespace */ diff --git a/src/smt_util/command.h b/src/smt_util/command.h deleted file mode 100644 index 248e69b0e..000000000 --- a/src/smt_util/command.h +++ /dev/null @@ -1,905 +0,0 @@ -/********************* */ -/*! \file command.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Kshitij Bansal, Christopher L. Conway, Dejan Jovanovic, Francois Bobot, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Implementation of the command pattern on SmtEngines. - ** - ** Implementation of the command pattern on SmtEngines. Command - ** objects are generated by the parser (typically) to implement the - ** commands in parsed input (see Parser::parseNextCommand()), or by - ** client code. - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__COMMAND_H -#define __CVC4__COMMAND_H - -#include -#include -#include -#include -#include - -#include "expr/datatype.h" -#include "expr/expr.h" -#include "expr/type.h" -#include "expr/variable_type_map.h" -#include "proof/unsat_core.h" -#include "util/proof.h" -#include "util/result.h" -#include "util/sexpr.h" - -namespace CVC4 { - -class SmtEngine; -class Command; -class CommandStatus; -class Model; - -std::ostream& operator<<(std::ostream&, const Command&) throw() CVC4_PUBLIC; -std::ostream& operator<<(std::ostream&, const Command*) throw() CVC4_PUBLIC; -std::ostream& operator<<(std::ostream&, const CommandStatus&) throw() CVC4_PUBLIC; -std::ostream& operator<<(std::ostream&, const CommandStatus*) throw() CVC4_PUBLIC; - -/** The status an SMT benchmark can have */ -enum BenchmarkStatus { - /** Benchmark is satisfiable */ - SMT_SATISFIABLE, - /** Benchmark is unsatisfiable */ - SMT_UNSATISFIABLE, - /** The status of the benchmark is unknown */ - SMT_UNKNOWN -};/* enum BenchmarkStatus */ - -std::ostream& operator<<(std::ostream& out, - BenchmarkStatus status) throw() CVC4_PUBLIC; - -/** - * IOStream manipulator to print success messages or not. - * - * out << Command::printsuccess(false) << CommandSuccess(); - * - * prints nothing, but - * - * out << Command::printsuccess(true) << CommandSuccess(); - * - * prints a success message (in a manner appropriate for the current - * output language). - */ -class CVC4_PUBLIC CommandPrintSuccess { - /** - * The allocated index in ios_base for our depth setting. - */ - static const int s_iosIndex; - - /** - * The default setting, for ostreams that haven't yet had a - * setdepth() applied to them. - */ - static const int s_defaultPrintSuccess = false; - - /** - * When this manipulator is used, the setting is stored here. - */ - bool d_printSuccess; - -public: - /** - * Construct a CommandPrintSuccess with the given setting. - */ - CommandPrintSuccess(bool printSuccess) throw() : d_printSuccess(printSuccess) {} - - inline void applyPrintSuccess(std::ostream& out) throw() { - out.iword(s_iosIndex) = d_printSuccess; - } - - static inline bool getPrintSuccess(std::ostream& out) throw() { - return out.iword(s_iosIndex); - } - - static inline void setPrintSuccess(std::ostream& out, bool printSuccess) throw() { - out.iword(s_iosIndex) = printSuccess; - } - - /** - * Set the print-success state on the output stream for the current - * stack scope. This makes sure the old state is reset on the - * stream after normal OR exceptional exit from the scope, using the - * RAII C++ idiom. - */ - class Scope { - std::ostream& d_out; - bool d_oldPrintSuccess; - - public: - - inline Scope(std::ostream& out, bool printSuccess) throw() : - d_out(out), - d_oldPrintSuccess(CommandPrintSuccess::getPrintSuccess(out)) { - CommandPrintSuccess::setPrintSuccess(out, printSuccess); - } - - inline ~Scope() throw() { - CommandPrintSuccess::setPrintSuccess(d_out, d_oldPrintSuccess); - } - - };/* class CommandPrintSuccess::Scope */ - -};/* class CommandPrintSuccess */ - -/** - * Sets the default print-success setting when pretty-printing an Expr - * to an ostream. Use like this: - * - * // let out be an ostream, e an Expr - * out << Expr::setdepth(n) << e << endl; - * - * The depth stays permanently (until set again) with the stream. - */ -inline std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) throw() CVC4_PUBLIC; -inline std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) throw() { - cps.applyPrintSuccess(out); - return out; -} - -class CVC4_PUBLIC CommandStatus { -protected: - // shouldn't construct a CommandStatus (use a derived class) - CommandStatus() throw() {} -public: - virtual ~CommandStatus() throw() {} - void toStream(std::ostream& out, - OutputLanguage language = language::output::LANG_AUTO) const throw(); - virtual CommandStatus& clone() const = 0; -};/* class CommandStatus */ - -class CVC4_PUBLIC CommandSuccess : public CommandStatus { - static const CommandSuccess* s_instance; -public: - static const CommandSuccess* instance() throw() { return s_instance; } - CommandStatus& clone() const { return const_cast(*this); } -};/* class CommandSuccess */ - -class CVC4_PUBLIC CommandInterrupted : public CommandStatus { - static const CommandInterrupted* s_instance; -public: - static const CommandInterrupted* instance() throw() { return s_instance; } - CommandStatus& clone() const { return const_cast(*this); } -};/* class CommandInterrupted */ - -class CVC4_PUBLIC CommandUnsupported : public CommandStatus { -public: - CommandStatus& clone() const { return *new CommandUnsupported(*this); } -};/* class CommandSuccess */ - -class CVC4_PUBLIC CommandFailure : public CommandStatus { - std::string d_message; -public: - CommandFailure(std::string message) throw() : d_message(message) {} - CommandFailure& clone() const { return *new CommandFailure(*this); } - ~CommandFailure() throw() {} - std::string getMessage() const throw() { return d_message; } -};/* class CommandFailure */ - -class CVC4_PUBLIC Command { -protected: - /** - * This field contains a command status if the command has been - * invoked, or NULL if it has not. This field is either a - * dynamically-allocated pointer, or it's a pointer to the singleton - * CommandSuccess instance. Doing so is somewhat asymmetric, but - * it avoids the need to dynamically allocate memory in the common - * case of a successful command. - */ - const CommandStatus* d_commandStatus; - - /** - * True if this command is "muted"---i.e., don't print "success" on - * successful execution. - */ - bool d_muted; - -public: - typedef CommandPrintSuccess printsuccess; - - Command() throw(); - Command(const Command& cmd); - - virtual ~Command() throw(); - - virtual void invoke(SmtEngine* smtEngine) throw() = 0; - virtual void invoke(SmtEngine* smtEngine, std::ostream& out) throw(); - - virtual void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const throw(); - - std::string toString() const throw(); - - virtual std::string getCommandName() const throw() = 0; - - /** - * If false, instruct this Command not to print a success message. - */ - void setMuted(bool muted) throw() { d_muted = muted; } - - /** - * Determine whether this Command will print a success message. - */ - bool isMuted() throw() { return d_muted; } - - /** - * Either the command hasn't run yet, or it completed successfully - * (CommandSuccess, not CommandUnsupported or CommandFailure). - */ - bool ok() const throw(); - - /** - * The command completed in a failure state (CommandFailure, not - * CommandSuccess or CommandUnsupported). - */ - bool fail() const throw(); - - /** - * The command was ran but was interrupted due to resource limiting. - */ - bool interrupted() const throw(); - - /** Get the command status (it's NULL if we haven't run yet). */ - const CommandStatus* getCommandStatus() const throw() { return d_commandStatus; } - - virtual void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); - - /** - * Maps this Command into one for a different ExprManager, using - * variableMap for the translation and extending it with any new - * mappings. - */ - virtual Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) = 0; - - /** - * Clone this Command (make a shallow copy). - */ - virtual Command* clone() const = 0; - -protected: - class ExportTransformer { - ExprManager* d_exprManager; - ExprManagerMapCollection& d_variableMap; - public: - ExportTransformer(ExprManager* exprManager, ExprManagerMapCollection& variableMap) : - d_exprManager(exprManager), - d_variableMap(variableMap) { - } - Expr operator()(Expr e) { - return e.exportTo(d_exprManager, d_variableMap); - } - Type operator()(Type t) { - return t.exportTo(d_exprManager, d_variableMap); - } - };/* class Command::ExportTransformer */ -};/* class Command */ - -/** - * EmptyCommands are the residue of a command after the parser handles - * them (and there's nothing left to do). - */ -class CVC4_PUBLIC EmptyCommand : public Command { -protected: - std::string d_name; -public: - EmptyCommand(std::string name = "") throw(); - ~EmptyCommand() throw() {} - std::string getName() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class EmptyCommand */ - -class CVC4_PUBLIC EchoCommand : public Command { -protected: - std::string d_output; -public: - EchoCommand(std::string output = "") throw(); - ~EchoCommand() throw() {} - std::string getOutput() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - void invoke(SmtEngine* smtEngine, std::ostream& out) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class EchoCommand */ - -class CVC4_PUBLIC AssertCommand : public Command { -protected: - Expr d_expr; - bool d_inUnsatCore; -public: - AssertCommand(const Expr& e, bool inUnsatCore = true) throw(); - ~AssertCommand() throw() {} - Expr getExpr() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class AssertCommand */ - -class CVC4_PUBLIC PushCommand : public Command { -public: - ~PushCommand() throw() {} - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class PushCommand */ - -class CVC4_PUBLIC PopCommand : public Command { -public: - ~PopCommand() throw() {} - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class PopCommand */ - -class CVC4_PUBLIC DeclarationDefinitionCommand : public Command { -protected: - std::string d_symbol; -public: - DeclarationDefinitionCommand(const std::string& id) throw(); - ~DeclarationDefinitionCommand() throw() {} - virtual void invoke(SmtEngine* smtEngine) throw() = 0; - std::string getSymbol() const throw(); -};/* class DeclarationDefinitionCommand */ - -class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand { -protected: - Expr d_func; - Type d_type; - bool d_printInModel; - bool d_printInModelSetByUser; -public: - DeclareFunctionCommand(const std::string& id, Expr func, Type type) throw(); - ~DeclareFunctionCommand() throw() {} - Expr getFunction() const throw(); - Type getType() const throw(); - bool getPrintInModel() const throw(); - bool getPrintInModelSetByUser() const throw(); - void setPrintInModel( bool p ); - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class DeclareFunctionCommand */ - -class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand { -protected: - size_t d_arity; - Type d_type; -public: - DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw(); - ~DeclareTypeCommand() throw() {} - size_t getArity() const throw(); - Type getType() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class DeclareTypeCommand */ - -class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand { -protected: - std::vector d_params; - Type d_type; -public: - DefineTypeCommand(const std::string& id, Type t) throw(); - DefineTypeCommand(const std::string& id, const std::vector& params, Type t) throw(); - ~DefineTypeCommand() throw() {} - const std::vector& getParameters() const throw(); - Type getType() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class DefineTypeCommand */ - -class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand { -protected: - Expr d_func; - std::vector d_formals; - Expr d_formula; -public: - DefineFunctionCommand(const std::string& id, Expr func, Expr formula) throw(); - DefineFunctionCommand(const std::string& id, Expr func, - const std::vector& formals, Expr formula) throw(); - ~DefineFunctionCommand() throw() {} - Expr getFunction() const throw(); - const std::vector& getFormals() const throw(); - Expr getFormula() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class DefineFunctionCommand */ - -/** - * This differs from DefineFunctionCommand only in that it instructs - * the SmtEngine to "remember" this function for later retrieval with - * getAssignment(). Used for :named attributes in SMT-LIBv2. - */ -class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand { -public: - DefineNamedFunctionCommand(const std::string& id, Expr func, - const std::vector& formals, Expr formula) throw(); - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; -};/* class DefineNamedFunctionCommand */ - -/** - * The command when an attribute is set by a user. In SMT-LIBv2 this is done - * via the syntax (! expr :attr) - */ -class CVC4_PUBLIC SetUserAttributeCommand : public Command { -protected: - std::string d_attr; - Expr d_expr; - std::vector d_expr_values; - std::string d_str_value; -public: - SetUserAttributeCommand( const std::string& attr, Expr expr ) throw(); - SetUserAttributeCommand( const std::string& attr, Expr expr, std::vector& values ) throw(); - SetUserAttributeCommand( const std::string& attr, Expr expr, const std::string& value ) throw(); - ~SetUserAttributeCommand() throw() {} - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class SetUserAttributeCommand */ - -class CVC4_PUBLIC CheckSatCommand : public Command { -protected: - Expr d_expr; - Result d_result; - bool d_inUnsatCore; -public: - CheckSatCommand() throw(); - CheckSatCommand(const Expr& expr, bool inUnsatCore = true) throw(); - ~CheckSatCommand() throw() {} - Expr getExpr() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Result getResult() const throw(); - void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class CheckSatCommand */ - -class CVC4_PUBLIC QueryCommand : public Command { -protected: - Expr d_expr; - Result d_result; - bool d_inUnsatCore; -public: - QueryCommand(const Expr& e, bool inUnsatCore = true) throw(); - ~QueryCommand() throw() {} - Expr getExpr() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Result getResult() const throw(); - void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class QueryCommand */ - -// this is TRANSFORM in the CVC presentation language -class CVC4_PUBLIC SimplifyCommand : public Command { -protected: - Expr d_term; - Expr d_result; -public: - SimplifyCommand(Expr term) throw(); - ~SimplifyCommand() throw() {} - Expr getTerm() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Expr getResult() const throw(); - void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class SimplifyCommand */ - -class CVC4_PUBLIC ExpandDefinitionsCommand : public Command { -protected: - Expr d_term; - Expr d_result; -public: - ExpandDefinitionsCommand(Expr term) throw(); - ~ExpandDefinitionsCommand() throw() {} - Expr getTerm() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Expr getResult() const throw(); - void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class ExpandDefinitionsCommand */ - -class CVC4_PUBLIC GetValueCommand : public Command { -protected: - std::vector d_terms; - Expr d_result; -public: - GetValueCommand(Expr term) throw(); - GetValueCommand(const std::vector& terms) throw(); - ~GetValueCommand() throw() {} - const std::vector& getTerms() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Expr getResult() const throw(); - void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class GetValueCommand */ - -class CVC4_PUBLIC GetAssignmentCommand : public Command { -protected: - SExpr d_result; -public: - GetAssignmentCommand() throw(); - ~GetAssignmentCommand() throw() {} - void invoke(SmtEngine* smtEngine) throw(); - SExpr getResult() const throw(); - void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class GetAssignmentCommand */ - -class CVC4_PUBLIC GetModelCommand : public Command { -protected: - Model* d_result; - SmtEngine* d_smtEngine; -public: - GetModelCommand() throw(); - ~GetModelCommand() throw() {} - void invoke(SmtEngine* smtEngine) throw(); - // Model is private to the library -- for now - //Model* getResult() const throw(); - void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class GetModelCommand */ - -class CVC4_PUBLIC GetProofCommand : public Command { -protected: - Proof* d_result; - SmtEngine* d_smtEngine; -public: - GetProofCommand() throw(); - ~GetProofCommand() throw() {} - void invoke(SmtEngine* smtEngine) throw(); - Proof* getResult() const throw(); - void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class GetProofCommand */ - -class CVC4_PUBLIC GetInstantiationsCommand : public Command { -protected: - //Instantiations* d_result; - SmtEngine* d_smtEngine; -public: - GetInstantiationsCommand() throw(); - ~GetInstantiationsCommand() throw() {} - void invoke(SmtEngine* smtEngine) throw(); - //Instantiations* getResult() const throw(); - void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class GetInstantiationsCommand */ - -class CVC4_PUBLIC GetSynthSolutionCommand : public Command { -protected: - SmtEngine* d_smtEngine; -public: - GetSynthSolutionCommand() throw(); - ~GetSynthSolutionCommand() throw() {} - void invoke(SmtEngine* smtEngine) throw(); - void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class GetSynthSolutionCommand */ - -class CVC4_PUBLIC GetUnsatCoreCommand : public Command { -protected: - UnsatCore d_result; - std::map d_names; -public: - GetUnsatCoreCommand() throw(); - GetUnsatCoreCommand(const std::map& names) throw(); - ~GetUnsatCoreCommand() throw() {} - void invoke(SmtEngine* smtEngine) throw(); - void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); - const UnsatCore& getUnsatCore() const throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class GetUnsatCoreCommand */ - -class CVC4_PUBLIC GetAssertionsCommand : public Command { -protected: - std::string d_result; -public: - GetAssertionsCommand() throw(); - ~GetAssertionsCommand() throw() {} - void invoke(SmtEngine* smtEngine) throw(); - std::string getResult() const throw(); - void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class GetAssertionsCommand */ - -class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command { -protected: - BenchmarkStatus d_status; -public: - SetBenchmarkStatusCommand(BenchmarkStatus status) throw(); - ~SetBenchmarkStatusCommand() throw() {} - BenchmarkStatus getStatus() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class SetBenchmarkStatusCommand */ - -class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command { -protected: - std::string d_logic; -public: - SetBenchmarkLogicCommand(std::string logic) throw(); - ~SetBenchmarkLogicCommand() throw() {} - std::string getLogic() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class SetBenchmarkLogicCommand */ - -class CVC4_PUBLIC SetInfoCommand : public Command { -protected: - std::string d_flag; - SExpr d_sexpr; -public: - SetInfoCommand(std::string flag, const SExpr& sexpr) throw(); - ~SetInfoCommand() throw() {} - std::string getFlag() const throw(); - SExpr getSExpr() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class SetInfoCommand */ - -class CVC4_PUBLIC GetInfoCommand : public Command { -protected: - std::string d_flag; - std::string d_result; -public: - GetInfoCommand(std::string flag) throw(); - ~GetInfoCommand() throw() {} - std::string getFlag() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - std::string getResult() const throw(); - void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class GetInfoCommand */ - -class CVC4_PUBLIC SetOptionCommand : public Command { -protected: - std::string d_flag; - SExpr d_sexpr; -public: - SetOptionCommand(std::string flag, const SExpr& sexpr) throw(); - ~SetOptionCommand() throw() {} - std::string getFlag() const throw(); - SExpr getSExpr() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class SetOptionCommand */ - -class CVC4_PUBLIC GetOptionCommand : public Command { -protected: - std::string d_flag; - std::string d_result; -public: - GetOptionCommand(std::string flag) throw(); - ~GetOptionCommand() throw() {} - std::string getFlag() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - std::string getResult() const throw(); - void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class GetOptionCommand */ - -class CVC4_PUBLIC DatatypeDeclarationCommand : public Command { -private: - std::vector d_datatypes; -public: - DatatypeDeclarationCommand(const DatatypeType& datatype) throw(); - ~DatatypeDeclarationCommand() throw() {} - DatatypeDeclarationCommand(const std::vector& datatypes) throw(); - const std::vector& getDatatypes() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class DatatypeDeclarationCommand */ - -class CVC4_PUBLIC RewriteRuleCommand : public Command { -public: - typedef std::vector< std::vector< Expr > > Triggers; -protected: - typedef std::vector< Expr > VExpr; - VExpr d_vars; - VExpr d_guards; - Expr d_head; - Expr d_body; - Triggers d_triggers; -public: - RewriteRuleCommand(const std::vector& vars, - const std::vector& guards, - Expr head, - Expr body, - const Triggers& d_triggers) throw(); - RewriteRuleCommand(const std::vector& vars, - Expr head, - Expr body) throw(); - ~RewriteRuleCommand() throw() {} - const std::vector& getVars() const throw(); - const std::vector& getGuards() const throw(); - Expr getHead() const throw(); - Expr getBody() const throw(); - const Triggers& getTriggers() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class RewriteRuleCommand */ - -class CVC4_PUBLIC PropagateRuleCommand : public Command { -public: - typedef std::vector< std::vector< Expr > > Triggers; -protected: - typedef std::vector< Expr > VExpr; - VExpr d_vars; - VExpr d_guards; - VExpr d_heads; - Expr d_body; - Triggers d_triggers; - bool d_deduction; -public: - PropagateRuleCommand(const std::vector& vars, - const std::vector& guards, - const std::vector& heads, - Expr body, - const Triggers& d_triggers, - /* true if we want a deduction rule */ - bool d_deduction = false) throw(); - PropagateRuleCommand(const std::vector& vars, - const std::vector& heads, - Expr body, - bool d_deduction = false) throw(); - ~PropagateRuleCommand() throw() {} - const std::vector& getVars() const throw(); - const std::vector& getGuards() const throw(); - const std::vector& getHeads() const throw(); - Expr getBody() const throw(); - const Triggers& getTriggers() const throw(); - bool isDeduction() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class PropagateRuleCommand */ - -class CVC4_PUBLIC ResetCommand : public Command { -public: - ResetCommand() throw() {} - ~ResetCommand() throw() {} - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class ResetCommand */ - -class CVC4_PUBLIC ResetAssertionsCommand : public Command { -public: - ResetAssertionsCommand() throw() {} - ~ResetAssertionsCommand() throw() {} - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class ResetAssertionsCommand */ - -class CVC4_PUBLIC QuitCommand : public Command { -public: - QuitCommand() throw() {} - ~QuitCommand() throw() {} - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class QuitCommand */ - -class CVC4_PUBLIC CommentCommand : public Command { - std::string d_comment; -public: - CommentCommand(std::string comment) throw(); - ~CommentCommand() throw() {} - std::string getComment() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class CommentCommand */ - -class CVC4_PUBLIC CommandSequence : public Command { -private: - /** All the commands to be executed (in sequence) */ - std::vector d_commandSequence; - /** Next command to be executed */ - unsigned int d_index; -public: - CommandSequence() throw(); - ~CommandSequence() throw(); - - void addCommand(Command* cmd) throw(); - void clear() throw(); - - void invoke(SmtEngine* smtEngine) throw(); - void invoke(SmtEngine* smtEngine, std::ostream& out) throw(); - - typedef std::vector::iterator iterator; - typedef std::vector::const_iterator const_iterator; - - const_iterator begin() const throw(); - const_iterator end() const throw(); - - iterator begin() throw(); - iterator end() throw(); - - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class CommandSequence */ - -class CVC4_PUBLIC DeclarationSequence : public CommandSequence { -public: - ~DeclarationSequence() throw() {} -};/* class DeclarationSequence */ - -}/* CVC4 namespace */ - -#endif /* __CVC4__COMMAND_H */ diff --git a/src/smt_util/command.i b/src/smt_util/command.i deleted file mode 100644 index e4744c4f4..000000000 --- a/src/smt_util/command.i +++ /dev/null @@ -1,77 +0,0 @@ -%{ -#include "smt_util/command.h" - -#ifdef SWIGJAVA - -#include "bindings/java_iterator_adapter.h" -#include "bindings/java_stream_adapters.h" - -#endif /* SWIGJAVA */ -%} - -%ignore CVC4::operator<<(std::ostream&, const Command&) throw(); -%ignore CVC4::operator<<(std::ostream&, const Command*) throw(); -%ignore CVC4::operator<<(std::ostream&, const CommandStatus&) throw(); -%ignore CVC4::operator<<(std::ostream&, const CommandStatus*) throw(); -%ignore CVC4::operator<<(std::ostream&, BenchmarkStatus status) throw(); -%ignore CVC4::operator<<(std::ostream&, CommandPrintSuccess) throw(); - -%ignore CVC4::GetProofCommand; -%ignore CVC4::CommandPrintSuccess::Scope; - -#ifdef SWIGJAVA - -// Instead of CommandSequence::begin() and end(), create an -// iterator() method on the Java side that returns a Java-style -// Iterator. -%ignore CVC4::CommandSequence::begin(); -%ignore CVC4::CommandSequence::end(); -%ignore CVC4::CommandSequence::begin() const; -%ignore CVC4::CommandSequence::end() const; -%extend CVC4::CommandSequence { - CVC4::JavaIteratorAdapter iterator() { - return CVC4::JavaIteratorAdapter(*$self); - } -} - -// CommandSequence is "iterable" on the Java side -%typemap(javainterfaces) CVC4::CommandSequence "java.lang.Iterable"; - -// the JavaIteratorAdapter should not be public, and implements Iterator -%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter "class"; -%typemap(javainterfaces) CVC4::JavaIteratorAdapter "java.util.Iterator"; -// add some functions to the Java side (do it here because there's no way to do these in C++) -%typemap(javacode) CVC4::JavaIteratorAdapter " - public void remove() { - throw new java.lang.UnsupportedOperationException(); - } - - public edu.nyu.acsys.CVC4.Command next() { - if(hasNext()) { - return getNext(); - } else { - throw new java.util.NoSuchElementException(); - } - } -" -// getNext() just allows C++ iterator access from Java-side next(), make it private -%javamethodmodifiers CVC4::JavaIteratorAdapter::getNext() "private"; - -// map the types appropriately -%typemap(jni) CVC4::CommandSequence::const_iterator::value_type "jobject"; -%typemap(jtype) CVC4::CommandSequence::const_iterator::value_type "edu.nyu.acsys.CVC4.Command"; -%typemap(jstype) CVC4::CommandSequence::const_iterator::value_type "edu.nyu.acsys.CVC4.Command"; -%typemap(javaout) CVC4::CommandSequence::const_iterator::value_type { return $jnicall; } - -#endif /* SWIGJAVA */ - -%include "smt_util/command.h" - -#ifdef SWIGJAVA - -%include "bindings/java_iterator_adapter.h" -%include "bindings/java_stream_adapters.h" - -%template(JavaIteratorAdapter_CommandSequence) CVC4::JavaIteratorAdapter; - -#endif /* SWIGJAVA */ diff --git a/src/smt_util/dump.cpp b/src/smt_util/dump.cpp deleted file mode 100644 index 66cb6e3d1..000000000 --- a/src/smt_util/dump.cpp +++ /dev/null @@ -1,221 +0,0 @@ -/********************* */ -/*! \file dump.cpp - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Dump utility classes and functions - ** - ** Dump utility classes and functions. - **/ -#include "smt_util/dump.h" - -#include "base/output.h" - -namespace CVC4 { - -DumpC DumpChannel CVC4_PUBLIC; - -std::ostream& DumpC::setStream(std::ostream* os) { - ::CVC4::DumpOutChannel.setStream(os); - return *os; -} -std::ostream& DumpC::getStream() { return ::CVC4::DumpOutChannel.getStream(); } -std::ostream* DumpC::getStreamPointer() { return ::CVC4::DumpOutChannel.getStreamPointer(); } - - -void DumpC::setDumpFromString(const std::string& optarg) { -#ifdef CVC4_DUMPING - char* optargPtr = strdup(optarg.c_str()); - char* tokstr = optargPtr; - char* toksave; - while((optargPtr = strtok_r(tokstr, ",", &toksave)) != NULL) { - tokstr = NULL; - if(!strcmp(optargPtr, "benchmark")) { - } else if(!strcmp(optargPtr, "declarations")) { - } else if(!strcmp(optargPtr, "assertions")) { - Dump.on("assertions:post-everything"); - } else if(!strncmp(optargPtr, "assertions:", 11)) { - const char* p = optargPtr + 11; - if(!strncmp(p, "pre-", 4)) { - p += 4; - } else if(!strncmp(p, "post-", 5)) { - p += 5; - } else { - throw OptionException(std::string("don't know how to dump `") + - optargPtr + "'. Please consult --dump help."); - } - if(!strcmp(p, "everything")) { - } else if(!strcmp(p, "definition-expansion")) { - } else if(!strcmp(p, "boolean-terms")) { - } else if(!strcmp(p, "constrain-subtypes")) { - } else if(!strcmp(p, "substitution")) { - } else if(!strcmp(p, "strings-pp")) { - } else if(!strcmp(p, "skolem-quant")) { - } else if(!strcmp(p, "simplify")) { - } else if(!strcmp(p, "static-learning")) { - } else if(!strcmp(p, "ite-removal")) { - } else if(!strcmp(p, "repeat-simplify")) { - } else if(!strcmp(p, "rewrite-apply-to-const")) { - } else if(!strcmp(p, "theory-preprocessing")) { - } else if(!strcmp(p, "nonclausal")) { - } else if(!strcmp(p, "theorypp")) { - } else if(!strcmp(p, "itesimp")) { - } else if(!strcmp(p, "unconstrained")) { - } else if(!strcmp(p, "repeatsimp")) { - } else { - throw OptionException(std::string("don't know how to dump `") + - optargPtr + "'. Please consult --dump help."); - } - Dump.on("assertions"); - } else if(!strcmp(optargPtr, "skolems")) { - } else if(!strcmp(optargPtr, "clauses")) { - } else if(!strcmp(optargPtr, "t-conflicts") || - !strcmp(optargPtr, "t-lemmas") || - !strcmp(optargPtr, "t-explanations") || - !strcmp(optargPtr, "bv-rewrites") || - !strcmp(optargPtr, "theory::fullcheck")) { - // These are "non-state-dumping" modes. If state (SAT decisions, - // propagations, etc.) is dumped, it will interfere with the validity - // of these generated queries. - if(Dump.isOn("state")) { - throw OptionException(std::string("dump option `") + optargPtr + - "' conflicts with a previous, " - "state-dumping dump option. You cannot " - "mix stateful and non-stateful dumping modes; " - "see --dump help."); - } else { - Dump.on("no-permit-state"); - } - } else if(!strcmp(optargPtr, "state") || - !strcmp(optargPtr, "missed-t-conflicts") || - !strcmp(optargPtr, "t-propagations") || - !strcmp(optargPtr, "missed-t-propagations")) { - // These are "state-dumping" modes. If state (SAT decisions, - // propagations, etc.) is not dumped, it will interfere with the - // validity of these generated queries. - if(Dump.isOn("no-permit-state")) { - throw OptionException(std::string("dump option `") + optargPtr + - "' conflicts with a previous, " - "non-state-dumping dump option. You cannot " - "mix stateful and non-stateful dumping modes; " - "see --dump help."); - } else { - Dump.on("state"); - } - } else if(!strcmp(optargPtr, "help")) { - puts(s_dumpHelp.c_str()); - exit(1); - } else if(!strcmp(optargPtr, "bv-abstraction")) { - Dump.on("bv-abstraction"); - } else if(!strcmp(optargPtr, "bv-algebraic")) { - Dump.on("bv-algebraic"); - } else { - throw OptionException(std::string("unknown option for --dump: `") + - optargPtr + "'. Try --dump help."); - } - - Dump.on(optargPtr); - Dump.on("benchmark"); - if(strcmp(optargPtr, "benchmark")) { - Dump.on("declarations"); - if(strcmp(optargPtr, "declarations")) { - Dump.on("skolems"); - } - } - } - free(optargPtr); -#else /* CVC4_DUMPING */ - throw OptionException("The dumping feature was disabled in this build of CVC4."); -#endif /* CVC4_DUMPING */ -} - - -const std::string DumpC::s_dumpHelp = "\ -Dump modes currently supported by the --dump option:\n\ -\n\ -benchmark\n\ -+ Dump the benchmark structure (set-logic, push/pop, queries, etc.), but\n\ - does not include any declarations or assertions. Implied by all following\n\ - modes.\n\ -\n\ -declarations\n\ -+ Dump user declarations. Implied by all following modes.\n\ -\n\ -skolems\n\ -+ Dump internally-created skolem variable declarations. These can\n\ - arise from preprocessing simplifications, existential elimination,\n\ - and a number of other things. Implied by all following modes.\n\ -\n\ -assertions\n\ -+ Output the assertions after preprocessing and before clausification.\n\ - Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\ - where PASS is one of the preprocessing passes: definition-expansion\n\ - boolean-terms constrain-subtypes substitution strings-pp skolem-quant\n\ - simplify static-learning ite-removal repeat-simplify\n\ - rewrite-apply-to-const theory-preprocessing.\n\ - PASS can also be the special value \"everything\", in which case the\n\ - assertions are printed before any preprocessing (with\n\ - \"assertions:pre-everything\") or after all preprocessing completes\n\ - (with \"assertions:post-everything\").\n\ -\n\ -clauses\n\ -+ Do all the preprocessing outlined above, and dump the CNF-converted\n\ - output\n\ -\n\ -state\n\ -+ Dump all contextual assertions (e.g., SAT decisions, propagations..).\n\ - Implied by all \"stateful\" modes below and conflicts with all\n\ - non-stateful modes below.\n\ -\n\ -t-conflicts [non-stateful]\n\ -+ Output correctness queries for all theory conflicts\n\ -\n\ -missed-t-conflicts [stateful]\n\ -+ Output completeness queries for theory conflicts\n\ -\n\ -t-propagations [stateful]\n\ -+ Output correctness queries for all theory propagations\n\ -\n\ -missed-t-propagations [stateful]\n\ -+ Output completeness queries for theory propagations (LARGE and EXPENSIVE)\n\ -\n\ -t-lemmas [non-stateful]\n\ -+ Output correctness queries for all theory lemmas\n\ -\n\ -t-explanations [non-stateful]\n\ -+ Output correctness queries for all theory explanations\n\ -\n\ -bv-rewrites [non-stateful]\n\ -+ Output correctness queries for all bitvector rewrites\n\ -\n\ -bv-abstraction [non-stateful]\n\ -+ Output correctness queries for all bv abstraction \n\ -\n\ -bv-algebraic [non-stateful]\n\ -+ Output correctness queries for bv algebraic solver. \n\ -\n\ -theory::fullcheck [non-stateful]\n \ -+ Output completeness queries for all full-check effort-level theory checks\n\ -\n\ -Dump modes can be combined with multiple uses of --dump. Generally you want\n\ -one from the assertions category (either assertions or clauses), and\n\ -perhaps one or more stateful or non-stateful modes for checking correctness\n\ -and completeness of decision procedure implementations. Stateful modes dump\n\ -the contextual assertions made by the core solver (all decisions and\n\ -propagations as assertions; that affects the validity of the resulting\n\ -correctness and completeness queries, so of course stateful and non-stateful\n\ -modes cannot be mixed in the same run.\n\ -\n\ -The --output-language option controls the language used for dumping, and\n\ -this allows you to connect CVC4 to another solver implementation via a UNIX\n\ -pipe to perform on-line checking. The --dump-to option can be used to dump\n\ -to a file.\n\ -"; - -}/* CVC4 namespace */ diff --git a/src/smt_util/dump.h b/src/smt_util/dump.h deleted file mode 100644 index 19f9118e3..000000000 --- a/src/smt_util/dump.h +++ /dev/null @@ -1,123 +0,0 @@ -/********************* */ -/*! \file dump.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Dump utility classes and functions - ** - ** Dump utility classes and functions. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__DUMP_H -#define __CVC4__DUMP_H - -#include "base/output.h" -#include "smt_util/command.h" - -namespace CVC4 { - -class CVC4_PUBLIC CVC4dumpstream { - -#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) - std::ostream* d_os; -#endif /* CVC4_DUMPING && !CVC4_MUZZLE */ - -#ifdef CVC4_PORTFOLIO - CommandSequence* d_commands; -#endif /* CVC4_PORTFOLIO */ - -public: - CVC4dumpstream() throw() -#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && defined(CVC4_PORTFOLIO) - : d_os(NULL), d_commands(NULL) -#elif defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) - : d_os(NULL) -#elif defined(CVC4_PORTFOLIO) - : d_commands(NULL) -#endif /* CVC4_PORTFOLIO */ - { } - - CVC4dumpstream(std::ostream& os, CommandSequence& commands) throw() -#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && defined(CVC4_PORTFOLIO) - : d_os(&os), d_commands(&commands) -#elif defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) - : d_os(&os) -#elif defined(CVC4_PORTFOLIO) - : d_commands(&commands) -#endif /* CVC4_PORTFOLIO */ - { } - - CVC4dumpstream& operator<<(const Command& c) { -#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) - if(d_os != NULL) { - (*d_os) << c << std::endl; - } -#endif -#if defined(CVC4_PORTFOLIO) - if(d_commands != NULL) { - d_commands->addCommand(c.clone()); - } -#endif - return *this; - } -};/* class CVC4dumpstream */ - -/** The dump class */ -class CVC4_PUBLIC DumpC { - std::set d_tags; - CommandSequence d_commands; - - static const std::string s_dumpHelp; - -public: - CVC4dumpstream operator()(const char* tag) { - if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) { - return CVC4dumpstream(getStream(), d_commands); - } else { - return CVC4dumpstream(); - } - } - - CVC4dumpstream operator()(std::string tag) { - if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) { - return CVC4dumpstream(getStream(), d_commands); - } else { - return CVC4dumpstream(); - } - } - - void clear() { d_commands.clear(); } - const CommandSequence& getCommands() const { return d_commands; } - - bool on (const char* tag) { d_tags.insert(std::string(tag)); return true; } - bool on (std::string tag) { d_tags.insert(tag); return true; } - bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; } - bool off(std::string tag) { d_tags.erase (tag); return false; } - bool off() { d_tags.clear(); return false; } - - bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); } - bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); } - - std::ostream& setStream(std::ostream* os); - std::ostream& getStream(); - std::ostream* getStreamPointer(); - - void setDumpFromString(const std::string& optarg); -};/* class DumpC */ - -/** The dump singleton */ -extern DumpC DumpChannel CVC4_PUBLIC; - -#define Dump ::CVC4::DumpChannel - -}/* CVC4 namespace */ - -#endif /* __CVC4__DUMP_H */ diff --git a/src/smt_util/ite_removal.cpp b/src/smt_util/ite_removal.cpp deleted file mode 100644 index 0d1c7b61e..000000000 --- a/src/smt_util/ite_removal.cpp +++ /dev/null @@ -1,192 +0,0 @@ -/********************* */ -/*! \file ite_removal.cpp - ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: Tim King, Morgan Deters - ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds, Clark Barrett - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Removal of term ITEs - ** - ** Removal of term ITEs. - **/ -#include "smt_util/ite_removal.h" - -#include - -#include "proof/proof_manager.h" -#include "smt_util/command.h" -#include "theory/ite_utilities.h" - -using namespace CVC4; -using namespace std; - -namespace CVC4 { - -RemoveITE::RemoveITE(context::UserContext* u) - : d_iteCache(u) -{ - d_containsVisitor = new theory::ContainsTermITEVisitor(); -} - -RemoveITE::~RemoveITE(){ - delete d_containsVisitor; -} - -void RemoveITE::garbageCollect(){ - d_containsVisitor->garbageCollect(); -} - -theory::ContainsTermITEVisitor* RemoveITE::getContainsVisitor() { - return d_containsVisitor; -} - -size_t RemoveITE::collectedCacheSizes() const{ - return d_containsVisitor->cache_size() + d_iteCache.size(); -} - -void RemoveITE::run(std::vector& output, IteSkolemMap& iteSkolemMap, bool reportDeps) -{ - size_t n = output.size(); - for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) { - // Do this in two steps to avoid Node problems(?) - // Appears related to bug 512, splitting this into two lines - // fixes the bug on clang on Mac OS - Node itesRemoved = run(output[i], output, iteSkolemMap, false); - // In some calling contexts, not necessary to report dependence information. - if(reportDeps && options::unsatCores()) { - // new assertions have a dependence on the node - PROOF( ProofManager::currentPM()->addDependence(itesRemoved, output[i]); ) - while(n < output.size()) { - PROOF( ProofManager::currentPM()->addDependence(output[n], output[i]); ) - ++n; - } - } - output[i] = itesRemoved; - } -} - -bool RemoveITE::containsTermITE(TNode e) const { - return d_containsVisitor->containsTermITE(e); -} - -Node RemoveITE::run(TNode node, std::vector& output, - IteSkolemMap& iteSkolemMap, bool inQuant) { - // Current node - Debug("ite") << "removeITEs(" << node << ")" << endl; - - if(node.isVar() || node.isConst() || - (options::biasedITERemoval() && !containsTermITE(node))){ - return Node(node); - } - - // The result may be cached already - std::pair cacheKey(node, inQuant); - NodeManager *nodeManager = NodeManager::currentNM(); - ITECache::const_iterator i = d_iteCache.find(cacheKey); - if(i != d_iteCache.end()) { - Node cached = (*i).second; - Debug("ite") << "removeITEs: in-cache: " << cached << endl; - return cached.isNull() ? Node(node) : cached; - } - - // Remember that we're inside a quantifier - if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) { - inQuant = true; - } - - // If an ITE replace it - if(node.getKind() == kind::ITE) { - TypeNode nodeType = node.getType(); - if(!nodeType.isBoolean() && (!inQuant || !node.hasBoundVar())) { - Node skolem; - // Make the skolem to represent the ITE - skolem = nodeManager->mkSkolem("termITE", nodeType, "a variable introduced due to term-level ITE removal"); - - // The new assertion - Node newAssertion = - nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]), - skolem.eqNode(node[2])); - Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl; - - // Attach the skolem - d_iteCache.insert(cacheKey, skolem); - - // Remove ITEs from the new assertion, rewrite it and push it to the output - newAssertion = run(newAssertion, output, iteSkolemMap, inQuant); - - iteSkolemMap[skolem] = output.size(); - output.push_back(newAssertion); - - // The representation is now the skolem - return skolem; - } - } - - // If not an ITE, go deep - vector newChildren; - bool somethingChanged = false; - if(node.getMetaKind() == kind::metakind::PARAMETERIZED) { - newChildren.push_back(node.getOperator()); - } - // Remove the ITEs from the children - for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) { - Node newChild = run(*it, output, iteSkolemMap, inQuant); - somethingChanged |= (newChild != *it); - newChildren.push_back(newChild); - } - - // If changes, we rewrite - if(somethingChanged) { - Node cached = nodeManager->mkNode(node.getKind(), newChildren); - d_iteCache.insert(cacheKey, cached); - return cached; - } else { - d_iteCache.insert(cacheKey, Node::null()); - return node; - } -} - -Node RemoveITE::replace(TNode node, bool inQuant) const { - if(node.isVar() || node.isConst() || - (options::biasedITERemoval() && !containsTermITE(node))){ - return Node(node); - } - - // Check the cache - NodeManager *nodeManager = NodeManager::currentNM(); - ITECache::const_iterator i = d_iteCache.find(make_pair(node, inQuant)); - if(i != d_iteCache.end()) { - Node cached = (*i).second; - return cached.isNull() ? Node(node) : cached; - } - - // Remember that we're inside a quantifier - if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) { - inQuant = true; - } - - vector newChildren; - bool somethingChanged = false; - if(node.getMetaKind() == kind::metakind::PARAMETERIZED) { - newChildren.push_back(node.getOperator()); - } - // Replace in children - for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) { - Node newChild = replace(*it, inQuant); - somethingChanged |= (newChild != *it); - newChildren.push_back(newChild); - } - - // If changes, we rewrite - if(somethingChanged) { - return nodeManager->mkNode(node.getKind(), newChildren); - } else { - return node; - } -} - -}/* CVC4 namespace */ diff --git a/src/smt_util/ite_removal.h b/src/smt_util/ite_removal.h deleted file mode 100644 index 0cc0ea5d0..000000000 --- a/src/smt_util/ite_removal.h +++ /dev/null @@ -1,93 +0,0 @@ -/********************* */ -/*! \file ite_removal.h - ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: Kshitij Bansal, Tim King, Morgan Deters - ** Minor contributors (to current version): Clark Barrett - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Removal of term ITEs - ** - ** Removal of term ITEs. - **/ - -#include "cvc4_private.h" - -#pragma once - -#include - -#include "context/cdinsert_hashmap.h" -#include "context/context.h" -#include "expr/node.h" -#include "smt_util/dump.h" -#include "util/bool.h" -#include "util/hash.h" - -namespace CVC4 { - -namespace theory { - class ContainsTermITEVisitor; -}/* CVC4::theory namespace */ - -typedef std::hash_map IteSkolemMap; - -class RemoveITE { - typedef context::CDInsertHashMap< std::pair, Node, PairHashFunction > ITECache; - ITECache d_iteCache; - - -public: - - RemoveITE(context::UserContext* u); - ~RemoveITE(); - - /** - * Removes the ITE nodes by introducing skolem variables. All - * additional assertions are pushed into assertions. iteSkolemMap - * contains a map from introduced skolem variables to the index in - * assertions containing the new Boolean ite created in conjunction - * with that skolem variable. - * - * With reportDeps true, report reasoning dependences to the proof - * manager (for unsat cores). - */ - void run(std::vector& assertions, IteSkolemMap& iteSkolemMap, bool reportDeps = false); - - /** - * Removes the ITE from the node by introducing skolem - * variables. All additional assertions are pushed into - * assertions. iteSkolemMap contains a map from introduced skolem - * variables to the index in assertions containing the new Boolean - * ite created in conjunction with that skolem variable. - */ - Node run(TNode node, std::vector& additionalAssertions, - IteSkolemMap& iteSkolemMap, bool inQuant); - - /** - * Substitute under node using pre-existing cache. Do not remove - * any ITEs not seen during previous runs. - */ - Node replace(TNode node, bool inQuant = false) const; - - /** Returns true if e contains a term ite. */ - bool containsTermITE(TNode e) const; - - /** Returns the collected size of the caches. */ - size_t collectedCacheSizes() const; - - /** Garbage collects non-context dependent data-structures. */ - void garbageCollect(); - - /** Return the RemoveITE's containsVisitor. */ - theory::ContainsTermITEVisitor* getContainsVisitor(); - -private: - theory::ContainsTermITEVisitor* d_containsVisitor; - -};/* class RemoveTTE */ - -}/* CVC4 namespace */ diff --git a/src/smt_util/model.cpp b/src/smt_util/model.cpp deleted file mode 100644 index ddac7e263..000000000 --- a/src/smt_util/model.cpp +++ /dev/null @@ -1,55 +0,0 @@ -/********************* */ -/*! \file model.cpp - ** \verbatim - ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief implementation of Model class - **/ - -#include "smt_util/model.h" - -#include - -#include "expr/expr_iomanip.h" -#include "options/base_options.h" -#include "printer/printer.h" -#include "smt/command_list.h" -#include "smt/smt_engine_scope.h" -#include "smt_util/command.h" - -using namespace std; - -namespace CVC4 { - -std::ostream& operator<<(std::ostream& out, const Model& m) { - smt::SmtScope smts(&m.d_smt); - expr::ExprDag::Scope scope(out, false); - Printer::getPrinter(options::outputLanguage())->toStream(out, m); - return out; -} - -Model::Model() : - d_smt(*smt::currentSmtEngine()) { -} - -size_t Model::getNumCommands() const { - return d_smt.d_modelCommands->size() + d_smt.d_modelGlobalCommands.size(); -} - -const Command* Model::getCommand(size_t i) const { - Assert(i < getNumCommands()); - // index the global commands first, then the locals - if(i < d_smt.d_modelGlobalCommands.size()) { - return d_smt.d_modelGlobalCommands[i]; - } else { - return (*d_smt.d_modelCommands)[i - d_smt.d_modelGlobalCommands.size()]; - } -} - -}/* CVC4 namespace */ diff --git a/src/smt_util/model.h b/src/smt_util/model.h deleted file mode 100644 index 33a9312a6..000000000 --- a/src/smt_util/model.h +++ /dev/null @@ -1,78 +0,0 @@ -/********************* */ -/*! \file model.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Andrew Reynolds - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Model class - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__MODEL_H -#define __CVC4__MODEL_H - -#include -#include - -#include "expr/expr.h" -#include "util/cardinality.h" - -namespace CVC4 { - -class Command; -class SmtEngine; -class Model; - -std::ostream& operator<<(std::ostream&, const Model&); - -class Model { - friend std::ostream& operator<<(std::ostream&, const Model&); - friend class SmtEngine; - - /** the input name (file name, etc.) this model is associated to */ - std::string d_inputName; - -protected: - /** The SmtEngine we're associated with */ - SmtEngine& d_smt; - - /** construct the base class; users cannot do this, only CVC4 internals */ - Model(); - -public: - /** virtual destructor */ - virtual ~Model() { } - /** get number of commands to report */ - size_t getNumCommands() const; - /** get command */ - const Command* getCommand(size_t i) const; - /** get the smt engine that this model is hooked up to */ - SmtEngine* getSmtEngine() { return &d_smt; } - /** get the smt engine (as a pointer-to-const) that this model is hooked up to */ - const SmtEngine* getSmtEngine() const { return &d_smt; } - /** get the input name (file name, etc.) this model is associated to */ - std::string getInputName() const { return d_inputName; } - -public: - /** get value for expression */ - virtual Expr getValue(Expr expr) const = 0; - /** get cardinality for sort */ - virtual Cardinality getCardinality(Type t) const = 0; -};/* class Model */ - -class ModelBuilder { -public: - ModelBuilder() { } - virtual ~ModelBuilder() { } - virtual void buildModel(Model* m, bool fullModel) = 0; -};/* class ModelBuilder */ - -}/* CVC4 namespace */ - -#endif /* __CVC4__MODEL_H */ diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index f9e036aa3..8f1ba5fca 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -21,9 +21,9 @@ #include "expr/kind.h" #include "options/arrays_options.h" #include "options/smt_options.h" +#include "smt/command.h" #include "smt/logic_exception.h" #include "smt/smt_statistics_registry.h" -#include "smt_util/command.h" #include "theory/rewriter.h" #include "theory/theory_model.h" #include "proof/theory_proof.h" diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp index 842ff60b1..27ca61cfd 100644 --- a/src/theory/bv/abstraction.cpp +++ b/src/theory/bv/abstraction.cpp @@ -15,7 +15,7 @@ #include "theory/bv/abstraction.h" #include "options/bv_options.h" -#include "smt_util/dump.h" +#include "smt/dump.h" #include "smt/smt_statistics_registry.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index af080a970..9f3c34e8e 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -22,7 +22,7 @@ #include #include "context/context.h" -#include "smt_util/command.h" +#include "smt/command.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory.h" #include "util/statistics_registry.h" diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 3ff0cda92..b02c9a740 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -14,7 +14,7 @@ #include "theory/quantifiers/ceg_instantiator.h" #include "options/quantifiers_options.h" -#include "smt_util/ite_removal.h" +#include "smt/ite_removal.h" #include "theory/arith/partial_model.h" #include "theory/arith/theory_arith.h" #include "theory/arith/theory_arith_private.h" diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 5790fc34a..d5ef2e290 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -14,7 +14,7 @@ #include "theory/quantifiers/inst_strategy_cbqi.h" #include "options/quantifiers_options.h" -#include "smt_util/ite_removal.h" +#include "smt/ite_removal.h" #include "theory/arith/partial_model.h" #include "theory/arith/theory_arith.h" #include "theory/arith/theory_arith_private.h" diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index c0a892926..529e69e82 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -22,7 +22,7 @@ #include "options/strings_options.h" #include "smt/logic_exception.h" #include "smt/smt_statistics_registry.h" -#include "smt_util/command.h" +#include "smt/command.h" #include "theory/rewriter.h" #include "theory/strings/theory_strings_rewriter.h" #include "theory/strings/type_enumerator.h" diff --git a/src/theory/theory.h b/src/theory/theory.h index 9849dd0b9..c988c9120 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -31,9 +31,9 @@ #include "options/options.h" #include "options/theory_options.h" #include "options/theoryof_mode.h" +#include "smt/command.h" +#include "smt/dump.h" #include "smt/logic_request.h" -#include "smt_util/command.h" -#include "smt_util/dump.h" #include "theory/logic_info.h" #include "theory/output_channel.h" #include "theory/valuation.h" diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 60716146e..45f7506de 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -28,8 +28,8 @@ #include "options/quantifiers_options.h" #include "proof/proof_manager.h" #include "proof/theory_proof.h" +#include "smt/ite_removal.h" #include "smt/logic_exception.h" -#include "smt_util/ite_removal.h" #include "smt_util/lemma_output_channel.h" #include "smt_util/node_visitor.h" #include "theory/arith/arith_ite_utils.h" diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index cdd05c096..886aa6863 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -30,7 +30,7 @@ #include "options/options.h" #include "options/smt_options.h" #include "prop/prop_engine.h" -#include "smt_util/command.h" +#include "smt/command.h" #include "smt_util/lemma_channels.h" #include "theory/atom_requests.h" #include "theory/bv/bv_to_bool.h" diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index e609bf703..0c2f109bb 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -17,7 +17,7 @@ #ifndef __CVC4__THEORY__THEORY_MODEL_H #define __CVC4__THEORY__THEORY_MODEL_H -#include "smt_util/model.h" +#include "smt/model.h" #include "theory/uf/equality_engine.h" #include "theory/rep_set.h" #include "theory/substitutions.h" diff --git a/test/system/ouroborous.cpp b/test/system/ouroborous.cpp index d27ebd9b3..1ceb7319f 100644 --- a/test/system/ouroborous.cpp +++ b/test/system/ouroborous.cpp @@ -33,7 +33,7 @@ #include "options/set_language.h" #include "parser/parser.h" #include "parser/parser_builder.h" -#include "smt_util/command.h" +#include "smt/command.h" using namespace CVC4; using namespace CVC4::parser; diff --git a/test/system/smt2_compliance.cpp b/test/system/smt2_compliance.cpp index bc976685e..68fbb9f59 100644 --- a/test/system/smt2_compliance.cpp +++ b/test/system/smt2_compliance.cpp @@ -23,8 +23,8 @@ #include "options/set_language.h" #include "parser/parser.h" #include "parser/parser_builder.h" +#include "smt/command.h" #include "smt/smt_engine.h" -#include "smt_util/command.h" using namespace CVC4; using namespace CVC4::parser; diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 6ecc76c2b..3c4171925 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -28,7 +28,7 @@ #include "parser/parser.h" #include "parser/parser_builder.h" #include "parser/smt2/smt2.h" -#include "smt_util/command.h" +#include "smt/command.h" using namespace CVC4; diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h index 029c95ec9..42d240668 100644 --- a/test/unit/parser/parser_builder_black.h +++ b/test/unit/parser/parser_builder_black.h @@ -28,7 +28,7 @@ #include "options/language.h" #include "parser/parser.h" #include "parser/parser_builder.h" -#include "smt_util/command.h" +#include "smt/command.h" typedef __gnu_cxx::stdio_filebuf filebuf_gnu;