diff options
74 files changed, 99 insertions, 93 deletions
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<JavaInputStreamAdapter*> 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 <cvc4/options/options.h> #include <cvc4/parser/parser.h> #include <cvc4/parser/parser_builder.h> +#include <cvc4/smt/command.h> #include <cvc4/smt/smt_engine.h> -#include <cvc4/smt_util/command.h> #include <cvc4/util/integer.h> #include <cvc4/util/rational.h> 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 <string> #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 <utility> #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 <stdint.h> -#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 <ext/hash_set> #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_util/command.cpp b/src/smt/command.cpp index 83298836f..d6ec0769a 100644 --- a/src/smt_util/command.cpp +++ b/src/smt/command.cpp @@ -14,7 +14,7 @@ ** Implementation of command objects. **/ -#include "smt_util/command.h" +#include "smt/command.h" #include <exception> #include <iostream> @@ -30,10 +30,10 @@ #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 "smt_util/dump.h" -#include "smt_util/model.h" #include "util/sexpr.h" using namespace std; diff --git a/src/smt_util/command.h b/src/smt/command.h index 248e69b0e..248e69b0e 100644 --- a/src/smt_util/command.h +++ b/src/smt/command.h diff --git a/src/smt_util/command.i b/src/smt/command.i index e4744c4f4..0c050201d 100644 --- a/src/smt_util/command.i +++ b/src/smt/command.i @@ -1,5 +1,5 @@ %{ -#include "smt_util/command.h" +#include "smt/command.h" #ifdef SWIGJAVA @@ -65,7 +65,7 @@ #endif /* SWIGJAVA */ -%include "smt_util/command.h" +%include "smt/command.h" #ifdef 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_util/dump.cpp b/src/smt/dump.cpp index 66cb6e3d1..3b9ec3273 100644 --- a/src/smt_util/dump.cpp +++ b/src/smt/dump.cpp @@ -13,7 +13,7 @@ ** ** Dump utility classes and functions. **/ -#include "smt_util/dump.h" +#include "smt/dump.h" #include "base/output.h" diff --git a/src/smt_util/dump.h b/src/smt/dump.h index 19f9118e3..a6fa899da 100644 --- a/src/smt_util/dump.h +++ b/src/smt/dump.h @@ -20,7 +20,7 @@ #define __CVC4__DUMP_H #include "base/output.h" -#include "smt_util/command.h" +#include "smt/command.h" namespace CVC4 { diff --git a/src/smt_util/ite_removal.cpp b/src/smt/ite_removal.cpp index 0d1c7b61e..c0c6ed02b 100644 --- a/src/smt_util/ite_removal.cpp +++ b/src/smt/ite_removal.cpp @@ -13,15 +13,13 @@ ** ** Removal of term ITEs. **/ -#include "smt_util/ite_removal.h" +#include "smt/ite_removal.h" #include <vector> #include "proof/proof_manager.h" -#include "smt_util/command.h" #include "theory/ite_utilities.h" -using namespace CVC4; using namespace std; namespace CVC4 { diff --git a/src/smt_util/ite_removal.h b/src/smt/ite_removal.h index 0cc0ea5d0..d6d820f89 100644 --- a/src/smt_util/ite_removal.h +++ b/src/smt/ite_removal.h @@ -23,7 +23,7 @@ #include "context/cdinsert_hashmap.h" #include "context/context.h" #include "expr/node.h" -#include "smt_util/dump.h" +#include "smt/dump.h" #include "util/bool.h" #include "util/hash.h" diff --git a/src/smt_util/model.cpp b/src/smt/model.cpp index ddac7e263..15ecbadfb 100644 --- a/src/smt_util/model.cpp +++ b/src/smt/model.cpp @@ -12,16 +12,16 @@ ** \brief implementation of Model class **/ -#include "smt_util/model.h" +#include "smt/model.h" #include <vector> #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" -#include "smt_util/command.h" using namespace std; diff --git a/src/smt_util/model.h b/src/smt/model.h index 33a9312a6..33a9312a6 100644 --- a/src/smt_util/model.h +++ b/src/smt/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/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 <sstream> #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<char> filebuf_gnu; |