projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 819eedc) | patch
Add bags inference generator (#5731)
authormudathirmahgoub <mudathirmahgoub@gmail.com>
Fri, 8 Jan 2021 16:07:50 +0000 (10:07 -0600)
committerGitHub <noreply@github.com>
Fri, 8 Jan 2021 16:07:50 +0000 (10:07 -0600)
commit63d27f031f8942607d869080d0e2cfb6078d40b1
tree0a29a6479a38d700a824951e343334c5d02d0183tree
parent819eedc38031d3befb9c3e855bbbfa0afa3bb3cccommit | diff
Add bags inference generator  (#5731)

This PR adds inference generator for basic bag rules.
29 files changed:
src/CMakeLists.txt diff | blob | history
src/api/cvc4cpp.cpp diff | blob | history
src/expr/type_node.cpp diff | blob | history
src/parser/smt2/smt2.cpp diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/theory/bags/bag_solver.cpp [new file with mode: 0644] blob
src/theory/bags/bag_solver.h [new file with mode: 0644] blob
src/theory/bags/bags_rewriter.cpp diff | blob | history
src/theory/bags/bags_rewriter.h diff | blob | history
src/theory/bags/infer_info.cpp [new file with mode: 0644] blob
src/theory/bags/infer_info.h [new file with mode: 0644] blob
src/theory/bags/inference_generator.cpp [new file with mode: 0644] blob
src/theory/bags/inference_generator.h [new file with mode: 0644] blob
src/theory/bags/inference_manager.cpp diff | blob | history
src/theory/bags/inference_manager.h diff | blob | history
src/theory/bags/normal_form.cpp diff | blob | history
src/theory/bags/normal_form.h diff | blob | history
src/theory/bags/solver_state.cpp diff | blob | history
src/theory/bags/solver_state.h diff | blob | history
src/theory/bags/theory_bags.cpp diff | blob | history
src/theory/bags/theory_bags.h diff | blob | history
src/theory/strings/base_solver.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/bags/disequality.smt2 [new file with mode: 0644] blob
test/regress/regress1/bags/subbag1.smt2 [new file with mode: 0644] blob
test/regress/regress1/bags/subbag2.smt2 [new file with mode: 0644] blob
test/regress/regress1/bags/union_disjoint.smt2 [new file with mode: 0644] blob
test/regress/regress1/bags/union_max1.smt2 [new file with mode: 0644] blob
test/regress/regress1/bags/union_max2.smt2 [new file with mode: 0644] blob