projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 18da214) | patch
Add support for quantifier-specific instantiation levels. Add option for setting...
authorajreynol <andrew.j.reynolds@gmail.com>
Mon, 18 Aug 2014 10:47:07 +0000 (12:47 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Mon, 18 Aug 2014 10:47:07 +0000 (12:47 +0200)
commitfe7a5119d5b48a2546ece43574bc4d07e86c14a7
treee64192933867061c3b215ee02e0d3aafad6b419etree
parent18da2141dcddf221f0a40782b02a24766f0ed2c7commit | diff
Add support for quantifier-specific instantiation levels.  Add option for setting inst-level 0 only for input terms.
16 files changed:
src/expr/command.cpp diff | blob | history
src/expr/command.h diff | blob | history
src/parser/smt2/Smt2.g diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/smt/smt_engine.h diff | blob | history
src/theory/quantifiers/options diff | blob | history
src/theory/quantifiers/quantifiers_attributes.cpp diff | blob | history
src/theory/quantifiers/quantifiers_attributes.h diff | blob | history
src/theory/quantifiers/term_database.h diff | blob | history
src/theory/quantifiers/theory_quantifiers.cpp diff | blob | history
src/theory/quantifiers/theory_quantifiers.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history
src/theory/theory.h diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
src/theory/theory_engine.h diff | blob | history