From 90e3b73fbd1b2eb262a7a7e2e72d701c8f9e3600 Mon Sep 17 00:00:00 2001 From: Tim King Date: Mon, 14 Dec 2015 18:51:40 -0800 Subject: [PATCH] Refactoring Options Handler & Library Cycle Breaking What to Know As a User: A number of files have moved. Users that include files in the public API in more refined ways than using #include should consult which files have moved. Note though that some files may move again after being cleaned up. A number of small tweaks have been made to the swig interfaces that may cause issues. Please file bug reports for any problems. The Problem: The build order of CVC4 used to be [roughly] specified as: options < expr < util < libcvc4 < parsers < main Each of these had their own directories and their own Makefile.am files. With the exception of the util/ directory, each of the subdirectories built exactly one convenience library. The util/ directory additionally built a statistics library. While the order above was partially correct, the build order was more complicated as options/Makefile.am executed building the sources for expr/Makefile.am as part of its BUILT_SOURCES phase. This options/Makefile.am also build the options/h and options.cpp files in other directories. There were cyclical library dependencies between the first four above libraries. All of these aspects combined to make options extremely brittle and hard to develop. Maintaining these between clang versus gcc, and bazel versus autotools has become increasing unpredictable. The Solution: To address these cyclic build problems, I am simplifying the build process. Here are the main things that have to happen: 1. util/ will be split into 3 separate directories: base, util, and smt_util. Each will have their own library and Makefile.am file. 2. Dependencies for options/ will be moved into options/. If a type appears as an option, this file will be moved into options. 3. All of the old options_handlers.h files have been refactored. 4. Some files have moved from util into expr/ to resolve cycles. Some of these moves are temporary. 5. I am removing the libstatistics library. The constraints that the CVC4 build system will eventually satisfy are: - The include order for both the .h and .cpp files for a directory must respect the order libraries are built. For example, a file in options/ cannot include from the expr/ directory. This includes built source files such as those coming from */kinds files and */options files. - The types definitions must also respect the build order. Forward type declarations will be allowed in exceptional, justified cases. - The Makefile.am for a directory cannot generate a file outside of the directory it controls. (Or call another Makefile.am except through subdirectory calls.) - One library per Makefile.am. - No extra copies of libraries will be built for the purpose of distinguishing between external and internal visibility in libraries for building parser/ or main/ libraries and binaries. Any function used by parser/ and main/ will be labeled with CVC4_PUBLIC and be in a public API. (AFAICT, libstatistics was being built exactly to skirt this.) The build order of CVC4 can now be [roughly] specified as base < options < util < expr < smt_util < libcvc4 < parsers < main The distinction between "base < options < util < expr" are currently clean. The relationship between expr and the subsequent directories/libraries are not yet clean. More details about the directories: base/ The new directory base/ contains the shared utilities that are absolutely crucial to starting cvc4. The list currently includes just: cvc4_assert.{h,cpp}, output.{h,cpp}, exception.{h,cpp}, and tls.{h, h.in, cpp}. These are things that are required everywhere. options/ The options/ directory is self contained. - It contains all of the enums that appear as options. This includes things like theory/bv/bitblast_mode.h . - There are exactly 4 classes that handled currently using forward declarations currently to this: LogicInfo, LemmaInputChannel, LemmaOutputChannel, and CommandSequence. These will all be removed from options. - Functionality of the options_handlers.h files has been moved into smt/smt_options_handler.h. The options library itself only uses an interface class defined in options/options_handler_interface.h. We are now using virtual dispatch to avoid using inlined functions as was previously done. - The */options_handlers.h files have been removed. - The generated smt/smt_options.cpp file has been be replaced by pushing the functionality that was generated into: options/options_handler_{get,set}_option_template.cpp . The non-generated functionality was moved into smt_engine.cpp. - All of the options files have been moved from their directories into options/. This means includes like theory/arith/options.h have changed to change to options/arith_options.h . util/ The util/ directory continues to contain core utility classes that may be used [almost] everywhere. The exception is that these are not used by options/ or base/. This includes things like rational and integer. These may not use anything in expr/ or libcvc4. A number of files have been moved out of this directory as they have cyclic dependencies graph with exprs and types. The build process up to this directory is currently clean. expr/ The expr/ directory continues to be the home of expressions. The major change is files moving from util/ moving into expr/. The reason for this is that these files form a cycle with files in expr/. - An example is datatype.h. This includes "expr/expr.h", "expr/type.h" while "expr/command.h" includes datatype.h. - Another example is predicate.h. This uses expr.h and is also declared in a kinds file and thus appears in kinds.h. - The rule of thumb is if expr/ pulls it in it needs to be independent of expr/, in which case it is in util/, or it is not, in which case it is pulled into expr/. - Some files do not have a strong justification currently. Result, ResourceManager and SExpr can be moved back into util/ once the iostream manipulation routines are refactored out of the Node and Expr classes. - Note the kinds files are expected to remain in the theory/ directories. These are only read in order to build sources. - This directory is not yet clean. It contains forward references into libcvc4 such as the printer. It also makes some classes used by main/ and parser CVC4_PUBLIC. smt_util/ The smt_util/ directory contains those utility classes which require exprs, but expr/ does not require them. These are mostly utilities for working with expressions and nodes. Examples include ite_removal.h, LemmaInputChannel and LemmaOutputChannel. What is up next: - A number of new #warning "TODO: ..." items have been scattered throughout the code as reminders to myself. Help with these issues is welcomed. - The expr/ directory needs to be cleaned up in a similar to options/. Before this happens statistics needs to be cleaned up. --- .travis.yml | 10 +- AUTHORS | 2 +- configure.ac | 4 +- contrib/depgraph | 2 +- contrib/new-theory | 23 +- contrib/new-theory.awk | 17 + .../options => optionsskel/DIR_options} | 2 +- contrib/theoryskel/options_handlers.h | 14 - examples/api/datatypes.cpp | 2 +- examples/hashsmt/sha1_collision.cpp | 2 +- examples/hashsmt/sha1_inversion.cpp | 2 +- examples/nra-translate/normalize.cpp | 11 +- examples/nra-translate/smt2info.cpp | 9 +- examples/nra-translate/smt2todreal.cpp | 10 +- examples/nra-translate/smt2toisat.cpp | 11 +- examples/nra-translate/smt2tomathematica.cpp | 11 +- examples/nra-translate/smt2toqepcad.cpp | 10 +- examples/nra-translate/smt2toredlog.cpp | 11 +- examples/sets-translate/sets_translate.cpp | 13 +- examples/translator.cpp | 17 +- src/Makefile.am | 96 +- src/base/Makefile.am | 40 + src/{util => base}/cvc4_assert.cpp | 3 +- src/{util => base}/cvc4_assert.h | 8 +- src/{util => base}/exception.cpp | 11 +- src/{util => base}/exception.h | 2 +- src/{util => base}/exception.i | 4 +- src/base/lemma_input_channel_forward.h | 30 + src/base/lemma_output_channel_forward.h | 35 + src/{smt => base}/modal_exception.h | 2 +- src/base/modal_exception.i | 7 + src/{util => base}/output.cpp | 2 +- src/{util => base}/output.h | 0 src/{util => base}/tls.h.in | 0 src/bindings/swig.h | 4 +- src/compat/cvc3_compat.cpp | 45 +- src/compat/cvc3_compat.h | 22 +- src/{util => context}/backtrackable.h | 0 src/context/cdchunk_list.h | 3 +- src/context/cdhashmap.h | 6 +- src/context/cdhashset.h | 3 +- src/context/cdinsert_hashmap.h | 15 +- src/context/cdlist.h | 5 +- src/context/cdo.h | 3 +- src/context/cdtrail_hashmap.h | 13 +- src/context/cdvector.h | 6 +- src/context/context.cpp | 3 +- src/context/context.h | 4 +- src/context/context_mm.cpp | 5 +- src/cvc4.i | 106 +- .../decision_attributes.h | 16 +- src/decision/decision_engine.cpp | 11 +- src/decision/decision_engine.h | 6 +- src/decision/decision_strategy.h | 2 +- src/decision/justification_heuristic.cpp | 21 +- src/decision/justification_heuristic.h | 9 +- src/decision/options_handlers.h | 76 - src/expr/Makefile.am | 101 +- src/{util => expr}/array.h | 0 src/expr/array.i | 5 + src/{util => expr}/array_store_all.cpp | 3 +- src/{util => expr}/array_store_all.h | 0 src/{util => expr}/array_store_all.i | 4 +- src/{util => expr}/ascription_type.h | 0 src/{util => expr}/ascription_type.i | 4 +- src/expr/attribute.cpp | 5 +- src/{util => expr}/chain.h | 0 src/{util => expr}/chain.i | 4 +- src/{util => expr}/datatype.cpp | 12 +- src/{util => expr}/datatype.h | 3 +- src/{util => expr}/datatype.i | 4 +- src/{util => expr}/emptyset.cpp | 5 +- src/{util => expr}/emptyset.h | 0 src/{util => expr}/emptyset.i | 4 +- src/expr/expr_manager_template.cpp | 9 +- src/expr/expr_manager_template.h | 7 +- src/expr/expr_template.cpp | 2 +- src/expr/expr_template.h | 15 +- src/expr/kind_template.h | 2 +- src/{util => expr}/matcher.h | 3 +- src/expr/metakind_template.h | 2 +- src/expr/node.cpp | 7 +- src/expr/node.h | 8 +- src/expr/node_builder.h | 7 +- src/expr/node_manager.cpp | 25 +- src/expr/node_manager.h | 13 +- src/expr/node_self_iterator.h | 2 +- src/expr/node_value.cpp | 9 +- src/expr/node_value.h | 9 +- src/expr/options_handlers.h | 69 - src/expr/pickle_data.cpp | 2 +- src/expr/pickler.cpp | 4 +- src/expr/pickler.h | 2 +- src/{util => expr}/predicate.cpp | 5 +- src/{util => expr}/predicate.h | 4 +- src/{util => expr}/predicate.i | 4 +- src/{util => expr}/record.cpp | 4 +- src/{util => expr}/record.h | 1 + src/{util => expr}/record.i | 4 +- src/{util => expr}/resource_manager.cpp | 16 +- src/{util => expr}/resource_manager.h | 2 +- src/expr/resource_manager.i | 5 + src/{util => expr}/result.cpp | 100 +- src/{util => expr}/result.h | 29 +- src/{util => expr}/result.i | 4 +- src/expr/sexpr.cpp | 233 +++ src/{util => expr}/sexpr.h | 233 ++- src/{util => expr}/sexpr.i | 4 +- src/{util => expr}/statistics.cpp | 7 +- src/{util => expr}/statistics.h | 6 +- src/{util => expr}/statistics.i | 4 +- src/{util => expr}/statistics_registry.cpp | 8 +- src/{util => expr}/statistics_registry.h | 49 +- src/expr/type.cpp | 4 +- src/expr/type_node.h | 2 +- src/expr/type_properties_template.h | 8 +- src/{util => expr}/uninterpreted_constant.cpp | 3 +- src/{util => expr}/uninterpreted_constant.h | 0 src/{util => expr}/uninterpreted_constant.i | 4 +- src/include/cvc4.h | 19 +- src/main/Makefile.am | 4 - src/main/command_executor.cpp | 20 +- src/main/command_executor.h | 12 +- src/main/command_executor_portfolio.cpp | 25 +- src/main/driver_unified.cpp | 48 +- src/main/interactive_shell.cpp | 44 +- src/main/interactive_shell.h | 4 +- src/main/main.cpp | 19 +- src/main/main.h | 12 +- src/main/options_handlers.h | 115 -- src/main/portfolio.cpp | 9 +- src/main/portfolio.h | 6 +- src/main/portfolio_util.cpp | 18 +- src/main/portfolio_util.h | 8 +- src/main/util.cpp | 13 +- src/options/Makefile.am | 495 +++-- .../arith_heuristic_pivot_rule.cpp | 3 +- .../arith_heuristic_pivot_rule.h | 4 +- .../arith/options => options/arith_options} | 8 +- .../arith_propagation_mode.cpp | 3 +- .../arith_propagation_mode.h | 4 +- .../arith_unate_lemma_mode.cpp | 3 +- .../arith_unate_lemma_mode.h | 0 .../arrays/options => options/arrays_options} | 2 +- src/options/base_handlers.h | 85 + src/options/base_options | 10 +- src/options/base_options_handlers.h | 241 --- .../boolean_term_conversion_mode.cpp | 3 +- .../boolean_term_conversion_mode.h | 0 .../options => options/booleans_options} | 4 +- .../options => options/builtin_options} | 2 +- .../bv_bitblast_mode.cpp} | 7 +- .../bv_bitblast_mode.h} | 0 src/{theory/bv/options => options/bv_options} | 10 +- .../options => options/datatypes_options} | 2 +- src/{decision => options}/decision_mode.cpp | 3 +- src/{decision => options}/decision_mode.h | 0 .../options => options/decision_options} | 8 +- .../decision_weight.h} | 23 +- src/{util => options}/didyoumean.cpp | 11 +- src/{util => options}/didyoumean.h | 4 +- src/{util => options}/didyoumean_test.cpp | 1 + src/{expr/options => options/expr_options} | 8 +- src/{theory/fp/options => options/fp_options} | 2 +- .../idl/options => options/idl_options} | 2 +- src/{util => options}/language.cpp | 2 +- src/{util => options}/language.h | 2 +- src/{util => options}/language.i | 4 +- src/options/logic_info_forward.h | 9 + src/{main/options => options/main_options} | 10 +- src/options/mkoptions | 106 +- src/options/option_exception.h | 2 +- src/options/options.h | 34 +- .../options_handler_get_option_template.cpp | 54 + src/options/options_handler_interface.cpp | 362 ++++ src/options/options_handler_interface.h | 275 +++ src/options/options_handler_interface.i | 5 + .../options_handler_set_option_template.cpp | 53 + src/options/options_template.cpp | 78 +- .../options => options/parser_options} | 2 +- .../modes.cpp => options/printer_modes.cpp} | 4 +- .../modes.h => options/printer_modes.h} | 2 +- src/options/printer_options | 14 + src/{proof/options => options/proof_options} | 2 +- src/{prop/options => options/prop_options} | 2 +- .../quantifiers_modes.cpp} | 5 +- .../modes.h => options/quantifiers_modes.h} | 60 +- .../options => options/quantifiers_options} | 28 +- .../sets/options => options/sets_options} | 2 +- src/{smt => options}/simplification_mode.cpp | 2 +- src/{smt => options}/simplification_mode.h | 0 src/{smt/options => options/smt_options} | 48 +- .../options => options/strings_options} | 8 +- src/options/theory_options | 15 + src/options/theoryof_mode.cpp | 21 + src/{theory => options}/theoryof_mode.h | 14 +- src/{theory/uf/options => options/uf_options} | 4 +- src/options/ufss_mode.h | 40 + src/parser/antlr_input.cpp | 15 +- src/parser/antlr_input.h | 6 +- src/parser/antlr_line_buffered_input.cpp | 2 +- src/parser/antlr_tracing.h | 3 +- src/parser/cvc/Cvc.g | 17 +- src/parser/input.cpp | 5 +- src/parser/input.h | 4 +- src/parser/memory_mapped_input_buffer.cpp | 2 +- src/parser/parser.cpp | 24 +- src/parser/parser_builder.cpp | 11 +- src/parser/parser_builder.h | 3 +- src/parser/parser_exception.h | 2 +- src/parser/smt1/Smt1.g | 9 +- src/parser/smt1/smt1.cpp | 2 +- src/parser/smt2/Smt2.g | 26 +- src/parser/smt2/smt2.cpp | 8 +- src/parser/tptp/Tptp.g | 13 +- src/parser/tptp/tptp.h | 11 +- src/printer/ast/ast_printer.cpp | 19 +- src/printer/cvc/cvc_printer.cpp | 41 +- src/printer/options | 14 - src/printer/options_handlers.h | 77 - src/printer/printer.cpp | 95 +- src/printer/printer.h | 91 +- src/printer/smt1/smt1_printer.cpp | 16 +- src/printer/smt2/smt2_printer.cpp | 102 +- src/printer/smt2/smt2_printer.h | 1 - src/printer/tptp/tptp_printer.cpp | 30 +- src/printer/tptp/tptp_printer.h | 2 - src/proof/proof.h | 2 +- src/proof/proof_manager.cpp | 17 +- src/{util => proof}/unsat_core.cpp | 7 +- src/{util => proof}/unsat_core.h | 0 src/{util => proof}/unsat_core.i | 4 +- src/prop/bvminisat/core/Solver.cc | 15 +- src/prop/bvminisat/simp/SimpSolver.cc | 7 +- src/prop/bvminisat/simp/SimpSolver.h | 6 +- src/prop/cnf_stream.cpp | 22 +- src/prop/minisat/core/Solver.cc | 15 +- src/prop/minisat/core/Solver.h | 14 +- src/prop/minisat/core/SolverTypes.h | 2 +- src/prop/minisat/minisat.cpp | 14 +- src/prop/minisat/simp/SimpSolver.cc | 5 +- src/prop/prop_engine.cpp | 39 +- src/prop/prop_engine.h | 9 +- src/prop/sat_solver.h | 8 +- src/prop/theory_proxy.cpp | 18 +- src/prop/theory_proxy.h | 6 +- src/smt/boolean_terms.cpp | 21 +- src/smt/command_list.cpp | 3 +- src/smt/logic_exception.h | 2 +- src/smt/modal_exception.i | 7 - src/smt/options_handlers.h | 517 ----- src/smt/smt_engine.cpp | 267 ++- src/smt/smt_engine.h | 34 +- src/smt/smt_engine.i | 1 - src/smt/smt_engine_check_proof.cpp | 12 +- src/smt/smt_engine_scope.h | 9 +- src/smt/smt_options_handler.cpp | 1729 +++++++++++++++++ src/smt/smt_options_handler.h | 198 ++ src/smt/smt_options_template.cpp | 138 -- src/smt_util/Makefile.am | 30 + .../boolean_simplification.cpp | 3 +- .../boolean_simplification.h | 2 +- src/{expr => smt_util}/command.cpp | 31 +- src/{expr => smt_util}/command.h | 8 +- src/{expr => smt_util}/command.i | 4 +- src/{util => smt_util}/dump.cpp | 5 +- src/{util => smt_util}/dump.h | 3 +- src/{util => smt_util}/ite_removal.cpp | 6 +- src/{util => smt_util}/ite_removal.h | 9 +- src/{util => smt_util}/lemma_input_channel.h | 1 + src/{util => smt_util}/lemma_output_channel.h | 1 + src/{util => smt_util}/model.cpp | 9 +- src/{util => smt_util}/model.h | 0 src/{util => smt_util}/nary_builder.cpp | 4 +- src/{util => smt_util}/nary_builder.h | 0 src/{util => smt_util}/node_visitor.h | 1 + src/theory/arith/approx_simplex.cpp | 13 +- src/theory/arith/approx_simplex.h | 7 +- src/theory/arith/arith_ite_utils.cpp | 11 +- src/theory/arith/arith_rewriter.cpp | 13 +- src/theory/arith/arith_static_learner.cpp | 16 +- src/theory/arith/arith_static_learner.h | 9 +- src/theory/arith/arith_utilities.h | 15 +- src/theory/arith/arithvar.h | 3 +- src/theory/arith/attempt_solution_simplex.cpp | 4 +- src/theory/arith/attempt_solution_simplex.h | 2 +- src/theory/arith/bound_counts.h | 3 +- src/theory/arith/callbacks.h | 5 +- src/theory/arith/congruence_manager.cpp | 4 +- src/theory/arith/congruence_manager.h | 15 +- src/theory/arith/constraint.cpp | 12 +- src/theory/arith/cut_log.cpp | 16 +- src/theory/arith/cut_log.h | 11 +- src/theory/arith/delta_rational.h | 9 +- src/theory/arith/dio_solver.cpp | 7 +- src/theory/arith/dio_solver.h | 18 +- src/theory/arith/dual_simplex.cpp | 6 +- src/theory/arith/dual_simplex.h | 3 +- src/theory/arith/error_set.h | 28 +- src/theory/arith/fc_simplex.cpp | 9 +- src/theory/arith/fc_simplex.h | 5 +- src/theory/arith/infer_bounds.h | 10 +- src/theory/arith/linear_equality.cpp | 3 +- src/theory/arith/linear_equality.h | 11 +- src/theory/arith/matrix.h | 11 +- src/theory/arith/normal_form.cpp | 4 +- src/theory/arith/normal_form.h | 15 +- src/theory/arith/options_handlers.h | 122 -- src/theory/arith/partial_model.cpp | 5 +- src/theory/arith/pseudoboolean_proc.cpp | 5 +- src/theory/arith/pseudoboolean_proc.h | 14 +- src/theory/arith/simplex.cpp | 5 +- src/theory/arith/simplex.h | 9 +- src/theory/arith/soi_simplex.cpp | 10 +- src/theory/arith/soi_simplex.h | 5 +- src/theory/arith/tableau.cpp | 1 + src/theory/arith/tableau.h | 8 +- src/theory/arith/tableau_sizes.cpp | 1 + src/theory/arith/theory_arith.cpp | 5 +- src/theory/arith/theory_arith_private.cpp | 92 +- src/theory/arith/theory_arith_private.h | 86 +- src/theory/arith/type_enumerator.h | 6 +- src/theory/arrays/array_info.h | 13 +- src/theory/arrays/kinds | 2 +- src/theory/arrays/static_fact_manager.cpp | 4 +- src/theory/arrays/theory_arrays.cpp | 15 +- src/theory/arrays/theory_arrays.h | 8 +- src/theory/arrays/union_find.cpp | 4 +- src/theory/booleans/options_handlers.h | 65 - src/theory/booleans/theory_bool.cpp | 2 +- src/theory/builtin/kinds | 6 +- .../builtin/theory_builtin_rewriter.cpp | 3 +- src/theory/builtin/type_enumerator.h | 8 +- src/theory/bv/abstraction.cpp | 11 +- src/theory/bv/abstraction.h | 6 +- src/theory/bv/aig_bitblaster.cpp | 4 +- src/theory/bv/bitblaster_template.h | 3 +- src/theory/bv/bv_eager_solver.cpp | 4 +- src/theory/bv/bv_quick_check.h | 4 +- src/theory/bv/bv_subtheory_algebraic.cpp | 11 +- src/theory/bv/bv_subtheory_bitblast.cpp | 28 +- src/theory/bv/bv_subtheory_core.cpp | 6 +- src/theory/bv/bv_subtheory_inequality.cpp | 4 +- src/theory/bv/bv_to_bool.cpp | 5 +- src/theory/bv/bv_to_bool.h | 5 +- src/theory/bv/eager_bitblaster.cpp | 42 +- src/theory/bv/lazy_bitblaster.cpp | 10 +- src/theory/bv/options_handlers.h | 160 -- src/theory/bv/slicer.cpp | 3 +- src/theory/bv/slicer.h | 10 +- src/theory/bv/theory_bv.cpp | 23 +- src/theory/bv/theory_bv.h | 13 +- src/theory/bv/theory_bv_rewrite_rules.h | 14 +- .../theory_bv_rewrite_rules_normalization.h | 1 + src/theory/bv/theory_bv_rewriter.cpp | 13 +- src/theory/bv/theory_bv_rewriter.h | 2 +- src/theory/bv/theory_bv_utils.cpp | 48 +- src/theory/bv/type_enumerator.h | 6 +- src/theory/datatypes/datatypes_rewriter.h | 5 +- src/theory/datatypes/datatypes_sygus.cpp | 6 +- src/theory/datatypes/datatypes_sygus.h | 10 +- src/theory/datatypes/kinds | 18 +- src/theory/datatypes/theory_datatypes.cpp | 22 +- src/theory/datatypes/theory_datatypes.h | 12 +- .../datatypes/theory_datatypes_type_rules.h | 2 +- src/theory/fp/options_handlers.h | 14 - src/theory/fp/theory_fp_rewriter.cpp | 7 +- src/theory/idl/theory_idl.cpp | 6 +- src/theory/interrupted.h | 2 +- src/theory/ite_utilities.h | 5 +- src/theory/logic_info.cpp | 7 +- src/theory/logic_info.h | 2 +- src/theory/options | 15 - src/theory/options_handlers.h | 69 - src/theory/output_channel.h | 6 +- src/theory/quantifiers/ambqi_builder.cpp | 2 +- src/theory/quantifiers/bounded_integers.cpp | 5 +- .../quantifiers/candidate_generator.cpp | 8 +- .../quantifiers/ce_guided_instantiation.cpp | 12 +- .../quantifiers/ce_guided_instantiation.h | 6 +- .../quantifiers/ce_guided_single_inv.cpp | 14 +- .../quantifiers/ce_guided_single_inv_ei.cpp | 10 +- .../quantifiers/ce_guided_single_inv_sol.cpp | 14 +- src/theory/quantifiers/ceg_instantiator.cpp | 12 +- src/theory/quantifiers/ceg_instantiator.h | 2 +- .../quantifiers/conjecture_generator.cpp | 6 +- src/theory/quantifiers/first_order_model.cpp | 8 +- src/theory/quantifiers/full_model_check.cpp | 4 +- .../quantifiers/inst_match_generator.cpp | 12 +- src/theory/quantifiers/inst_strategy_cbqi.cpp | 12 +- src/theory/quantifiers/inst_strategy_cbqi.h | 5 +- .../quantifiers/inst_strategy_e_matching.cpp | 7 +- .../quantifiers/inst_strategy_e_matching.h | 8 +- .../quantifiers/instantiation_engine.cpp | 6 +- src/theory/quantifiers/macros.cpp | 11 +- src/theory/quantifiers/model_builder.cpp | 15 +- src/theory/quantifiers/model_engine.cpp | 15 +- src/theory/quantifiers/options_handlers.h | 480 ----- .../quantifiers/quant_conflict_find.cpp | 7 +- .../quantifiers/quantifiers_attributes.cpp | 3 +- .../quantifiers/quantifiers_rewriter.cpp | 5 +- src/theory/quantifiers/rewrite_engine.cpp | 9 +- src/theory/quantifiers/symmetry_breaking.cpp | 9 +- src/theory/quantifiers/symmetry_breaking.h | 15 +- src/theory/quantifiers/term_database.cpp | 20 +- src/theory/quantifiers/theory_quantifiers.cpp | 15 +- src/theory/quantifiers/theory_quantifiers.h | 10 +- .../theory_quantifiers_type_rules.h | 2 +- src/theory/quantifiers/trigger.cpp | 11 +- src/theory/quantifiers_engine.cpp | 43 +- src/theory/quantifiers_engine.h | 17 +- src/theory/rewriter.cpp | 5 +- src/theory/rewriter.h | 2 - src/theory/sets/expr_patterns.h | 2 + src/theory/sets/kinds | 2 +- src/theory/sets/theory_sets_private.cpp | 15 +- src/theory/shared_terms_database.h | 4 +- src/{util => theory}/sort_inference.cpp | 16 +- src/{util => theory}/sort_inference.h | 0 src/theory/strings/regexp_operation.cpp | 3 +- src/theory/strings/theory_strings.cpp | 17 +- .../strings/theory_strings_preprocess.cpp | 9 +- .../strings/theory_strings_rewriter.cpp | 7 +- .../strings/theory_strings_type_rules.h | 2 +- src/theory/term_registration_visitor.cpp | 3 +- src/theory/theory.cpp | 8 +- src/theory/theory.h | 36 +- src/theory/theory_engine.cpp | 55 +- src/theory/theory_engine.h | 30 +- src/theory/theory_model.cpp | 8 +- src/theory/theory_model.h | 2 +- src/theory/theory_test_utils.h | 12 +- src/theory/theory_traits_template.h | 2 +- src/theory/type_enumerator.h | 4 +- src/theory/type_enumerator_template.cpp | 4 +- src/theory/uf/equality_engine.h | 15 +- src/theory/uf/options_handlers.h | 70 - src/theory/uf/symmetry_breaker.h | 6 +- src/theory/uf/theory_uf.cpp | 9 +- src/theory/uf/theory_uf_model.cpp | 12 +- src/theory/uf/theory_uf_strong_solver.cpp | 3 +- src/theory/uf/theory_uf_strong_solver.h | 10 +- src/theory/unconstrained_simplifier.h | 2 +- src/theory/valuation.h | 2 +- src/util/Makefile.am | 177 +- src/util/abstract_value.cpp | 5 + src/util/abstract_value.h | 11 +- src/util/array.i | 5 - src/util/bin_heap.h | 2 +- src/util/bitvector.h | 3 +- src/util/cardinality.h | 2 +- src/util/channel.h | 10 +- src/util/configuration.cpp | 9 +- src/util/configuration.h | 6 +- src/util/dense_map.h | 6 +- src/util/divisible.cpp | 3 +- src/util/divisible.h | 3 +- src/util/dynamic_array.h | 2 +- src/util/floatingpoint.cpp | 4 +- src/util/floatingpoint.h | 38 +- src/util/integer_cln_imp.cpp | 8 +- src/util/integer_cln_imp.h | 2 +- src/util/integer_gmp_imp.cpp | 9 +- src/util/integer_gmp_imp.h | 2 +- src/util/maybe.h | 3 +- src/util/rational_cln_imp.cpp | 7 +- src/util/rational_cln_imp.h | 3 +- src/util/rational_gmp_imp.cpp | 9 +- src/util/rational_gmp_imp.h | 3 +- src/util/regexp.cpp | 3 +- src/util/regexp.h | 4 +- src/util/resource_manager.i | 5 - src/util/smt2_quote_string.cpp | 41 + src/util/{sexpr.cpp => smt2_quote_string.h} | 27 +- src/util/subrange_bound.h | 6 +- src/util/unsafe_interrupt_exception.h | 4 +- test/system/ouroborous.cpp | 2 +- test/system/smt2_compliance.cpp | 10 +- test/system/statistics.cpp | 8 +- test/unit/context/cdlist_black.h | 8 +- test/unit/context/cdmap_white.h | 2 +- test/unit/context/cdo_black.h | 7 +- test/unit/context/context_black.h | 8 +- test/unit/context/context_white.h | 2 +- test/unit/expr/attribute_white.h | 12 +- test/unit/expr/expr_manager_public.h | 2 +- test/unit/expr/expr_public.h | 9 +- test/unit/expr/node_black.h | 8 +- test/unit/expr/node_builder_black.h | 8 +- test/unit/expr/node_manager_black.h | 3 +- test/unit/expr/node_manager_white.h | 3 +- test/unit/expr/node_white.h | 6 +- test/unit/expr/symbol_table_black.h | 8 +- test/unit/main/interactive_shell_black.h | 4 +- test/unit/memory.h | 2 +- test/unit/parser/parser_black.h | 9 +- test/unit/parser/parser_builder_black.h | 11 +- test/unit/prop/cnf_stream_white.h | 13 +- test/unit/theory/logic_info_white.h | 3 +- test/unit/theory/theory_arith_white.h | 20 +- test/unit/theory/theory_engine_white.h | 20 +- test/unit/theory/type_enumerator_white.h | 8 +- test/unit/util/array_store_all_black.h | 2 +- test/unit/util/assert_white.h | 2 +- test/unit/util/boolean_simplification_black.h | 15 +- test/unit/util/cardinality_public.h | 8 +- test/unit/util/datatype_black.h | 3 +- test/unit/util/exception_black.h | 2 +- test/unit/util/integer_black.h | 3 +- test/unit/util/output_black.h | 2 +- test/unit/util/stats_black.h | 2 +- test/unit/util/subrange_bound_white.h | 9 +- 512 files changed, 6485 insertions(+), 5254 deletions(-) create mode 100755 contrib/new-theory.awk rename contrib/{theoryskel/options => optionsskel/DIR_options} (73%) delete mode 100644 contrib/theoryskel/options_handlers.h create mode 100644 src/base/Makefile.am rename src/{util => base}/cvc4_assert.cpp (98%) rename src/{util => base}/cvc4_assert.h (98%) rename src/{util => base}/exception.cpp (93%) rename src/{util => base}/exception.h (99%) rename src/{util => base}/exception.i (82%) create mode 100644 src/base/lemma_input_channel_forward.h create mode 100644 src/base/lemma_output_channel_forward.h rename src/{smt => base}/modal_exception.h (97%) create mode 100644 src/base/modal_exception.i rename src/{util => base}/output.cpp (99%) rename src/{util => base}/output.h (100%) rename src/{util => base}/tls.h.in (100%) rename src/{util => context}/backtrackable.h (100%) rename src/{theory => decision}/decision_attributes.h (66%) delete mode 100644 src/decision/options_handlers.h rename src/{util => expr}/array.h (100%) create mode 100644 src/expr/array.i rename src/{util => expr}/array_store_all.cpp (96%) rename src/{util => expr}/array_store_all.h (100%) rename src/{util => expr}/array_store_all.i (90%) rename src/{util => expr}/ascription_type.h (100%) rename src/{util => expr}/ascription_type.i (81%) rename src/{util => expr}/chain.h (100%) rename src/{util => expr}/chain.i (84%) rename src/{util => expr}/datatype.cpp (99%) rename src/{util => expr}/datatype.h (99%) rename src/{util => expr}/datatype.i (99%) rename src/{util => expr}/emptyset.cpp (94%) rename src/{util => expr}/emptyset.h (100%) rename src/{util => expr}/emptyset.i (91%) rename src/{util => expr}/matcher.h (99%) delete mode 100644 src/expr/options_handlers.h rename src/{util => expr}/predicate.cpp (96%) rename src/{util => expr}/predicate.h (91%) rename src/{util => expr}/predicate.i (83%) rename src/{util => expr}/record.cpp (95%) rename src/{util => expr}/record.h (98%) rename src/{util => expr}/record.i (98%) rename src/{util => expr}/resource_manager.cpp (96%) rename src/{util => expr}/resource_manager.h (99%) create mode 100644 src/expr/resource_manager.i rename src/{util => expr}/result.cpp (69%) rename src/{util => expr}/result.h (84%) rename src/{util => expr}/result.i (92%) create mode 100644 src/expr/sexpr.cpp rename src/{util => expr}/sexpr.h (55%) rename src/{util => expr}/sexpr.i (91%) rename src/{util => expr}/statistics.cpp (97%) rename src/{util => expr}/statistics.h (99%) rename src/{util => expr}/statistics.i (98%) rename src/{util => expr}/statistics_registry.cpp (96%) rename src/{util => expr}/statistics_registry.h (97%) rename src/{util => expr}/uninterpreted_constant.cpp (96%) rename src/{util => expr}/uninterpreted_constant.h (100%) rename src/{util => expr}/uninterpreted_constant.i (90%) delete mode 100644 src/main/options_handlers.h rename src/{theory/arith => options}/arith_heuristic_pivot_rule.cpp (94%) rename src/{theory/arith => options}/arith_heuristic_pivot_rule.h (96%) rename src/{theory/arith/options => options/arith_options} (92%) rename src/{theory/arith => options}/arith_propagation_mode.cpp (95%) rename src/{theory/arith => options}/arith_propagation_mode.h (96%) rename src/{theory/arith => options}/arith_unate_lemma_mode.cpp (95%) rename src/{theory/arith => options}/arith_unate_lemma_mode.h (100%) rename src/{theory/arrays/options => options/arrays_options} (95%) create mode 100644 src/options/base_handlers.h delete mode 100644 src/options/base_options_handlers.h rename src/{theory/booleans => options}/boolean_term_conversion_mode.cpp (95%) rename src/{theory/booleans => options}/boolean_term_conversion_mode.h (100%) rename src/{theory/booleans/options => options/booleans_options} (57%) rename src/{theory/builtin/options => options/builtin_options} (67%) rename src/{theory/bv/bitblast_mode.cpp => options/bv_bitblast_mode.cpp} (92%) rename src/{theory/bv/bitblast_mode.h => options/bv_bitblast_mode.h} (100%) rename src/{theory/bv/options => options/bv_options} (79%) rename src/{theory/datatypes/options => options/datatypes_options} (94%) rename src/{decision => options}/decision_mode.cpp (96%) rename src/{decision => options}/decision_mode.h (100%) rename src/{decision/options => options/decision_options} (64%) rename src/{theory/sets/options_handlers.h => options/decision_weight.h} (52%) rename src/{util => options}/didyoumean.cpp (98%) rename src/{util => options}/didyoumean.h (99%) rename src/{util => options}/didyoumean_test.cpp (99%) rename src/{expr/options => options/expr_options} (76%) rename src/{theory/fp/options => options/fp_options} (77%) rename src/{theory/idl/options => options/idl_options} (91%) rename src/{util => options}/language.cpp (99%) rename src/{util => options}/language.h (99%) rename src/{util => options}/language.i (96%) create mode 100644 src/options/logic_info_forward.h rename src/{main/options => options/main_options} (81%) create mode 100644 src/options/options_handler_get_option_template.cpp create mode 100644 src/options/options_handler_interface.cpp create mode 100644 src/options/options_handler_interface.h create mode 100644 src/options/options_handler_interface.i create mode 100644 src/options/options_handler_set_option_template.cpp rename src/{parser/options => options/parser_options} (96%) rename src/{printer/modes.cpp => options/printer_modes.cpp} (95%) rename src/{printer/modes.h => options/printer_modes.h} (98%) create mode 100644 src/options/printer_options rename src/{proof/options => options/proof_options} (73%) rename src/{prop/options => options/prop_options} (96%) rename src/{theory/quantifiers/modes.cpp => options/quantifiers_modes.cpp} (96%) rename src/{theory/quantifiers/modes.h => options/quantifiers_modes.h} (88%) rename src/{theory/quantifiers/options => options/quantifiers_options} (86%) rename src/{theory/sets/options => options/sets_options} (92%) rename src/{smt => options}/simplification_mode.cpp (96%) rename src/{smt => options}/simplification_mode.h (100%) rename src/{smt/options => options/smt_options} (73%) rename src/{theory/strings/options => options/strings_options} (88%) create mode 100644 src/options/theory_options create mode 100644 src/options/theoryof_mode.cpp rename src/{theory => options}/theoryof_mode.h (72%) rename src/{theory/uf/options => options/uf_options} (89%) create mode 100644 src/options/ufss_mode.h delete mode 100644 src/printer/options delete mode 100644 src/printer/options_handlers.h rename src/{util => proof}/unsat_core.cpp (95%) rename src/{util => proof}/unsat_core.h (100%) rename src/{util => proof}/unsat_core.i (97%) delete mode 100644 src/smt/modal_exception.i delete mode 100644 src/smt/options_handlers.h create mode 100644 src/smt/smt_options_handler.cpp create mode 100644 src/smt/smt_options_handler.h delete mode 100644 src/smt/smt_options_template.cpp create mode 100644 src/smt_util/Makefile.am rename src/{util => smt_util}/boolean_simplification.cpp (97%) rename src/{util => smt_util}/boolean_simplification.h (99%) rename src/{expr => smt_util}/command.cpp (99%) rename src/{expr => smt_util}/command.h (99%) rename src/{expr => smt_util}/command.i (97%) rename src/{util => smt_util}/dump.cpp (92%) rename src/{util => smt_util}/dump.h (98%) rename src/{util => smt_util}/ite_removal.cpp (98%) rename src/{util => smt_util}/ite_removal.h (99%) rename src/{util => smt_util}/lemma_input_channel.h (95%) rename src/{util => smt_util}/lemma_output_channel.h (96%) rename src/{util => smt_util}/model.cpp (95%) rename src/{util => smt_util}/model.h (100%) rename src/{util => smt_util}/nary_builder.cpp (99%) rename src/{util => smt_util}/nary_builder.h (100%) rename src/{util => smt_util}/node_visitor.h (99%) delete mode 100644 src/theory/arith/options_handlers.h delete mode 100644 src/theory/booleans/options_handlers.h delete mode 100644 src/theory/bv/options_handlers.h delete mode 100644 src/theory/fp/options_handlers.h delete mode 100644 src/theory/options delete mode 100644 src/theory/options_handlers.h delete mode 100644 src/theory/quantifiers/options_handlers.h rename src/{util => theory}/sort_inference.cpp (99%) rename src/{util => theory}/sort_inference.h (100%) delete mode 100644 src/theory/uf/options_handlers.h delete mode 100644 src/util/array.i delete mode 100644 src/util/resource_manager.i create mode 100644 src/util/smt2_quote_string.cpp rename src/util/{sexpr.cpp => smt2_quote_string.h} (53%) diff --git a/.travis.yml b/.travis.yml index 5ee1410f1..08b7b0241 100644 --- a/.travis.yml +++ b/.travis.yml @@ -54,18 +54,18 @@ script: exit 1; } makeDistcheck() { - make -j2 distcheck CVC4_REGRESSION_ARGS='--no-early-exit' DISTCHECK_CONFIGURE_FLAGS="CXXTEST=$HOME/cxxtest" || + make V=1 -j2 distcheck CVC4_REGRESSION_ARGS='--no-early-exit' DISTCHECK_CONFIGURE_FLAGS="CXXTEST=$HOME/cxxtest" || error "DISTCHECK (WITH NEWTHEORY TESTS) FAILED"; } makeCheck() { - make -j2 check CVC4_REGRESSION_ARGS='--no-early-exit' || error "BUILD/TEST FAILED"; + make V=1 -j2 check CVC4_REGRESSION_ARGS='--no-early-exit' || error "BUILD/TEST FAILED"; } makeCheckPortfolio() { - make check BINARY=pcvc4 CVC4_REGRESSION_ARGS='--fallback-sequential --no-early-exit' RUN_REGRESSION_ARGS= || + make check V=1 BINARY=pcvc4 CVC4_REGRESSION_ARGS='--fallback-sequential --no-early-exit' RUN_REGRESSION_ARGS= || error "PORTFOLIO TEST FAILED"; } makeExamples() { - make -j2 examples || error "COULD NOT BUILD EXAMPLES${normal}"; + make V=1 -j2 examples || error "COULD NOT BUILD EXAMPLES${normal}"; } addNewTheoryTest() { contrib/new-theory test_newtheory || error "NEWTHEORY FAILED"; @@ -101,4 +101,4 @@ matrix: notifications: email: on_success: change - on_failure: always \ No newline at end of file + on_failure: always diff --git a/AUTHORS b/AUTHORS index 98205ef98..3e85b13c7 100644 --- a/AUTHORS +++ b/AUTHORS @@ -13,7 +13,7 @@ The core designers and authors of CVC4 are: Morgan Deters, New York University Liana Hadarean, New York University & Mentor Graphics Corporation Dejan Jovanovic, New York University & SRI International - Tim King, New York University + Tim King, New York University, Universite Joseph Fourier & Google, Inc. Tianyi Liang, The University of Iowa Andrew Reynolds, The University of Iowa & EPFL Cesare Tinelli, The University of Iowa diff --git a/configure.ac b/configure.ac index fe3d7b8d9..c3c29db38 100644 --- a/configure.ac +++ b/configure.ac @@ -1410,9 +1410,9 @@ if test -n "$CVC4_LANGUAGE_BINDINGS"; then fi fi -CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h]) +CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/base/tls.h]) CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h]) -CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/tls.h]) +CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h]) CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.1_template]) CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.5]) diff --git a/contrib/depgraph b/contrib/depgraph index e85bcd694..2c4eba595 100755 --- a/contrib/depgraph +++ b/contrib/depgraph @@ -88,6 +88,7 @@ for path in $paths; do if [ -n "$target" -a "$target" != "$package" ]; then continue; fi for inc in $incs; do case "$inc" in + base/tls.h) inc=base/tls.h.in ;; expr/expr.h) inc=expr/expr_template.h ;; expr/expr_manager.h) inc=expr/expr_manager_template.h ;; expr/kind.h) inc=expr/kind_template.h ;; @@ -95,7 +96,6 @@ for path in $paths; do theory/theoryof_table.h) inc=theory/theoryof_table_template.h ;; util/integer.h) inc=util/integer.h.in ;; util/rational.h) inc=util/rational.h.in ;; - util/tls.h) inc=util/tls.h.in ;; cvc4autoconfig.h) inc=cvc4autoconfig.h.in ;; esac incpath= diff --git a/contrib/new-theory b/contrib/new-theory index 8f9714372..0d9e45647 100755 --- a/contrib/new-theory +++ b/contrib/new-theory @@ -119,6 +119,15 @@ function copyaltskel { > "src/theory/$dir/$dest" } +function copyoptions { + src="$1" + dest="`echo "$src" | sed "s/DIR/$dir/g"`" + echo "Creating src/options/$dest..." + sed "s/\$dir/$dir/g;s/\$camel/$camel/g;s/\$id/$id/g;s/\$alt_id/$alt_id/g" \ + contrib/optionsskel/$src \ + > "src/options/$dest" +} + # copy files from the skeleton, with proper replacements if $alternate; then alternate01=1 @@ -131,6 +140,11 @@ else copyskel "$file" done fi +# Copy the options file independently +for file in `ls contrib/optionsskel`; do + copyoptions "$file" +done + echo echo "Adding $dir to THEORIES to src/Makefile.theories..." @@ -158,19 +172,18 @@ perl -e ' while(<>) { if(!/\\$/) { chomp; print "$_ \\\n\ttheory/'"$dir"'/theory_'"$dir"'.h \\\n\ttheory/'"$dir"'/theory_'"$dir"'.cpp \\\n\ttheory/'"$dir"'/theory_'"$dir"'_rewriter.h \\\n\ttheory/'"$dir"'/theory_'"$dir"'_type_rules.h\n"; last; } else { print; } } } while(<>) { print; last if /^EXTRA_DIST = /; } - while(<>) { if(!/\\$/) { chomp; print "$_ \\\n\ttheory/'"$dir"'/kinds \\\n\ttheory/'"$dir"'/options_handlers.h\n"; last; } else { print; } } + while(<>) { if(!/\\$/) { chomp; print "$_ \\\n\ttheory/'"$dir"'/kinds\n"; last; } else { print; } } while(<>) { print; }' src/Makefile.am > src/Makefile.am.new-theory if ! mv -f src/Makefile.am.new-theory src/Makefile.am; then echo "ERROR: cannot replace src/Makefile.am !" >&2 exit 1 fi -echo "Adding ../theory/$dir/options.cpp to OPTIONS_FILES_SRCS" -echo " and nodist_liboptions_la_SOURCES to src/options/Makefile.am..." -if grep -q '^ \.\./theory/'"$dir"'/options\.cpp\>' src/options/Makefile.am &>/dev/null; then +echo "Adding ${dir}_options to src/options/Makefile.am..." +if grep -q '^ ${dir}_options' src/options/Makefile.am &>/dev/null; then echo "NOTE: src/options/Makefile.am already seems to link to $dir option files" else - awk '!/^OPTIONS_FILES_SRCS = \\|^nodist_liboptions_la_SOURCES = / {print$0} /^OPTIONS_FILES_SRCS = \\|^nodist_liboptions_la_SOURCES = / {while(/\\ *$/){print $0;getline} print $0,"\\";print "\t../theory/'"$dir"'/options.cpp","\\";print "\t../theory/'"$dir"'/options.h";}' src/options/Makefile.am > src/options/Makefile.am.new-theory + awk -v name="$dir" -f contrib/new-theory.awk src/options/Makefile.am > src/options/Makefile.am.new-theory if ! cp -f src/options/Makefile.am src/options/Makefile.am~; then echo "ERROR: cannot copy src/options/Makefile.am !" >&2 exit 1 diff --git a/contrib/new-theory.awk b/contrib/new-theory.awk new file mode 100755 index 000000000..6c523f259 --- /dev/null +++ b/contrib/new-theory.awk @@ -0,0 +1,17 @@ +#!/bin/awk -v name=theory_new -f +# + +# The do nothing rule +!/^OPTIONS_SRC_FILES = \\|^OPTIONS_TEMPS = \\|^OPTIONS_OPTIONS_FILES = \\|^OPTIONS_SEDS = \\|^OPTIONS_HEADS = \\|^OPTIONS_CPPS = \\/ {print$0} +# Add the name to the correct locations. +/^OPTIONS_SRC_FILES = \\/{print $0; printf "\t%s_options \\\n", name;} +/^OPTIONS_TEMPS = \\/{print $0; printf "\t%s_options.tmp \\\n", name;} +/^OPTIONS_OPTIONS_FILES = \\/{print $0; printf "\t%s_options.options \\\n", name;} +/^OPTIONS_SEDS = \\/{print $0; printf "\t%s_options.sed \\\n", name;} +/^OPTIONS_HEADS = \\/{print $0; printf "\t%s_options.h \\\n", name;} +/^OPTIONS_CPPS = \\/{print $0; printf "\t%s_options.cpp \\\n", name;} +# Add the rule for name_options. +END{printf "%s_options:;\n", name} +# Add the rules for name_options.tmp +END{printf ".PHONY: %s_options.tmp\n", name} +END{printf "%s_options.tmp:\n\techo \"$@\" \"$(@:.tmp=)\"\n\t$(AM_V_GEN)(cp \"@srcdir@/$(@:.tmp=)\" \"$@\" || true)\n", name} diff --git a/contrib/theoryskel/options b/contrib/optionsskel/DIR_options similarity index 73% rename from contrib/theoryskel/options rename to contrib/optionsskel/DIR_options index f627dc4a0..de160df6d 100644 --- a/contrib/theoryskel/options +++ b/contrib/optionsskel/DIR_options @@ -3,6 +3,6 @@ # See src/options/base_options for a description of this file format # -module $id "theory/$dir/options.h" $camel +module $id "options/$dir_options.h" $camel endmodule diff --git a/contrib/theoryskel/options_handlers.h b/contrib/theoryskel/options_handlers.h deleted file mode 100644 index d384e84d9..000000000 --- a/contrib/theoryskel/options_handlers.h +++ /dev/null @@ -1,14 +0,0 @@ -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__$id__OPTIONS_HANDLERS_H -#define __CVC4__THEORY__$id__OPTIONS_HANDLERS_H - -namespace CVC4 { -namespace theory { -namespace $dir { - -}/* CVC4::theory::$dir namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__$id__OPTIONS_HANDLERS_H */ diff --git a/examples/api/datatypes.cpp b/examples/api/datatypes.cpp index 463cf9534..3da8cfa4a 100644 --- a/examples/api/datatypes.cpp +++ b/examples/api/datatypes.cpp @@ -15,8 +15,8 @@ **/ #include +#include "options/language.h" // for use with make examples #include "smt/smt_engine.h" // for use with make examples -#include "util/language.h" // for use with make examples //#include // To follow the wiki using namespace CVC4; diff --git a/examples/hashsmt/sha1_collision.cpp b/examples/hashsmt/sha1_collision.cpp index ad3705a94..e23be29bf 100644 --- a/examples/hashsmt/sha1_collision.cpp +++ b/examples/hashsmt/sha1_collision.cpp @@ -29,7 +29,7 @@ #include "word.h" #include "sha1.hpp" -#include "expr/command.h" +#include "smt_util/command.h" #include diff --git a/examples/hashsmt/sha1_inversion.cpp b/examples/hashsmt/sha1_inversion.cpp index 51267ba06..fadc6ecb9 100644 --- a/examples/hashsmt/sha1_inversion.cpp +++ b/examples/hashsmt/sha1_inversion.cpp @@ -29,7 +29,7 @@ #include "word.h" #include "sha1.hpp" -#include "expr/command.h" +#include "smt_util/command.h" #include diff --git a/examples/nra-translate/normalize.cpp b/examples/nra-translate/normalize.cpp index 2dd450c4e..d4aecbba9 100644 --- a/examples/nra-translate/normalize.cpp +++ b/examples/nra-translate/normalize.cpp @@ -15,20 +15,19 @@ ** \todo document this file **/ -#include +#include #include +#include +#include #include -#include #include -#include - -#include "options/options.h" #include "expr/expr.h" -#include "expr/command.h" +#include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "smt/smt_engine.h" +#include "smt_util/command.h" using namespace std; using namespace CVC4; diff --git a/examples/nra-translate/smt2info.cpp b/examples/nra-translate/smt2info.cpp index a2c12f05d..d59f9f4c4 100644 --- a/examples/nra-translate/smt2info.cpp +++ b/examples/nra-translate/smt2info.cpp @@ -15,18 +15,17 @@ ** \todo document this file **/ -#include +#include #include +#include #include -#include #include - -#include "options/options.h" #include "expr/expr.h" -#include "expr/command.h" +#include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.h" +#include "smt_util/command.h" using namespace std; using namespace CVC4; diff --git a/examples/nra-translate/smt2todreal.cpp b/examples/nra-translate/smt2todreal.cpp index 4413c480a..97c5c5d04 100644 --- a/examples/nra-translate/smt2todreal.cpp +++ b/examples/nra-translate/smt2todreal.cpp @@ -15,19 +15,19 @@ ** \todo document this file **/ -#include +#include #include +#include +#include #include -#include #include -#include -#include "options/options.h" #include "expr/expr.h" -#include "expr/command.h" +#include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "smt/smt_engine.h" +#include "smt_util/command.h" using namespace std; using namespace CVC4; diff --git a/examples/nra-translate/smt2toisat.cpp b/examples/nra-translate/smt2toisat.cpp index eae77e1ce..9c94cdd43 100644 --- a/examples/nra-translate/smt2toisat.cpp +++ b/examples/nra-translate/smt2toisat.cpp @@ -15,20 +15,19 @@ ** \todo document this file **/ -#include +#include #include +#include +#include #include -#include #include -#include - -#include "options/options.h" #include "expr/expr.h" -#include "expr/command.h" +#include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.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 3158243a5..86aaf786f 100644 --- a/examples/nra-translate/smt2tomathematica.cpp +++ b/examples/nra-translate/smt2tomathematica.cpp @@ -15,19 +15,18 @@ ** \todo document this file **/ -#include +#include #include +#include +#include #include -#include #include -#include - -#include "options/options.h" #include "expr/expr.h" -#include "expr/command.h" +#include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.h" +#include "smt_util/command.h" using namespace std; using namespace CVC4; diff --git a/examples/nra-translate/smt2toqepcad.cpp b/examples/nra-translate/smt2toqepcad.cpp index cb4855a38..058fa8e0d 100644 --- a/examples/nra-translate/smt2toqepcad.cpp +++ b/examples/nra-translate/smt2toqepcad.cpp @@ -15,18 +15,18 @@ ** \todo document this file **/ -#include +#include #include +#include +#include #include -#include #include -#include -#include "options/options.h" #include "expr/expr.h" -#include "expr/command.h" +#include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.h" +#include "smt_util/command.h" using namespace std; using namespace CVC4; diff --git a/examples/nra-translate/smt2toredlog.cpp b/examples/nra-translate/smt2toredlog.cpp index 71d7229af..1ebd6ea59 100644 --- a/examples/nra-translate/smt2toredlog.cpp +++ b/examples/nra-translate/smt2toredlog.cpp @@ -15,20 +15,19 @@ ** \todo document this file **/ -#include +#include #include +#include +#include #include -#include #include -#include - -#include "options/options.h" #include "expr/expr.h" -#include "expr/command.h" +#include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.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 acf0fcafe..c33ccb367 100644 --- a/examples/sets-translate/sets_translate.cpp +++ b/examples/sets-translate/sets_translate.cpp @@ -15,20 +15,19 @@ ** \todo document this file **/ -#include +#include // include Boost, a C++ library +#include #include +#include #include -#include #include -#include // include Boost, a C++ library - -#include "options/options.h" #include "expr/expr.h" -#include "theory/logic_info.h" -#include "expr/command.h" +#include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.h" +#include "smt_util/command.h" +#include "theory/logic_info.h" using namespace std; using namespace CVC4; diff --git a/examples/translator.cpp b/examples/translator.cpp index 7aa969e06..522d88573 100644 --- a/examples/translator.cpp +++ b/examples/translator.cpp @@ -15,18 +15,19 @@ ** CVC4's input languages to one of its output languages. **/ -#include +#include +#include +#include #include #include -#include -#include -#include -#include "smt/smt_engine.h" -#include "util/language.h" -#include "expr/command.h" +#include + #include "expr/expr.h" -#include "parser/parser_builder.h" +#include "options/language.h" #include "parser/parser.h" +#include "parser/parser_builder.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 fe38ddf71..773acf67e 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -19,7 +19,7 @@ AM_CPPFLAGS = \ -I@builddir@ -I@srcdir@/include -I@srcdir@ -I@top_srcdir@/proofs/lfsc_checker AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(FLAG_VISIBILITY_HIDDEN) -SUBDIRS = lib options expr util prop/minisat prop/bvminisat . parser compat bindings main +SUBDIRS = lib base options util expr smt_util prop/minisat prop/bvminisat . parser compat bindings main # The THEORIES list has been moved to Makefile.theories include @top_srcdir@/src/Makefile.theories @@ -33,6 +33,7 @@ nodist_EXTRA_libcvc4_la_SOURCES = dummy.cpp libcvc4_la_SOURCES = \ git_versioninfo.cpp \ svn_versioninfo.cpp \ + context/backtrackable.h \ context/context.cpp \ context/context.h \ context/context_mm.cpp \ @@ -56,20 +57,16 @@ libcvc4_la_SOURCES = \ context/stacking_map.h \ context/stacking_vector.h \ context/cddense_set.h \ - decision/decision_mode.h \ - decision/decision_mode.cpp \ + decision/decision_attributes.h \ decision/decision_engine.h \ decision/decision_engine.cpp \ decision/decision_strategy.h \ decision/justification_heuristic.h \ decision/justification_heuristic.cpp \ - decision/options_handlers.h \ printer/printer.h \ printer/printer.cpp \ printer/dagification_visitor.h \ printer/dagification_visitor.cpp \ - printer/modes.h \ - printer/modes.cpp \ printer/ast/ast_printer.h \ printer/ast/ast_printer.cpp \ printer/smt1/smt1_printer.h \ @@ -80,7 +77,6 @@ libcvc4_la_SOURCES = \ printer/cvc/cvc_printer.cpp \ printer/tptp/tptp_printer.h \ printer/tptp/tptp_printer.cpp \ - printer/options_handlers.h \ proof/proof.h \ proof/sat_proof.h \ proof/sat_proof.cpp \ @@ -90,6 +86,8 @@ libcvc4_la_SOURCES = \ proof/theory_proof.cpp \ proof/proof_manager.h \ proof/proof_manager.cpp \ + proof/unsat_core.cpp \ + proof/unsat_core.h \ prop/registrar.h \ prop/prop_engine.cpp \ prop/prop_engine.h \ @@ -106,31 +104,29 @@ libcvc4_la_SOURCES = \ smt/smt_engine.h \ smt/model_postprocessor.cpp \ smt/model_postprocessor.h \ + smt/smt_options_handler.cpp \ + smt/smt_options_handler.h \ smt/smt_engine_scope.cpp \ smt/smt_engine_scope.h \ smt/command_list.cpp \ smt/command_list.h \ - smt/modal_exception.h \ smt/boolean_terms.h \ smt/boolean_terms.cpp \ smt/logic_exception.h \ smt/logic_request.h \ smt/logic_request.cpp \ - smt/simplification_mode.h \ - smt/simplification_mode.cpp \ - smt/options_handlers.h \ - theory/decision_attributes.h \ theory/logic_info.h \ theory/logic_info.cpp \ theory/output_channel.h \ theory/interrupted.h \ + theory/sort_inference.cpp \ + theory/sort_inference.h \ theory/type_enumerator.h \ theory/theory_engine.h \ theory/theory_engine.cpp \ theory/theory_test_utils.h \ theory/theory.h \ theory/theory.cpp \ - theory/theoryof_mode.h \ theory/theory_registrar.h \ theory/rewriter.h \ theory/rewriter_attributes.h \ @@ -155,7 +151,6 @@ libcvc4_la_SOURCES = \ theory/rep_set.cpp \ theory/atom_requests.h \ theory/atom_requests.cpp \ - theory/options_handlers.h \ theory/uf/theory_uf.h \ theory/uf/theory_uf.cpp \ theory/uf/theory_uf_type_rules.h \ @@ -169,7 +164,6 @@ libcvc4_la_SOURCES = \ theory/uf/theory_uf_strong_solver.cpp \ theory/uf/theory_uf_model.h \ theory/uf/theory_uf_model.cpp \ - theory/uf/options_handlers.h \ theory/bv/theory_bv_utils.h \ theory/bv/theory_bv_utils.cpp \ theory/bv/type_enumerator.h \ @@ -211,9 +205,6 @@ libcvc4_la_SOURCES = \ theory/bv/bv_quick_check.cpp \ theory/bv/bv_subtheory_algebraic.h \ theory/bv/bv_subtheory_algebraic.cpp \ - theory/bv/options_handlers.h \ - theory/bv/bitblast_mode.h \ - theory/bv/bitblast_mode.cpp \ theory/bv/bitblast_utils.h \ theory/bv/bvintropow2.h \ theory/bv/bvintropow2.cpp \ @@ -241,7 +232,6 @@ libcvc4_la_SOURCES = \ theory/datatypes/datatypes_sygus.cpp \ theory/sets/expr_patterns.h \ theory/sets/normal_form.h \ - theory/sets/options_handlers.h \ theory/sets/scrutinize.h \ theory/sets/term_info.h \ theory/sets/theory_sets.cpp \ @@ -289,8 +279,6 @@ libcvc4_la_SOURCES = \ theory/quantifiers/inst_match.cpp \ theory/quantifiers/model_engine.h \ theory/quantifiers/model_engine.cpp \ - theory/quantifiers/modes.cpp \ - theory/quantifiers/modes.h \ theory/quantifiers/term_database.h \ theory/quantifiers/term_database.cpp \ theory/quantifiers/first_order_model.h \ @@ -345,7 +333,6 @@ libcvc4_la_SOURCES = \ theory/quantifiers/quant_equality_engine.cpp \ theory/quantifiers/ceg_instantiator.h \ theory/quantifiers/ceg_instantiator.cpp \ - theory/quantifiers/options_handlers.h \ theory/arith/theory_arith_type_rules.h \ theory/arith/type_enumerator.h \ theory/arith/arithvar.h \ @@ -404,17 +391,10 @@ libcvc4_la_SOURCES = \ theory/arith/theory_arith_private.cpp \ theory/arith/dio_solver.h \ theory/arith/dio_solver.cpp \ - theory/arith/arith_heuristic_pivot_rule.h \ - theory/arith/arith_heuristic_pivot_rule.cpp \ - theory/arith/arith_unate_lemma_mode.h \ - theory/arith/arith_unate_lemma_mode.cpp \ - theory/arith/arith_propagation_mode.h \ - theory/arith/arith_propagation_mode.cpp \ theory/arith/pseudoboolean_proc.h \ theory/arith/pseudoboolean_proc.cpp \ theory/arith/cut_log.h \ theory/arith/cut_log.cpp \ - theory/arith/options_handlers.h \ theory/booleans/type_enumerator.h \ theory/booleans/theory_bool.h \ theory/booleans/theory_bool.cpp \ @@ -423,9 +403,6 @@ libcvc4_la_SOURCES = \ theory/booleans/theory_bool_rewriter.cpp \ theory/booleans/circuit_propagator.h \ theory/booleans/circuit_propagator.cpp \ - theory/booleans/boolean_term_conversion_mode.h \ - theory/booleans/boolean_term_conversion_mode.cpp \ - theory/booleans/options_handlers.h \ theory/fp/theory_fp.h \ theory/fp/theory_fp.cpp \ theory/fp/theory_fp_rewriter.h \ @@ -433,15 +410,16 @@ libcvc4_la_SOURCES = \ theory/fp/theory_fp_type_rules.h nodist_libcvc4_la_SOURCES = \ - smt/smt_options.cpp \ theory/rewriter_tables.h \ theory/theory_traits.h \ theory/type_enumerator.cpp libcvc4_la_LIBADD = \ + @builddir@/base/libbase.la \ @builddir@/options/liboptions.la \ @builddir@/util/libutil.la \ @builddir@/expr/libexpr.la \ + @builddir@/smt_util/libsmtutil.la \ @builddir@/prop/minisat/libminisat.la \ @builddir@/prop/bvminisat/libbvminisat.la if CVC4_PROOF @@ -484,42 +462,40 @@ CLEANFILES = \ $(top_builddir)/src/.subdirs EXTRA_DIST = \ + Makefile.theories \ + cvc4.i \ + include/cvc4.h \ + include/cvc4_private.h \ include/cvc4_private_library.h \ + include/cvc4_public.h \ include/cvc4parser_private.h \ include/cvc4parser_public.h \ - include/cvc4_private.h \ - include/cvc4_public.h \ - include/cvc4.h \ - cvc4.i \ mksubdirs \ - Makefile.theories \ - smt/smt_options_template.cpp \ - smt/modal_exception.i \ smt/logic_exception.i \ smt/smt_engine.i \ - theory/logic_info.i \ - theory/rewriter_tables_template.h \ - theory/theory_traits_template.h \ - theory/type_enumerator_template.cpp \ - theory/mktheorytraits \ - theory/mkrewriter \ - theory/uf/kinds \ - theory/bv/kinds \ - theory/idl/kinds \ - theory/builtin/kinds \ - theory/datatypes/kinds \ - theory/sets/kinds \ - theory/strings/kinds \ - theory/arrays/kinds \ - theory/quantifiers/kinds \ + proof/unsat_core.i \ theory/arith/kinds \ + theory/arrays/kinds \ theory/booleans/kinds \ - theory/example/ecdata.h \ + theory/builtin/kinds \ + theory/bv/kinds \ + theory/datatypes/kinds \ theory/example/ecdata.cpp \ - theory/example/theory_uf_tim.h \ + theory/example/ecdata.h \ theory/example/theory_uf_tim.cpp \ + theory/example/theory_uf_tim.h \ theory/fp/kinds \ - theory/fp/options_handlers.h + theory/idl/kinds \ + theory/logic_info.i \ + theory/mkrewriter \ + theory/mktheorytraits \ + theory/quantifiers/kinds \ + theory/rewriter_tables_template.h \ + theory/sets/kinds \ + theory/strings/kinds \ + theory/theory_traits_template.h \ + theory/type_enumerator_template.cpp \ + theory/uf/kinds svn_versioninfo.cpp: svninfo $(AM_V_GEN)( \ @@ -581,7 +557,7 @@ install-data-local: (echo include/cvc4.h; \ echo include/cvc4_public.h; \ echo include/cvc4parser_public.h; \ - echo util/tls.h; \ + echo base/tls.h; \ echo util/integer.h; \ echo util/rational.h; \ find * -name '*.h' | \ @@ -614,7 +590,7 @@ uninstall-local: -(echo include/cvc4.h; \ echo include/cvc4_public.h; \ echo include/cvc4parser_public.h; \ - echo util/tls.h; \ + echo base/tls.h; \ echo util/integer.h; \ echo util/rational.h; \ find * -name '*.h' | \ diff --git a/src/base/Makefile.am b/src/base/Makefile.am new file mode 100644 index 000000000..b03b61aee --- /dev/null +++ b/src/base/Makefile.am @@ -0,0 +1,40 @@ +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@builddir@/.. -I@srcdir@/../include -I@srcdir@/.. +AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) + +noinst_LTLIBRARIES = libbase.la + +# Do not list built sources (like tls.h) here! +# Rather, list them under BUILT_SOURCES, and their .in versions under +# EXTRA_DIST. Otherwise, they're packaged up in the tarball, which is +# no good---they belong in the configured builds/ directory. If they +# end up in the source directory, they build the cvc4 that was +# configured at the time of the "make dist", which (1) may not be the +# configuration that the user wants, and (2) might cause link errors. +libbase_la_SOURCES = \ + Makefile.am \ + Makefile.in \ + cvc4_assert.cpp \ + cvc4_assert.h \ + exception.cpp \ + exception.h \ + lemma_input_channel_forward.h \ + lemma_output_channel_forward.h \ + modal_exception.h \ + output.cpp \ + output.h + + + +BUILT_SOURCES = \ + tls.h + +EXTRA_DIST = \ + exception.i \ + modal_exception.i \ + tls.h.in + +DISTCLEANFILES = \ + tls.h.tmp \ + tls.h diff --git a/src/util/cvc4_assert.cpp b/src/base/cvc4_assert.cpp similarity index 98% rename from src/util/cvc4_assert.cpp rename to src/base/cvc4_assert.cpp index 3db285182..6e51845dd 100644 --- a/src/util/cvc4_assert.cpp +++ b/src/base/cvc4_assert.cpp @@ -18,7 +18,8 @@ #include #include -#include "util/cvc4_assert.h" +#include "base/cvc4_assert.h" +#include "base/output.h" using namespace std; diff --git a/src/util/cvc4_assert.h b/src/base/cvc4_assert.h similarity index 98% rename from src/util/cvc4_assert.h rename to src/base/cvc4_assert.h index cc854278b..6dca5c81d 100644 --- a/src/util/cvc4_assert.h +++ b/src/base/cvc4_assert.h @@ -25,12 +25,14 @@ #include #include -#include "util/exception.h" -#include "util/tls.h" +#include "base/exception.h" +#include "base/tls.h" + // output.h not strictly needed for this header, but it _is_ needed to // actually _use_ anything in this header, so let's include it. -#include "util/output.h" +// Tim : Disabling this and moving it into cvc4_assert.cpp +//#include "util/output.h" namespace CVC4 { diff --git a/src/util/exception.cpp b/src/base/exception.cpp similarity index 93% rename from src/util/exception.cpp rename to src/base/exception.cpp index ab510c27d..d8eee50bc 100644 --- a/src/util/exception.cpp +++ b/src/base/exception.cpp @@ -14,16 +14,19 @@ ** CVC4's exception base class and some associated utilities. **/ -#include "util/exception.h" +#include "base/exception.h" #include #include #include #include -#include "util/cvc4_assert.h" + +#include "base/cvc4_assert.h" using namespace std; -using namespace CVC4; +#warning "TODO: Remove the second definition of CheckArgument and DebugCheckArgument." + +namespace CVC4 { void IllegalArgumentException::construct(const char* header, const char* extra, const char* function, const char* fmt, va_list args) { @@ -113,3 +116,5 @@ void IllegalArgumentException::construct(const char* header, const char* extra, delete [] buf; #endif /* CVC4_DEBUG */ } + +} /* namespace CVC4 */ diff --git a/src/util/exception.h b/src/base/exception.h similarity index 99% rename from src/util/exception.h rename to src/base/exception.h index 937729f0c..78bb160cc 100644 --- a/src/util/exception.h +++ b/src/base/exception.h @@ -130,7 +130,7 @@ inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() { }/* CVC4 namespace */ #if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT) -# include "util/cvc4_assert.h" +# include "base/cvc4_assert.h" #endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) && !__BUILDING_STATISTICS_FOR_EXPORT */ namespace CVC4 { diff --git a/src/util/exception.i b/src/base/exception.i similarity index 82% rename from src/util/exception.i rename to src/base/exception.i index 422f34b10..083670567 100644 --- a/src/util/exception.i +++ b/src/base/exception.i @@ -1,5 +1,5 @@ %{ -#include "util/exception.h" +#include "base/exception.h" %} %ignore CVC4::operator<<(std::ostream&, const Exception&) throw(); @@ -8,4 +8,4 @@ %rename(CVC4IllegalArgumentException) CVC4::IllegalArgumentException; -%include "util/exception.h" +%include "base/exception.h" diff --git a/src/base/lemma_input_channel_forward.h b/src/base/lemma_input_channel_forward.h new file mode 100644 index 000000000..f74e24b4a --- /dev/null +++ b/src/base/lemma_input_channel_forward.h @@ -0,0 +1,30 @@ +/********************* */ +/*! \file lemma_input_channel_forward.h + ** \verbatim + ** Original author: Tim King + ** 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 Forward declaration of LemmaInputChannel. + ** + ** This forward declaration of LemmaInputChannel is needed for the option + ** lemmaInputChannel (defined in smt_options) can be a LemmaInputChannel* + ** without including expr.h. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__LEMMA_INPUT_CHANNEL_FORWARD_H +#define __CVC4__LEMMA_INPUT_CHANNEL_FORWARD_H + +namespace CVC4 { + +class CVC4_PUBLIC LemmaInputChannel; + +}/* CVC4 namespace */ + +#endif /* __CVC4__LEMMA_INPUT_CHANNEL_FORWARD_H */ diff --git a/src/base/lemma_output_channel_forward.h b/src/base/lemma_output_channel_forward.h new file mode 100644 index 000000000..c53bcc36f --- /dev/null +++ b/src/base/lemma_output_channel_forward.h @@ -0,0 +1,35 @@ +/********************* */ +/*! \file lemma_output_channel_forward.h + ** \verbatim + ** Original author: Tim King + ** 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 Forward declaration of the LemmaOutputChannel + ** + ** This forward declaration of LemmaOutputChannel is needed for the option + ** lemmaOutputChannel (defined in smt_options) can be a LemmaInputChannel* + ** without including expr.h. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__LEMMA_OUTPUT_CHANNEL_FORWARD_H +#define __CVC4__LEMMA_OUTPUT_CHANNEL_FORWARD_H + +namespace CVC4 { + +/** + * This interface describes a mechanism for the propositional and theory + * engines to communicate with the "outside world" about new lemmas being + * discovered. + */ +class CVC4_PUBLIC LemmaOutputChannel; + +}/* CVC4 namespace */ + +#endif /* __CVC4__LEMMA_OUTPUT_CHANNEL_FORWARD_H */ diff --git a/src/smt/modal_exception.h b/src/base/modal_exception.h similarity index 97% rename from src/smt/modal_exception.h rename to src/base/modal_exception.h index 11e78ab19..44f133372 100644 --- a/src/smt/modal_exception.h +++ b/src/base/modal_exception.h @@ -22,7 +22,7 @@ #ifndef __CVC4__SMT__MODAL_EXCEPTION_H #define __CVC4__SMT__MODAL_EXCEPTION_H -#include "util/exception.h" +#include "base/exception.h" namespace CVC4 { diff --git a/src/base/modal_exception.i b/src/base/modal_exception.i new file mode 100644 index 000000000..7df4c8f83 --- /dev/null +++ b/src/base/modal_exception.i @@ -0,0 +1,7 @@ +%{ +#include "base/modal_exception.h" +%} + +%ignore CVC4::ModalException::ModalException(const char*); + +%include "base/modal_exception.h" diff --git a/src/util/output.cpp b/src/base/output.cpp similarity index 99% rename from src/util/output.cpp rename to src/base/output.cpp index 462043805..be0f10fda 100644 --- a/src/util/output.cpp +++ b/src/base/output.cpp @@ -14,7 +14,7 @@ ** Output utility classes and functions. **/ -#include "util/output.h" +#include "base/output.h" #include diff --git a/src/util/output.h b/src/base/output.h similarity index 100% rename from src/util/output.h rename to src/base/output.h diff --git a/src/util/tls.h.in b/src/base/tls.h.in similarity index 100% rename from src/util/tls.h.in rename to src/base/tls.h.in diff --git a/src/bindings/swig.h b/src/bindings/swig.h index 790873ef6..9bece4ecd 100644 --- a/src/bindings/swig.h +++ b/src/bindings/swig.h @@ -26,8 +26,8 @@ #endif /* SWIG_VERSION */ %import "cvc4_public.h" -#warning Working around a SWIG segfault in C++ template parsing. -//%import "util/tls.h" +#warning "Working around a SWIG segfault in C++ template parsing." +//%import "base/tls.h" #define CVC4_THREADLOCAL(__type...) __type #define CVC4_THREADLOCAL_PUBLIC(__type...) CVC4_PUBLIC __type #define CVC4_THREADLOCAL_TYPE(__type...) __type diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 08146760f..35211a49a 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -16,30 +16,29 @@ #include "compat/cvc3_compat.h" -#include "expr/kind.h" -#include "expr/command.h" +#include +#include +#include +#include +#include +#include -#include "util/rational.h" -#include "util/integer.h" +#include "base/output.h" +#include "expr/kind.h" +#include "expr/predicate.h" +#include "expr/sexpr.h" +#include "options/expr_options.h" +#include "options/parser_options.h" +#include "options/smt_options.h" +#include "parser/parser.h" +#include "parser/parser_builder.h" +#include "smt_util/command.h" #include "util/bitvector.h" #include "util/hash.h" +#include "util/integer.h" +#include "util/rational.h" #include "util/subrange_bound.h" -#include "util/predicate.h" -#include "util/output.h" - -#include "parser/parser.h" -#include "parser/parser_builder.h" - -#include "parser/options.h" -#include "smt/options.h" -#include "expr/options.h" -#include -#include -#include -#include -#include -#include using namespace std; @@ -2498,8 +2497,8 @@ void ValidityChecker::loadFile(const std::string& fileName, CVC4::Options opts = d_em->getOptions(); stringstream langss; langss << lang; - d_smt->setOption("input-language", langss.str()); - d_smt->setOption("interactive-mode", string(interactive ? "true" : "false")); + d_smt->setOption("input-language", CVC4::SExpr(langss.str())); + d_smt->setOption("interactive-mode", CVC4::SExpr(interactive ? true : false)); CVC4::parser::ParserBuilder parserBuilder(d_em, fileName, opts); CVC4::parser::Parser* p = parserBuilder.build(); p->useDeclarationsFrom(d_parserContext); @@ -2513,8 +2512,8 @@ void ValidityChecker::loadFile(std::istream& is, CVC4::Options opts = d_em->getOptions(); stringstream langss; langss << lang; - d_smt->setOption("input-language", langss.str()); - d_smt->setOption("interactive-mode", string(interactive ? "true" : "false")); + d_smt->setOption("input-language", CVC4::SExpr(langss.str())); + d_smt->setOption("interactive-mode", CVC4::SExpr(interactive ? true : false)); CVC4::parser::ParserBuilder parserBuilder(d_em, "[stream]", opts); CVC4::parser::Parser* p = parserBuilder.withStreamInput(is).build(); d_parserContext = p; diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h index 0fa4a7ce5..5fefa6871 100644 --- a/src/compat/cvc3_compat.h +++ b/src/compat/cvc3_compat.h @@ -48,23 +48,19 @@ #define _cvc3__include__queryresult_h_ #define _cvc3__include__formula_value_h_ -#include "expr/expr_manager.h" +#include +#include +#include + +#include "base/exception.h" #include "expr/expr.h" +#include "expr/expr_manager.h" #include "expr/type.h" - +#include "parser/parser.h" #include "smt/smt_engine.h" - -#include "util/rational.h" -#include "util/integer.h" - -#include "util/exception.h" #include "util/hash.h" - -#include "parser/parser.h" - -#include -#include -#include +#include "util/integer.h" +#include "util/rational.h" //class CInterface; diff --git a/src/util/backtrackable.h b/src/context/backtrackable.h similarity index 100% rename from src/util/backtrackable.h rename to src/context/backtrackable.h diff --git a/src/context/cdchunk_list.h b/src/context/cdchunk_list.h index 8c2e4066e..62a87ffcc 100644 --- a/src/context/cdchunk_list.h +++ b/src/context/cdchunk_list.h @@ -24,9 +24,10 @@ #include #include +#include "base/cvc4_assert.h" #include "context/context.h" #include "context/context_mm.h" -#include "util/cvc4_assert.h" + namespace CVC4 { namespace context { diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h index 338c46b0d..51fd3b411 100644 --- a/src/context/cdhashmap.h +++ b/src/context/cdhashmap.h @@ -95,12 +95,12 @@ #ifndef __CVC4__CONTEXT__CDHASHMAP_H #define __CVC4__CONTEXT__CDHASHMAP_H -#include -#include #include +#include +#include +#include "base/cvc4_assert.h" #include "context/context.h" -#include "util/cvc4_assert.h" #include "context/cdhashmap_forward.h" namespace CVC4 { diff --git a/src/context/cdhashset.h b/src/context/cdhashset.h index 76bab5a94..533a09a0a 100644 --- a/src/context/cdhashset.h +++ b/src/context/cdhashset.h @@ -19,9 +19,10 @@ #ifndef __CVC4__CONTEXT__CDHASHSET_H #define __CVC4__CONTEXT__CDHASHSET_H +#include "base/cvc4_assert.h" #include "context/context.h" #include "context/cdinsert_hashmap.h" -#include "util/cvc4_assert.h" + namespace CVC4 { namespace context { diff --git a/src/context/cdinsert_hashmap.h b/src/context/cdinsert_hashmap.h index 1c8f94143..b65784ddf 100644 --- a/src/context/cdinsert_hashmap.h +++ b/src/context/cdinsert_hashmap.h @@ -33,16 +33,17 @@ #include "cvc4_private.h" -#include "context/context.h" -#include "context/cdinsert_hashmap_forward.h" -#include -#include +#include #include -#include "util/cvc4_assert.h" -#include "util/output.h" +#include +#include +#include "base/cvc4_assert.h" +#include "base/output.h" +#include "context/context.h" +#include "context/cdinsert_hashmap_forward.h" #include "expr/node.h" -#include + #pragma once diff --git a/src/context/cdlist.h b/src/context/cdlist.h index 7c673a4be..dbc00bd69 100644 --- a/src/context/cdlist.h +++ b/src/context/cdlist.h @@ -20,17 +20,16 @@ #ifndef __CVC4__CONTEXT__CDLIST_H #define __CVC4__CONTEXT__CDLIST_H +#include #include #include #include #include +#include "base/cvc4_assert.h" #include "context/context.h" #include "context/context_mm.h" #include "context/cdlist_forward.h" -#include "util/cvc4_assert.h" - -#include namespace CVC4 { namespace context { diff --git a/src/context/cdo.h b/src/context/cdo.h index 5fa0a4d8b..486626ae5 100644 --- a/src/context/cdo.h +++ b/src/context/cdo.h @@ -19,8 +19,9 @@ #ifndef __CVC4__CONTEXT__CDO_H #define __CVC4__CONTEXT__CDO_H +#include "base/cvc4_assert.h" #include "context/context.h" -#include "util/cvc4_assert.h" + namespace CVC4 { namespace context { diff --git a/src/context/cdtrail_hashmap.h b/src/context/cdtrail_hashmap.h index f4220ef43..befd396a9 100644 --- a/src/context/cdtrail_hashmap.h +++ b/src/context/cdtrail_hashmap.h @@ -44,17 +44,16 @@ #pragma once -#include "context/context.h" -#include "context/cdtrail_hashmap_forward.h" -#include +#include #include #include -#include "util/cvc4_assert.h" -#include "util/output.h" +#include +#include "base/cvc4_assert.h" +#include "base/output.h" +#include "context/context.h" +#include "context/cdtrail_hashmap_forward.h" #include "expr/node.h" -#include - namespace CVC4 { namespace context { diff --git a/src/context/cdvector.h b/src/context/cdvector.h index 30699670f..fe8f77c6d 100644 --- a/src/context/cdvector.h +++ b/src/context/cdvector.h @@ -20,11 +20,11 @@ #ifndef __CVC4__CONTEXT__CDVECTOR_H #define __CVC4__CONTEXT__CDVECTOR_H -#include "context/context.h" -#include "context/cdlist.h" -#include "util/cvc4_assert.h" #include +#include "base/cvc4_assert.h" +#include "context/context.h" +#include "context/cdlist.h" namespace CVC4 { namespace context { diff --git a/src/context/context.cpp b/src/context/context.cpp index c427e89c9..99a98e63f 100644 --- a/src/context/context.cpp +++ b/src/context/context.cpp @@ -18,8 +18,9 @@ #include #include +#include "base/cvc4_assert.h" #include "context/context.h" -#include "util/cvc4_assert.h" + namespace CVC4 { namespace context { diff --git a/src/context/context.h b/src/context/context.h index 9c631b202..b88f36786 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -26,8 +26,10 @@ #include #include +#include "base/cvc4_assert.h" +#include "base/output.h" #include "context/context_mm.h" -#include "util/cvc4_assert.h" + namespace CVC4 { namespace context { diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp index e7b234a95..f30413650 100644 --- a/src/context/context_mm.cpp +++ b/src/context/context_mm.cpp @@ -19,9 +19,10 @@ #include #include #include + +#include "base/cvc4_assert.h" +#include "base/output.h" #include "context/context_mm.h" -#include "util/cvc4_assert.h" -#include "util/output.h" namespace CVC4 { namespace context { diff --git a/src/cvc4.i b/src/cvc4.i index d845c1a27..ad042d398 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -48,12 +48,17 @@ using namespace CVC4; #include #include -#include "util/sexpr.h" -#include "util/exception.h" -#include "expr/type.h" +#include "base/exception.h" +#include "base/modal_exception.h" +#include "expr/datatype.h" #include "expr/expr.h" -#include "util/datatype.h" -#include "expr/command.h" +#include "expr/sexpr.h" +#include "expr/type.h" +#include "options/option_exception.h" +#include "smt_util/command.h" +#include "util/integer.h" +#include "util/bitvector.h" +#include "util/unsafe_interrupt_exception.h" #ifdef SWIGJAVA #include "bindings/java_stream_adapters.h" @@ -143,17 +148,21 @@ std::set CVC4::JavaInputStreamAdapter::s_adapters; assert(status == 0); %} -%typemap(throws) ModalException = Exception; -%typemap(throws) LogicException = Exception; -%typemap(throws) OptionException = Exception; -%typemap(throws) IllegalArgumentException = Exception; -%typemap(throws) AssertionException = Exception; +%typemap(throws) CVC4::ModalException = CVC4::Exception; +%typemap(throws) CVC4::LogicException = CVC4::Exception; +%typemap(throws) CVC4::OptionException = CVC4::Exception; +%typemap(throws) CVC4::IllegalArgumentException = CVC4::Exception; +%typemap(throws) CVC4::AssertionException = CVC4::Exception; %typemap(throws) CVC4::TypeCheckingException = CVC4::Exception; %typemap(throws) CVC4::ScopeException = CVC4::Exception; %typemap(throws) CVC4::IllegalArgumentException = CVC4::Exception; +%typemap(throws) IllegalArgumentException = Exception; %typemap(throws) CVC4::AssertionException = CVC4::Exception; + +// TIM: Really unclear why both of these are required %typemap(throws) CVC4::UnsafeInterruptException = CVC4::Exception; +%typemap(throws) UnsafeInterruptException = CVC4::Exception; %typemap(throws) CVC4::parser::InputStreamException = CVC4::Exception; %typemap(throws) CVC4::parser::ParserException = CVC4::Exception; @@ -293,53 +302,60 @@ std::set CVC4::JavaInputStreamAdapter::s_adapters; #endif /* SWIGJAVA */ -%include "util/exception.i" +// TIM: +// At the moment, the header includes seem to need to follow a special order. +// I don't know why. I am following the build order +%include "base/exception.i" %include "util/unsafe_interrupt_exception.i" %include "util/integer.i" %include "util/rational.i" -//%include "util/floatingpoint.i" -%include "util/language.i" -%include "util/cardinality.i" -%include "util/bool.i" -%include "util/sexpr.i" -%include "options/options.i" -%include "util/statistics.i" -%include "util/result.i" +%include "options/language.i" %include "util/configuration.i" +%include "util/bool.i" +%include "util/cardinality.i" +%include "base/modal_exception.i" +%include "expr/sexpr.i" + %include "util/bitvector.i" -%include "util/subrange_bound.i" -%include "util/array.i" -%include "util/array_store_all.i" -%include "util/predicate.i" -%include "util/hash.i" -%include "expr/type.i" -%include "util/ascription_type.i" -%include "util/emptyset.i" -%include "util/datatype.i" -%include "util/tuple.i" -%include "util/record.i" -%include "util/regexp.i" -%include "util/uninterpreted_constant.i" + +%include "util/hash.i" %include "util/proof.i" -%include "util/resource_manager.i" -%include "util/unsat_core.i" +%include "util/regexp.i" +%include "util/subrange_bound.i" +%include "util/tuple.i" +//%include "util/floatingpoint.i" +%include "expr/uninterpreted_constant.i" +%include "expr/statistics.i" +%include "expr/array_store_all.i" +%include "expr/ascription_type.i" +%include "expr/emptyset.i" +%include "expr/datatype.i" +%include "expr/predicate.i" +%include "expr/record.i" +%include "expr/resource_manager.i" +%include "expr/result.i" +%include "proof/unsat_core.i" + +// TIM: +// Have these before the rest of expr/. +// Again, no clue why. +%include "expr/array.i" %include "expr/kind.i" +%include "expr/type.i" + +// TIM: +// The remainder of the includes: %include "expr/expr.i" -%include "expr/command.i" -%include "expr/symbol_table.i" %include "expr/expr_manager.i" %include "expr/expr_stream.i" +%include "expr/symbol_table.i" %include "expr/variable_type_map.i" - -%include "theory/logic_info.i" - -%include "smt/smt_engine.i" -%include "smt/modal_exception.i" -%include "smt/logic_exception.i" - -%include "options/options.i" %include "options/option_exception.i" - +%include "options/options.i" %include "parser/cvc4parser.i" +%include "smt/logic_exception.i" +%include "smt/smt_engine.i" +%include "smt_util/command.i" +%include "theory/logic_info.i" diff --git a/src/theory/decision_attributes.h b/src/decision/decision_attributes.h similarity index 66% rename from src/theory/decision_attributes.h rename to src/decision/decision_attributes.h index 1ea1bb21d..03229ac84 100644 --- a/src/theory/decision_attributes.h +++ b/src/decision/decision_attributes.h @@ -16,23 +16,21 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__DECISION_ATTRIBUTES -#define __CVC4__THEORY__DECISION_ATTRIBUTES +#ifndef __CVC4__DECISION__DECISION_ATTRIBUTES_H +#define __CVC4__DECISION__DECISION_ATTRIBUTES_H +#include "options/decision_weight.h" #include "expr/attribute.h" namespace CVC4 { namespace decision { -typedef uint64_t DecisionWeight; -} -namespace theory { namespace attr { struct DecisionWeightTag {}; -}/* CVC4::theory::attr namespace */ +}/* CVC4::decision::attr namespace */ -typedef expr::Attribute DecisionWeightAttr; +typedef expr::Attribute DecisionWeightAttr; -}/* CVC4::theory namespace */ +}/* CVC4::decision namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__DECISION_ATTRIBUTES */ +#endif /* __CVC4__DECISION__DECISION_ATTRIBUTES_H */ diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index d7d463d79..12400a3b1 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -13,15 +13,14 @@ ** ** Decision engine **/ - #include "decision/decision_engine.h" -#include "decision/justification_heuristic.h" +#include "decision/decision_attributes.h" +#include "decision/justification_heuristic.h" #include "expr/node.h" -#include "decision/options.h" -#include "decision/decision_mode.h" - -#include "smt/options.h" +#include "options/decision_mode.h" +#include "options/decision_options.h" +#include "options/smt_options.h" using namespace std; diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index ffcf2db63..7f1b7fbe2 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -21,16 +21,14 @@ #include +#include "base/output.h" #include "decision/decision_strategy.h" - #include "expr/node.h" #include "prop/cnf_stream.h" #include "prop/prop_engine.h" #include "prop/sat_solver_types.h" -#include "theory/decision_attributes.h" -#include "util/ite_removal.h" -#include "util/output.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 94db110c2..210628afc 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 "util/ite_removal.h" +#include "smt_util/ite_removal.h" namespace CVC4 { diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index 082f3cdbf..68c7379ce 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -16,17 +16,16 @@ ** ** It needs access to the simplified but non-clausal formula. **/ - #include "justification_heuristic.h" -#include "expr/node_manager.h" #include "expr/kind.h" +#include "expr/node_manager.h" +#include "options/decision_options.h" #include "theory/rewriter.h" -#include "decision/options.h" -#include "util/ite_removal.h" +#include "smt_util/ite_removal.h" -using namespace CVC4; +namespace CVC4 { JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de, context::UserContext *uc, @@ -297,7 +296,7 @@ DecisionWeight JustificationHeuristic::getWeightPolarized(TNode n, bool polarity } DecisionWeight JustificationHeuristic::getWeight(TNode n) { - if(!n.hasAttribute(theory::DecisionWeightAttr()) ) { + if(!n.hasAttribute(DecisionWeightAttr()) ) { DecisionWeightInternal combiningFn = options::decisionWeightInternal(); @@ -305,7 +304,7 @@ DecisionWeight JustificationHeuristic::getWeight(TNode n) { if(combiningFn == DECISION_WEIGHT_INTERNAL_OFF || n.getNumChildren() == 0) { if(options::decisionRandomWeight() != 0) { - n.setAttribute(theory::DecisionWeightAttr(), rand() % options::decisionRandomWeight()); + n.setAttribute(DecisionWeightAttr(), rand() % options::decisionRandomWeight()); } } else if(combiningFn == DECISION_WEIGHT_INTERNAL_MAX) { @@ -313,21 +312,21 @@ DecisionWeight JustificationHeuristic::getWeight(TNode n) { DecisionWeight dW = 0; for(TNode::iterator i=n.begin(); i != n.end(); ++i) dW = max(dW, getWeight(*i)); - n.setAttribute(theory::DecisionWeightAttr(), dW); + n.setAttribute(DecisionWeightAttr(), dW); } else if(combiningFn == DECISION_WEIGHT_INTERNAL_SUM || combiningFn == DECISION_WEIGHT_INTERNAL_USR1) { DecisionWeight dW = 0; for(TNode::iterator i=n.begin(); i != n.end(); ++i) dW = max(dW, getWeight(*i)); - n.setAttribute(theory::DecisionWeightAttr(), dW); + n.setAttribute(DecisionWeightAttr(), dW); } else { Unreachable(); } } - return n.getAttribute(theory::DecisionWeightAttr()); + return n.getAttribute(DecisionWeightAttr()); } typedef vector ChildList; @@ -711,3 +710,5 @@ JustificationHeuristic::SearchResult JustificationHeuristic::handleEmbeddedITEs( } return noSplitter ? NO_SPLITTER : DONT_KNOW; } + +} /* namespace CVC4 */ diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index e1ed431d1..5b0deca1b 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -23,17 +23,16 @@ #ifndef __CVC4__DECISION__JUSTIFICATION_HEURISTIC #define __CVC4__DECISION__JUSTIFICATION_HEURISTIC -#include "decision_engine.h" -#include "decision_strategy.h" - +#include "context/cdhashmap.h" #include "context/cdhashset.h" #include "context/cdlist.h" -#include "context/cdhashmap.h" +#include "decision/decision_attributes.h" +#include "decision/decision_engine.h" +#include "decision/decision_strategy.h" #include "expr/node.h" #include "prop/sat_solver_types.h" namespace CVC4 { - namespace decision { class JustificationHeuristic : public ITEDecisionStrategy { diff --git a/src/decision/options_handlers.h b/src/decision/options_handlers.h deleted file mode 100644 index 723fb243c..000000000 --- a/src/decision/options_handlers.h +++ /dev/null @@ -1,76 +0,0 @@ -/********************* */ -/*! \file options_handlers.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Kshitij Bansal - ** 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 Custom handlers and predicates for DecisionEngine options - ** - ** Custom handlers and predicates for DecisionEngine options. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__DECISION__OPTIONS_HANDLERS_H -#define __CVC4__DECISION__OPTIONS_HANDLERS_H - -#include "decision/decision_mode.h" -#include "main/options.h" - -namespace CVC4 { -namespace decision { - -static const std::string decisionModeHelp = "\ -Decision modes currently supported by the --decision option:\n\ -\n\ -internal (default)\n\ -+ Use the internal decision heuristics of the SAT solver\n\ -\n\ -justification\n\ -+ An ATGP-inspired justification heuristic\n\ -\n\ -justification-stoponly\n\ -+ Use the justification heuristic only to stop early, not for decisions\n\ -"; - -inline DecisionMode stringToDecisionMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - options::decisionStopOnly.set(false); - - if(optarg == "internal") { - return DECISION_STRATEGY_INTERNAL; - } else if(optarg == "justification") { - return DECISION_STRATEGY_JUSTIFICATION; - } else if(optarg == "justification-stoponly") { - options::decisionStopOnly.set(true); - return DECISION_STRATEGY_JUSTIFICATION; - } else if(optarg == "help") { - puts(decisionModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --decision: `") + - optarg + "'. Try --decision help."); - } -} - -inline DecisionWeightInternal stringToDecisionWeightInternal(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "off") - return DECISION_WEIGHT_INTERNAL_OFF; - else if(optarg == "max") - return DECISION_WEIGHT_INTERNAL_MAX; - else if(optarg == "sum") - return DECISION_WEIGHT_INTERNAL_SUM; - else if(optarg == "usr1") - return DECISION_WEIGHT_INTERNAL_USR1; - else - throw OptionException(std::string("--decision-weight-internal must be off, max or sum.")); -} - -}/* CVC4::decision namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__DECISION__OPTIONS_HANDLERS_H */ diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index c5a032abc..dc6ad5833 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -3,41 +3,75 @@ AM_CPPFLAGS = \ -I@builddir@/.. -I@srcdir@/../include -I@srcdir@/.. AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) +#noinst_LTLIBRARIES = libexpr.la libstatistics.la noinst_LTLIBRARIES = libexpr.la +# libstatistics_la_CPPFLAGS = $(CPPFLAGS) $(AM_CPPFLAGS) -D__BUILDING_STATISTICS_FOR_EXPORT +# libstatistics_la_SOURCES = \ +# statistics_registry.h \ +# statistics_registry.cpp + +# EXTRA_libstatistics_la_DEPENDENCIES = \ +# builts + +# For some reason statistics were in libutil. No idea why though. libexpr_la_SOURCES = \ - node.h \ + statistics.cpp \ + statistics.h \ + statistics_registry.cpp \ + statistics_registry.h \ + array.h \ + array_store_all.cpp \ + array_store_all.h \ + ascription_type.h \ + attribute.h \ + attribute.cpp \ + attribute_internals.h \ + attribute_unique_id.h \ + convenience_node_builders.h \ + chain.h \ + emptyset.cpp \ + emptyset.h \ + expr_manager_scope.h \ + expr_stream.h \ + kind_map.h \ + matcher.h \ node.cpp \ - type_node.h \ - type_node.cpp \ + node.h \ node_builder.h \ - convenience_node_builders.h \ - type.h \ - type.cpp \ - node_value.h \ - node_value.cpp \ - node_manager.h \ node_manager.cpp \ + node_manager.h \ node_manager_attributes.h \ - type_checker.h \ - attribute_unique_id.h \ - attribute.h \ - attribute_internals.h \ - attribute.cpp \ - command.h \ - command.cpp \ - symbol_table.h \ - symbol_table.cpp \ - expr_manager_scope.h \ node_self_iterator.h \ - variable_type_map.h \ - pickle_data.h \ + node_self_iterator.h \ + node_value.cpp \ + node_value.h \ pickle_data.cpp \ - pickler.h \ + pickle_data.h \ pickler.cpp \ - node_self_iterator.h \ - expr_stream.h \ - kind_map.h + pickler.h \ + resource_manager.cpp \ + resource_manager.h \ + sexpr.cpp \ + sexpr.h \ + symbol_table.cpp \ + symbol_table.h \ + type.cpp \ + type.h \ + type_checker.h \ + type_node.cpp \ + type_node.h \ + variable_type_map.h \ + datatype.h \ + datatype.cpp \ + predicate.h \ + predicate.cpp \ + record.cpp \ + record.h \ + result.cpp \ + result.h \ + uninterpreted_constant.cpp \ + uninterpreted_constant.h nodist_libexpr_la_SOURCES = \ kind.h \ @@ -50,6 +84,12 @@ nodist_libexpr_la_SOURCES = \ type_checker.cpp EXTRA_DIST = \ + array.i \ + chain.i \ + array_store_all.i \ + ascription_type.i \ + datatype.i \ + emptyset.i \ kind_template.h \ metakind_template.h \ type_properties_template.h \ @@ -58,18 +98,23 @@ EXTRA_DIST = \ expr_template.h \ expr_template.cpp \ type_checker_template.cpp \ - options_handlers.h \ mkkind \ mkmetakind \ mkexpr \ expr_stream.i \ expr_manager.i \ symbol_table.i \ - command.i \ + statistics.i \ type.i \ kind.i \ expr.i \ - variable_type_map.i + resource_manager.i \ + sexpr.i \ + record.i \ + result.i \ + predicate.i \ + variable_type_map.i \ + uninterpreted_constant.i BUILT_SOURCES = \ kind.h \ diff --git a/src/util/array.h b/src/expr/array.h similarity index 100% rename from src/util/array.h rename to src/expr/array.h diff --git a/src/expr/array.i b/src/expr/array.i new file mode 100644 index 000000000..4acd7bf0c --- /dev/null +++ b/src/expr/array.i @@ -0,0 +1,5 @@ +%{ +#include "expr/array.h" +%} + +%include "expr/array.h" diff --git a/src/util/array_store_all.cpp b/src/expr/array_store_all.cpp similarity index 96% rename from src/util/array_store_all.cpp rename to src/expr/array_store_all.cpp index dfd021e75..62c8ec978 100644 --- a/src/util/array_store_all.cpp +++ b/src/expr/array_store_all.cpp @@ -16,7 +16,8 @@ ** the same for all indices). **/ -#include "util/array_store_all.h" +#include "expr/array_store_all.h" + #include using namespace std; diff --git a/src/util/array_store_all.h b/src/expr/array_store_all.h similarity index 100% rename from src/util/array_store_all.h rename to src/expr/array_store_all.h diff --git a/src/util/array_store_all.i b/src/expr/array_store_all.i similarity index 90% rename from src/util/array_store_all.i rename to src/expr/array_store_all.i index aee550314..b66e4a178 100644 --- a/src/util/array_store_all.i +++ b/src/expr/array_store_all.i @@ -1,5 +1,5 @@ %{ -#include "util/array_store_all.h" +#include "expr/array_store_all.h" %} %rename(equals) CVC4::ArrayStoreAll::operator==(const ArrayStoreAll&) const; @@ -14,4 +14,4 @@ %ignore CVC4::operator<<(std::ostream&, const ArrayStoreAll&); %include "expr/type.i" -%include "util/array_store_all.h" +%include "expr/array_store_all.h" diff --git a/src/util/ascription_type.h b/src/expr/ascription_type.h similarity index 100% rename from src/util/ascription_type.h rename to src/expr/ascription_type.h diff --git a/src/util/ascription_type.i b/src/expr/ascription_type.i similarity index 81% rename from src/util/ascription_type.i rename to src/expr/ascription_type.i index fe8856bcc..57d8f97fe 100644 --- a/src/util/ascription_type.i +++ b/src/expr/ascription_type.i @@ -1,5 +1,5 @@ %{ -#include "util/ascription_type.h" +#include "expr/ascription_type.h" %} %rename(equals) CVC4::AscriptionType::operator==(const AscriptionType&) const; @@ -9,4 +9,4 @@ %ignore CVC4::operator<<(std::ostream&, AscriptionType); -%include "util/ascription_type.h" +%include "expr/ascription_type.h" diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp index 63ea770ca..cd5b35384 100644 --- a/src/expr/attribute.cpp +++ b/src/expr/attribute.cpp @@ -13,14 +13,13 @@ ** ** AttributeManager implementation. **/ +#include +#include "base/output.h" #include "expr/attribute.h" #include "expr/node_value.h" -#include "util/output.h" #include "smt/smt_engine.h" -#include - using namespace std; namespace CVC4 { diff --git a/src/util/chain.h b/src/expr/chain.h similarity index 100% rename from src/util/chain.h rename to src/expr/chain.h diff --git a/src/util/chain.i b/src/expr/chain.i similarity index 84% rename from src/util/chain.i rename to src/expr/chain.i index 1c97a527f..8de1665ce 100644 --- a/src/util/chain.i +++ b/src/expr/chain.i @@ -1,5 +1,5 @@ %{ -#include "util/chain.h" +#include "expr/chain.h" %} %rename(equals) CVC4::Chain::operator==(const Chain&) const; @@ -9,4 +9,4 @@ %rename(apply) CVC4::ChainHashFunction::operator()(const CVC4::Chain&) const; -%include "util/chain.h" +%include "expr/chain.h" diff --git a/src/util/datatype.cpp b/src/expr/datatype.cpp similarity index 99% rename from src/util/datatype.cpp rename to src/expr/datatype.cpp index a53759c08..c758fe297 100644 --- a/src/util/datatype.cpp +++ b/src/expr/datatype.cpp @@ -14,19 +14,19 @@ ** A class representing a Datatype definition for the theory of ** inductive datatypes. **/ +#include "expr/datatype.h" #include #include -#include "util/datatype.h" -#include "expr/type.h" +#include "base/cvc4_assert.h" +#include "expr/attribute.h" #include "expr/expr_manager.h" #include "expr/expr_manager_scope.h" -#include "expr/node_manager.h" +#include "expr/matcher.h" #include "expr/node.h" -#include "expr/attribute.h" -#include "util/matcher.h" -#include "util/cvc4_assert.h" +#include "expr/node_manager.h" +#include "expr/type.h" using namespace std; diff --git a/src/util/datatype.h b/src/expr/datatype.h similarity index 99% rename from src/util/datatype.h rename to src/expr/datatype.h index 85668cd55..c1ec475e5 100644 --- a/src/util/datatype.h +++ b/src/expr/datatype.h @@ -31,10 +31,11 @@ namespace CVC4 { class CVC4_PUBLIC Datatype; }/* CVC4 namespace */ +#include "base/exception.h" #include "expr/expr.h" #include "expr/type.h" #include "util/hash.h" -#include "util/exception.h" + namespace CVC4 { diff --git a/src/util/datatype.i b/src/expr/datatype.i similarity index 99% rename from src/util/datatype.i rename to src/expr/datatype.i index 403fb31bc..a7456df38 100644 --- a/src/util/datatype.i +++ b/src/expr/datatype.i @@ -1,5 +1,5 @@ %{ -#include "util/datatype.h" +#include "expr/datatype.h" #ifdef SWIGJAVA @@ -162,7 +162,7 @@ #endif /* SWIGJAVA */ -%include "util/datatype.h" +%include "expr/datatype.h" #ifdef SWIGJAVA diff --git a/src/util/emptyset.cpp b/src/expr/emptyset.cpp similarity index 94% rename from src/util/emptyset.cpp rename to src/expr/emptyset.cpp index 7905f11fb..69e34b848 100644 --- a/src/util/emptyset.cpp +++ b/src/expr/emptyset.cpp @@ -15,10 +15,9 @@ ** \todo document this file **/ -#include "util/emptyset.h" -#include +#include "expr/emptyset.h" -using namespace std; +#include namespace CVC4 { diff --git a/src/util/emptyset.h b/src/expr/emptyset.h similarity index 100% rename from src/util/emptyset.h rename to src/expr/emptyset.h diff --git a/src/util/emptyset.i b/src/expr/emptyset.i similarity index 91% rename from src/util/emptyset.i rename to src/expr/emptyset.i index ce4f3a4b7..ada3dd583 100644 --- a/src/util/emptyset.i +++ b/src/expr/emptyset.i @@ -1,5 +1,5 @@ %{ -#include "util/emptyset.h" +#include "expr/emptyset.h" %} %rename(equals) CVC4::EmptySet::operator==(const EmptySet&) const; @@ -14,4 +14,4 @@ %ignore CVC4::operator<<(std::ostream& out, const EmptySet& es); -%include "util/emptyset.h" +%include "expr/emptyset.h" diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 91387bc41..e7088a395 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -14,14 +14,15 @@ ** Public-facing expression manager interface, implementation. **/ -#include "expr/node_manager.h" #include "expr/expr_manager.h" -#include "expr/variable_type_map.h" -#include "options/options.h" -#include "util/statistics_registry.h" #include +#include "expr/node_manager.h" +#include "expr/statistics_registry.h" +#include "expr/variable_type_map.h" +#include "options/options.h" + ${includes} // This is a hack, but an important one: if there's an error, the diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index d7c89ecdc..31983d5a9 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -21,12 +21,11 @@ #include +#include "expr/expr.h" #include "expr/kind.h" #include "expr/type.h" -#include "expr/expr.h" +#include "expr/statistics.h" #include "util/subrange_bound.h" -#include "util/statistics.h" -#include "util/sexpr.h" ${includes} @@ -34,7 +33,7 @@ ${includes} // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 38 "${template}" +#line 37 "${template}" namespace CVC4 { diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 47042b458..0739e3355 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -14,11 +14,11 @@ ** Public-facing expression interface, implementation. **/ +#include "base/cvc4_assert.h" #include "expr/expr.h" #include "expr/node.h" #include "expr/expr_manager_scope.h" #include "expr/variable_type_map.h" -#include "util/cvc4_assert.h" #include "expr/node_manager_attributes.h" #include diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index ae0fad897..f609d8990 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -26,21 +26,22 @@ ${includes} #ifndef __CVC4__EXPR_H #define __CVC4__EXPR_H -#include +#include #include #include -#include -#include "util/exception.h" -#include "util/language.h" +#include + +#include "base/exception.h" +#include "options/expr_options.h" +#include "options/language.h" #include "util/hash.h" -#include "expr/options.h" // This is a hack, but an important one: if there's an error, the // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 44 "${template}" +#line 45 "${template}" namespace CVC4 { @@ -934,7 +935,7 @@ public: ${getConst_instantiations} -#line 938 "${template}" +#line 939 "${template}" namespace expr { diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index f93df4132..c2ccb6b5e 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -22,7 +22,7 @@ #include #include -#include "util/exception.h" +#include "base/exception.h" namespace CVC4 { namespace kind { diff --git a/src/util/matcher.h b/src/expr/matcher.h similarity index 99% rename from src/util/matcher.h rename to src/expr/matcher.h index 107891a54..92b1ce109 100644 --- a/src/util/matcher.h +++ b/src/expr/matcher.h @@ -23,7 +23,8 @@ #include #include #include -#include "util/cvc4_assert.h" + +#include "base/cvc4_assert.h" #include "expr/node.h" #include "expr/type_node.h" diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index 73f48ba04..539db1c91 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -21,8 +21,8 @@ #include +#include "base/cvc4_assert.h" #include "expr/kind.h" -#include "util/cvc4_assert.h" namespace CVC4 { diff --git a/src/expr/node.cpp b/src/expr/node.cpp index deceda840..2b5c0a2c8 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -13,14 +13,15 @@ ** ** Reference-counted encapsulation of a pointer to node information. **/ - #include "expr/node.h" -#include "expr/attribute.h" -#include "util/output.h" #include #include +#include "base/output.h" +#include "expr/attribute.h" + + using namespace std; namespace CVC4 { diff --git a/src/expr/node.h b/src/expr/node.h index 2a884d35a..384dbcc03 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -30,15 +30,15 @@ #include #include +#include "base/cvc4_assert.h" +#include "base/exception.h" +#include "base/output.h" #include "expr/type.h" #include "expr/kind.h" #include "expr/metakind.h" #include "expr/expr.h" -#include "util/cvc4_assert.h" +#include "options/language.h" #include "util/configuration.h" -#include "util/output.h" -#include "util/exception.h" -#include "util/language.h" #include "util/utility.h" #include "util/hash.h" diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index bea51b576..e1a083a78 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -169,11 +169,12 @@ namespace CVC4 { class NodeManager; }/* CVC4 namespace */ +#include "base/cvc4_assert.h" +#include "base/output.h" #include "expr/kind.h" #include "expr/metakind.h" -#include "util/cvc4_assert.h" #include "expr/node_value.h" -#include "util/output.h" + namespace CVC4 { @@ -751,7 +752,7 @@ public: #include "expr/node.h" #include "expr/node_manager.h" -#include "expr/options.h" +#include "options/expr_options.h" namespace CVC4 { diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index dad21e90a..1b9bfcd10 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -15,24 +15,23 @@ ** ** Reviewed by Chris Conway, Apr 5 2010 (bug #65). **/ - #include "expr/node_manager.h" -#include "expr/node_manager_attributes.h" - -#include "expr/attribute.h" -#include "util/cvc4_assert.h" -#include "options/options.h" -#include "smt/options.h" -#include "util/statistics_registry.h" -#include "util/resource_manager.h" -#include "util/tls.h" - -#include "expr/type_checker.h" #include +#include #include #include -#include + +#include "base/cvc4_assert.h" +#include "base/tls.h" +#include "expr/attribute.h" +#include "expr/node_manager_attributes.h" +#include "expr/type_checker.h" +#include "options/options.h" +#include "options/smt_options.h" +#include "expr/resource_manager.h" +#include "expr/statistics_registry.h" + using namespace std; using namespace CVC4::expr; diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index f52c7732f..390af8967 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -32,11 +32,11 @@ #include #include +#include "base/tls.h" #include "expr/kind.h" #include "expr/metakind.h" #include "expr/node_value.h" #include "util/subrange_bound.h" -#include "util/tls.h" #include "options/options.h" namespace CVC4 { @@ -940,24 +940,25 @@ public: class NodeManagerScope { /** The old NodeManager, to be restored on destruction. */ NodeManager* d_oldNodeManager; - + Options::OptionsScope d_optionsScope; public: - NodeManagerScope(NodeManager* nm) : - d_oldNodeManager(NodeManager::s_current) { + NodeManagerScope(NodeManager* nm) + : d_oldNodeManager(NodeManager::s_current) + , d_optionsScope(nm ? nm->d_options : NULL) { // There are corner cases where nm can be NULL and it's ok. // For example, if you write { Expr e; }, then when the null // Expr is destructed, there's no active node manager. //Assert(nm != NULL); NodeManager::s_current = nm; - Options::s_current = nm ? nm->d_options : NULL; + //Options::s_current = nm ? nm->d_options : NULL; Debug("current") << "node manager scope: " << NodeManager::s_current << "\n"; } ~NodeManagerScope() { NodeManager::s_current = d_oldNodeManager; - Options::s_current = d_oldNodeManager ? d_oldNodeManager->d_options : NULL; + //Options::s_current = d_oldNodeManager ? d_oldNodeManager->d_options : NULL; Debug("current") << "node manager scope: " << "returning to " << NodeManager::s_current << "\n"; } diff --git a/src/expr/node_self_iterator.h b/src/expr/node_self_iterator.h index 401cc6152..77fc05e3b 100644 --- a/src/expr/node_self_iterator.h +++ b/src/expr/node_self_iterator.h @@ -21,7 +21,7 @@ #include -#include "util/cvc4_assert.h" +#include "base/cvc4_assert.h" #include "expr/node.h" namespace CVC4 { diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index 6b48fd9b7..dbe7d09eb 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -17,15 +17,16 @@ ** cvc4::Node rather than by pointer; cvc4::Node maintains the ** reference count on NodeValue instances and **/ - #include "expr/node_value.h" -#include "expr/node.h" + +#include + #include "expr/kind.h" #include "expr/metakind.h" -#include "util/language.h" +#include "expr/node.h" +#include "options/language.h" #include "options/options.h" #include "printer/printer.h" -#include using namespace std; diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 785f8909f..c39c14604 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -26,12 +26,13 @@ #ifndef __CVC4__EXPR__NODE_VALUE_H #define __CVC4__EXPR__NODE_VALUE_H -#include "expr/kind.h" -#include "util/language.h" - #include -#include + #include +#include + +#include "expr/kind.h" +#include "options/language.h" namespace CVC4 { diff --git a/src/expr/options_handlers.h b/src/expr/options_handlers.h deleted file mode 100644 index e2a92ade7..000000000 --- a/src/expr/options_handlers.h +++ /dev/null @@ -1,69 +0,0 @@ -/********************* */ -/*! \file options_handlers.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 Custom handlers and predicates for expression package options - ** - ** Custom handlers and predicates for expression package options. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__EXPR__OPTIONS_HANDLERS_H -#define __CVC4__EXPR__OPTIONS_HANDLERS_H - -#include "util/output.h" -#include "util/dump.h" - -namespace CVC4 { -namespace expr { - -inline void setDefaultExprDepth(std::string option, int depth, SmtEngine* smt) { - if(depth < -1) { - throw OptionException("--default-expr-depth requires a positive argument, or -1."); - } - - Debug.getStream() << Expr::setdepth(depth); - Trace.getStream() << Expr::setdepth(depth); - Notice.getStream() << Expr::setdepth(depth); - Chat.getStream() << Expr::setdepth(depth); - Message.getStream() << Expr::setdepth(depth); - Warning.getStream() << Expr::setdepth(depth); - // intentionally exclude Dump stream from this list -} - -inline void setDefaultDagThresh(std::string option, int dag, SmtEngine* smt) { - if(dag < 0) { - throw OptionException("--default-dag-thresh requires a nonnegative argument."); - } - - Debug.getStream() << Expr::dag(dag); - Trace.getStream() << Expr::dag(dag); - Notice.getStream() << Expr::dag(dag); - Chat.getStream() << Expr::dag(dag); - Message.getStream() << Expr::dag(dag); - Warning.getStream() << Expr::dag(dag); - Dump.getStream() << Expr::dag(dag); -} - -inline void setPrintExprTypes(std::string option, SmtEngine* smt) { - Debug.getStream() << Expr::printtypes(true); - Trace.getStream() << Expr::printtypes(true); - Notice.getStream() << Expr::printtypes(true); - Chat.getStream() << Expr::printtypes(true); - Message.getStream() << Expr::printtypes(true); - Warning.getStream() << Expr::printtypes(true); - // intentionally exclude Dump stream from this list -} - -}/* CVC4::expr namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__EXPR__OPTIONS_HANDLERS_H */ diff --git a/src/expr/pickle_data.cpp b/src/expr/pickle_data.cpp index 6f47f9207..e273bcece 100644 --- a/src/expr/pickle_data.cpp +++ b/src/expr/pickle_data.cpp @@ -22,6 +22,7 @@ #include #include +#include "base/cvc4_assert.h" #include "expr/pickle_data.h" #include "expr/expr.h" #include "expr/node.h" @@ -29,7 +30,6 @@ #include "expr/node_value.h" #include "expr/expr_manager_scope.h" #include "expr/variable_type_map.h" -#include "util/cvc4_assert.h" #include "expr/kind.h" #include "expr/metakind.h" diff --git a/src/expr/pickler.cpp b/src/expr/pickler.cpp index 20e8859e3..d0501ca2b 100644 --- a/src/expr/pickler.cpp +++ b/src/expr/pickler.cpp @@ -20,6 +20,8 @@ #include #include +#include "base/cvc4_assert.h" +#include "base/output.h" #include "expr/pickler.h" #include "expr/pickle_data.h" #include "expr/expr.h" @@ -28,10 +30,8 @@ #include "expr/node_value.h" #include "expr/expr_manager_scope.h" #include "expr/variable_type_map.h" -#include "util/cvc4_assert.h" #include "expr/kind.h" #include "expr/metakind.h" -#include "util/output.h" namespace CVC4 { namespace expr { diff --git a/src/expr/pickler.h b/src/expr/pickler.h index 8c3da5f40..cf1754d93 100644 --- a/src/expr/pickler.h +++ b/src/expr/pickler.h @@ -23,7 +23,7 @@ #include "expr/variable_type_map.h" #include "expr/expr.h" -#include "util/exception.h" +#include "base/exception.h" #include #include diff --git a/src/util/predicate.cpp b/src/expr/predicate.cpp similarity index 96% rename from src/util/predicate.cpp rename to src/expr/predicate.cpp index 787d329aa..b88951bf9 100644 --- a/src/util/predicate.cpp +++ b/src/expr/predicate.cpp @@ -15,10 +15,11 @@ ** Instances of this class are carried as the payload of ** the CONSTANT-metakinded SUBTYPE_TYPE types. **/ +#include "expr/predicate.h" +#include "base/cvc4_assert.h" #include "expr/expr.h" -#include "util/predicate.h" -#include "util/cvc4_assert.h" + using namespace std; diff --git a/src/util/predicate.h b/src/expr/predicate.h similarity index 91% rename from src/util/predicate.h rename to src/expr/predicate.h index 5ead2f090..cc3e8b576 100644 --- a/src/util/predicate.h +++ b/src/expr/predicate.h @@ -21,7 +21,7 @@ #ifndef __CVC4__PREDICATE_H #define __CVC4__PREDICATE_H -#include "util/exception.h" +#include "base/exception.h" namespace CVC4 { @@ -35,6 +35,8 @@ struct CVC4_PUBLIC PredicateHashFunction { }/* CVC4 namespace */ +// TIM: This needs to be here due to a circular dependency. +#warning "TODO: Track down the circular dependence on expr.h." #include "expr/expr.h" namespace CVC4 { diff --git a/src/util/predicate.i b/src/expr/predicate.i similarity index 83% rename from src/util/predicate.i rename to src/expr/predicate.i index eedbb2e83..aa80a98b5 100644 --- a/src/util/predicate.i +++ b/src/expr/predicate.i @@ -1,5 +1,5 @@ %{ -#include "util/predicate.h" +#include "expr/predicate.h" %} %rename(equals) CVC4::Predicate::operator==(const Predicate&) const; @@ -9,4 +9,4 @@ %ignore CVC4::operator<<(std::ostream&, const Predicate&); -%include "util/predicate.h" +%include "expr/predicate.h" diff --git a/src/util/record.cpp b/src/expr/record.cpp similarity index 95% rename from src/util/record.cpp rename to src/expr/record.cpp index ea9b5495a..dfcba0d46 100644 --- a/src/util/record.cpp +++ b/src/expr/record.cpp @@ -14,9 +14,7 @@ ** A class representing a record definition. **/ -#include "util/record.h" - -using namespace std; +#include "expr/record.h" namespace CVC4 { diff --git a/src/util/record.h b/src/expr/record.h similarity index 98% rename from src/util/record.h rename to src/expr/record.h index 5689a4209..a255649da 100644 --- a/src/util/record.h +++ b/src/expr/record.h @@ -74,6 +74,7 @@ inline std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) { }/* CVC4 namespace */ +#warning "TODO: Address circular dependence in Record." #include "expr/expr.h" #include "expr/type.h" diff --git a/src/util/record.i b/src/expr/record.i similarity index 98% rename from src/util/record.i rename to src/expr/record.i index 0cc1bc579..283f01106 100644 --- a/src/util/record.i +++ b/src/expr/record.i @@ -1,5 +1,5 @@ %{ -#include "util/record.h" +#include "expr/record.h" #ifdef SWIGJAVA @@ -98,7 +98,7 @@ #endif /* SWIGJAVA */ -%include "util/record.h" +%include "expr/record.h" #ifdef SWIGJAVA diff --git a/src/util/resource_manager.cpp b/src/expr/resource_manager.cpp similarity index 96% rename from src/util/resource_manager.cpp rename to src/expr/resource_manager.cpp index 22496a433..f36200282 100644 --- a/src/util/resource_manager.cpp +++ b/src/expr/resource_manager.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file resource_manager.h +/*! \file resource_manager.cpp ** \verbatim ** Original author: Liana Hadarean ** Major contributors: none @@ -13,16 +13,20 @@ ** ** Manages and updates various resource and time limits. **/ +#include "expr/resource_manager.h" -#include "util/resource_manager.h" -#include "util/output.h" +#include "base/output.h" +#include "options/smt_options.h" #include "smt/smt_engine_scope.h" -#include "smt/options.h" #include "theory/rewriter.h" -using namespace CVC4; +#warning "TODO: Break the dependence of the ResourceManager on the theory" +#warning "rewriter and scope. Move this file back into util/ afterwards." + using namespace std; +namespace CVC4 { + void Timer::set(uint64_t millis, bool wallTime) { d_ms = millis; Trace("limit") << "Timer::set(" << d_ms << ")" << std::endl; @@ -283,3 +287,5 @@ void ResourceManager::enable(bool on) { Trace("limit") << "ResourceManager::enable("<< on <<")\n"; d_on = on; } + +} /* namespace CVC4 */ diff --git a/src/util/resource_manager.h b/src/expr/resource_manager.h similarity index 99% rename from src/util/resource_manager.h rename to src/expr/resource_manager.h index e84917db0..c4ad35564 100644 --- a/src/util/resource_manager.h +++ b/src/expr/resource_manager.h @@ -22,7 +22,7 @@ #include #include -#include "util/exception.h" +#include "base/exception.h" #include "util/unsafe_interrupt_exception.h" namespace CVC4 { diff --git a/src/expr/resource_manager.i b/src/expr/resource_manager.i new file mode 100644 index 000000000..77edbd8c3 --- /dev/null +++ b/src/expr/resource_manager.i @@ -0,0 +1,5 @@ +%{ +#include "expr/resource_manager.h" +%} + +%include "expr/resource_manager.h" diff --git a/src/util/result.cpp b/src/expr/result.cpp similarity index 69% rename from src/util/result.cpp rename to src/expr/result.cpp index 91b671262..95e382b98 100644 --- a/src/util/result.cpp +++ b/src/expr/result.cpp @@ -13,18 +13,20 @@ ** ** Encapsulation of the result of a query. **/ +#include "expr/result.h" -#include #include -#include #include +#include +#include -#include "util/result.h" -#include "util/cvc4_assert.h" -#include "printer/printer.h" +#include "base/cvc4_assert.h" +#include "expr/node.h" using namespace std; +#warning "TODO: Move Node::setLanguage out of Node and into util/. Then move Result back into util/." + namespace CVC4 { Result::Result(const std::string& instr, std::string inputName) : @@ -185,8 +187,7 @@ ostream& operator<<(ostream& out, enum Result::Validity v) { return out; } -ostream& operator<<(ostream& out, - enum Result::UnknownExplanation e) { +ostream& operator<<(ostream& out, enum Result::UnknownExplanation e) { switch(e) { case Result::REQUIRES_FULL_CHECK: out << "REQUIRES_FULL_CHECK"; break; case Result::INCOMPLETE: out << "INCOMPLETE"; break; @@ -204,8 +205,91 @@ ostream& operator<<(ostream& out, } ostream& operator<<(ostream& out, const Result& r) { - Printer::getPrinter(Node::setlanguage::getLanguage(out))->toStream(out, r); + r.toStream(out, Node::setlanguage::getLanguage(out)); return out; }/* operator<<(ostream&, const Result&) */ + +void Result::toStreamDefault(std::ostream& out) const throw() { + if(getType() == Result::TYPE_SAT) { + switch(isSat()) { + case Result::UNSAT: + out << "unsat"; + break; + case Result::SAT: + out << "sat"; + break; + case Result::SAT_UNKNOWN: + out << "unknown"; + if(whyUnknown() != Result::UNKNOWN_REASON) { + out << " (" << whyUnknown() << ")"; + } + break; + } + } else { + switch(isValid()) { + case Result::INVALID: + out << "invalid"; + break; + case Result::VALID: + out << "valid"; + break; + case Result::VALIDITY_UNKNOWN: + out << "unknown"; + if(whyUnknown() != Result::UNKNOWN_REASON) { + out << " (" << whyUnknown() << ")"; + } + break; + } + } +}/* Result::toStreamDefault() */ + + +void Result::toStreamSmt2(ostream& out) const throw(){ + if(getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN) { + out << "unknown"; + } else { + toStreamDefault(out); + } +} + +void Result::toStreamTptp(std::ostream& out) const throw() { + out << "% SZS status "; + if(isSat() == Result::SAT) { + out << "Satisfiable"; + } else if(isSat() == Result::UNSAT) { + out << "Unsatisfiable"; + } else if(isValid() == Result::VALID) { + out << "Theorem"; + } else if(isValid() == Result::INVALID) { + out << "CounterSatisfiable"; + } else { + out << "GaveUp"; + } + out << " for " << getInputName(); +} + +void Result::toStream(std::ostream& out, OutputLanguage language) const throw() { + switch(language) { + case language::output::LANG_SMTLIB_V2_0: + case language::output::LANG_SMTLIB_V2_5: + case language::output::LANG_SYGUS: + case language::output::LANG_Z3STR: + toStreamSmt2(out); + break; + case language::output::LANG_TPTP: + toStreamTptp(out); + break; + case language::output::LANG_AST: + case language::output::LANG_AUTO: + case language::output::LANG_CVC3: + case language::output::LANG_CVC4: + case language::output::LANG_MAX: + case language::output::LANG_SMTLIB_V1: + default: + toStreamDefault(out); + break; + }; +} + }/* CVC4 namespace */ diff --git a/src/util/result.h b/src/expr/result.h similarity index 84% rename from src/util/result.h rename to src/expr/result.h index 8c804daa7..74697eba6 100644 --- a/src/util/result.h +++ b/src/expr/result.h @@ -22,7 +22,8 @@ #include #include -#include "util/exception.h" +#include "base/exception.h" +#include "options/language.h" namespace CVC4 { @@ -155,6 +156,32 @@ public: std::string getInputName() const { return d_inputName; } + /** + * Write a Result out to a stream in this language. + */ + void toStream(std::ostream& out, OutputLanguage language) const throw(); + + /** + * This is mostly the same the default + * If getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN, + * + */ + void toStreamSmt2(std::ostream& out) const throw(); + + /** + * Write a Result out to a stream in the Tptp format + */ + void toStreamTptp(std::ostream& out) const throw(); + + /** + * Write a Result out to a stream. + * + * The default implementation writes a reasonable string in lowercase + * for sat, unsat, valid, invalid, or unknown results. This behavior + * is overridable by each Printer, since sometimes an output language + * has a particular preference for how results should appear. + */ + void toStreamDefault(std::ostream& out) const throw(); };/* class Result */ inline bool Result::operator!=(const Result& r) const throw() { diff --git a/src/util/result.i b/src/expr/result.i similarity index 92% rename from src/util/result.i rename to src/expr/result.i index b77bfd881..becbe9aa9 100644 --- a/src/util/result.i +++ b/src/expr/result.i @@ -1,5 +1,5 @@ %{ -#include "util/result.h" +#include "expr/result.h" %} %ignore CVC4::operator<<(std::ostream&, const Result& r); @@ -17,4 +17,4 @@ %ignore CVC4::operator==(enum Result::Validity, const Result&); %ignore CVC4::operator!=(enum Result::Validity, const Result&); -%include "util/result.h" +%include "expr/result.h" diff --git a/src/expr/sexpr.cpp b/src/expr/sexpr.cpp new file mode 100644 index 000000000..a321f85aa --- /dev/null +++ b/src/expr/sexpr.cpp @@ -0,0 +1,233 @@ +/********************* */ +/*! \file sexpr.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 Simple representation of S-expressions + ** + ** Simple representation of S-expressions. + ** + ** SExprs have their own language specific printing procedures. The reason for + ** this being implemented on SExpr and not on the Printer class is that the + ** Printer class lives in libcvc4. It has to currently as it prints fairly + ** complicated objects, like Model, which in turn uses SmtEngine pointers. + ** However, SExprs need to be printed by Statistics. To get the output consistent + ** with the previous version, the printing of SExprs in different languages is + ** handled in the SExpr class and the libexpr library. + **/ + +#include "expr/sexpr.h" + +#include +#include +#include + +#include "base/cvc4_assert.h" +#include "expr/expr.h" +#include "util/smt2_quote_string.h" + + +namespace CVC4 { + +const int PrettySExprs::s_iosIndex = std::ios_base::xalloc(); + +std::ostream& operator<<(std::ostream& out, PrettySExprs ps) { + ps.applyPrettySExprs(out); + return out; +} + +std::string SExpr::toString() const { + std::stringstream ss; + ss << (*this); + return ss.str(); +} + +std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) { + SExpr::toStream(out, sexpr); + return out; +} + +void SExpr::toStream(std::ostream& out, const SExpr& sexpr) throw() { + toStream(out, sexpr, Expr::setlanguage::getLanguage(out)); +} + +void SExpr::toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language) throw() { + toStream(out, sexpr, language, PrettySExprs::getPrettySExprs(out) ? 2 : 0); +} + +void SExpr::toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language, int indent) throw() { + if( sexpr.isKeyword() && languageQuotesKeywords(language) ){ + out << quoteSymbol(sexpr.getValue()); + } else { + toStreamRec(out, sexpr, language, indent); + } +} + + +void SExpr::toStreamRec(std::ostream& out, const SExpr& sexpr, OutputLanguage language, int indent) throw() { + if(sexpr.isInteger()) { + out << sexpr.getIntegerValue(); + } else if(sexpr.isRational()) { + out << std::fixed << sexpr.getRationalValue().getDouble(); + } else if(sexpr.isKeyword()) { + out << sexpr.getValue(); + } else if(sexpr.isString()) { + std::string s = sexpr.getValue(); + // escape backslash and quote + for(size_t i = 0; i < s.length(); ++i) { + if(s[i] == '"') { + s.replace(i, 1, "\\\""); + ++i; + } else if(s[i] == '\\') { + s.replace(i, 1, "\\\\"); + ++i; + } + } + out << "\"" << s << "\""; + } else { + const std::vector& kids = sexpr.getChildren(); + out << (indent > 0 && kids.size() > 1 ? "( " : "("); + bool first = true; + for(std::vector::const_iterator i = kids.begin(); i != kids.end(); ++i) { + if(first) { + first = false; + } else { + if(indent > 0) { + out << "\n" << std::string(indent, ' '); + } else { + out << ' '; + } + } + toStreamRec(out, *i, language, indent <= 0 || indent > 2 ? 0 : indent + 2); + } + if(indent > 0 && kids.size() > 1) { + out << '\n'; + if(indent > 2) { + out << std::string(indent - 2, ' '); + } + } + out << ')'; + } +}/* toStreamRec() */ + + +bool SExpr::languageQuotesKeywords(OutputLanguage language) { + switch(language) { + case language::output::LANG_SMTLIB_V1: + case language::output::LANG_SMTLIB_V2_0: + case language::output::LANG_SMTLIB_V2_5: + case language::output::LANG_SYGUS: + case language::output::LANG_TPTP: + case language::output::LANG_Z3STR: + return true; + case language::output::LANG_AST: + case language::output::LANG_CVC3: + case language::output::LANG_CVC4: + default: + return false; + }; +} + + + +std::string SExpr::getValue() const { + CheckArgument( isAtom(), this ); + switch(d_sexprType) { + case SEXPR_INTEGER: + return d_integerValue.toString(); + case SEXPR_RATIONAL: { + // We choose to represent rationals as decimal strings rather than + // "numerator/denominator." Perhaps an additional SEXPR_DECIMAL + // could be added if we need both styles, even if it's backed by + // the same Rational object. + std::stringstream ss; + ss << std::fixed << d_rationalValue.getDouble(); + return ss.str(); + } + case SEXPR_STRING: + case SEXPR_KEYWORD: + return d_stringValue; + case SEXPR_NOT_ATOM: + return std::string(); + } + return std::string(); + +} + +const CVC4::Integer& SExpr::getIntegerValue() const { + CheckArgument( isInteger(), this ); + return d_integerValue; +} + +const CVC4::Rational& SExpr::getRationalValue() const { + CheckArgument( isRational(), this ); + return d_rationalValue; +} + +const std::vector& SExpr::getChildren() const { + CheckArgument( !isAtom(), this ); + return d_children; +} + +bool SExpr::operator==(const SExpr& s) const { + return d_sexprType == s.d_sexprType && + d_integerValue == s.d_integerValue && + d_rationalValue == s.d_rationalValue && + d_stringValue == s.d_stringValue && + d_children == s.d_children; +} + +bool SExpr::operator!=(const SExpr& s) const { + return !(*this == s); +} + + +SExpr SExpr::parseAtom(const std::string& atom) { + if(atom == "true"){ + return SExpr(true); + } else if(atom == "false"){ + return SExpr(false); + } else { + try { + Integer z(atom); + return SExpr(z); + }catch(std::invalid_argument&){ + // Fall through to the next case + } + try { + Rational q(atom); + return SExpr(q); + }catch(std::invalid_argument&){ + // Fall through to the next case + } + return SExpr(atom); + } +} + +SExpr SExpr::parseListOfAtoms(const std::vector& atoms) { + std::vector parsedAtoms; + typedef std::vector::const_iterator const_iterator; + for(const_iterator i = atoms.begin(), i_end=atoms.end(); i != i_end; ++i){ + parsedAtoms.push_back(parseAtom(*i)); + } + return SExpr(parsedAtoms); +} + +SExpr SExpr::parseListOfListOfAtoms(const std::vector< std::vector >& atoms_lists) { + std::vector parsedListsOfAtoms; + typedef std::vector< std::vector >::const_iterator const_iterator; + for(const_iterator i = atoms_lists.begin(), i_end = atoms_lists.end(); i != i_end; ++i){ + parsedListsOfAtoms.push_back(parseListOfAtoms(*i)); + } + return SExpr(parsedListsOfAtoms); +} + + + +}/* CVC4 namespace */ diff --git a/src/util/sexpr.h b/src/expr/sexpr.h similarity index 55% rename from src/util/sexpr.h rename to src/expr/sexpr.h index a121b5195..f30045c68 100644 --- a/src/util/sexpr.h +++ b/src/expr/sexpr.h @@ -26,14 +26,15 @@ #ifndef __CVC4__SEXPR_H #define __CVC4__SEXPR_H -#include -#include #include #include +#include +#include +#include "base/exception.h" +#include "options/language.h" #include "util/integer.h" #include "util/rational.h" -#include "util/exception.h" namespace CVC4 { @@ -157,7 +158,8 @@ public: * This is internally handled as the strings "true" and "false" */ SExpr(bool value) : - d_sexprType(SEXPR_STRING), +#warning "TODO: Discuss this change with Clark." + d_sexprType(SEXPR_KEYWORD), d_integerValue(0), d_rationalValue(0), d_stringValue(value ? "true" : "false"), @@ -181,19 +183,36 @@ public: } /** Is this S-expression an atom? */ - bool isAtom() const; + bool isAtom() const { + return d_sexprType != SEXPR_NOT_ATOM; + } /** Is this S-expression an integer? */ - bool isInteger() const; + bool isInteger() const { + return d_sexprType == SEXPR_INTEGER; + } /** Is this S-expression a rational? */ - bool isRational() const; + bool isRational() const { + return d_sexprType == SEXPR_RATIONAL; + } /** Is this S-expression a string? */ - bool isString() const; + bool isString() const { + return d_sexprType == SEXPR_STRING; + } /** Is this S-expression a keyword? */ - bool isKeyword() const; + bool isKeyword() const { + return d_sexprType == SEXPR_KEYWORD; + } + + /** + * This wraps the toStream() printer. + * NOTE: toString() and getValue() may differ on Keywords based on + * the current language set in expr. + */ + std::string toString() const; /** * Get the string value of this S-expression. This will cause an @@ -225,79 +244,139 @@ public: /** Is this S-expression different from another? */ bool operator!=(const SExpr& s) const; + + /** + * This returns the best match in the following order: + * match atom with + * "true", "false" -> SExpr(value) + * | is and integer -> as integer + * | is a rational -> as rational + * | _ -> SExpr() + */ + static SExpr parseAtom(const std::string& atom); + + /** + * Parses a list of atoms. + */ + static SExpr parseListOfAtoms(const std::vector& atoms); + + /** + * Parses a list of list of atoms. + */ + static SExpr parseListOfListOfAtoms(const std::vector< std::vector >& atoms_lists); + + + /** + * Outputs the SExpr onto the ostream out. This version reads defaults to the + * OutputLanguage, Expr::setlanguage::getLanguage(out). The indent level is + * set to 2 if PrettySExprs::getPrettySExprs() is on and is 0 otherwise. + */ + static void toStream(std::ostream& out, const SExpr& sexpr) throw(); + + /** + * Outputs the SExpr onto the ostream out. This version sets the indent level + * to 2 if PrettySExprs::getPrettySExprs() is on. + */ + static void toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language) throw(); + + /** + * Outputs the SExpr onto the ostream out. + * If the languageQuotesKeywords(language), then a top level keyword, " X", + * that needs quoting according to the SMT2 language standard is printed with + * quotes, "| X|". + * Otherwise this prints using toStreamRec(). + * + * TIM: Keywords that are children are not currently quoted. This seems + * incorrect but I am just reproduicing the old behavior even if it does not make + * sense. + */ + static void toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language, int indent) throw(); + +private: + + /** + * Simple printer for SExpr to an ostream. + * The current implementation is language independent. + */ + static void toStreamRec(std::ostream& out, const SExpr& sexpr, OutputLanguage language, int indent) throw(); + + + /** Returns true if this language quotes Keywords when printing. */ + static bool languageQuotesKeywords(OutputLanguage language); + };/* class SExpr */ -inline bool SExpr::isAtom() const { - return d_sexprType != SEXPR_NOT_ATOM; -} - -inline bool SExpr::isInteger() const { - return d_sexprType == SEXPR_INTEGER; -} - -inline bool SExpr::isRational() const { - return d_sexprType == SEXPR_RATIONAL; -} - -inline bool SExpr::isString() const { - return d_sexprType == SEXPR_STRING; -} - -inline bool SExpr::isKeyword() const { - return d_sexprType == SEXPR_KEYWORD; -} - -inline std::string SExpr::getValue() const { - CheckArgument( isAtom(), this ); - switch(d_sexprType) { - case SEXPR_INTEGER: - return d_integerValue.toString(); - case SEXPR_RATIONAL: { - // We choose to represent rationals as decimal strings rather than - // "numerator/denominator." Perhaps an additional SEXPR_DECIMAL - // could be added if we need both styles, even if it's backed by - // the same Rational object. - std::stringstream ss; - ss << std::fixed << d_rationalValue.getDouble(); - return ss.str(); +/** Prints an SExpr. */ +std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) CVC4_PUBLIC; + +/** + * IOStream manipulator to pretty-print SExprs. + */ +class CVC4_PUBLIC PrettySExprs { + /** + * The allocated index in ios_base for our setting. + */ + static const int s_iosIndex; + + /** + * When this manipulator is used, the setting is stored here. + */ + bool d_prettySExprs; + +public: + /** + * Construct a PrettySExprs with the given setting. + */ + PrettySExprs(bool prettySExprs) : d_prettySExprs(prettySExprs) {} + + inline void applyPrettySExprs(std::ostream& out) { + out.iword(s_iosIndex) = d_prettySExprs; } - case SEXPR_STRING: - case SEXPR_KEYWORD: - return d_stringValue; - case SEXPR_NOT_ATOM: - return std::string(); + + static inline bool getPrettySExprs(std::ostream& out) { + return out.iword(s_iosIndex); } - return std::string(); -} - -inline const CVC4::Integer& SExpr::getIntegerValue() const { - CheckArgument( isInteger(), this ); - return d_integerValue; -} - -inline const CVC4::Rational& SExpr::getRationalValue() const { - CheckArgument( isRational(), this ); - return d_rationalValue; -} - -inline const std::vector& SExpr::getChildren() const { - CheckArgument( !isAtom(), this ); - return d_children; -} - -inline bool SExpr::operator==(const SExpr& s) const { - return d_sexprType == s.d_sexprType && - d_integerValue == s.d_integerValue && - d_rationalValue == s.d_rationalValue && - d_stringValue == s.d_stringValue && - d_children == s.d_children; -} - -inline bool SExpr::operator!=(const SExpr& s) const { - return !(*this == s); -} -std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) CVC4_PUBLIC; + static inline void setPrettySExprs(std::ostream& out, bool prettySExprs) { + out.iword(s_iosIndex) = prettySExprs; + } + + /** + * Set the pretty-sexprs 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_oldPrettySExprs; + + public: + + inline Scope(std::ostream& out, bool prettySExprs) : + d_out(out), + d_oldPrettySExprs(PrettySExprs::getPrettySExprs(out)) { + PrettySExprs::setPrettySExprs(out, prettySExprs); + } + + inline ~Scope() { + PrettySExprs::setPrettySExprs(d_out, d_oldPrettySExprs); + } + + };/* class PrettySExprs::Scope */ + +};/* class PrettySExprs */ + +/** + * Sets the default pretty-sexprs setting for an ostream. Use like this: + * + * // let out be an ostream, s an SExpr + * out << PrettySExprs(true) << s << endl; + * + * The setting stays permanently (until set again) with the stream. + */ +std::ostream& operator<<(std::ostream& out, PrettySExprs ps); + }/* CVC4 namespace */ diff --git a/src/util/sexpr.i b/src/expr/sexpr.i similarity index 91% rename from src/util/sexpr.i rename to src/expr/sexpr.i index 4c89c5019..f6229782e 100644 --- a/src/util/sexpr.i +++ b/src/expr/sexpr.i @@ -1,5 +1,5 @@ %{ -#include "util/sexpr.h" +#include "expr/sexpr.h" %} %ignore CVC4::operator<<(std::ostream&, const SExpr&); @@ -18,4 +18,4 @@ %rename(equals) CVC4::SExpr::operator==(const SExpr&) const; %ignore CVC4::SExpr::operator!=(const SExpr&) const; -%include "util/sexpr.h" +%include "expr/sexpr.h" diff --git a/src/util/statistics.cpp b/src/expr/statistics.cpp similarity index 97% rename from src/util/statistics.cpp rename to src/expr/statistics.cpp index ff31e7b4b..e5d3f6e69 100644 --- a/src/util/statistics.cpp +++ b/src/expr/statistics.cpp @@ -15,11 +15,12 @@ ** \todo document this file **/ -#include "util/statistics.h" -#include "util/statistics_registry.h" // for details about class Stat - #include +#include "expr/statistics.h" +#include "expr/statistics_registry.h" // for details about class Stat + + namespace CVC4 { std::string StatisticsBase::s_regDelim("::"); diff --git a/src/util/statistics.h b/src/expr/statistics.h similarity index 99% rename from src/util/statistics.h rename to src/expr/statistics.h index a7088f5c5..425404692 100644 --- a/src/util/statistics.h +++ b/src/expr/statistics.h @@ -20,12 +20,12 @@ #ifndef __CVC4__STATISTICS_H #define __CVC4__STATISTICS_H -#include "util/sexpr.h" +#include "expr/sexpr.h" -#include +#include #include #include -#include +#include #include namespace CVC4 { diff --git a/src/util/statistics.i b/src/expr/statistics.i similarity index 98% rename from src/util/statistics.i rename to src/expr/statistics.i index bd3a4eeb9..990f465f5 100644 --- a/src/util/statistics.i +++ b/src/expr/statistics.i @@ -1,5 +1,5 @@ %{ -#include "util/statistics.h" +#include "expr/statistics.h" #ifdef SWIGJAVA @@ -67,7 +67,7 @@ #endif /* SWIGJAVA */ -%include "util/statistics.h" +%include "expr/statistics.h" #ifdef SWIGJAVA diff --git a/src/util/statistics_registry.cpp b/src/expr/statistics_registry.cpp similarity index 96% rename from src/util/statistics_registry.cpp rename to src/expr/statistics_registry.cpp index 097869bc7..c1db992c5 100644 --- a/src/util/statistics_registry.cpp +++ b/src/expr/statistics_registry.cpp @@ -15,7 +15,8 @@ ** \todo document this file **/ -#include "util/statistics_registry.h" +#include "expr/statistics_registry.h" + #include "expr/expr_manager.h" #include "lib/clock_gettime.h" #include "smt/smt_engine.h" @@ -30,6 +31,9 @@ # define __CVC4_USE_STATISTICS false #endif +#warning "TODO: Make StatisticsRegistry non-public again." +#warning "TODO: Make TimerStat non-public again." + namespace CVC4 { namespace stats { @@ -157,6 +161,8 @@ RegisterStatistic::RegisterStatistic(SmtEngine& smt, Stat* stat) : d_reg->registerStat_(d_stat); } + + }/* CVC4 namespace */ #undef __CVC4_USE_STATISTICS diff --git a/src/util/statistics_registry.h b/src/expr/statistics_registry.h similarity index 97% rename from src/util/statistics_registry.h rename to src/expr/statistics_registry.h index b9e3eaf8b..89efe4021 100644 --- a/src/util/statistics_registry.h +++ b/src/expr/statistics_registry.h @@ -21,17 +21,18 @@ #ifndef __CVC4__STATISTICS_REGISTRY_H #define __CVC4__STATISTICS_REGISTRY_H -#include "util/statistics.h" -#include "util/exception.h" -#include "lib/clock_gettime.h" +#include -#include -#include +#include #include -#include +#include #include -#include -#include +#include +#include + +#include "base/exception.h" +#include "expr/statistics.h" +#include "lib/clock_gettime.h" namespace CVC4 { @@ -108,7 +109,7 @@ public: virtual SExpr getValue() const { std::stringstream ss; flushInformation(ss); - return ss.str(); + return SExpr(ss.str()); } };/* class Stat */ @@ -122,27 +123,27 @@ template inline SExpr mkSExpr(const T& x) { std::stringstream ss; ss << x; - return ss.str(); + return SExpr(ss.str()); } template <> inline SExpr mkSExpr(const uint64_t& x) { - return Integer(x); + return SExpr(Integer(x)); } template <> inline SExpr mkSExpr(const int64_t& x) { - return Integer(x); + return SExpr(Integer(x)); } template <> inline SExpr mkSExpr(const int& x) { - return Integer(x); + return SExpr(Integer(x)); } template <> inline SExpr mkSExpr(const Integer& x) { - return x; + return SExpr(x); } template <> @@ -150,12 +151,12 @@ inline SExpr mkSExpr(const double& x) { // roundabout way to get a Rational from a double std::stringstream ss; ss << std::fixed << std::setprecision(8) << x; - return Rational::fromDecimal(ss.str()); + return SExpr(Rational::fromDecimal(ss.str())); } template <> inline SExpr mkSExpr(const Rational& x) { - return x; + return SExpr(x); } /** @@ -483,7 +484,10 @@ public: };/* class AverageStat */ /** A statistic that contains a SExpr. */ -class SExprStat : public BackedStat { +class SExprStat : public Stat { +private: + SExpr d_data; + public: /** @@ -491,7 +495,10 @@ public: * initial value. */ SExprStat(const std::string& name, const SExpr& init) : - BackedStat(name, init) { + Stat(name), d_data(init){} + + virtual void flushInformation(std::ostream& out) const { + out << d_data << std::endl; } SExpr getValue() const { @@ -587,7 +594,7 @@ public: * The main statistics registry. This registry maintains the list of * currently active statistics and is able to "flush" them all. */ -class StatisticsRegistry : public StatisticsBase, public Stat { +class CVC4_PUBLIC StatisticsRegistry : public StatisticsBase, public Stat { private: /** Private copy constructor undefined (no copy permitted). */ @@ -632,7 +639,7 @@ public: std::vector v; for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) { std::vector w; - w.push_back((*i)->getName()); + w.push_back(SExpr((*i)->getName())); w.push_back((*i)->getValue()); v.push_back(SExpr(w)); } @@ -774,7 +781,7 @@ class CodeTimer; * arbitrarily, like a stopwatch; the value of the statistic at the * end is the accumulated time over all (start,stop) pairs. */ -class TimerStat : public BackedStat { +class CVC4_PUBLIC TimerStat : public BackedStat { // strange: timespec isn't placed in 'std' namespace ?! /** The last start time of this timer */ diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 46705a849..327be72eb 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -13,16 +13,16 @@ ** ** Implementation of expression types. **/ +#include "expr/type.h" #include #include #include +#include "base/exception.h" #include "expr/node_manager.h" #include "expr/node_manager_attributes.h" -#include "expr/type.h" #include "expr/type_node.h" -#include "util/exception.h" using namespace std; diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 0f5e020d8..ce006a4f1 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -27,9 +27,9 @@ #include #include +#include "base/cvc4_assert.h" #include "expr/kind.h" #include "expr/metakind.h" -#include "util/cvc4_assert.h" #include "util/cardinality.h" namespace CVC4 { diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h index b54fd8809..bc780a7e5 100644 --- a/src/expr/type_properties_template.h +++ b/src/expr/type_properties_template.h @@ -21,13 +21,13 @@ #line 23 "${template}" +#include + +#include "base/cvc4_assert.h" +#include "options/language.h" #include "expr/type_node.h" -#include "util/cvc4_assert.h" #include "expr/kind.h" #include "expr/expr.h" -#include "util/language.h" - -#include ${type_properties_includes} diff --git a/src/util/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp similarity index 96% rename from src/util/uninterpreted_constant.cpp rename to src/expr/uninterpreted_constant.cpp index f0d9a42d2..d41ab1045 100644 --- a/src/util/uninterpreted_constant.cpp +++ b/src/expr/uninterpreted_constant.cpp @@ -14,7 +14,8 @@ ** Representation of constants of uninterpreted sorts. **/ -#include "util/uninterpreted_constant.h" +#include "expr/uninterpreted_constant.h" + #include #include #include diff --git a/src/util/uninterpreted_constant.h b/src/expr/uninterpreted_constant.h similarity index 100% rename from src/util/uninterpreted_constant.h rename to src/expr/uninterpreted_constant.h diff --git a/src/util/uninterpreted_constant.i b/src/expr/uninterpreted_constant.i similarity index 90% rename from src/util/uninterpreted_constant.i rename to src/expr/uninterpreted_constant.i index 9a49f0642..1636eba5b 100644 --- a/src/util/uninterpreted_constant.i +++ b/src/expr/uninterpreted_constant.i @@ -1,5 +1,5 @@ %{ -#include "util/uninterpreted_constant.h" +#include "expr/uninterpreted_constant.h" %} %rename(less) CVC4::UninterpretedConstant::operator<(const UninterpretedConstant&) const; @@ -14,4 +14,4 @@ %ignore CVC4::operator<<(std::ostream&, const UninterpretedConstant&); -%include "util/uninterpreted_constant.h" +%include "expr/uninterpreted_constant.h" diff --git a/src/include/cvc4.h b/src/include/cvc4.h index 77fcbad41..d41fce056 100644 --- a/src/include/cvc4.h +++ b/src/include/cvc4.h @@ -18,20 +18,17 @@ #ifndef __CVC4__CVC4_H #define __CVC4__CVC4_H -#include - -#include +#include +#include #include -#include - -#include -#include -#include -#include +#include #include -#include - #include #include +#include +#include +#include +#include +#include #endif /* __CVC4__CVC4_H */ diff --git a/src/main/Makefile.am b/src/main/Makefile.am index 3ac0db7cb..478d3f3ee 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -30,7 +30,6 @@ pcvc4_LDADD = \ libmain.a \ @builddir@/../parser/libcvc4parser.la \ @builddir@/../libcvc4.la \ - @builddir@/../util/libstatistics.la \ $(READLINE_LIBS) if CVC4_NEEDS_REPLACEMENT_FUNCTIONS pcvc4_LDADD += \ @@ -55,7 +54,6 @@ cvc4_LDADD = \ libmain.a \ @builddir@/../parser/libcvc4parser.la \ @builddir@/../libcvc4.la \ - @builddir@/../util/libstatistics.la \ $(READLINE_LIBS) if CVC4_NEEDS_REPLACEMENT_FUNCTIONS cvc4_LDADD += \ @@ -80,8 +78,6 @@ smt2_tokens.h: @srcdir@/../parser/smt2/Smt2.g tptp_tokens.h: @srcdir@/../parser/tptp/Tptp.g $(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9_-][a-zA-Z0-9_-]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9_-]*\)'\''.*/"\1",/' | sort -u >$@ -EXTRA_DIST = \ - options_handlers.h clean-local: rm -f $(BUILT_SOURCES) diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 460274515..0b53c3cbe 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -12,22 +12,22 @@ ** \brief An additional layer between commands and invoking them. **/ -#include -#include - #include "main/command_executor.h" -#include "expr/command.h" - -#include "main/main.h" - -#include "main/options.h" -#include "smt/options.h" -#include "printer/options.h" #ifndef __WIN32__ # include #endif /* ! __WIN32__ */ +#include +#include + +#include "main/main.h" +#include "options/main_options.h" +#include "options/printer_options.h" +#include "options/smt_options.h" +#include "smt_util/command.h" + + namespace CVC4 { namespace main { diff --git a/src/main/command_executor.h b/src/main/command_executor.h index 9fe6347be..49d18a153 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -15,14 +15,14 @@ #ifndef __CVC4__MAIN__COMMAND_EXECUTOR_H #define __CVC4__MAIN__COMMAND_EXECUTOR_H +#include +#include + #include "expr/expr_manager.h" -#include "smt/smt_engine.h" -#include "util/statistics_registry.h" +#include "expr/statistics_registry.h" #include "options/options.h" -#include "expr/command.h" - -#include -#include +#include "smt/smt_engine.h" +#include "smt_util/command.h" namespace CVC4 { namespace main { diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index f0d87cdf2..bb6487bf0 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -15,27 +15,28 @@ ** threads. **/ -#include -#include +#include "main/command_executor_portfolio.h" + +#if HAVE_UNISTD_H +# include +#endif /* HAVE_UNISTD_H */ + #include #include +#include +#include #include -#include "expr/command.h" +#include "cvc4autoconfig.h" #include "expr/pickler.h" -#include "main/command_executor_portfolio.h" #include "main/main.h" -#include "main/options.h" #include "main/portfolio.h" +#include "options/main_options.h" #include "options/options.h" -#include "smt/options.h" -#include "printer/options.h" - -#include "cvc4autoconfig.h" +#include "options/printer_options.h" +#include "options/smt_options.h" +#include "smt_util/command.h" -#if HAVE_UNISTD_H -# include -#endif /* HAVE_UNISTD_H */ using namespace std; diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index c29ba55a4..df78df0f3 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -13,39 +13,38 @@ ** sequential and portfolio versions **/ +#include +#include + #include #include #include #include #include -#include - -#include -#include +#include "base/output.h" #include "cvc4autoconfig.h" -#include "main/main.h" -#include "main/interactive_shell.h" -#include "main/options.h" -#include "parser/parser.h" -#include "parser/parser_builder.h" -#include "parser/parser_exception.h" #include "expr/expr_manager.h" -#include "expr/command.h" -#include "util/configuration.h" -#include "options/options.h" -#include "theory/quantifiers/options.h" +#include "expr/result.h" +#include "expr/statistics_registry.h" #include "main/command_executor.h" #ifdef PORTFOLIO_BUILD # include "main/command_executor_portfolio.h" #endif -#include "main/options.h" -#include "smt/options.h" -#include "util/output.h" -#include "util/result.h" -#include "util/statistics_registry.h" +#include "main/interactive_shell.h" +#include "main/main.h" +#include "options/main_options.h" +#include "options/options.h" +#include "options/quantifiers_options.h" +#include "options/smt_options.h" +#include "parser/parser.h" +#include "parser/parser_builder.h" +#include "parser/parser_exception.h" +#include "smt/smt_options_handler.h" +#include "smt_util/command.h" +#include "util/configuration.h" using namespace std; using namespace CVC4; @@ -130,8 +129,11 @@ int runCvc4(int argc, char* argv[], Options& opts) { progPath = argv[0]; +#warning "TODO: Check that the SmtEngine pointer should be NULL with Kshitij." + smt::SmtOptionsHandler optionsHandler(NULL); + // Parse the options - vector filenames = opts.parseOptions(argc, argv); + vector filenames = opts.parseOptions(argc, argv, &optionsHandler); # ifndef PORTFOLIO_BUILD if( opts.wasSetByUser(options::threads) || @@ -302,7 +304,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { } #ifndef PORTFOLIO_BUILD if(!opts.wasSetByUser(options::incrementalSolving)) { - cmd = new SetOptionCommand("incremental", true); + cmd = new SetOptionCommand("incremental", SExpr(true)); cmd->setMuted(true); pExecutor->doCommand(cmd); delete cmd; @@ -349,7 +351,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { throw OptionException("--tear-down-incremental incompatible with --incremental"); } - cmd = new SetOptionCommand("incremental", false); + cmd = new SetOptionCommand("incremental", SExpr(false)); cmd->setMuted(true); pExecutor->doCommand(cmd); delete cmd; @@ -488,7 +490,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { delete parser; } else { if(!opts.wasSetByUser(options::incrementalSolving)) { - cmd = new SetOptionCommand("incremental", false); + cmd = new SetOptionCommand("incremental", SExpr(false)); cmd->setMuted(true); pExecutor->doCommand(cmd); delete cmd; diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 3b237f6a4..da2813e24 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -14,31 +14,17 @@ ** This file is the implementation for the CVC4 interactive shell. ** The shell supports the readline library. **/ +#include "main/interactive_shell.h" -#include +#include +#include #include -#include -#include +#include #include -#include -#include - -#include "cvc4autoconfig.h" - -#include "main/interactive_shell.h" - -#include "expr/command.h" -#include "parser/input.h" -#include "parser/parser.h" -#include "parser/parser_builder.h" -#include "options/options.h" -#include "smt/options.h" -#include "main/options.h" -#include "util/language.h" -#include "util/output.h" - #include -#include +#include +#include +#include #if HAVE_LIBREADLINE # include @@ -48,6 +34,19 @@ # endif /* HAVE_EXT_STDIO_FILEBUF_H */ #endif /* HAVE_LIBREADLINE */ + +#include "base/output.h" +#include "cvc4autoconfig.h" +#include "options/language.h" +#include "options/main_options.h" +#include "options/options.h" +#include "options/smt_options.h" +#include "parser/input.h" +#include "parser/parser.h" +#include "parser/parser_builder.h" +#include "theory/logic_info.h" +#include "smt_util/command.h" + using namespace std; namespace CVC4 { @@ -99,7 +98,7 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager, /* Create parser with bogus input. */ d_parser = parserBuilder.withStringInput("").build(); if(d_options.wasSetByUser(options::forceLogic)) { - d_parser->forceLogic(d_options[options::forceLogic].getLogicString()); + d_parser->forceLogic(d_options[options::forceLogic]->getLogicString()); } #if HAVE_LIBREADLINE @@ -401,4 +400,3 @@ char* commandGenerator(const char* text, int state) { #endif /* HAVE_LIBREADLINE */ }/* CVC4 namespace */ - diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h index ef55919a1..1b1031776 100644 --- a/src/main/interactive_shell.h +++ b/src/main/interactive_shell.h @@ -18,9 +18,9 @@ #include #include -#include "util/language.h" -#include "util/unsafe_interrupt_exception.h" +#include "options/language.h" #include "options/options.h" +#include "util/unsafe_interrupt_exception.h" namespace CVC4 { diff --git a/src/main/main.cpp b/src/main/main.cpp index 1c825bc35..36a339d94 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -13,30 +13,29 @@ ** ** Main driver for CVC4 executable. **/ +#include "main/main.h" #include #include #include #include - #include #include -#include "main/main.h" -#include "main/interactive_shell.h" +#include "base/output.h" +#include "expr/expr_manager.h" +#include "expr/result.h" +#include "expr/statistics.h" #include "main/command_executor.h" +#include "main/interactive_shell.h" +#include "options/language.h" +#include "options/main_options.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "parser/parser_exception.h" -#include "expr/expr_manager.h" #include "smt/smt_engine.h" -#include "expr/command.h" +#include "smt_util/command.h" #include "util/configuration.h" -#include "main/options.h" -#include "util/output.h" -#include "util/result.h" -#include "util/statistics.h" -#include "util/language.h" using namespace std; using namespace CVC4; diff --git a/src/main/main.h b/src/main/main.h index a2e813c6c..7dda429af 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -17,14 +17,14 @@ #include #include -#include "options/options.h" +#include "base/exception.h" +#include "base/tls.h" +#include "cvc4autoconfig.h" #include "expr/expr_manager.h" +#include "expr/statistics.h" +#include "expr/statistics_registry.h" +#include "options/options.h" #include "smt/smt_engine.h" -#include "util/exception.h" -#include "util/statistics.h" -#include "util/tls.h" -#include "util/statistics_registry.h" -#include "cvc4autoconfig.h" #ifndef __CVC4__MAIN__MAIN_H #define __CVC4__MAIN__MAIN_H diff --git a/src/main/options_handlers.h b/src/main/options_handlers.h deleted file mode 100644 index 00f192d2f..000000000 --- a/src/main/options_handlers.h +++ /dev/null @@ -1,115 +0,0 @@ -/********************* */ -/*! \file options_handlers.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 Custom handlers and predicates for main driver options - ** - ** Custom handlers and predicates for main driver options. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__MAIN__OPTIONS_HANDLERS_H -#define __CVC4__MAIN__OPTIONS_HANDLERS_H - -namespace CVC4 { -namespace main { - -inline void showConfiguration(std::string option, SmtEngine* smt) { - fputs(Configuration::about().c_str(), stdout); - printf("\n"); - printf("version : %s\n", Configuration::getVersionString().c_str()); - if(Configuration::isGitBuild()) { - const char* branchName = Configuration::getGitBranchName(); - if(*branchName == '\0') { - branchName = "-"; - } - printf("scm : git [%s %s%s]\n", - branchName, - std::string(Configuration::getGitCommit()).substr(0, 8).c_str(), - Configuration::hasGitModifications() ? - " (with modifications)" : ""); - } else if(Configuration::isSubversionBuild()) { - printf("scm : svn [%s r%u%s]\n", - Configuration::getSubversionBranchName(), - Configuration::getSubversionRevision(), - Configuration::hasSubversionModifications() ? - " (with modifications)" : ""); - } else { - printf("scm : no\n"); - } - printf("\n"); - printf("library : %u.%u.%u\n", - Configuration::getVersionMajor(), - Configuration::getVersionMinor(), - Configuration::getVersionRelease()); - printf("\n"); - printf("debug code : %s\n", Configuration::isDebugBuild() ? "yes" : "no"); - printf("statistics : %s\n", Configuration::isStatisticsBuild() ? "yes" : "no"); - printf("replay : %s\n", Configuration::isReplayBuild() ? "yes" : "no"); - printf("tracing : %s\n", Configuration::isTracingBuild() ? "yes" : "no"); - printf("dumping : %s\n", Configuration::isDumpingBuild() ? "yes" : "no"); - printf("muzzled : %s\n", Configuration::isMuzzledBuild() ? "yes" : "no"); - printf("assertions : %s\n", Configuration::isAssertionBuild() ? "yes" : "no"); - printf("proof : %s\n", Configuration::isProofBuild() ? "yes" : "no"); - printf("coverage : %s\n", Configuration::isCoverageBuild() ? "yes" : "no"); - printf("profiling : %s\n", Configuration::isProfilingBuild() ? "yes" : "no"); - printf("competition: %s\n", Configuration::isCompetitionBuild() ? "yes" : "no"); - printf("\n"); - printf("cudd : %s\n", Configuration::isBuiltWithCudd() ? "yes" : "no"); - printf("cln : %s\n", Configuration::isBuiltWithCln() ? "yes" : "no"); - printf("gmp : %s\n", Configuration::isBuiltWithGmp() ? "yes" : "no"); - printf("glpk : %s\n", Configuration::isBuiltWithGlpk() ? "yes" : "no"); - printf("abc : %s\n", Configuration::isBuiltWithAbc() ? "yes" : "no"); - printf("readline : %s\n", Configuration::isBuiltWithReadline() ? "yes" : "no"); - printf("tls : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no"); - exit(0); -} - -inline void showDebugTags(std::string option, SmtEngine* smt) { - if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) { - printf("available tags:"); - unsigned ntags = Configuration::getNumDebugTags(); - char const* const* tags = Configuration::getDebugTags(); - for(unsigned i = 0; i < ntags; ++ i) { - printf(" %s", tags[i]); - } - printf("\n"); - } else if(! Configuration::isDebugBuild()) { - throw OptionException("debug tags not available in non-debug builds"); - } else { - throw OptionException("debug tags not available in non-tracing builds"); - } - exit(0); -} - -inline void showTraceTags(std::string option, SmtEngine* smt) { - if(Configuration::isTracingBuild()) { - printf("available tags:"); - unsigned ntags = Configuration::getNumTraceTags(); - char const* const* tags = Configuration::getTraceTags(); - for (unsigned i = 0; i < ntags; ++ i) { - printf(" %s", tags[i]); - } - printf("\n"); - } else { - throw OptionException("trace tags not available in non-tracing build"); - } - exit(0); -} - -inline void threadN(std::string option, SmtEngine* smt) { - throw OptionException(option + " is not a real option by itself. Use e.g. --thread0=\"--random-seed=10 --random-freq=0.02\" --thread1=\"--random-seed=20 --random-freq=0.05\""); -} - -}/* CVC4::main namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__MAIN__OPTIONS_HANDLERS_H */ diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp index 51b4779cc..884c3eda7 100644 --- a/src/main/portfolio.cpp +++ b/src/main/portfolio.cpp @@ -19,11 +19,12 @@ #include #include -#include "smt/smt_engine.h" -#include "util/output.h" -#include "util/result.h" -#include "util/statistics_registry.h" +#include "base/output.h" +#include "expr/result.h" +#include "expr/statistics_registry.h" #include "options/options.h" +#include "smt/smt_engine.h" + namespace CVC4 { diff --git a/src/main/portfolio.h b/src/main/portfolio.h index f89c8f548..5a730c005 100644 --- a/src/main/portfolio.h +++ b/src/main/portfolio.h @@ -19,10 +19,10 @@ #include #include -#include "smt/smt_engine.h" -#include "expr/command.h" +#include "expr/statistics_registry.h" #include "options/options.h" -#include "util/statistics_registry.h" +#include "smt/smt_engine.h" +#include "smt_util/command.h" namespace CVC4 { diff --git a/src/main/portfolio_util.cpp b/src/main/portfolio_util.cpp index 7a4beb0d0..6b5fe4723 100644 --- a/src/main/portfolio_util.cpp +++ b/src/main/portfolio_util.cpp @@ -12,13 +12,16 @@ ** \brief Code relevant only for portfolio builds **/ +#include + #include #include -#include + +#include "options/main_options.h" #include "options/options.h" -#include "main/options.h" -#include "prop/options.h" -#include "smt/options.h" +#include "options/prop_options.h" +#include "options/smt_options.h" +#include "smt/smt_options_handler.h" using namespace std; @@ -28,6 +31,9 @@ vector parseThreadSpecificOptions(Options opts) { vector threadOptions; +#warning "TODO: Check that the SmtEngine pointer should be NULL with Kshitij." + smt::SmtOptionsHandler optionsHandler(NULL); + unsigned numThreads = opts[options::threads]; for(unsigned i = 0; i < numThreads; ++i) { @@ -37,7 +43,7 @@ vector parseThreadSpecificOptions(Options opts) // Set thread identifier tOpts.set(options::thread_id, i); - if(i < opts[options::threadArgv].size() && + if(i < opts[options::threadArgv].size() && !opts[options::threadArgv][i].empty()) { // separate out the thread's individual configuration string @@ -60,7 +66,7 @@ vector parseThreadSpecificOptions(Options opts) *vp++ = NULL; if(targc > 1) { // this is necessary in case you do e.g. --thread0=" " try { - tOpts.parseOptions(targc, targv); + tOpts.parseOptions(targc, targv, &optionsHandler); } catch(OptionException& e) { stringstream ss; ss << optid << ": " << e.getMessage(); diff --git a/src/main/portfolio_util.h b/src/main/portfolio_util.h index 8ae730506..d6d6a2d02 100644 --- a/src/main/portfolio_util.h +++ b/src/main/portfolio_util.h @@ -17,12 +17,12 @@ #include +#include "base/output.h" #include "expr/pickler.h" +#include "options/main_options.h" +#include "smt_util/lemma_input_channel.h" +#include "smt_util/lemma_output_channel.h" #include "util/channel.h" -#include "util/lemma_input_channel.h" -#include "util/lemma_output_channel.h" -#include "util/output.h" -#include "main/options.h" namespace CVC4 { diff --git a/src/main/util.cpp b/src/main/util.cpp index f0cab25fa..86272ee53 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -28,15 +28,14 @@ #endif /* __WIN32__ */ -#include "util/exception.h" -#include "options/options.h" -#include "util/statistics.h" -#include "util/tls.h" -#include "smt/smt_engine.h" - +#include "base/exception.h" +#include "base/tls.h" #include "cvc4autoconfig.h" -#include "main/main.h" +#include "expr/statistics.h" #include "main/command_executor.h" +#include "main/main.h" +#include "options/options.h" +#include "smt/smt_engine.h" using CVC4::Exception; using namespace std; diff --git a/src/options/Makefile.am b/src/options/Makefile.am index 0d4b970d8..d871bfb0a 100644 --- a/src/options/Makefile.am +++ b/src/options/Makefile.am @@ -1,65 +1,177 @@ -OPTIONS_FILES_SRCS = \ - base_options.cpp \ - base_options.h \ - ../expr/options.cpp \ - ../expr/options.h \ - ../theory/booleans/options.cpp \ - ../theory/booleans/options.h \ - ../theory/options.cpp \ - ../theory/options.h \ - ../theory/bv/options.cpp \ - ../theory/bv/options.h \ - ../theory/datatypes/options.cpp \ - ../theory/datatypes/options.h \ - ../theory/builtin/options.cpp \ - ../theory/builtin/options.h \ - ../theory/arith/options.cpp \ - ../theory/arith/options.h \ - ../theory/uf/options.cpp \ - ../theory/uf/options.h \ - ../theory/arrays/options.cpp \ - ../theory/arrays/options.h \ - ../theory/quantifiers/options.cpp \ - ../theory/quantifiers/options.h \ - ../theory/strings/options.cpp \ - ../theory/strings/options.h \ - ../prop/options.cpp \ - ../prop/options.h \ - ../proof/options.cpp \ - ../proof/options.h \ - ../printer/options.cpp \ - ../printer/options.h \ - ../smt/options.cpp \ - ../smt/options.h \ - ../decision/options.cpp \ - ../decision/options.h \ - ../main/options.cpp \ - ../main/options.h \ - ../parser/options.cpp \ - ../parser/options.h \ - ../theory/idl/options.cpp \ - ../theory/idl/options.h \ - ../theory/sets/options.cpp \ - ../theory/sets/options.h \ - ../theory/fp/options.cpp \ - ../theory/fp/options.h - -OPTIONS_FILES = \ - $(patsubst %.cpp,%,$(filter %.cpp,$(OPTIONS_FILES_SRCS))) - -OPTIONS_CPPS = \ - $(filter %.cpp,$(OPTIONS_FILES_SRCS)) - -OPTIONS_HEADS = \ - $(filter %.h,$(OPTIONS_FILES_SRCS)) +# How options are built: +# Step 1: Copy the X_options source file into builddir as X_options.tmp. +# X_options.tmp is a .PHONY rule to force this step to always be done. +# Step 2: Compare X_options.tmp to X_options.options. +# If they are different, overwrite "X_options.options". +# This is the file that we use to generate options from. +# This is always up to dat with X_options. The change in name is just +# to keep Makefile stage more explicit. +# Step 3: Generate X_options.sed from X_options.options using mkoptions. +# Step 4: Generate X_options.h from X_options.sed +# Step 5: Generate X_options.cpp from X_options.sed. +# This stage also waits for X_options.h as otherwise it cannot compile. +# + +OPTIONS_SRC_FILES = \ + arith_options \ + arrays_options \ + base_options \ + booleans_options \ + builtin_options \ + bv_options \ + datatypes_options \ + decision_options \ + expr_options \ + fp_options \ + idl_options \ + main_options \ + parser_options \ + printer_options \ + proof_options \ + prop_options \ + quantifiers_options \ + sets_options \ + smt_options \ + strings_options \ + theory_options \ + uf_options + +OPTIONS_TEMPS = \ + arith_options.tmp \ + arrays_options.tmp \ + base_options.tmp \ + booleans_options.tmp \ + builtin_options.tmp \ + bv_options.tmp \ + datatypes_options.tmp \ + decision_options.tmp \ + expr_options.tmp \ + fp_options.tmp \ + idl_options.tmp \ + main_options.tmp \ + parser_options.tmp \ + printer_options.tmp \ + proof_options.tmp \ + prop_options.tmp \ + quantifiers_options.tmp \ + sets_options.tmp \ + smt_options.tmp \ + strings_options.tmp \ + theory_options.tmp \ + uf_options.tmp + +OPTIONS_OPTIONS_FILES = \ + arith_options.options \ + arrays_options.options \ + base_options.options \ + booleans_options.options \ + builtin_options.options \ + bv_options.options \ + datatypes_options.options \ + decision_options.options \ + expr_options.options \ + fp_options.options \ + idl_options.options \ + main_options.options \ + parser_options.options \ + printer_options.options \ + proof_options.options \ + prop_options.options \ + quantifiers_options.options \ + sets_options.options \ + smt_options.options \ + strings_options.options \ + theory_options.options \ + uf_options.options OPTIONS_SEDS = \ - $(patsubst %,%.sed,$(OPTIONS_FILES)) + arith_options.sed \ + arrays_options.sed \ + base_options.sed \ + booleans_options.sed \ + builtin_options.sed \ + bv_options.sed \ + datatypes_options.sed \ + decision_options.sed \ + expr_options.sed \ + fp_options.sed \ + idl_options.sed \ + main_options.sed \ + parser_options.sed \ + printer_options.sed \ + proof_options.sed \ + prop_options.sed \ + quantifiers_options.sed \ + sets_options.sed \ + smt_options.sed \ + strings_options.sed \ + theory_options.sed \ + uf_options.sed -OPTIONS_OBJ = \ - $(patsubst %.cpp,%.$(OBJEXT),$(OPTIONS_CPP)) +OPTIONS_HEADS = \ + arith_options.h \ + arrays_options.h \ + base_options.h \ + booleans_options.h \ + builtin_options.h \ + bv_options.h \ + datatypes_options.h \ + decision_options.h \ + expr_options.h \ + fp_options.h \ + idl_options.h \ + main_options.h \ + parser_options.h \ + printer_options.h \ + proof_options.h \ + prop_options.h \ + quantifiers_options.h \ + sets_options.h \ + smt_options.h \ + strings_options.h \ + theory_options.h \ + uf_options.h +OPTIONS_CPPS = \ + arith_options.cpp \ + arrays_options.cpp \ + base_options.cpp \ + booleans_options.cpp \ + builtin_options.cpp \ + bv_options.cpp \ + datatypes_options.cpp \ + decision_options.cpp \ + expr_options.cpp \ + fp_options.cpp \ + idl_options.cpp \ + main_options.cpp \ + parser_options.cpp \ + printer_options.cpp \ + proof_options.cpp \ + prop_options.cpp \ + quantifiers_options.cpp \ + sets_options.cpp \ + smt_options.cpp \ + strings_options.cpp \ + theory_options.cpp \ + uf_options.cpp + + +CPP_TEMPLATE_FILES = \ + base_options_template.h \ + base_options_template.cpp \ + options_holder_template.h \ + options_template.cpp \ + options_handler_get_option_template.cpp \ + options_handler_set_option_template.cpp +CPP_TEMPLATE_SEDS = \ + base_options_template.h.sed \ + base_options_template.cpp.sed \ + options_holder_template.h.sed \ + options_template.cpp.sed \ + options_handler_get_option_template.cpp.sed \ + options_handler_set_option_template.cpp.sed DOCUMENTATION_FILES = \ @@ -68,19 +180,17 @@ DOCUMENTATION_FILES = \ ../../doc/SmtEngine.3cvc \ ../../doc/options.3cvc -TEMPLATE_FILES = \ - base_options_template.h \ - base_options_template.cpp \ - options_holder_template.h \ - options_template.cpp \ - ../smt/smt_options_template.cpp \ +DOCUMENTATION_TEMPLATE_FILES = \ ../../doc/cvc4.1_template \ ../../doc/libcvc4.3_template \ ../../doc/SmtEngine.3cvc_template \ ../../doc/options.3cvc_template -TEMPLATE_SEDS = \ - $(patsubst %,%.sed,$(TEMPLATE_FILES)) +DOCUMENTATION_TEMPLATE_SEDS = \ + ../../doc/cvc4.1_template.sed \ + ../../doc/libcvc4.3_template.sed \ + ../../doc/SmtEngine.3cvc_template.sed \ + ../../doc/options.3cvc_template.sed AM_CPPFLAGS = \ -D__BUILDING_CVC4LIB \ @@ -90,63 +200,98 @@ AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = liboptions.la liboptions_la_SOURCES = \ + arith_heuristic_pivot_rule.cpp \ + arith_heuristic_pivot_rule.h \ + arith_propagation_mode.cpp \ + arith_propagation_mode.h \ + arith_unate_lemma_mode.cpp \ + arith_unate_lemma_mode.h \ + base_handlers.h \ + boolean_term_conversion_mode.cpp \ + boolean_term_conversion_mode.h \ + bv_bitblast_mode.cpp \ + bv_bitblast_mode.h \ + decision_mode.cpp \ + decision_mode.h \ + decision_weight.h \ + didyoumean.cpp \ + didyoumean.h \ + language.cpp \ + language.h \ + logic_info_forward.h \ + option_exception.h \ options.h \ - base_options_handlers.h \ - option_exception.h + options_handler_interface.cpp \ + options_handler_interface.h \ + printer_modes.cpp \ + printer_modes.h \ + quantifiers_modes.cpp \ + quantifiers_modes.h \ + simplification_mode.cpp \ + simplification_mode.h \ + theoryof_mode.cpp \ + theoryof_mode.h \ + ufss_mode.h + nodist_liboptions_la_SOURCES = \ options.cpp \ options_holder.h \ - $(OPTIONS_FILES_SRCS) + $(OPTIONS_HEADS) \ + $(OPTIONS_CPPS) \ + options_handler_get_option.cpp \ + options_handler_set_option.cpp BUILT_SOURCES = \ - exprs-builts \ - ../smt/smt_options.cpp \ + $(CPP_TEMPLATE_SEDS) \ + $(DOCUMENTATION_FILES) \ + $(DOCUMENTATION_TEMPLATE_SEDS) \ + $(OPTIONS_CPPS) \ + $(OPTIONS_HEADS) \ + $(OPTIONS_OPTIONS_FILES) \ + $(OPTIONS_SEDS) \ options.cpp \ + options_handler_get_option.cpp \ + options_handler_set_option.cpp \ options_holder.h \ - $(OPTIONS_FILES_SRCS) \ - $(OPTIONS_SEDS) \ - summary.sed \ - $(TEMPLATE_SEDS) - + summary.sed -# The documentation files are added to BUILT_SOURCES to get the files to -# be built. Alternative suggestions for building these files would be -# appreciated. +# listing {Debug,Trace}_tags too ensures that make doesn't auto-remove it +# after building (if it does, we don't get the "cached" effect with +# the .tmp files below, and we have to re-compile and re-link each +# time, even when there are no changes). BUILT_SOURCES += \ - $(DOCUMENTATION_FILES) - + Debug_tags.h \ + Debug_tags \ + Trace_tags.h \ + Trace_tags CLEANFILES = \ - $(OPTIONS_FILES_SRCS) \ $(BUILT_SOURCES) \ - $(DOCUMENTATION_FILES) + $(DOCUMENTATION_FILES) \ + $(OPTIONS_TEMPS) EXTRA_DIST = \ - mkoptions \ - base_options_template.h \ + $(DOCUMENTATION_FILES) \ + $(OPTIONS_CPPS) \ + $(OPTIONS_HEADS) \ + $(OPTIONS_SRC_FILES) \ base_options_template.cpp \ - options_template.cpp \ - options_holder_template.h \ - options.i \ - option_exception.i \ - $(OPTIONS_FILES) \ + base_options_template.h \ + language.i \ + mkoptions \ mktagheaders \ mktags \ - $(DOCUMENTATION_FILES) + option_exception.i \ + options.i \ + options_handler_get_option_template.cpp \ + options_handler_interface.i \ + options_handler_set_option_template.cpp \ + options_holder_template.h \ + options_template.cpp -# listing {Debug,Trace}_tags too ensures that make doesn't auto-remove it -# after building (if it does, we don't get the "cached" effect with -# the .tmp files below, and we have to re-compile and re-link each -# time, even when there are no changes). -BUILT_SOURCES += \ - Debug_tags.h \ - Debug_tags \ - Trace_tags.h \ - Trace_tags - %_tags.h: %_tags mktagheaders $(AM_V_at)chmod +x @srcdir@/mktagheaders $(AM_V_GEN)( @srcdir@/mktagheaders "$<" "$<" ) >"$@" @@ -175,52 +320,72 @@ MOSTLYCLEANFILES = \ Debug_tags.h \ Trace_tags.h -# mkoptions template-sed template-file (options-file)* -# mkoptions apply-sed-files-to-template sed-file template-file filename +# Make sure the implicit rules never mistake a _template.cpp or _template.h file for source file. +options_holder_template.h options_template.cpp options_handler_get_option_template.cpp options_handler_set_option_template.cpp base_options_template.h base_options_template.cpp :; + +# Make sure the implicit rules never mistake X_options for the -o file for a +# CPP file. +arith_options arrays_options base_options booleans_options builtin_options bv_options datatypes_options decision_options expr_options fp_options idl_options main_options parser_options printer_options proof_options prop_options quantifiers_options sets_options smt_options strings_options theory_options uf_options:; -$(OPTIONS_FILES):; -options_holder_template.h options_template.cpp ../smt/smt_options_template.cpp base_options_template.h base_options_template.cpp :; +# These are phony to force them to be made everytime. +.PHONY: arith_options.tmp arrays_options.tmp base_options.tmp booleans_options.tmp builtin_options.tmp bv_options.tmp datatypes_options.tmp decision_options.tmp expr_options.tmp fp_options.tmp idl_options.tmp main_options.tmp parser_options.tmp printer_options.tmp proof_options.tmp prop_options.tmp quantifiers_options.tmp sets_options.tmp smt_options.tmp strings_options.tmp theory_options.tmp uf_options.tmp + +# Make is happier being listed explictly. Not sure why. +arith_options.tmp arrays_options.tmp base_options.tmp booleans_options.tmp builtin_options.tmp bv_options.tmp datatypes_options.tmp decision_options.tmp expr_options.tmp fp_options.tmp idl_options.tmp main_options.tmp parser_options.tmp printer_options.tmp proof_options.tmp prop_options.tmp quantifiers_options.tmp sets_options.tmp smt_options.tmp strings_options.tmp theory_options.tmp uf_options.tmp: + echo "$@" "$(@:.tmp=)" + $(AM_V_GEN)(cp "@srcdir@/$(@:.tmp=)" "$@" || true) +#TIM: +#The (... || true) here is to make distcheck not fail. + +%_options.options: %_options.tmp + $(AM_V_GEN)\ + diff -q "$^" "$@" &>/dev/null || mv "$^" "$@" || true -$(TEMPLATE_SEDS) : %.sed : % mkoptions + +# This bit is kinda tricky. +# We use the updating of %_options.options to signal that the options file updated. +# However, we use the original file in src to generate the file. +%_options.sed: %_options.options mkoptions + $(AM_V_at)chmod +x @srcdir@/mkoptions + $(AM_V_GEN)(@srcdir@/mkoptions module-sed "@srcdir@/$(@:.sed=)" ) > "$@" + + +$(CPP_TEMPLATE_SEDS): %.sed : % mkoptions # echo "template seds" # echo "$@" # echo $(TEMPLATE_SEDS) $(AM_V_at)chmod +x @srcdir@/mkoptions $(AM_V_GEN)(@srcdir@/mkoptions template-sed "$<" ) > "$@" - -$(OPTIONS_SEDS) : %.sed : % mkoptions -# echo "sedheads" +$(DOCUMENTATION_TEMPLATE_SEDS): %.sed : % mkoptions +# echo "template seds" # echo "$@" -# echo $(OPTIONS_SEDS) +# echo $(TEMPLATE_SEDS) $(AM_V_at)chmod +x @srcdir@/mkoptions - $(AM_V_at)mkdir -p `dirname "$@"` - $(AM_V_GEN)(@srcdir@/mkoptions module-sed "$<" ) > "$@" + $(AM_V_GEN)(@srcdir@/mkoptions template-sed "$<" ) > "$@" -$(OPTIONS_HEADS) : %.h : %.sed mkoptions base_options_template.h base_options_template.h.sed +%_options.h : %_options.sed mkoptions base_options_template.h base_options_template.h.sed # echo heads # echo "$@" # echo $(OPTIONS_HEADS) $(AM_V_at)chmod +x @srcdir@/mkoptions - $(AM_V_at)mkdir -p `dirname "$@"` $(AM_V_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \ @srcdir@/base_options_template.h \ base_options_template.h.sed \ "$<" \ ) > "$@" -summary.sed : mkoptions $(OPTIONS_FILES) +summary.sed : mkoptions $(OPTIONS_OPTIONS_FILES) $(AM_V_at)chmod +x @srcdir@/mkoptions $(AM_V_GEN)(@srcdir@/mkoptions summary-sed \ - $(foreach o,$(OPTIONS_FILES),"$(srcdir)/$(o)") \ + $(OPTIONS_OPTIONS_FILES) \ ) > summary.sed # mkoptions apply-sed-to-template sed-file template-file -options_holder.h : options_holder_template.h options_holder_template.h.sed summary.sed mkoptions -# echo "$(OPTIONS_FILES)" +options_holder.h : options_holder_template.h options_holder_template.h.sed summary.sed mkoptions $(OPTIONS_HEADS) $(AM_V_at)chmod +x @srcdir@/mkoptions $(AM_V_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \ @srcdir@/options_holder_template.h \ @@ -228,19 +393,9 @@ options_holder.h : options_holder_template.h options_holder_template.h.sed summa summary.sed \ ) > "$@" -gen-heads-stamp : $(OPTIONS_HEADS) options_holder.h -.PHONY : gen-heads-stamp - - -# Bit of a hack here. The .h file needs to always be built before the .cpp file is compiled. -$(OPTIONS_CPPS) : %.cpp : %.sed mkoptions base_options_template.cpp base_options_template.cpp.sed gen-heads-stamp -# echo "cpps" -# echo "$@" -# echo "$<" -# echo $(OPTIONS_CPPS) -# echo $(OPTIONS_FILES_SRCS) +# Make sure not to match with "options.cpp" too. +%_options.cpp: %_options.sed %_options.h mkoptions options_holder.h base_options_template.cpp base_options_template.cpp.sed $(AM_V_at)chmod +x @srcdir@/mkoptions - $(AM_V_at)mkdir -p `dirname "$@"` $(AM_V_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \ @srcdir@/base_options_template.cpp \ base_options_template.cpp.sed \ @@ -249,9 +404,9 @@ $(OPTIONS_CPPS) : %.cpp : %.sed mkoptions base_options_template.cpp base_options + # mkoptions apply-sed-to-template sed-file template-file -options.cpp : options_template.cpp options_template.cpp.sed mkoptions summary.sed gen-heads-stamp -# echo "$(OPTIONS_FILES)" +options.cpp : options_template.cpp options_template.cpp.sed mkoptions summary.sed $(OPTIONS_HEADS) options_holder.h $(AM_V_at)chmod +x @srcdir@/mkoptions $(AM_V_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \ @srcdir@/options_template.cpp \ @@ -261,15 +416,21 @@ options.cpp : options_template.cpp options_template.cpp.sed mkoptions summary.se # mkoptions apply-sed-to-template sed-file template-file -../smt/smt_options.cpp : ../smt/smt_options_template.cpp ../smt/smt_options_template.cpp.sed mkoptions summary.sed gen-heads-stamp -# echo "$(OPTIONS_FILES)" +options_handler_get_option.cpp : options_handler_get_option_template.cpp options_handler_get_option_template.cpp.sed mkoptions summary.sed $(OPTIONS_HEADS) $(AM_V_at)chmod +x @srcdir@/mkoptions $(AM_V_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \ - @srcdir@/../smt/smt_options_template.cpp \ - @builddir@/../smt/smt_options_template.cpp.sed \ + @srcdir@/options_handler_get_option_template.cpp \ + @builddir@/options_handler_get_option_template.cpp.sed \ summary.sed \ ) > "$@" +options_handler_set_option.cpp : options_handler_set_option_template.cpp options_handler_set_option_template.cpp.sed mkoptions summary.sed $(OPTIONS_HEADS) + $(AM_V_at)chmod +x @srcdir@/mkoptions + $(AM_V_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \ + @srcdir@/options_handler_set_option_template.cpp \ + @builddir@/options_handler_set_option_template.cpp.sed \ + summary.sed \ + ) > "$@" @@ -285,7 +446,7 @@ $(DOCUMENTATION_FILES) : % : %_template %_template.sed mkoptions summary.sed -#options-stamp: options_holder_template.h options_template.cpp ../smt/smt_options_template.cpp base_options_template.h base_options_template.cpp mkoptions $(OPTIONS_FILE_SRCS) +#options-stamp: options_holder_template.h options_template.cpp smt_options_template.cpp base_options_template.h base_options_template.cpp mkoptions $(OPTIONS_FILE_SRCS) # This rule is ugly. It's needed to ensure that automake's dependence @@ -294,65 +455,3 @@ $(DOCUMENTATION_FILES) : % : %_template %_template.sed mkoptions summary.sed # fails. %.Plo:; $(MKDIR_P) "$(dir $@)" && : > "$@" -# Tim: -# This is insanely ugly and brittle! -# *Any* proposal to clean this up is welcomed! -# We are overloading automake's default distclean here. We have to overload -# distclean because otherwise it deletes the dependency directory -# "src/expr/.deps", then when running make distclean in src/expr it attempts to -# include .Plo files "defined in src/expr/.deps". -# An example from src/expr/Makefile.ina : -# @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/attribute.Plo@am__quote@ -# The include must fail because this make file deleted that directory and -# distclean cannot proceed. So we override distclean to only remove -# "-rm -rf ./$(DEPDIR)". We then do manual massaging to finish up removing the -# extra files. To reproduce this, you can comment out the distclean below, run -# a distcheck and repeat this process. -# Why was this not a problem before? I do not know. -MANUAL_RM = \ - $(CLEANFILES) \ - ../main/.dirstamp \ - ../expr/.dirstamp \ - ../options/options.lo \ - ../options/base_options.lo \ - ../options/.libs/options.o \ - ../options/.libs/base_options.o \ - ../options/.libs/liboptions.a \ - ../options/Trace_tags.tmp \ - ../options/Debug_tags.tmp \ - ../options/liboptions.la \ - ../parser/.dirstamp \ - ../expr/.deps/options.Plo \ - ../main/.deps/options.Plo \ - ../parser/.deps/options.Plo \ - ../prop/options.lo \ - ../decision/options.lo \ - ../printer/options.lo \ - ../proof/options.lo \ - ../smt/options.lo \ - ../theory/arith/options.lo \ - ../theory/arrays/options.lo \ - ../theory/booleans/options.lo \ - ../theory/builtin/options.lo \ - ../theory/bv/options.lo \ - ../theory/datatypes/options.lo \ - ../theory/fp/options.lo \ - ../theory/idl/options.lo \ - ../theory/quantifiers/options.lo \ - ../theory/sets/options.lo \ - ../theory/strings/options.lo \ - ../theory/test_newalttheory/options.lo \ - ../theory/test_newtheory/options.lo \ - ../theory/uf/options.lo \ - ../theory/options.lo - - - -distclean: - -rm -rf ./$(DEPDIR) - -rm -f Makefile - -rm -f $(MANUAL_RM) - -.PHONY: exprs-builts -exprs-builts:; $(AM_V_at)[ "$(FROM_EXPR)" != 1 ] && $(MAKE) -C ../expr builts || true - diff --git a/src/theory/arith/arith_heuristic_pivot_rule.cpp b/src/options/arith_heuristic_pivot_rule.cpp similarity index 94% rename from src/theory/arith/arith_heuristic_pivot_rule.cpp rename to src/options/arith_heuristic_pivot_rule.cpp index 8ef2385c7..ff5f2102a 100644 --- a/src/theory/arith/arith_heuristic_pivot_rule.cpp +++ b/src/options/arith_heuristic_pivot_rule.cpp @@ -15,7 +15,7 @@ ** \todo document this file **/ -#include "theory/arith/arith_heuristic_pivot_rule.h" +#include "options/arith_heuristic_pivot_rule.h" namespace CVC4 { @@ -38,4 +38,3 @@ std::ostream& operator<<(std::ostream& out, ErrorSelectionRule rule) { } }/* CVC4 namespace */ - diff --git a/src/theory/arith/arith_heuristic_pivot_rule.h b/src/options/arith_heuristic_pivot_rule.h similarity index 96% rename from src/theory/arith/arith_heuristic_pivot_rule.h rename to src/options/arith_heuristic_pivot_rule.h index a64a7c846..e44b8105b 100644 --- a/src/theory/arith/arith_heuristic_pivot_rule.h +++ b/src/options/arith_heuristic_pivot_rule.h @@ -24,12 +24,12 @@ namespace CVC4 { -typedef enum { +enum ErrorSelectionRule { VAR_ORDER, MINIMUM_AMOUNT, MAXIMUM_AMOUNT, SUM_METRIC -} ErrorSelectionRule; +}; std::ostream& operator<<(std::ostream& out, ErrorSelectionRule rule) CVC4_PUBLIC; diff --git a/src/theory/arith/options b/src/options/arith_options similarity index 92% rename from src/theory/arith/options rename to src/options/arith_options index ea9658eb3..9737d5382 100644 --- a/src/theory/arith/options +++ b/src/options/arith_options @@ -3,12 +3,12 @@ # See src/options/base_options for a description of this file format # -module ARITH "theory/arith/options.h" Arithmetic theory +module ARITH "options/arith_options.h" Arithmetic theory -option arithUnateLemmaMode --unate-lemmas=MODE ArithUnateLemmaMode :handler CVC4::theory::arith::stringToArithUnateLemmaMode :default ALL_PRESOLVE_LEMMAS :handler-include "theory/arith/options_handlers.h" :include "theory/arith/arith_unate_lemma_mode.h" +option arithUnateLemmaMode --unate-lemmas=MODE ArithUnateLemmaMode :handler CVC4::options::stringToArithUnateLemmaMode :default ALL_PRESOLVE_LEMMAS :handler-include "options/options_handler_interface.h" :include "options/arith_unate_lemma_mode.h" determines which lemmas to add before solving (default is 'all', see --unate-lemmas=help) -option arithPropagationMode --arith-prop=MODE ArithPropagationMode :handler CVC4::theory::arith::stringToArithPropagationMode :default BOTH_PROP :handler-include "theory/arith/options_handlers.h" :include "theory/arith/arith_propagation_mode.h" +option arithPropagationMode --arith-prop=MODE ArithPropagationMode :handler CVC4::options::stringToArithPropagationMode :default BOTH_PROP :handler-include "options/options_handler_interface.h" :include "options/arith_propagation_mode.h" turns on arithmetic propagation (default is 'old', see --arith-prop=help) # The maximum number of difference pivots to do per invocation of simplex. @@ -25,7 +25,7 @@ option arithHeuristicPivots --heuristic-pivots=N int16_t :default 0 :read-write expert-option arithStandardCheckVarOrderPivots --standard-effort-variable-order-pivots=N int16_t :default -1 :read-write limits the number of pivots in a single invocation of check() at a non-full effort level using Bland's pivot rule -option arithErrorSelectionRule --error-selection-rule=RULE ErrorSelectionRule :handler CVC4::theory::arith::stringToErrorSelectionRule :default MINIMUM_AMOUNT :handler-include "theory/arith/options_handlers.h" :include "theory/arith/arith_heuristic_pivot_rule.h" +option arithErrorSelectionRule --error-selection-rule=RULE ErrorSelectionRule :handler CVC4::options::stringToErrorSelectionRule :default MINIMUM_AMOUNT :handler-include "options/options_handler_interface.h" :include "options/arith_heuristic_pivot_rule.h" change the pivot rule for the basic variable (default is 'min', see --pivot-rule help) # The number of pivots before simplex rechecks every basic variable for a conflict diff --git a/src/theory/arith/arith_propagation_mode.cpp b/src/options/arith_propagation_mode.cpp similarity index 95% rename from src/theory/arith/arith_propagation_mode.cpp rename to src/options/arith_propagation_mode.cpp index 119761906..7f18a0356 100644 --- a/src/theory/arith/arith_propagation_mode.cpp +++ b/src/options/arith_propagation_mode.cpp @@ -15,7 +15,7 @@ ** \todo document this file **/ -#include "theory/arith/arith_propagation_mode.h" +#include "options/arith_propagation_mode.h" namespace CVC4 { @@ -41,4 +41,3 @@ std::ostream& operator<<(std::ostream& out, ArithPropagationMode mode) { } }/* CVC4 namespace */ - diff --git a/src/theory/arith/arith_propagation_mode.h b/src/options/arith_propagation_mode.h similarity index 96% rename from src/theory/arith/arith_propagation_mode.h rename to src/options/arith_propagation_mode.h index fe8f8c9cc..fa89496f0 100644 --- a/src/theory/arith/arith_propagation_mode.h +++ b/src/options/arith_propagation_mode.h @@ -24,12 +24,12 @@ namespace CVC4 { -typedef enum { +enum ArithPropagationMode { NO_PROP, UNATE_PROP, BOUND_INFERENCE_PROP, BOTH_PROP -} ArithPropagationMode; +}; std::ostream& operator<<(std::ostream& out, ArithPropagationMode rule) CVC4_PUBLIC; diff --git a/src/theory/arith/arith_unate_lemma_mode.cpp b/src/options/arith_unate_lemma_mode.cpp similarity index 95% rename from src/theory/arith/arith_unate_lemma_mode.cpp rename to src/options/arith_unate_lemma_mode.cpp index bb6066bb4..55fd8a01f 100644 --- a/src/theory/arith/arith_unate_lemma_mode.cpp +++ b/src/options/arith_unate_lemma_mode.cpp @@ -15,7 +15,7 @@ ** \todo document this file **/ -#include "theory/arith/arith_unate_lemma_mode.h" +#include "options/arith_unate_lemma_mode.h" namespace CVC4 { @@ -41,4 +41,3 @@ std::ostream& operator<<(std::ostream& out, ArithUnateLemmaMode mode) { } }/* CVC4 namespace */ - diff --git a/src/theory/arith/arith_unate_lemma_mode.h b/src/options/arith_unate_lemma_mode.h similarity index 100% rename from src/theory/arith/arith_unate_lemma_mode.h rename to src/options/arith_unate_lemma_mode.h diff --git a/src/theory/arrays/options b/src/options/arrays_options similarity index 95% rename from src/theory/arrays/options rename to src/options/arrays_options index 8ed80c1f1..096d773ca 100644 --- a/src/theory/arrays/options +++ b/src/options/arrays_options @@ -3,7 +3,7 @@ # See src/options/base_options for a description of this file format # -module ARRAYS "theory/arrays/options.h" Arrays theory +module ARRAYS "options/arrays_options.h" Arrays theory option arraysOptimizeLinear --arrays-optimize-linear bool :default true :read-write turn on optimization for linear array terms (see de Moura FMCAD 09 arrays paper) diff --git a/src/options/base_handlers.h b/src/options/base_handlers.h new file mode 100644 index 000000000..b37dde5c6 --- /dev/null +++ b/src/options/base_handlers.h @@ -0,0 +1,85 @@ +/********************* */ +/*! \file base_handlers.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: Kshitij Bansal + ** 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 [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__BASE_HANDLERS_H +#define __CVC4__BASE_HANDLERS_H + +#include +#include +#include + +namespace CVC4 { +namespace options { + +template