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

author	Mathias Preiner <mathias.preiner@gmail.com>
	Wed, 30 Mar 2022 22:16:46 +0000 (15:16 -0700)
committer	GitHub <noreply@github.com>
	Wed, 30 Mar 2022 22:16:46 +0000 (22:16 +0000)
commit	014ff8cdd6294f4b1375888c11dc8a1f3a5de0d4
tree	978efcfab6d9e1ea86a04cd51be16cfc69e560e4	tree
parent	c56a361253836f38e275651165a957664c7e126a	commit \| diff

Move cvc5::internal::context to cvc5::context. (#8451)

137 files changed:

src/base/check.h		diff \| blob \| history
src/base/exception.h		diff \| blob \| history
src/base/map_util.h		diff \| blob \| history
src/base/output.h		diff \| blob \| history
src/base/versioninfo.cpp.in		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/expr/kind_template.cpp		diff \| blob \| history
src/expr/kind_template.h		diff \| blob \| history
src/expr/metakind_template.cpp		diff \| blob \| history
src/expr/metakind_template.h		diff \| blob \| history
src/expr/node_value.h		diff \| blob \| history
src/expr/symbol_manager.cpp		diff \| blob \| history
src/expr/symbol_table.cpp		diff \| blob \| history
src/preprocessing/learned_literal_manager.h		diff \| blob \| history
src/preprocessing/passes/unconstrained_simplifier.h		diff \| blob \| history
src/prop/minisat/core/Solver.cc		diff \| blob \| history
src/prop/minisat/core/Solver.h		diff \| blob \| history
src/prop/minisat/minisat.h		diff \| blob \| history
src/prop/minisat/simp/SimpSolver.cc		diff \| blob \| history
src/prop/minisat/simp/SimpSolver.h		diff \| blob \| history
src/prop/sat_solver.h		diff \| blob \| history
src/smt/env.h		diff \| blob \| history
src/smt/env_obj.h		diff \| blob \| history
src/smt/solver_engine.cpp		diff \| blob \| history
src/smt/solver_engine.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/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/dio_solver.h		diff \| blob \| history
src/theory/arith/nl/coverings/proof_generator.cpp		diff \| blob \| history
src/theory/arith/nl/nl_model.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/theory_arith_private.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/theory_arrays.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.h		diff \| blob \| history
src/theory/arrays/union_find.h		diff \| blob \| history
src/theory/atom_requests.cpp		diff \| blob \| history
src/theory/bags/bag_solver.cpp		diff \| blob \| history
src/theory/bags/card_solver.cpp		diff \| blob \| history
src/theory/bv/bv_solver_bitblast.cpp		diff \| blob \| history
src/theory/bv/int_blaster.h		diff \| blob \| history
src/theory/datatypes/sygus_extension.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes.h		diff \| blob \| history
src/theory/engine_output_channel.h		diff \| blob \| history
src/theory/fp/fp_word_blaster.cpp		diff \| blob \| history
src/theory/fp/theory_fp.cpp		diff \| blob \| history
src/theory/fp/theory_fp_rewriter.cpp		diff \| blob \| history
src/theory/quantifiers/candidate_rewrite_database.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_arith_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/conjecture_generator.h		diff \| blob \| history
src/theory/quantifiers/ematching/instantiation_engine.cpp		diff \| blob \| history
src/theory/quantifiers/entailment_check.cpp		diff \| blob \| history
src/theory/quantifiers/equality_query.cpp		diff \| blob \| history
src/theory/quantifiers/equality_query.h		diff \| blob \| history
src/theory/quantifiers/first_order_model.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/model_builder.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/model_engine.cpp		diff \| blob \| history
src/theory/quantifiers/inst_match_trie.cpp		diff \| blob \| history
src/theory/quantifiers/inst_strategy_enumerative.cpp		diff \| blob \| history
src/theory/quantifiers/inst_strategy_pool.cpp		diff \| blob \| history
src/theory/quantifiers/instantiate.cpp		diff \| blob \| history
src/theory/quantifiers/quant_relevance.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_attributes.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_modules.h		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_eval_unfold.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.cpp		diff \| blob \| history
src/theory/quantifiers/theory_quantifiers.cpp		diff \| blob \| history
src/theory/quantifiers_engine.h		diff \| blob \| history
src/theory/sep/theory_sep.cpp		diff \| blob \| history
src/theory/sep/theory_sep.h		diff \| blob \| history
src/theory/sets/theory_sets_private.h		diff \| blob \| history
src/theory/shared_terms_database.h		diff \| blob \| history
src/theory/strings/array_core_solver.cpp		diff \| blob \| history
src/theory/strings/array_solver.cpp		diff \| blob \| history
src/theory/strings/base_solver.cpp		diff \| blob \| history
src/theory/strings/core_solver.cpp		diff \| blob \| history
src/theory/strings/eqc_info.cpp		diff \| blob \| history
src/theory/strings/extf_solver.cpp		diff \| blob \| history
src/theory/strings/inference_manager.cpp		diff \| blob \| history
src/theory/strings/regexp_solver.cpp		diff \| blob \| history
src/theory/strings/sequences_rewriter.cpp		diff \| blob \| history
src/theory/strings/solver_state.cpp		diff \| blob \| history
src/theory/strings/strings_fmf.cpp		diff \| blob \| history
src/theory/strings/term_registry.cpp		diff \| blob \| history
src/theory/strings/theory_strings.cpp		diff \| blob \| history
src/theory/theory.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_model.cpp		diff \| blob \| history
src/theory/theory_model_builder.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.h		diff \| blob \| history
src/theory/uf/symmetry_breaker.cpp		diff \| blob \| history
src/theory/uf/symmetry_breaker.h		diff \| blob \| history
src/util/floatingpoint.h		diff \| blob \| history
src/util/floatingpoint_literal_symfpu.cpp		diff \| blob \| history
src/util/floatingpoint_literal_symfpu_traits.h		diff \| blob \| history
src/util/string.cpp		diff \| blob \| history
src/util/string.h		diff \| blob \| history
test/unit/base/map_util_black.cpp		diff \| blob \| history
test/unit/context/cdhashmap_black.cpp		diff \| blob \| history
test/unit/context/cdhashmap_white.cpp		diff \| blob \| history
test/unit/context/cdlist_black.cpp		diff \| blob \| history
test/unit/context/cdo_black.cpp		diff \| blob \| history
test/unit/context/context_black.cpp		diff \| blob \| history
test/unit/context/context_mm_black.cpp		diff \| blob \| history
test/unit/context/context_white.cpp		diff \| blob \| history
test/unit/prop/cnf_stream_white.cpp		diff \| blob \| history
test/unit/test_context.h		diff \| blob \| history
test/unit/theory/theory_engine_white.cpp		diff \| blob \| history

RSS Atom