git.libre-soc.org Git - cvc5.git/commit

author	Aina Niemetz <aina.niemetz@gmail.com>
	Tue, 26 Mar 2019 18:33:55 +0000 (11:33 -0700)
committer	Aina Niemetz <aina.niemetz@gmail.com>
	Tue, 26 Mar 2019 18:33:55 +0000 (11:33 -0700)
commit	a6bd02c5c442b806b5e01fed40ab9d1017e42bc3
tree	13e5cd29c8d50100b8d8eb6a2db8839a6b661841	tree
parent	3090423f2cb47666a85db7b2f2df982239e7874d	commit \| diff

Update copyright headers.

1009 files changed:

examples/SimpleVC.java		diff \| blob \| history
examples/api/bitvectors-new.cpp		diff \| blob \| history
examples/api/bitvectors.cpp		diff \| blob \| history
examples/api/bitvectors_and_arrays-new.cpp		diff \| blob \| history
examples/api/bitvectors_and_arrays.cpp		diff \| blob \| history
examples/api/combination-new.cpp		diff \| blob \| history
examples/api/combination.cpp		diff \| blob \| history
examples/api/datatypes-new.cpp		diff \| blob \| history
examples/api/datatypes.cpp		diff \| blob \| history
examples/api/extract-new.cpp		diff \| blob \| history
examples/api/extract.cpp		diff \| blob \| history
examples/api/helloworld-new.cpp		diff \| blob \| history
examples/api/helloworld.cpp		diff \| blob \| history
examples/api/java/BitVectors.java		diff \| blob \| history
examples/api/java/BitVectorsAndArrays.java		diff \| blob \| history
examples/api/java/CVC4Streams.java		diff \| blob \| history
examples/api/java/Combination.java		diff \| blob \| history
examples/api/java/Datatypes.java		diff \| blob \| history
examples/api/java/HelloWorld.java		diff \| blob \| history
examples/api/java/LinearArith.java		diff \| blob \| history
examples/api/java/PipedInput.java		diff \| blob \| history
examples/api/java/Strings.java		diff \| blob \| history
examples/api/linear_arith-new.cpp		diff \| blob \| history
examples/api/linear_arith.cpp		diff \| blob \| history
examples/api/sets-new.cpp		diff \| blob \| history
examples/api/sets.cpp		diff \| blob \| history
examples/api/strings-new.cpp		diff \| blob \| history
examples/api/strings.cpp		diff \| blob \| history
examples/hashsmt/sha1.hpp		diff \| blob \| history
examples/hashsmt/sha1_collision.cpp		diff \| blob \| history
examples/hashsmt/sha1_inversion.cpp		diff \| blob \| history
examples/hashsmt/word.cpp		diff \| blob \| history
examples/hashsmt/word.h		diff \| blob \| history
examples/nra-translate/normalize.cpp		diff \| blob \| history
examples/nra-translate/smt2info.cpp		diff \| blob \| history
examples/nra-translate/smt2todreal.cpp		diff \| blob \| history
examples/nra-translate/smt2toisat.cpp		diff \| blob \| history
examples/nra-translate/smt2tomathematica.cpp		diff \| blob \| history
examples/nra-translate/smt2toqepcad.cpp		diff \| blob \| history
examples/nra-translate/smt2toredlog.cpp		diff \| blob \| history
examples/sets-translate/sets_translate.cpp		diff \| blob \| history
examples/simple_vc_cxx.cpp		diff \| blob \| history
examples/simple_vc_quant_cxx.cpp		diff \| blob \| history
examples/translator.cpp		diff \| blob \| history
src/api/cvc4cpp.cpp		diff \| blob \| history
src/api/cvc4cpp.h		diff \| blob \| history
src/api/cvc4cppkind.h		diff \| blob \| history
src/base/configuration.cpp		diff \| blob \| history
src/base/configuration.h		diff \| blob \| history
src/base/configuration_private.h		diff \| blob \| history
src/base/cvc4_assert.cpp		diff \| blob \| history
src/base/cvc4_assert.h		diff \| blob \| history
src/base/cvc4_check.cpp		diff \| blob \| history
src/base/cvc4_check.h		diff \| blob \| history
src/base/exception.cpp		diff \| blob \| history
src/base/exception.h		diff \| blob \| history
src/base/git_versioninfo.cpp.in		diff \| blob \| history
src/base/listener.cpp		diff \| blob \| history
src/base/listener.h		diff \| blob \| history
src/base/map_util.h		diff \| blob \| history
src/base/modal_exception.h		diff \| blob \| history
src/base/output.cpp		diff \| blob \| history
src/base/output.h		diff \| blob \| history
src/bindings/java_iterator_adapter.h		diff \| blob \| history
src/bindings/java_stream_adapters.h		diff \| blob \| history
src/bindings/swig.h		diff \| blob \| history
src/context/backtrackable.h		diff \| blob \| history
src/context/cddense_set.h		diff \| blob \| history
src/context/cdhashmap.h		diff \| blob \| history
src/context/cdhashmap_forward.h		diff \| blob \| history
src/context/cdhashset.h		diff \| blob \| history
src/context/cdhashset_forward.h		diff \| blob \| history
src/context/cdinsert_hashmap.h		diff \| blob \| history
src/context/cdinsert_hashmap_forward.h		diff \| blob \| history
src/context/cdlist.h		diff \| blob \| history
src/context/cdlist_forward.h		diff \| blob \| history
src/context/cdmaybe.h		diff \| blob \| history
src/context/cdo.h		diff \| blob \| history
src/context/cdqueue.h		diff \| blob \| history
src/context/cdtrail_queue.h		diff \| blob \| history
src/context/context.cpp		diff \| blob \| history
src/context/context.h		diff \| blob \| history
src/context/context_mm.cpp		diff \| blob \| history
src/context/context_mm.h		diff \| blob \| history
src/decision/decision_attributes.h		diff \| blob \| history
src/decision/decision_engine.cpp		diff \| blob \| history
src/decision/decision_engine.h		diff \| blob \| history
src/decision/decision_strategy.h		diff \| blob \| history
src/decision/justification_heuristic.cpp		diff \| blob \| history
src/decision/justification_heuristic.h		diff \| blob \| history
src/expr/array.h		diff \| blob \| history
src/expr/array_store_all.cpp		diff \| blob \| history
src/expr/array_store_all.h		diff \| blob \| history
src/expr/ascription_type.h		diff \| blob \| history
src/expr/attribute.cpp		diff \| blob \| history
src/expr/attribute.h		diff \| blob \| history
src/expr/attribute_internals.h		diff \| blob \| history
src/expr/attribute_unique_id.h		diff \| blob \| history
src/expr/chain.h		diff \| blob \| history
src/expr/datatype.cpp		diff \| blob \| history
src/expr/datatype.h		diff \| blob \| history
src/expr/emptyset.cpp		diff \| blob \| history
src/expr/emptyset.h		diff \| blob \| history
src/expr/expr_iomanip.cpp		diff \| blob \| history
src/expr/expr_iomanip.h		diff \| blob \| history
src/expr/expr_manager_scope.h		diff \| blob \| history
src/expr/expr_manager_template.cpp		diff \| blob \| history
src/expr/expr_manager_template.h		diff \| blob \| history
src/expr/expr_stream.h		diff \| blob \| history
src/expr/expr_template.cpp		diff \| blob \| history
src/expr/expr_template.h		diff \| blob \| history
src/expr/kind_map.h		diff \| blob \| history
src/expr/kind_template.cpp		diff \| blob \| history
src/expr/kind_template.h		diff \| blob \| history
src/expr/matcher.h		diff \| blob \| history
src/expr/metakind_template.cpp		diff \| blob \| history
src/expr/metakind_template.h		diff \| blob \| history
src/expr/node.cpp		diff \| blob \| history
src/expr/node.h		diff \| blob \| history
src/expr/node_algorithm.cpp		diff \| blob \| history
src/expr/node_algorithm.h		diff \| blob \| history
src/expr/node_builder.h		diff \| blob \| history
src/expr/node_manager.cpp		diff \| blob \| history
src/expr/node_manager.h		diff \| blob \| history
src/expr/node_manager_attributes.h		diff \| blob \| history
src/expr/node_manager_listeners.cpp		diff \| blob \| history
src/expr/node_manager_listeners.h		diff \| blob \| history
src/expr/node_self_iterator.h		diff \| blob \| history
src/expr/node_trie.cpp		diff \| blob \| history
src/expr/node_trie.h		diff \| blob \| history
src/expr/node_value.cpp		diff \| blob \| history
src/expr/node_value.h		diff \| blob \| history
src/expr/pickle_data.cpp		diff \| blob \| history
src/expr/pickle_data.h		diff \| blob \| history
src/expr/pickler.cpp		diff \| blob \| history
src/expr/pickler.h		diff \| blob \| history
src/expr/record.cpp		diff \| blob \| history
src/expr/record.h		diff \| blob \| history
src/expr/symbol_table.cpp		diff \| blob \| history
src/expr/symbol_table.h		diff \| blob \| history
src/expr/type.cpp		diff \| blob \| history
src/expr/type.h		diff \| blob \| history
src/expr/type_checker.h		diff \| blob \| history
src/expr/type_checker_template.cpp		diff \| blob \| history
src/expr/type_node.cpp		diff \| blob \| history
src/expr/type_node.h		diff \| blob \| history
src/expr/type_properties_template.h		diff \| blob \| history
src/expr/uninterpreted_constant.cpp		diff \| blob \| history
src/expr/uninterpreted_constant.h		diff \| blob \| history
src/expr/variable_type_map.h		diff \| blob \| history
src/include/cvc4.h		diff \| blob \| history
src/include/cvc4_private.h		diff \| blob \| history
src/include/cvc4_private_library.h		diff \| blob \| history
src/include/cvc4_public.h		diff \| blob \| history
src/include/cvc4parser_private.h		diff \| blob \| history
src/include/cvc4parser_public.h		diff \| blob \| history
src/lib/clock_gettime.c		diff \| blob \| history
src/lib/clock_gettime.h		diff \| blob \| history
src/lib/ffs.c		diff \| blob \| history
src/lib/ffs.h		diff \| blob \| history
src/lib/replacements.h		diff \| blob \| history
src/lib/strtok_r.c		diff \| blob \| history
src/lib/strtok_r.h		diff \| blob \| history
src/main/command_executor.cpp		diff \| blob \| history
src/main/command_executor.h		diff \| blob \| history
src/main/command_executor_portfolio.cpp		diff \| blob \| history
src/main/command_executor_portfolio.h		diff \| blob \| history
src/main/driver_unified.cpp		diff \| blob \| history
src/main/interactive_shell.cpp		diff \| blob \| history
src/main/interactive_shell.h		diff \| blob \| history
src/main/main.cpp		diff \| blob \| history
src/main/main.h		diff \| blob \| history
src/main/portfolio.cpp		diff \| blob \| history
src/main/portfolio.h		diff \| blob \| history
src/main/portfolio_util.cpp		diff \| blob \| history
src/main/portfolio_util.h		diff \| blob \| history
src/main/util.cpp		diff \| blob \| history
src/options/argument_extender.h		diff \| blob \| history
src/options/argument_extender_implementation.cpp		diff \| blob \| history
src/options/argument_extender_implementation.h		diff \| blob \| history
src/options/arith_heuristic_pivot_rule.cpp		diff \| blob \| history
src/options/arith_heuristic_pivot_rule.h		diff \| blob \| history
src/options/arith_propagation_mode.cpp		diff \| blob \| history
src/options/arith_propagation_mode.h		diff \| blob \| history
src/options/arith_unate_lemma_mode.cpp		diff \| blob \| history
src/options/arith_unate_lemma_mode.h		diff \| blob \| history
src/options/base_handlers.h		diff \| blob \| history
src/options/bool_to_bv_mode.cpp		diff \| blob \| history
src/options/bool_to_bv_mode.h		diff \| blob \| history
src/options/bv_bitblast_mode.cpp		diff \| blob \| history
src/options/bv_bitblast_mode.h		diff \| blob \| history
src/options/datatypes_modes.h		diff \| blob \| history
src/options/decision_mode.cpp		diff \| blob \| history
src/options/decision_mode.h		diff \| blob \| history
src/options/decision_weight.h		diff \| blob \| history
src/options/didyoumean.cpp		diff \| blob \| history
src/options/didyoumean.h		diff \| blob \| history
src/options/didyoumean_test.cpp		diff \| blob \| history
src/options/language.cpp		diff \| blob \| history
src/options/language.h		diff \| blob \| history
src/options/module_template.cpp		diff \| blob \| history
src/options/module_template.h		diff \| blob \| history
src/options/open_ostream.cpp		diff \| blob \| history
src/options/open_ostream.h		diff \| blob \| history
src/options/option_exception.cpp		diff \| blob \| history
src/options/option_exception.h		diff \| blob \| history
src/options/options.h		diff \| blob \| history
src/options/options_handler.cpp		diff \| blob \| history
src/options/options_handler.h		diff \| blob \| history
src/options/options_holder_template.h		diff \| blob \| history
src/options/options_public_functions.cpp		diff \| blob \| history
src/options/options_template.cpp		diff \| blob \| history
src/options/printer_modes.cpp		diff \| blob \| history
src/options/printer_modes.h		diff \| blob \| history
src/options/quantifiers_modes.cpp		diff \| blob \| history
src/options/quantifiers_modes.h		diff \| blob \| history
src/options/set_language.cpp		diff \| blob \| history
src/options/set_language.h		diff \| blob \| history
src/options/smt_modes.cpp		diff \| blob \| history
src/options/smt_modes.h		diff \| blob \| history
src/options/sygus_out_mode.h		diff \| blob \| history
src/options/theoryof_mode.cpp		diff \| blob \| history
src/options/theoryof_mode.h		diff \| blob \| history
src/options/ufss_mode.h		diff \| blob \| history
src/parser/antlr_input.cpp		diff \| blob \| history
src/parser/antlr_input.h		diff \| blob \| history
src/parser/antlr_input_imports.cpp		diff \| blob \| history
src/parser/antlr_line_buffered_input.cpp		diff \| blob \| history
src/parser/antlr_line_buffered_input.h		diff \| blob \| history
src/parser/antlr_tracing.h		diff \| blob \| history
src/parser/bounded_token_buffer.cpp		diff \| blob \| history
src/parser/bounded_token_buffer.h		diff \| blob \| history
src/parser/bounded_token_factory.cpp		diff \| blob \| history
src/parser/bounded_token_factory.h		diff \| blob \| history
src/parser/cvc/Cvc.g		diff \| blob \| history
src/parser/cvc/cvc_input.cpp		diff \| blob \| history
src/parser/cvc/cvc_input.h		diff \| blob \| history
src/parser/input.cpp		diff \| blob \| history
src/parser/input.h		diff \| blob \| history
src/parser/line_buffer.cpp		diff \| blob \| history
src/parser/line_buffer.h		diff \| blob \| history
src/parser/memory_mapped_input_buffer.cpp		diff \| blob \| history
src/parser/memory_mapped_input_buffer.h		diff \| blob \| history
src/parser/parser.cpp		diff \| blob \| history
src/parser/parser.h		diff \| blob \| history
src/parser/parser_builder.cpp		diff \| blob \| history
src/parser/parser_builder.h		diff \| blob \| history
src/parser/parser_exception.h		diff \| blob \| history
src/parser/smt1/Smt1.g		diff \| blob \| history
src/parser/smt1/smt1.cpp		diff \| blob \| history
src/parser/smt1/smt1.h		diff \| blob \| history
src/parser/smt1/smt1_input.cpp		diff \| blob \| history
src/parser/smt1/smt1_input.h		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/parser/smt2/smt2.cpp		diff \| blob \| history
src/parser/smt2/smt2.h		diff \| blob \| history
src/parser/smt2/smt2_input.cpp		diff \| blob \| history
src/parser/smt2/smt2_input.h		diff \| blob \| history
src/parser/smt2/sygus_input.cpp		diff \| blob \| history
src/parser/smt2/sygus_input.h		diff \| blob \| history
src/parser/tptp/Tptp.g		diff \| blob \| history
src/parser/tptp/tptp.cpp		diff \| blob \| history
src/parser/tptp/tptp.h		diff \| blob \| history
src/parser/tptp/tptp_input.cpp		diff \| blob \| history
src/parser/tptp/tptp_input.h		diff \| blob \| history
src/preprocessing/assertion_pipeline.cpp		diff \| blob \| history
src/preprocessing/assertion_pipeline.h		diff \| blob \| history
src/preprocessing/passes/apply_substs.cpp		diff \| blob \| history
src/preprocessing/passes/apply_substs.h		diff \| blob \| history
src/preprocessing/passes/apply_to_const.cpp		diff \| blob \| history
src/preprocessing/passes/apply_to_const.h		diff \| blob \| history
src/preprocessing/passes/bool_to_bv.cpp		diff \| blob \| history
src/preprocessing/passes/bool_to_bv.h		diff \| blob \| history
src/preprocessing/passes/bv_abstraction.cpp		diff \| blob \| history
src/preprocessing/passes/bv_abstraction.h		diff \| blob \| history
src/preprocessing/passes/bv_ackermann.cpp		diff \| blob \| history
src/preprocessing/passes/bv_ackermann.h		diff \| blob \| history
src/preprocessing/passes/bv_eager_atoms.cpp		diff \| blob \| history
src/preprocessing/passes/bv_eager_atoms.h		diff \| blob \| history
src/preprocessing/passes/bv_gauss.cpp		diff \| blob \| history
src/preprocessing/passes/bv_gauss.h		diff \| blob \| history
src/preprocessing/passes/bv_intro_pow2.cpp		diff \| blob \| history
src/preprocessing/passes/bv_intro_pow2.h		diff \| blob \| history
src/preprocessing/passes/bv_to_bool.cpp		diff \| blob \| history
src/preprocessing/passes/bv_to_bool.h		diff \| blob \| history
src/preprocessing/passes/extended_rewriter_pass.cpp		diff \| blob \| history
src/preprocessing/passes/extended_rewriter_pass.h		diff \| blob \| history
src/preprocessing/passes/global_negate.cpp		diff \| blob \| history
src/preprocessing/passes/global_negate.h		diff \| blob \| history
src/preprocessing/passes/int_to_bv.cpp		diff \| blob \| history
src/preprocessing/passes/int_to_bv.h		diff \| blob \| history
src/preprocessing/passes/ite_removal.cpp		diff \| blob \| history
src/preprocessing/passes/ite_removal.h		diff \| blob \| history
src/preprocessing/passes/ite_simp.cpp		diff \| blob \| history
src/preprocessing/passes/ite_simp.h		diff \| blob \| history
src/preprocessing/passes/miplib_trick.cpp		diff \| blob \| history
src/preprocessing/passes/miplib_trick.h		diff \| blob \| history
src/preprocessing/passes/nl_ext_purify.cpp		diff \| blob \| history
src/preprocessing/passes/nl_ext_purify.h		diff \| blob \| history
src/preprocessing/passes/non_clausal_simp.cpp		diff \| blob \| history
src/preprocessing/passes/non_clausal_simp.h		diff \| blob \| history
src/preprocessing/passes/pseudo_boolean_processor.cpp		diff \| blob \| history
src/preprocessing/passes/pseudo_boolean_processor.h		diff \| blob \| history
src/preprocessing/passes/quantifier_macros.cpp		diff \| blob \| history
src/preprocessing/passes/quantifier_macros.h		diff \| blob \| history
src/preprocessing/passes/quantifiers_preprocess.cpp		diff \| blob \| history
src/preprocessing/passes/quantifiers_preprocess.h		diff \| blob \| history
src/preprocessing/passes/real_to_int.cpp		diff \| blob \| history
src/preprocessing/passes/real_to_int.h		diff \| blob \| history
src/preprocessing/passes/rewrite.cpp		diff \| blob \| history
src/preprocessing/passes/rewrite.h		diff \| blob \| history
src/preprocessing/passes/sep_skolem_emp.cpp		diff \| blob \| history
src/preprocessing/passes/sep_skolem_emp.h		diff \| blob \| history
src/preprocessing/passes/sort_infer.cpp		diff \| blob \| history
src/preprocessing/passes/sort_infer.h		diff \| blob \| history
src/preprocessing/passes/static_learning.cpp		diff \| blob \| history
src/preprocessing/passes/static_learning.h		diff \| blob \| history
src/preprocessing/passes/sygus_abduct.cpp		diff \| blob \| history
src/preprocessing/passes/sygus_inference.cpp		diff \| blob \| history
src/preprocessing/passes/sygus_inference.h		diff \| blob \| history
src/preprocessing/passes/symmetry_breaker.cpp		diff \| blob \| history
src/preprocessing/passes/symmetry_breaker.h		diff \| blob \| history
src/preprocessing/passes/symmetry_detect.cpp		diff \| blob \| history
src/preprocessing/passes/symmetry_detect.h		diff \| blob \| history
src/preprocessing/passes/synth_rew_rules.cpp		diff \| blob \| history
src/preprocessing/passes/synth_rew_rules.h		diff \| blob \| history
src/preprocessing/passes/theory_preprocess.cpp		diff \| blob \| history
src/preprocessing/passes/theory_preprocess.h		diff \| blob \| history
src/preprocessing/passes/unconstrained_simplifier.cpp		diff \| blob \| history
src/preprocessing/passes/unconstrained_simplifier.h		diff \| blob \| history
src/preprocessing/preprocessing_pass.cpp		diff \| blob \| history
src/preprocessing/preprocessing_pass.h		diff \| blob \| history
src/preprocessing/preprocessing_pass_context.cpp		diff \| blob \| history
src/preprocessing/preprocessing_pass_context.h		diff \| blob \| history
src/preprocessing/preprocessing_pass_registry.cpp		diff \| blob \| history
src/preprocessing/preprocessing_pass_registry.h		diff \| blob \| history
src/preprocessing/util/ite_utilities.cpp		diff \| blob \| history
src/preprocessing/util/ite_utilities.h		diff \| blob \| history
src/printer/ast/ast_printer.cpp		diff \| blob \| history
src/printer/ast/ast_printer.h		diff \| blob \| history
src/printer/cvc/cvc_printer.cpp		diff \| blob \| history
src/printer/cvc/cvc_printer.h		diff \| blob \| history
src/printer/dagification_visitor.cpp		diff \| blob \| history
src/printer/dagification_visitor.h		diff \| blob \| history
src/printer/printer.cpp		diff \| blob \| history
src/printer/printer.h		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.h		diff \| blob \| history
src/printer/sygus_print_callback.cpp		diff \| blob \| history
src/printer/sygus_print_callback.h		diff \| blob \| history
src/printer/tptp/tptp_printer.cpp		diff \| blob \| history
src/printer/tptp/tptp_printer.h		diff \| blob \| history
src/proof/arith_proof.cpp		diff \| blob \| history
src/proof/arith_proof.h		diff \| blob \| history
src/proof/arith_proof_recorder.cpp		diff \| blob \| history
src/proof/arith_proof_recorder.h		diff \| blob \| history
src/proof/array_proof.cpp		diff \| blob \| history
src/proof/array_proof.h		diff \| blob \| history
src/proof/bitvector_proof.cpp		diff \| blob \| history
src/proof/bitvector_proof.h		diff \| blob \| history
src/proof/clausal_bitvector_proof.h		diff \| blob \| history
src/proof/clause_id.h		diff \| blob \| history
src/proof/cnf_proof.cpp		diff \| blob \| history
src/proof/cnf_proof.h		diff \| blob \| history
src/proof/dimacs_printer.cpp		diff \| blob \| history
src/proof/dimacs_printer.h		diff \| blob \| history
src/proof/drat/drat_proof.cpp		diff \| blob \| history
src/proof/drat/drat_proof.h		diff \| blob \| history
src/proof/lemma_proof.cpp		diff \| blob \| history
src/proof/lemma_proof.h		diff \| blob \| history
src/proof/lfsc_proof_printer.cpp		diff \| blob \| history
src/proof/lfsc_proof_printer.h		diff \| blob \| history
src/proof/lrat/lrat_proof.cpp		diff \| blob \| history
src/proof/lrat/lrat_proof.h		diff \| blob \| history
src/proof/proof.h		diff \| blob \| history
src/proof/proof_manager.cpp		diff \| blob \| history
src/proof/proof_manager.h		diff \| blob \| history
src/proof/proof_output_channel.cpp		diff \| blob \| history
src/proof/proof_output_channel.h		diff \| blob \| history
src/proof/proof_utils.cpp		diff \| blob \| history
src/proof/proof_utils.h		diff \| blob \| history
src/proof/resolution_bitvector_proof.cpp		diff \| blob \| history
src/proof/resolution_bitvector_proof.h		diff \| blob \| history
src/proof/sat_proof.h		diff \| blob \| history
src/proof/sat_proof_implementation.h		diff \| blob \| history
src/proof/simplify_boolean_node.cpp		diff \| blob \| history
src/proof/simplify_boolean_node.h		diff \| blob \| history
src/proof/skolemization_manager.cpp		diff \| blob \| history
src/proof/skolemization_manager.h		diff \| blob \| history
src/proof/theory_proof.cpp		diff \| blob \| history
src/proof/theory_proof.h		diff \| blob \| history
src/proof/uf_proof.cpp		diff \| blob \| history
src/proof/uf_proof.h		diff \| blob \| history
src/proof/unsat_core.cpp		diff \| blob \| history
src/proof/unsat_core.h		diff \| blob \| history
src/prop/bv_sat_solver_notify.h		diff \| blob \| history
src/prop/bvminisat/bvminisat.cpp		diff \| blob \| history
src/prop/bvminisat/bvminisat.h		diff \| blob \| history
src/prop/cadical.cpp		diff \| blob \| history
src/prop/cadical.h		diff \| blob \| history
src/prop/cnf_stream.cpp		diff \| blob \| history
src/prop/cnf_stream.h		diff \| blob \| history
src/prop/cryptominisat.cpp		diff \| blob \| history
src/prop/cryptominisat.h		diff \| blob \| history
src/prop/minisat/minisat.cpp		diff \| blob \| history
src/prop/minisat/minisat.h		diff \| blob \| history
src/prop/prop_engine.cpp		diff \| blob \| history
src/prop/prop_engine.h		diff \| blob \| history
src/prop/registrar.h		diff \| blob \| history
src/prop/sat_solver.h		diff \| blob \| history
src/prop/sat_solver_factory.cpp		diff \| blob \| history
src/prop/sat_solver_factory.h		diff \| blob \| history
src/prop/sat_solver_types.h		diff \| blob \| history
src/prop/theory_proxy.cpp		diff \| blob \| history
src/prop/theory_proxy.h		diff \| blob \| history
src/smt/command.cpp		diff \| blob \| history
src/smt/command.h		diff \| blob \| history
src/smt/command_list.cpp		diff \| blob \| history
src/smt/command_list.h		diff \| blob \| history
src/smt/dump.cpp		diff \| blob \| history
src/smt/dump.h		diff \| blob \| history
src/smt/logic_exception.h		diff \| blob \| history
src/smt/logic_request.cpp		diff \| blob \| history
src/smt/logic_request.h		diff \| blob \| history
src/smt/managed_ostreams.cpp		diff \| blob \| history
src/smt/managed_ostreams.h		diff \| blob \| history
src/smt/model.cpp		diff \| blob \| history
src/smt/model.h		diff \| blob \| history
src/smt/model_core_builder.cpp		diff \| blob \| history
src/smt/model_core_builder.h		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine.h		diff \| blob \| history
src/smt/smt_engine_scope.cpp		diff \| blob \| history
src/smt/smt_engine_scope.h		diff \| blob \| history
src/smt/smt_statistics_registry.cpp		diff \| blob \| history
src/smt/smt_statistics_registry.h		diff \| blob \| history
src/smt/term_formula_removal.cpp		diff \| blob \| history
src/smt/term_formula_removal.h		diff \| blob \| history
src/smt/update_ostream.h		diff \| blob \| history
src/smt_util/boolean_simplification.cpp		diff \| blob \| history
src/smt_util/boolean_simplification.h		diff \| blob \| history
src/smt_util/lemma_channels.cpp		diff \| blob \| history
src/smt_util/lemma_channels.h		diff \| blob \| history
src/smt_util/lemma_input_channel.h		diff \| blob \| history
src/smt_util/lemma_output_channel.h		diff \| blob \| history
src/smt_util/nary_builder.cpp		diff \| blob \| history
src/smt_util/nary_builder.h		diff \| blob \| history
src/smt_util/node_visitor.h		diff \| blob \| history
src/theory/arith/approx_simplex.cpp		diff \| blob \| history
src/theory/arith/approx_simplex.h		diff \| blob \| history
src/theory/arith/arith_ite_utils.cpp		diff \| blob \| history
src/theory/arith/arith_ite_utils.h		diff \| blob \| history
src/theory/arith/arith_msum.cpp		diff \| blob \| history
src/theory/arith/arith_msum.h		diff \| blob \| history
src/theory/arith/arith_rewriter.cpp		diff \| blob \| history
src/theory/arith/arith_rewriter.h		diff \| blob \| history
src/theory/arith/arith_static_learner.cpp		diff \| blob \| history
src/theory/arith/arith_static_learner.h		diff \| blob \| history
src/theory/arith/arith_utilities.h		diff \| blob \| history
src/theory/arith/arithvar.cpp		diff \| blob \| history
src/theory/arith/arithvar.h		diff \| blob \| history
src/theory/arith/arithvar_node_map.h		diff \| blob \| history
src/theory/arith/attempt_solution_simplex.cpp		diff \| blob \| history
src/theory/arith/attempt_solution_simplex.h		diff \| blob \| history
src/theory/arith/bound_counts.h		diff \| blob \| history
src/theory/arith/callbacks.cpp		diff \| blob \| history
src/theory/arith/callbacks.h		diff \| blob \| history
src/theory/arith/congruence_manager.cpp		diff \| blob \| history
src/theory/arith/congruence_manager.h		diff \| blob \| history
src/theory/arith/constraint.cpp		diff \| blob \| history
src/theory/arith/constraint.h		diff \| blob \| history
src/theory/arith/constraint_forward.h		diff \| blob \| history
src/theory/arith/cut_log.cpp		diff \| blob \| history
src/theory/arith/cut_log.h		diff \| blob \| history
src/theory/arith/delta_rational.cpp		diff \| blob \| history
src/theory/arith/delta_rational.h		diff \| blob \| history
src/theory/arith/dio_solver.cpp		diff \| blob \| history
src/theory/arith/dio_solver.h		diff \| blob \| history
src/theory/arith/dual_simplex.cpp		diff \| blob \| history
src/theory/arith/dual_simplex.h		diff \| blob \| history
src/theory/arith/error_set.cpp		diff \| blob \| history
src/theory/arith/error_set.h		diff \| blob \| history
src/theory/arith/fc_simplex.cpp		diff \| blob \| history
src/theory/arith/fc_simplex.h		diff \| blob \| history
src/theory/arith/infer_bounds.cpp		diff \| blob \| history
src/theory/arith/infer_bounds.h		diff \| blob \| history
src/theory/arith/linear_equality.cpp		diff \| blob \| history
src/theory/arith/linear_equality.h		diff \| blob \| history
src/theory/arith/matrix.cpp		diff \| blob \| history
src/theory/arith/matrix.h		diff \| blob \| history
src/theory/arith/nonlinear_extension.cpp		diff \| blob \| history
src/theory/arith/nonlinear_extension.h		diff \| blob \| history
src/theory/arith/normal_form.cpp		diff \| blob \| history
src/theory/arith/normal_form.h		diff \| blob \| history
src/theory/arith/partial_model.cpp		diff \| blob \| history
src/theory/arith/partial_model.h		diff \| blob \| history
src/theory/arith/simplex.cpp		diff \| blob \| history
src/theory/arith/simplex.h		diff \| blob \| history
src/theory/arith/simplex_update.cpp		diff \| blob \| history
src/theory/arith/simplex_update.h		diff \| blob \| history
src/theory/arith/soi_simplex.cpp		diff \| blob \| history
src/theory/arith/soi_simplex.h		diff \| blob \| history
src/theory/arith/tableau.cpp		diff \| blob \| history
src/theory/arith/tableau.h		diff \| blob \| history
src/theory/arith/tableau_sizes.cpp		diff \| blob \| history
src/theory/arith/tableau_sizes.h		diff \| blob \| history
src/theory/arith/theory_arith.cpp		diff \| blob \| history
src/theory/arith/theory_arith.h		diff \| blob \| history
src/theory/arith/theory_arith_private.cpp		diff \| blob \| history
src/theory/arith/theory_arith_private.h		diff \| blob \| history
src/theory/arith/theory_arith_private_forward.h		diff \| blob \| history
src/theory/arith/theory_arith_type_rules.h		diff \| blob \| history
src/theory/arith/type_enumerator.h		diff \| blob \| history
src/theory/arrays/array_info.cpp		diff \| blob \| history
src/theory/arrays/array_info.h		diff \| blob \| history
src/theory/arrays/array_proof_reconstruction.cpp		diff \| blob \| history
src/theory/arrays/array_proof_reconstruction.h		diff \| blob \| history
src/theory/arrays/static_fact_manager.cpp		diff \| blob \| history
src/theory/arrays/static_fact_manager.h		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.h		diff \| blob \| history
src/theory/arrays/theory_arrays_rewriter.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays_rewriter.h		diff \| blob \| history
src/theory/arrays/theory_arrays_type_rules.h		diff \| blob \| history
src/theory/arrays/type_enumerator.h		diff \| blob \| history
src/theory/arrays/union_find.cpp		diff \| blob \| history
src/theory/arrays/union_find.h		diff \| blob \| history
src/theory/assertion.cpp		diff \| blob \| history
src/theory/assertion.h		diff \| blob \| history
src/theory/atom_requests.cpp		diff \| blob \| history
src/theory/atom_requests.h		diff \| blob \| history
src/theory/booleans/circuit_propagator.cpp		diff \| blob \| history
src/theory/booleans/circuit_propagator.h		diff \| blob \| history
src/theory/booleans/theory_bool.cpp		diff \| blob \| history
src/theory/booleans/theory_bool.h		diff \| blob \| history
src/theory/booleans/theory_bool_rewriter.cpp		diff \| blob \| history
src/theory/booleans/theory_bool_rewriter.h		diff \| blob \| history
src/theory/booleans/theory_bool_type_rules.h		diff \| blob \| history
src/theory/booleans/type_enumerator.h		diff \| blob \| history
src/theory/builtin/theory_builtin.cpp		diff \| blob \| history
src/theory/builtin/theory_builtin.h		diff \| blob \| history
src/theory/builtin/theory_builtin_rewriter.cpp		diff \| blob \| history
src/theory/builtin/theory_builtin_rewriter.h		diff \| blob \| history
src/theory/builtin/theory_builtin_type_rules.h		diff \| blob \| history
src/theory/builtin/type_enumerator.cpp		diff \| blob \| history
src/theory/builtin/type_enumerator.h		diff \| blob \| history
src/theory/bv/abstraction.cpp		diff \| blob \| history
src/theory/bv/abstraction.h		diff \| blob \| history
src/theory/bv/bitblast/aig_bitblaster.cpp		diff \| blob \| history
src/theory/bv/bitblast/aig_bitblaster.h		diff \| blob \| history
src/theory/bv/bitblast/bitblast_strategies_template.h		diff \| blob \| history
src/theory/bv/bitblast/bitblast_utils.h		diff \| blob \| history
src/theory/bv/bitblast/bitblaster.h		diff \| blob \| history
src/theory/bv/bitblast/eager_bitblaster.cpp		diff \| blob \| history
src/theory/bv/bitblast/eager_bitblaster.h		diff \| blob \| history
src/theory/bv/bitblast/lazy_bitblaster.cpp		diff \| blob \| history
src/theory/bv/bitblast/lazy_bitblaster.h		diff \| blob \| history
src/theory/bv/bv_eager_solver.cpp		diff \| blob \| history
src/theory/bv/bv_eager_solver.h		diff \| blob \| history
src/theory/bv/bv_inequality_graph.cpp		diff \| blob \| history
src/theory/bv/bv_inequality_graph.h		diff \| blob \| history
src/theory/bv/bv_quick_check.cpp		diff \| blob \| history
src/theory/bv/bv_quick_check.h		diff \| blob \| history
src/theory/bv/bv_subtheory.h		diff \| blob \| history
src/theory/bv/bv_subtheory_algebraic.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_algebraic.h		diff \| blob \| history
src/theory/bv/bv_subtheory_bitblast.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_bitblast.h		diff \| blob \| history
src/theory/bv/bv_subtheory_core.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_core.h		diff \| blob \| history
src/theory/bv/bv_subtheory_inequality.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_inequality.h		diff \| blob \| history
src/theory/bv/slicer.cpp		diff \| blob \| history
src/theory/bv/slicer.h		diff \| blob \| history
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/bv/theory_bv.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_core.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_normalization.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_simplification.h		diff \| blob \| history
src/theory/bv/theory_bv_rewriter.cpp		diff \| blob \| history
src/theory/bv/theory_bv_rewriter.h		diff \| blob \| history
src/theory/bv/theory_bv_type_rules.h		diff \| blob \| history
src/theory/bv/theory_bv_utils.cpp		diff \| blob \| history
src/theory/bv/theory_bv_utils.h		diff \| blob \| history
src/theory/bv/type_enumerator.h		diff \| blob \| history
src/theory/care_graph.h		diff \| blob \| history
src/theory/datatypes/datatypes_rewriter.cpp		diff \| blob \| history
src/theory/datatypes/datatypes_rewriter.h		diff \| blob \| history
src/theory/datatypes/datatypes_sygus.cpp		diff \| blob \| history
src/theory/datatypes/datatypes_sygus.h		diff \| blob \| history
src/theory/datatypes/sygus_simple_sym.cpp		diff \| blob \| history
src/theory/datatypes/sygus_simple_sym.h		diff \| blob \| history
src/theory/datatypes/theory_datatypes.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes.h		diff \| blob \| history
src/theory/datatypes/theory_datatypes_type_rules.h		diff \| blob \| history
src/theory/datatypes/type_enumerator.cpp		diff \| blob \| history
src/theory/datatypes/type_enumerator.h		diff \| blob \| history
src/theory/decision_manager.cpp		diff \| blob \| history
src/theory/decision_manager.h		diff \| blob \| history
src/theory/decision_strategy.cpp		diff \| blob \| history
src/theory/decision_strategy.h		diff \| blob \| history
src/theory/evaluator.cpp		diff \| blob \| history
src/theory/evaluator.h		diff \| blob \| history
src/theory/example/ecdata.cpp		diff \| blob \| history
src/theory/example/ecdata.h		diff \| blob \| history
src/theory/example/theory_uf_tim.cpp		diff \| blob \| history
src/theory/example/theory_uf_tim.h		diff \| blob \| history
src/theory/ext_theory.cpp		diff \| blob \| history
src/theory/ext_theory.h		diff \| blob \| history
src/theory/fp/fp_converter.cpp		diff \| blob \| history
src/theory/fp/fp_converter.h		diff \| blob \| history
src/theory/fp/theory_fp.cpp		diff \| blob \| history
src/theory/fp/theory_fp.h		diff \| blob \| history
src/theory/fp/theory_fp_rewriter.cpp		diff \| blob \| history
src/theory/fp/theory_fp_rewriter.h		diff \| blob \| history
src/theory/fp/theory_fp_type_rules.h		diff \| blob \| history
src/theory/fp/type_enumerator.h		diff \| blob \| history
src/theory/idl/idl_assertion.cpp		diff \| blob \| history
src/theory/idl/idl_assertion.h		diff \| blob \| history
src/theory/idl/idl_assertion_db.cpp		diff \| blob \| history
src/theory/idl/idl_assertion_db.h		diff \| blob \| history
src/theory/idl/idl_model.cpp		diff \| blob \| history
src/theory/idl/idl_model.h		diff \| blob \| history
src/theory/idl/theory_idl.cpp		diff \| blob \| history
src/theory/idl/theory_idl.h		diff \| blob \| history
src/theory/interrupted.h		diff \| blob \| history
src/theory/logic_info.cpp		diff \| blob \| history
src/theory/logic_info.h		diff \| blob \| history
src/theory/output_channel.h		diff \| blob \| history
src/theory/quantifiers/alpha_equivalence.cpp		diff \| blob \| history
src/theory/quantifiers/alpha_equivalence.h		diff \| blob \| history
src/theory/quantifiers/anti_skolem.cpp		diff \| blob \| history
src/theory/quantifiers/anti_skolem.h		diff \| blob \| history
src/theory/quantifiers/bv_inverter.cpp		diff \| blob \| history
src/theory/quantifiers/bv_inverter.h		diff \| blob \| history
src/theory/quantifiers/bv_inverter_utils.cpp		diff \| blob \| history
src/theory/quantifiers/bv_inverter_utils.h		diff \| blob \| history
src/theory/quantifiers/candidate_rewrite_database.cpp		diff \| blob \| history
src/theory/quantifiers/candidate_rewrite_database.h		diff \| blob \| history
src/theory/quantifiers/candidate_rewrite_filter.cpp		diff \| blob \| history
src/theory/quantifiers/candidate_rewrite_filter.h		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_arith_instantiator.h		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_bv_instantiator.h		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_dt_instantiator.h		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_epr_instantiator.h		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_instantiator.h		diff \| blob \| history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.h		diff \| blob \| history
src/theory/quantifiers/conjecture_generator.cpp		diff \| blob \| history
src/theory/quantifiers/conjecture_generator.h		diff \| blob \| history
src/theory/quantifiers/dynamic_rewrite.cpp		diff \| blob \| history
src/theory/quantifiers/dynamic_rewrite.h		diff \| blob \| history
src/theory/quantifiers/ematching/candidate_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/candidate_generator.h		diff \| blob \| history
src/theory/quantifiers/ematching/ho_trigger.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/ho_trigger.h		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator.h		diff \| blob \| history
src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_strategy_e_matching.h		diff \| blob \| history
src/theory/quantifiers/ematching/instantiation_engine.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/instantiation_engine.h		diff \| blob \| history
src/theory/quantifiers/ematching/trigger.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/trigger.h		diff \| blob \| history
src/theory/quantifiers/equality_infer.cpp		diff \| blob \| history
src/theory/quantifiers/equality_infer.h		diff \| blob \| history
src/theory/quantifiers/equality_query.cpp		diff \| blob \| history
src/theory/quantifiers/equality_query.h		diff \| blob \| history
src/theory/quantifiers/expr_miner.cpp		diff \| blob \| history
src/theory/quantifiers/expr_miner.h		diff \| blob \| history
src/theory/quantifiers/expr_miner_manager.cpp		diff \| blob \| history
src/theory/quantifiers/expr_miner_manager.h		diff \| blob \| history
src/theory/quantifiers/extended_rewrite.cpp		diff \| blob \| history
src/theory/quantifiers/extended_rewrite.h		diff \| blob \| history
src/theory/quantifiers/first_order_model.cpp		diff \| blob \| history
src/theory/quantifiers/first_order_model.h		diff \| blob \| history
src/theory/quantifiers/fmf/bounded_integers.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/bounded_integers.h		diff \| blob \| history
src/theory/quantifiers/fmf/full_model_check.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/full_model_check.h		diff \| blob \| history
src/theory/quantifiers/fmf/model_builder.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/model_builder.h		diff \| blob \| history
src/theory/quantifiers/fmf/model_engine.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/model_engine.h		diff \| blob \| history
src/theory/quantifiers/fun_def_process.cpp		diff \| blob \| history
src/theory/quantifiers/fun_def_process.h		diff \| blob \| history
src/theory/quantifiers/inst_match.cpp		diff \| blob \| history
src/theory/quantifiers/inst_match.h		diff \| blob \| history
src/theory/quantifiers/inst_match_trie.cpp		diff \| blob \| history
src/theory/quantifiers/inst_match_trie.h		diff \| blob \| history
src/theory/quantifiers/inst_propagator.cpp		diff \| blob \| history
src/theory/quantifiers/inst_propagator.h		diff \| blob \| history
src/theory/quantifiers/inst_strategy_enumerative.cpp		diff \| blob \| history
src/theory/quantifiers/inst_strategy_enumerative.h		diff \| blob \| history
src/theory/quantifiers/instantiate.cpp		diff \| blob \| history
src/theory/quantifiers/instantiate.h		diff \| blob \| history
src/theory/quantifiers/lazy_trie.cpp		diff \| blob \| history
src/theory/quantifiers/lazy_trie.h		diff \| blob \| history
src/theory/quantifiers/local_theory_ext.cpp		diff \| blob \| history
src/theory/quantifiers/local_theory_ext.h		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.cpp		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.h		diff \| blob \| history
src/theory/quantifiers/quant_epr.cpp		diff \| blob \| history
src/theory/quantifiers/quant_epr.h		diff \| blob \| history
src/theory/quantifiers/quant_relevance.cpp		diff \| blob \| history
src/theory/quantifiers/quant_relevance.h		diff \| blob \| history
src/theory/quantifiers/quant_split.cpp		diff \| blob \| history
src/theory/quantifiers/quant_split.h		diff \| blob \| history
src/theory/quantifiers/quant_util.cpp		diff \| blob \| history
src/theory/quantifiers/quant_util.h		diff \| blob \| history
src/theory/quantifiers/quantifiers_attributes.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_attributes.h		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.h		diff \| blob \| history
src/theory/quantifiers/query_generator.cpp		diff \| blob \| history
src/theory/quantifiers/query_generator.h		diff \| blob \| history
src/theory/quantifiers/relevant_domain.cpp		diff \| blob \| history
src/theory/quantifiers/relevant_domain.h		diff \| blob \| history
src/theory/quantifiers/rewrite_engine.cpp		diff \| blob \| history
src/theory/quantifiers/rewrite_engine.h		diff \| blob \| history
src/theory/quantifiers/single_inv_partition.cpp		diff \| blob \| history
src/theory/quantifiers/single_inv_partition.h		diff \| blob \| history
src/theory/quantifiers/skolemize.cpp		diff \| blob \| history
src/theory/quantifiers/skolemize.h		diff \| blob \| history
src/theory/quantifiers/solution_filter.cpp		diff \| blob \| history
src/theory/quantifiers/solution_filter.h		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_single_inv.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_single_inv.h		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h		diff \| blob \| history
src/theory/quantifiers/sygus/cegis.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis.h		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_unif.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_unif.h		diff \| blob \| history
src/theory/quantifiers/sygus/enum_stream_substitution.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/enum_stream_substitution.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_enumerator.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_enumerator.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_eval_unfold.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_eval_unfold.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_explain.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_explain.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_cons.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_norm.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_norm.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_red.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_red.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_invariance.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_invariance.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_module.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_module.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_pbe.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_pbe.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_process_conj.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_process_conj.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_repair_const.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_repair_const.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_io.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_io.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_rl.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_rl.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_strat.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_strat.h		diff \| blob \| history
src/theory/quantifiers/sygus/synth_conjecture.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_conjecture.h		diff \| blob \| history
src/theory/quantifiers/sygus/synth_engine.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_engine.h		diff \| blob \| history
src/theory/quantifiers/sygus/term_database_sygus.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/term_database_sygus.h		diff \| blob \| history
src/theory/quantifiers/sygus_sampler.cpp		diff \| blob \| history
src/theory/quantifiers/sygus_sampler.h		diff \| blob \| history
src/theory/quantifiers/term_canonize.cpp		diff \| blob \| history
src/theory/quantifiers/term_canonize.h		diff \| blob \| history
src/theory/quantifiers/term_database.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.h		diff \| blob \| history
src/theory/quantifiers/term_enumeration.cpp		diff \| blob \| history
src/theory/quantifiers/term_enumeration.h		diff \| blob \| history
src/theory/quantifiers/term_util.cpp		diff \| blob \| history
src/theory/quantifiers/term_util.h		diff \| blob \| history
src/theory/quantifiers/theory_quantifiers.cpp		diff \| blob \| history
src/theory/quantifiers/theory_quantifiers.h		diff \| blob \| history
src/theory/quantifiers/theory_quantifiers_type_rules.h		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/quantifiers_engine.h		diff \| blob \| history
src/theory/rep_set.cpp		diff \| blob \| history
src/theory/rep_set.h		diff \| blob \| history
src/theory/rewriter.cpp		diff \| blob \| history
src/theory/rewriter.h		diff \| blob \| history
src/theory/rewriter_attributes.h		diff \| blob \| history
src/theory/rewriter_tables_template.h		diff \| blob \| history
src/theory/sep/theory_sep.cpp		diff \| blob \| history
src/theory/sep/theory_sep.h		diff \| blob \| history
src/theory/sep/theory_sep_rewriter.cpp		diff \| blob \| history
src/theory/sep/theory_sep_rewriter.h		diff \| blob \| history
src/theory/sep/theory_sep_type_rules.h		diff \| blob \| history
src/theory/sets/normal_form.h		diff \| blob \| history
src/theory/sets/rels_utils.h		diff \| blob \| history
src/theory/sets/theory_sets.cpp		diff \| blob \| history
src/theory/sets/theory_sets.h		diff \| blob \| history
src/theory/sets/theory_sets_private.cpp		diff \| blob \| history
src/theory/sets/theory_sets_private.h		diff \| blob \| history
src/theory/sets/theory_sets_rels.cpp		diff \| blob \| history
src/theory/sets/theory_sets_rels.h		diff \| blob \| history
src/theory/sets/theory_sets_rewriter.cpp		diff \| blob \| history
src/theory/sets/theory_sets_rewriter.h		diff \| blob \| history
src/theory/sets/theory_sets_type_enumerator.h		diff \| blob \| history
src/theory/sets/theory_sets_type_rules.h		diff \| blob \| history
src/theory/shared_terms_database.cpp		diff \| blob \| history
src/theory/shared_terms_database.h		diff \| blob \| history
src/theory/sort_inference.cpp		diff \| blob \| history
src/theory/sort_inference.h		diff \| blob \| history
src/theory/strings/regexp_elim.cpp		diff \| blob \| history
src/theory/strings/regexp_elim.h		diff \| blob \| history
src/theory/strings/regexp_operation.cpp		diff \| blob \| history
src/theory/strings/regexp_operation.h		diff \| blob \| history
src/theory/strings/regexp_solver.cpp		diff \| blob \| history
src/theory/strings/regexp_solver.h		diff \| blob \| history
src/theory/strings/skolem_cache.cpp		diff \| blob \| history
src/theory/strings/skolem_cache.h		diff \| blob \| history
src/theory/strings/theory_strings.cpp		diff \| blob \| history
src/theory/strings/theory_strings.h		diff \| blob \| history
src/theory/strings/theory_strings_preprocess.cpp		diff \| blob \| history
src/theory/strings/theory_strings_preprocess.h		diff \| blob \| history
src/theory/strings/theory_strings_rewriter.cpp		diff \| blob \| history
src/theory/strings/theory_strings_rewriter.h		diff \| blob \| history
src/theory/strings/theory_strings_type_rules.h		diff \| blob \| history
src/theory/strings/type_enumerator.h		diff \| blob \| history
src/theory/subs_minimize.cpp		diff \| blob \| history
src/theory/subs_minimize.h		diff \| blob \| history
src/theory/substitutions.cpp		diff \| blob \| history
src/theory/substitutions.h		diff \| blob \| history
src/theory/term_registration_visitor.cpp		diff \| blob \| history
src/theory/term_registration_visitor.h		diff \| blob \| history
src/theory/theory.cpp		diff \| blob \| history
src/theory/theory.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/theory/theory_model.cpp		diff \| blob \| history
src/theory/theory_model.h		diff \| blob \| history
src/theory/theory_model_builder.cpp		diff \| blob \| history
src/theory/theory_model_builder.h		diff \| blob \| history
src/theory/theory_registrar.h		diff \| blob \| history
src/theory/theory_test_utils.h		diff \| blob \| history
src/theory/theory_traits_template.h		diff \| blob \| history
src/theory/type_enumerator.h		diff \| blob \| history
src/theory/type_enumerator_template.cpp		diff \| blob \| history
src/theory/type_set.cpp		diff \| blob \| history
src/theory/type_set.h		diff \| blob \| history
src/theory/uf/equality_engine.cpp		diff \| blob \| history
src/theory/uf/equality_engine.h		diff \| blob \| history
src/theory/uf/equality_engine_types.h		diff \| blob \| history
src/theory/uf/symmetry_breaker.cpp		diff \| blob \| history
src/theory/uf/symmetry_breaker.h		diff \| blob \| history
src/theory/uf/theory_uf.cpp		diff \| blob \| history
src/theory/uf/theory_uf.h		diff \| blob \| history
src/theory/uf/theory_uf_model.cpp		diff \| blob \| history
src/theory/uf/theory_uf_model.h		diff \| blob \| history
src/theory/uf/theory_uf_rewriter.h		diff \| blob \| history
src/theory/uf/theory_uf_strong_solver.cpp		diff \| blob \| history
src/theory/uf/theory_uf_strong_solver.h		diff \| blob \| history
src/theory/uf/theory_uf_type_rules.h		diff \| blob \| history
src/theory/valuation.cpp		diff \| blob \| history
src/theory/valuation.h		diff \| blob \| history
src/util/abstract_value.cpp		diff \| blob \| history
src/util/abstract_value.h		diff \| blob \| history
src/util/bin_heap.h		diff \| blob \| history
src/util/bitvector.cpp		diff \| blob \| history
src/util/bitvector.h		diff \| blob \| history
src/util/bool.h		diff \| blob \| history
src/util/cardinality.cpp		diff \| blob \| history
src/util/cardinality.h		diff \| blob \| history
src/util/debug.h		diff \| blob \| history
src/util/dense_map.h		diff \| blob \| history
src/util/divisible.cpp		diff \| blob \| history
src/util/divisible.h		diff \| blob \| history
src/util/floatingpoint.cpp		diff \| blob \| history
src/util/floatingpoint.h.in		diff \| blob \| history
src/util/gmp_util.h		diff \| blob \| history
src/util/hash.h		diff \| blob \| history
src/util/index.cpp		diff \| blob \| history
src/util/index.h		diff \| blob \| history
src/util/integer.h.in		diff \| blob \| history
src/util/integer_cln_imp.cpp		diff \| blob \| history
src/util/integer_cln_imp.h		diff \| blob \| history
src/util/integer_gmp_imp.cpp		diff \| blob \| history
src/util/integer_gmp_imp.h		diff \| blob \| history
src/util/maybe.h		diff \| blob \| history
src/util/ostream_util.cpp		diff \| blob \| history
src/util/ostream_util.h		diff \| blob \| history
src/util/proof.h		diff \| blob \| history
src/util/random.cpp		diff \| blob \| history
src/util/random.h		diff \| blob \| history
src/util/rational.h.in		diff \| blob \| history
src/util/rational_cln_imp.cpp		diff \| blob \| history
src/util/rational_cln_imp.h		diff \| blob \| history
src/util/rational_gmp_imp.cpp		diff \| blob \| history
src/util/rational_gmp_imp.h		diff \| blob \| history
src/util/regexp.cpp		diff \| blob \| history
src/util/regexp.h		diff \| blob \| history
src/util/resource_manager.cpp		diff \| blob \| history
src/util/resource_manager.h		diff \| blob \| history
src/util/result.cpp		diff \| blob \| history
src/util/result.h		diff \| blob \| history
src/util/safe_print.cpp		diff \| blob \| history
src/util/safe_print.h		diff \| blob \| history
src/util/sampler.cpp		diff \| blob \| history
src/util/sampler.h		diff \| blob \| history
src/util/sexpr.cpp		diff \| blob \| history
src/util/sexpr.h		diff \| blob \| history
src/util/smt2_quote_string.cpp		diff \| blob \| history
src/util/smt2_quote_string.h		diff \| blob \| history
src/util/statistics.cpp		diff \| blob \| history
src/util/statistics.h		diff \| blob \| history
src/util/statistics_registry.cpp		diff \| blob \| history
src/util/statistics_registry.h		diff \| blob \| history
src/util/tuple.h		diff \| blob \| history
src/util/unsafe_interrupt_exception.h		diff \| blob \| history
src/util/utility.h		diff \| blob \| history
test/java/BitVectors.java		diff \| blob \| history
test/java/BitVectorsAndArrays.java		diff \| blob \| history
test/java/Combination.java		diff \| blob \| history
test/java/HelloWorld.java		diff \| blob \| history
test/java/LinearArith.java		diff \| blob \| history
test/system/CVC4JavaTest.java		diff \| blob \| history
test/system/boilerplate.cpp		diff \| blob \| history
test/system/ouroborous.cpp		diff \| blob \| history
test/system/reset_assertions.cpp		diff \| blob \| history
test/system/sep_log_api.cpp		diff \| blob \| history
test/system/smt2_compliance.cpp		diff \| blob \| history
test/system/statistics.cpp		diff \| blob \| history
test/system/two_smt_engines.cpp		diff \| blob \| history
test/unit/api/datatype_api_black.h		diff \| blob \| history
test/unit/api/opterm_black.h		diff \| blob \| history
test/unit/api/solver_black.h		diff \| blob \| history
test/unit/api/sort_black.h		diff \| blob \| history
test/unit/api/term_black.h		diff \| blob \| history
test/unit/base/map_util_black.h		diff \| blob \| history
test/unit/context/cdlist_black.h		diff \| blob \| history
test/unit/context/cdmap_black.h		diff \| blob \| history
test/unit/context/cdmap_white.h		diff \| blob \| history
test/unit/context/cdo_black.h		diff \| blob \| history
test/unit/context/context_black.h		diff \| blob \| history
test/unit/context/context_mm_black.h		diff \| blob \| history
test/unit/context/context_white.h		diff \| blob \| history
test/unit/expr/attribute_black.h		diff \| blob \| history
test/unit/expr/attribute_white.h		diff \| blob \| history
test/unit/expr/expr_manager_public.h		diff \| blob \| history
test/unit/expr/expr_public.h		diff \| blob \| history
test/unit/expr/kind_black.h		diff \| blob \| history
test/unit/expr/kind_map_black.h		diff \| blob \| history
test/unit/expr/node_black.h		diff \| blob \| history
test/unit/expr/node_builder_black.h		diff \| blob \| history
test/unit/expr/node_manager_black.h		diff \| blob \| history
test/unit/expr/node_manager_white.h		diff \| blob \| history
test/unit/expr/node_self_iterator_black.h		diff \| blob \| history
test/unit/expr/node_white.h		diff \| blob \| history
test/unit/expr/symbol_table_black.h		diff \| blob \| history
test/unit/expr/type_cardinality_public.h		diff \| blob \| history
test/unit/expr/type_node_white.h		diff \| blob \| history
test/unit/main/interactive_shell_black.h		diff \| blob \| history
test/unit/memory.h		diff \| blob \| history
test/unit/parser/parser_black.h		diff \| blob \| history
test/unit/parser/parser_builder_black.h		diff \| blob \| history
test/unit/preprocessing/pass_bv_gauss_white.h		diff \| blob \| history
test/unit/proof/drat_proof_black.h		diff \| blob \| history
test/unit/proof/lfsc_proof_printer_black.h		diff \| blob \| history
test/unit/prop/cnf_stream_white.h		diff \| blob \| history
test/unit/theory/evaluator_white.h		diff \| blob \| history
test/unit/theory/logic_info_white.h		diff \| blob \| history
test/unit/theory/theory_arith_white.h		diff \| blob \| history
test/unit/theory/theory_black.h		diff \| blob \| history
test/unit/theory/theory_bv_white.h		diff \| blob \| history
test/unit/theory/theory_engine_white.h		diff \| blob \| history
test/unit/theory/theory_quantifiers_bv_instantiator_white.h		diff \| blob \| history
test/unit/theory/theory_quantifiers_bv_inverter_white.h		diff \| blob \| history
test/unit/theory/theory_strings_rewriter_white.h		diff \| blob \| history
test/unit/theory/theory_strings_skolem_cache_black.h		diff \| blob \| history
test/unit/theory/theory_white.h		diff \| blob \| history
test/unit/theory/type_enumerator_white.h		diff \| blob \| history
test/unit/util/array_store_all_black.h		diff \| blob \| history
test/unit/util/assert_white.h		diff \| blob \| history
test/unit/util/binary_heap_black.h		diff \| blob \| history
test/unit/util/bitvector_black.h		diff \| blob \| history
test/unit/util/boolean_simplification_black.h		diff \| blob \| history
test/unit/util/cardinality_public.h		diff \| blob \| history
test/unit/util/check_white.h		diff \| blob \| history
test/unit/util/configuration_black.h		diff \| blob \| history
test/unit/util/datatype_black.h		diff \| blob \| history
test/unit/util/exception_black.h		diff \| blob \| history
test/unit/util/integer_black.h		diff \| blob \| history
test/unit/util/integer_white.h		diff \| blob \| history
test/unit/util/listener_black.h		diff \| blob \| history
test/unit/util/output_black.h		diff \| blob \| history
test/unit/util/rational_black.h		diff \| blob \| history
test/unit/util/rational_white.h		diff \| blob \| history
test/unit/util/stats_black.h		diff \| blob \| history

RSS Atom