Fix bug in --term-db-mode=relevant with variable triggers. Support inst-closure...
authorajreynol <andrew.j.reynolds@gmail.com>
Tue, 25 Nov 2014 15:15:10 +0000 (16:15 +0100)
committerajreynol <andrew.j.reynolds@gmail.com>
Tue, 25 Nov 2014 15:15:10 +0000 (16:15 +0100)
commit29bdfca306a7cd35801c7d9cb3023d78a8b82a1f
tree1c50ca8eb48010b3f327d3d9ada06161e27d9834
parent38e077ab219082ee044c2e17ed809e3519c80842
Fix bug in --term-db-mode=relevant with variable triggers.  Support inst-closure predicate and mode --term-db-inst-closure.  Minor changes to theory_quantifiers.
12 files changed:
src/parser/smt2/Smt2.g
src/theory/quantifiers/candidate_generator.cpp
src/theory/quantifiers/ce_guided_instantiation.cpp
src/theory/quantifiers/kinds
src/theory/quantifiers/options
src/theory/quantifiers/term_database.cpp
src/theory/quantifiers/term_database.h
src/theory/quantifiers/theory_quantifiers.cpp
src/theory/quantifiers/theory_quantifiers.h
src/theory/quantifiers/theory_quantifiers_type_rules.h
src/theory/quantifiers_engine.cpp
src/theory/quantifiers_engine.h