Refactor preprocessing of models in fmf. Fix options --fmf-empty-sorts and --fmf...
authorajreynol <andrew.j.reynolds@gmail.com>
Fri, 2 Dec 2016 14:51:29 +0000 (08:51 -0600)
committerajreynol <andrew.j.reynolds@gmail.com>
Fri, 2 Dec 2016 14:51:29 +0000 (08:51 -0600)
commit623e701247ed08e3f59d57b18ebe42f4d4db221e
tree663fa6451f9055a7256bd5c5ba4b558aeb58f46e
parent9d6a0bda98ac2c3e3c59f55f349e029d623b264a
Refactor preprocessing of models in fmf. Fix options --fmf-empty-sorts and --fmf-fun-rlv, fixes bug 723.
src/theory/quantifiers/full_model_check.cpp
src/theory/quantifiers/model_builder.cpp
src/theory/quantifiers/model_builder.h
src/theory/quantifiers/model_engine.cpp
src/theory/quantifiers/model_engine.h
src/theory/quantifiers_engine.cpp
src/theory/rep_set.cpp
src/theory/rep_set.h
src/theory/theory_model.cpp
test/regress/regress0/fmf/Makefile.am
test/regress/regress0/fmf/bug723-irrelevant-funs.smt2 [new file with mode: 0644]