Ensure that expand definitions is called on all non-variable expressi… (#1070)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sun, 10 Sep 2017 06:12:34 +0000 (08:12 +0200)
committerGitHub <noreply@github.com>
Sun, 10 Sep 2017 06:12:34 +0000 (08:12 +0200)
commitd5b0866bd2a2551143caf591d453993ab5a48840
tree71d9bf61a8134be3ca13596ab0d8f278a2021eb9
parent8a68cca2f9cf76b42187c39d09a4a40bd19622c1
Ensure that expand definitions is called on all non-variable expressi… (#1070)

* Ensure that expand definitions is called on all non-variable expressions. In particular, it is necessary that the sets theory is notified when a set universe term occurs in the input to ensure options are set correctly. The commit moves this check from within check() to expandDefinitions(), and also adds the check for join image which relies on universe set. This fixes a bug reported by Arjun. Add and update regressions.

* Add comments concerning expandDefinitions

* Expand comment, move to .h
16 files changed:
src/smt/smt_engine.cpp
src/theory/sets/theory_sets.cpp
src/theory/sets/theory_sets.h
src/theory/sets/theory_sets_private.cpp
src/theory/sets/theory_sets_private.h
src/theory/theory.h
test/regress/regress0/fmf/quant_real_univ.cvc
test/regress/regress0/rels/joinImg_0.cvc
test/regress/regress0/rels/joinImg_0_1.cvc
test/regress/regress0/rels/joinImg_1.cvc
test/regress/regress0/rels/joinImg_1_1.cvc
test/regress/regress0/rels/joinImg_2.cvc
test/regress/regress0/rels/joinImg_2_1.cvc
test/regress/regress0/sets/Makefile.am
test/regress/regress0/sets/arjun-set-univ.cvc [new file with mode: 0644]
test/regress/regress0/sets/univ-set-uf-elim.smt2 [new file with mode: 0644]