Make sort inference a preprocessing pass (#2309)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 15 Aug 2018 18:02:46 +0000 (13:02 -0500)
committerGitHub <noreply@github.com>
Wed, 15 Aug 2018 18:02:46 +0000 (13:02 -0500)
commit4748af3ee298ce5aae36a8ab8cad4426d1398c17
tree94ce5eb140a1f5898b9145a9ecc1ebe92b0ced0e
parente09be1045fc6cc8c5373f9eb96137add66b8d5d5
Make sort inference a preprocessing pass (#2309)
src/Makefile.am
src/preprocessing/passes/sort_infer.cpp [new file with mode: 0644]
src/preprocessing/passes/sort_infer.h [new file with mode: 0644]
src/smt/smt_engine.cpp
src/theory/sort_inference.cpp
src/theory/sort_inference.h
test/regress/Makefile.tests
test/regress/regress0/fmf/sort-inf-int.smt2 [new file with mode: 0644]
test/regress/regress1/fmf/ALG008-1.smt2