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

author	Mathias Preiner <mathias.preiner@gmail.com>
	Wed, 30 Oct 2019 22:27:10 +0000 (15:27 -0700)
committer	GitHub <noreply@github.com>
	Wed, 30 Oct 2019 22:27:10 +0000 (15:27 -0700)
commit	43ab3f4cd1aa5549cb1aa3c20a2d589614bcb8fc
tree	cf7b5d7f73a4d4ddc34492334a7d0eb90b57b77b	tree
parent	8dda9531995953c3cec094339002f2ee7cadae08	commit \| diff

Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)

290 files changed:

src/api/cvc4cpp.cpp		diff \| blob \| history
src/base/CMakeLists.txt		diff \| blob \| history
src/base/check.cpp	[new file with mode: 0644]	blob
src/base/check.h	[new file with mode: 0644]	blob
src/base/cvc4_assert.cpp	[deleted file]	blob \| history
src/base/cvc4_assert.h	[deleted file]	blob \| history
src/base/cvc4_check.cpp	[deleted file]	blob \| history
src/base/cvc4_check.h	[deleted file]	blob \| history
src/base/exception.cpp		diff \| blob \| history
src/base/listener.cpp		diff \| blob \| history
src/base/map_util.h		diff \| blob \| history
src/context/backtrackable.h		diff \| blob \| history
src/context/cdhashmap.h		diff \| blob \| history
src/context/cdhashset.h		diff \| blob \| history
src/context/cdinsert_hashmap.h		diff \| blob \| history
src/context/cdlist.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/decision/decision_engine.h		diff \| blob \| history
src/decision/justification_heuristic.cpp		diff \| blob \| history
src/expr/array_store_all.cpp		diff \| blob \| history
src/expr/attribute.cpp		diff \| blob \| history
src/expr/attribute_internals.h		diff \| blob \| history
src/expr/datatype.cpp		diff \| blob \| history
src/expr/expr_manager_template.cpp		diff \| blob \| history
src/expr/expr_template.cpp		diff \| blob \| history
src/expr/kind_map.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/mkkind		diff \| blob \| history
src/expr/node.h		diff \| blob \| history
src/expr/node_algorithm.cpp		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_self_iterator.h		diff \| blob \| history
src/expr/node_value.h		diff \| blob \| history
src/expr/record.cpp		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/options/argument_extender_implementation.cpp		diff \| blob \| history
src/options/options_handler.cpp		diff \| blob \| history
src/options/options_template.cpp		diff \| blob \| history
src/preprocessing/passes/ackermann.cpp		diff \| blob \| history
src/preprocessing/passes/apply_to_const.cpp		diff \| blob \| history
src/preprocessing/passes/bv_gauss.cpp		diff \| blob \| history
src/preprocessing/passes/miplib_trick.cpp		diff \| blob \| history
src/preprocessing/passes/quantifier_macros.cpp		diff \| blob \| history
src/preprocessing/preprocessing_pass_registry.cpp		diff \| blob \| history
src/printer/cvc/cvc_printer.cpp		diff \| blob \| history
src/printer/dagification_visitor.cpp		diff \| blob \| history
src/printer/printer.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/printer/tptp/tptp_printer.cpp		diff \| blob \| history
src/proof/arith_proof.cpp		diff \| blob \| history
src/proof/array_proof.cpp		diff \| blob \| history
src/proof/bitvector_proof.cpp		diff \| blob \| history
src/proof/clausal_bitvector_proof.cpp		diff \| blob \| history
src/proof/cnf_proof.cpp		diff \| blob \| history
src/proof/dimacs.cpp		diff \| blob \| history
src/proof/drat/drat_proof.cpp		diff \| blob \| history
src/proof/er/er_proof.cpp		diff \| blob \| history
src/proof/lemma_proof.cpp		diff \| blob \| history
src/proof/lrat/lrat_proof.cpp		diff \| blob \| history
src/proof/proof_manager.cpp		diff \| blob \| history
src/proof/proof_output_channel.cpp		diff \| blob \| history
src/proof/proof_utils.h		diff \| blob \| history
src/proof/resolution_bitvector_proof.cpp		diff \| blob \| history
src/proof/skolemization_manager.cpp		diff \| blob \| history
src/proof/theory_proof.cpp		diff \| blob \| history
src/proof/uf_proof.cpp		diff \| blob \| history
src/proof/unsat_core.cpp		diff \| blob \| history
src/prop/bvminisat/bvminisat.cpp		diff \| blob \| history
src/prop/bvminisat/bvminisat.h		diff \| blob \| history
src/prop/bvminisat/core/Solver.cc		diff \| blob \| history
src/prop/cadical.cpp		diff \| blob \| history
src/prop/cnf_stream.cpp		diff \| blob \| history
src/prop/cryptominisat.cpp		diff \| blob \| history
src/prop/minisat/core/Solver.cc		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/sat_solver.h		diff \| blob \| history
src/prop/sat_solver_factory.cpp		diff \| blob \| history
src/prop/theory_proxy.cpp		diff \| blob \| history
src/smt/command.cpp		diff \| blob \| history
src/smt/managed_ostreams.cpp		diff \| blob \| history
src/smt/model_core_builder.cpp		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine_scope.cpp		diff \| blob \| history
src/smt/update_ostream.h		diff \| blob \| history
src/smt_util/boolean_simplification.h		diff \| blob \| history
src/smt_util/nary_builder.cpp		diff \| blob \| history
src/theory/arith/approx_simplex.cpp		diff \| blob \| history
src/theory/arith/arith_ite_utils.cpp		diff \| blob \| history
src/theory/arith/arith_rewriter.cpp		diff \| blob \| history
src/theory/arith/arith_static_learner.cpp		diff \| blob \| history
src/theory/arith/arith_utilities.h		diff \| blob \| history
src/theory/arith/attempt_solution_simplex.cpp		diff \| blob \| history
src/theory/arith/bound_counts.h		diff \| blob \| history
src/theory/arith/callbacks.cpp		diff \| blob \| history
src/theory/arith/congruence_manager.cpp		diff \| blob \| history
src/theory/arith/constraint.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/error_set.h		diff \| blob \| history
src/theory/arith/fc_simplex.cpp		diff \| blob \| history
src/theory/arith/linear_equality.cpp		diff \| blob \| history
src/theory/arith/matrix.h		diff \| blob \| history
src/theory/arith/nonlinear_extension.cpp		diff \| blob \| history
src/theory/arith/normal_form.cpp		diff \| blob \| history
src/theory/arith/normal_form.h		diff \| blob \| history
src/theory/arith/simplex.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/tableau.cpp		diff \| blob \| history
src/theory/arith/theory_arith_private.cpp		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/static_fact_manager.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays_type_rules.h		diff \| blob \| history
src/theory/arrays/union_find.cpp		diff \| blob \| history
src/theory/booleans/circuit_propagator.cpp		diff \| blob \| history
src/theory/booleans/type_enumerator.h		diff \| blob \| history
src/theory/builtin/theory_builtin_rewriter.cpp		diff \| blob \| history
src/theory/builtin/theory_builtin_type_rules.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/bitblast_strategies_template.h		diff \| blob \| history
src/theory/bv/bitblast/bitblast_utils.h		diff \| blob \| history
src/theory/bv/bitblast/eager_bitblaster.cpp		diff \| blob \| history
src/theory/bv/bitblast/lazy_bitblaster.cpp		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_subtheory_algebraic.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_algebraic.h		diff \| blob \| history
src/theory/bv/bv_subtheory_core.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_inequality.cpp		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_rewrite_rules.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_normalization.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_simplification.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/datatypes/datatypes_sygus.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes.cpp		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/example/theory_uf_tim.cpp		diff \| blob \| history
src/theory/ext_theory.cpp		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_rewriter.cpp		diff \| blob \| history
src/theory/fp/type_enumerator.h		diff \| blob \| history
src/theory/logic_info.cpp		diff \| blob \| history
src/theory/output_channel.h		diff \| blob \| history
src/theory/quantifiers/alpha_equivalence.cpp		diff \| blob \| history
src/theory/quantifiers/anti_skolem.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp		diff \| blob \| history
src/theory/quantifiers/conjecture_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/candidate_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/instantiation_engine.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/trigger.cpp		diff \| blob \| history
src/theory/quantifiers/equality_infer.cpp		diff \| blob \| history
src/theory/quantifiers/equality_query.cpp		diff \| blob \| history
src/theory/quantifiers/first_order_model.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/bounded_integers.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/full_model_check.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/model_engine.cpp		diff \| blob \| history
src/theory/quantifiers/fun_def_process.cpp		diff \| blob \| history
src/theory/quantifiers/inst_match.cpp		diff \| blob \| history
src/theory/quantifiers/inst_propagator.cpp		diff \| blob \| history
src/theory/quantifiers/local_theory_ext.cpp		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_attributes.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.cpp		diff \| blob \| history
src/theory/quantifiers/query_generator.cpp		diff \| blob \| history
src/theory/quantifiers/relevant_domain.cpp		diff \| blob \| history
src/theory/quantifiers/rewrite_engine.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_single_inv.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_pbe.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_io.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/term_database_sygus.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/type_info.cpp		diff \| blob \| history
src/theory/quantifiers/sygus_sampler.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.cpp		diff \| blob \| history
src/theory/quantifiers/term_util.cpp		diff \| blob \| history
src/theory/quantifiers/theory_quantifiers.cpp		diff \| blob \| history
src/theory/quantifiers/theory_quantifiers_type_rules.h		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/rep_set.cpp		diff \| blob \| history
src/theory/rewriter.cpp		diff \| blob \| history
src/theory/sep/theory_sep.cpp		diff \| blob \| history
src/theory/sep/theory_sep_rewriter.cpp		diff \| blob \| history
src/theory/sets/cardinality_extension.cpp		diff \| blob \| history
src/theory/sets/rels_utils.h		diff \| blob \| history
src/theory/sets/theory_sets_private.cpp		diff \| blob \| history
src/theory/sets/theory_sets_rels.cpp		diff \| blob \| history
src/theory/sets/theory_sets_rewriter.cpp		diff \| blob \| history
src/theory/sets/theory_sets_type_rules.h		diff \| blob \| history
src/theory/sort_inference.cpp		diff \| blob \| history
src/theory/strings/regexp_operation.cpp		diff \| blob \| history
src/theory/strings/regexp_solver.cpp		diff \| blob \| history
src/theory/strings/theory_strings.cpp		diff \| blob \| history
src/theory/strings/theory_strings_rewriter.cpp		diff \| blob \| history
src/theory/strings/type_enumerator.h		diff \| blob \| history
src/theory/substitutions.cpp		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_builder.cpp		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/uf/cardinality_extension.cpp		diff \| blob \| history
src/theory/uf/cardinality_extension.h		diff \| blob \| history
src/theory/uf/equality_engine.cpp		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/theory_uf.cpp		diff \| blob \| history
src/theory/uf/theory_uf_model.cpp		diff \| blob \| history
src/theory/uf/theory_uf_rewriter.h		diff \| blob \| history
src/theory/uf/theory_uf_type_rules.h		diff \| blob \| history
src/util/abstract_value.cpp		diff \| blob \| history
src/util/bin_heap.h		diff \| blob \| history
src/util/cardinality.cpp		diff \| blob \| history
src/util/dense_map.h		diff \| blob \| history
src/util/divisible.cpp		diff \| blob \| history
src/util/floatingpoint.cpp		diff \| blob \| history
src/util/integer_cln_imp.cpp		diff \| blob \| history
src/util/integer_gmp_imp.cpp		diff \| blob \| history
src/util/random.cpp		diff \| blob \| history
src/util/rational_cln_imp.cpp		diff \| blob \| history
src/util/rational_gmp_imp.cpp		diff \| blob \| history
src/util/regexp.cpp		diff \| blob \| history
src/util/resource_manager.cpp		diff \| blob \| history
src/util/result.cpp		diff \| blob \| history
src/util/sampler.cpp		diff \| blob \| history
src/util/sexpr.cpp		diff \| blob \| history
src/util/statistics_registry.cpp		diff \| blob \| history
src/util/utility.cpp		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_white.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_white.h		diff \| blob \| history
test/unit/expr/symbol_table_black.h		diff \| blob \| history
test/unit/memory.h		diff \| blob \| history
test/unit/preprocessing/pass_bv_gauss_white.h		diff \| blob \| history
test/unit/prop/cnf_stream_white.h		diff \| blob \| history
test/unit/test_utils.h		diff \| blob \| history
test/unit/theory/theory_engine_white.h		diff \| blob \| history
test/unit/theory/theory_quantifiers_bv_inverter_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/check_white.h		diff \| blob \| history
test/unit/util/stats_black.h		diff \| blob \| history

RSS Atom