projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 35c67d1) | patch
Move linear arithmetic solver to theory::arith::linear (#8628)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 19 Apr 2022 18:05:12 +0000 (13:05 -0500)
committerGitHub <noreply@github.com>
Tue, 19 Apr 2022 18:05:12 +0000 (18:05 +0000)
commitf37078447757601cf24eb3ee92970f275a434d82
treea669c596ac299805842de8bc44d4049aa7e885fatree
parent35c67d1d8aed4633c1c814f4196d2e328f015476commit | diff
Move linear arithmetic solver to theory::arith::linear (#8628)

This moves the current linear arithmetic solver to src/theory/arith/linear, and inside `cvc5::internal::theory::arith::linear`.

Some code uses internal utilities from `arith::linear`, although this should be minimized.

This is preparation for breaking dependencies with the old code.
112 files changed:
src/CMakeLists.txt diff | blob | history
src/preprocessing/passes/pseudo_boolean_processor.cpp diff | blob | history
src/theory/arith/approx_simplex.cpp [deleted file] blob | history
src/theory/arith/approx_simplex.h [deleted file] 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_rewriter.h diff | blob | history
src/theory/arith/arith_state.cpp diff | blob | history
src/theory/arith/arith_state.h diff | blob | history
src/theory/arith/arith_static_learner.cpp [deleted file] blob | history
src/theory/arith/arith_static_learner.h [deleted file] blob | history
src/theory/arith/arith_utilities.h diff | blob | history
src/theory/arith/arithvar.cpp [deleted file] blob | history
src/theory/arith/arithvar.h [deleted file] blob | history
src/theory/arith/arithvar_node_map.h [deleted file] blob | history
src/theory/arith/attempt_solution_simplex.cpp [deleted file] blob | history
src/theory/arith/attempt_solution_simplex.h [deleted file] blob | history
src/theory/arith/bound_counts.h [deleted file] blob | history
src/theory/arith/bound_inference.cpp diff | blob | history
src/theory/arith/callbacks.cpp [deleted file] blob | history
src/theory/arith/callbacks.h [deleted file] blob | history
src/theory/arith/congruence_manager.cpp [deleted file] blob | history
src/theory/arith/congruence_manager.h [deleted file] blob | history
src/theory/arith/constraint.cpp [deleted file] blob | history
src/theory/arith/constraint.h [deleted file] blob | history
src/theory/arith/constraint_forward.h [deleted file] blob | history
src/theory/arith/cut_log.cpp [deleted file] blob | history
src/theory/arith/cut_log.h [deleted file] blob | history
src/theory/arith/dio_solver.cpp [deleted file] blob | history
src/theory/arith/dio_solver.h [deleted file] blob | history
src/theory/arith/dual_simplex.cpp [deleted file] blob | history
src/theory/arith/dual_simplex.h [deleted file] blob | history
src/theory/arith/error_set.cpp [deleted file] blob | history
src/theory/arith/error_set.h [deleted file] blob | history
src/theory/arith/fc_simplex.cpp [deleted file] blob | history
src/theory/arith/fc_simplex.h [deleted file] blob | history
src/theory/arith/infer_bounds.cpp [deleted file] blob | history
src/theory/arith/infer_bounds.h [deleted file] blob | history
src/theory/arith/linear/approx_simplex.cpp [new file with mode: 0644] blob
src/theory/arith/linear/approx_simplex.h [new file with mode: 0644] blob
src/theory/arith/linear/arith_static_learner.cpp [new file with mode: 0644] blob
src/theory/arith/linear/arith_static_learner.h [new file with mode: 0644] blob
src/theory/arith/linear/arithvar.cpp [new file with mode: 0644] blob
src/theory/arith/linear/arithvar.h [new file with mode: 0644] blob
src/theory/arith/linear/arithvar_node_map.h [new file with mode: 0644] blob
src/theory/arith/linear/attempt_solution_simplex.cpp [new file with mode: 0644] blob
src/theory/arith/linear/attempt_solution_simplex.h [new file with mode: 0644] blob
src/theory/arith/linear/bound_counts.h [new file with mode: 0644] blob
src/theory/arith/linear/callbacks.cpp [new file with mode: 0644] blob
src/theory/arith/linear/callbacks.h [new file with mode: 0644] blob
src/theory/arith/linear/congruence_manager.cpp [new file with mode: 0644] blob
src/theory/arith/linear/congruence_manager.h [new file with mode: 0644] blob
src/theory/arith/linear/constraint.cpp [new file with mode: 0644] blob
src/theory/arith/linear/constraint.h [new file with mode: 0644] blob
src/theory/arith/linear/constraint_forward.h [new file with mode: 0644] blob
src/theory/arith/linear/cut_log.cpp [new file with mode: 0644] blob
src/theory/arith/linear/cut_log.h [new file with mode: 0644] blob
src/theory/arith/linear/dio_solver.cpp [new file with mode: 0644] blob
src/theory/arith/linear/dio_solver.h [new file with mode: 0644] blob
src/theory/arith/linear/dual_simplex.cpp [new file with mode: 0644] blob
src/theory/arith/linear/dual_simplex.h [new file with mode: 0644] blob
src/theory/arith/linear/error_set.cpp [new file with mode: 0644] blob
src/theory/arith/linear/error_set.h [new file with mode: 0644] blob
src/theory/arith/linear/fc_simplex.cpp [new file with mode: 0644] blob
src/theory/arith/linear/fc_simplex.h [new file with mode: 0644] blob
src/theory/arith/linear/infer_bounds.cpp [new file with mode: 0644] blob
src/theory/arith/linear/infer_bounds.h [new file with mode: 0644] blob
src/theory/arith/linear/linear_equality.cpp [new file with mode: 0644] blob
src/theory/arith/linear/linear_equality.h [new file with mode: 0644] blob
src/theory/arith/linear/matrix.cpp [new file with mode: 0644] blob
src/theory/arith/linear/matrix.h [new file with mode: 0644] blob
src/theory/arith/linear/normal_form.cpp [new file with mode: 0644] blob
src/theory/arith/linear/normal_form.h [new file with mode: 0644] blob
src/theory/arith/linear/partial_model.cpp [new file with mode: 0644] blob
src/theory/arith/linear/partial_model.h [new file with mode: 0644] blob
src/theory/arith/linear/simplex.cpp [new file with mode: 0644] blob
src/theory/arith/linear/simplex.h [new file with mode: 0644] blob
src/theory/arith/linear/simplex_update.cpp [new file with mode: 0644] blob
src/theory/arith/linear/simplex_update.h [new file with mode: 0644] blob
src/theory/arith/linear/soi_simplex.cpp [new file with mode: 0644] blob
src/theory/arith/linear/soi_simplex.h [new file with mode: 0644] blob
src/theory/arith/linear/tableau.cpp [new file with mode: 0644] blob
src/theory/arith/linear/tableau.h [new file with mode: 0644] blob
src/theory/arith/linear/tableau_sizes.cpp [new file with mode: 0644] blob
src/theory/arith/linear/tableau_sizes.h [new file with mode: 0644] blob
src/theory/arith/linear/theory_arith_private.cpp [new file with mode: 0644] blob
src/theory/arith/linear/theory_arith_private.h [new file with mode: 0644] blob
src/theory/arith/linear_equality.cpp [deleted file] blob | history
src/theory/arith/linear_equality.h [deleted file] blob | history
src/theory/arith/matrix.cpp [deleted file] blob | history
src/theory/arith/matrix.h [deleted file] blob | history
src/theory/arith/nl/icp/icp_solver.cpp diff | blob | history
src/theory/arith/normal_form.cpp [deleted file] blob | history
src/theory/arith/normal_form.h [deleted file] blob | history
src/theory/arith/partial_model.cpp [deleted file] blob | history
src/theory/arith/partial_model.h [deleted file] blob | history
src/theory/arith/proof_checker.cpp diff | blob | history
src/theory/arith/simplex.cpp [deleted file] blob | history
src/theory/arith/simplex.h [deleted file] blob | history
src/theory/arith/simplex_update.cpp [deleted file] blob | history
src/theory/arith/simplex_update.h [deleted file] blob | history
src/theory/arith/soi_simplex.cpp [deleted file] blob | history
src/theory/arith/soi_simplex.h [deleted file] blob | history
src/theory/arith/tableau.cpp [deleted file] blob | history
src/theory/arith/tableau.h [deleted file] blob | history
src/theory/arith/tableau_sizes.cpp [deleted file] blob | history
src/theory/arith/tableau_sizes.h [deleted file] 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 [deleted file] blob | history
src/theory/arith/theory_arith_private.h [deleted file] blob | history
src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp diff | blob | history