Enable CEGQI for non-linear (#1674)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 20 Mar 2018 04:16:45 +0000 (23:16 -0500)
committerGitHub <noreply@github.com>
Tue, 20 Mar 2018 04:16:45 +0000 (23:16 -0500)
commitdb83224b35a218a0bb449850530f0d2bea484eae
tree648d33a0c6c4df66e6b0c60e9192fcc6995b4916
parent3b6ef254e92ab0918db05a0c6084baa8892a2183
Enable CEGQI for non-linear (#1674)
src/theory/quantifiers/cegqi/ceg_instantiator.cpp
src/theory/quantifiers/cegqi/ceg_instantiator.h
src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
src/theory/quantifiers/ematching/trigger.cpp
src/theory/quantifiers/ematching/trigger.h
test/regress/regress0/quantifiers/Makefile.am
test/regress/regress0/quantifiers/cegqi-nl-simp.cvc [new file with mode: 0644]
test/regress/regress0/quantifiers/cegqi-nl-sq.smt2 [new file with mode: 0644]