projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 65c2e16) | patch
Module to infer alpha equivalence of quantified formulas. Minor clean up of options.
authorajreynol <andrew.j.reynolds@gmail.com>
Mon, 29 Jun 2015 11:30:44 +0000 (13:30 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Mon, 29 Jun 2015 11:30:44 +0000 (13:30 +0200)
commita401cd2deb921c3499d8fdbe0d14cfee67c92737
tree5d92f83ef10fca5a05912a1a93527fbe555451aftree
parent65c2e1688d83dfeb913b689c10d9b43c5dc89cc0commit | diff
Module to infer alpha equivalence of quantified formulas.  Minor clean up of options.
15 files changed:
src/Makefile.am diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/datatypes/datatypes_sygus.cpp diff | blob | history
src/theory/quantifiers/alpha_equivalence.cpp [new file with mode: 0755] blob
src/theory/quantifiers/alpha_equivalence.h [new file with mode: 0755] blob
src/theory/quantifiers/ce_guided_single_inv_sol.cpp diff | blob | history
src/theory/quantifiers/conjecture_generator.cpp diff | blob | history
src/theory/quantifiers/conjecture_generator.h diff | blob | history
src/theory/quantifiers/first_order_reasoning.cpp [deleted file] blob | history
src/theory/quantifiers/first_order_reasoning.h [deleted file] blob | history
src/theory/quantifiers/options diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers/term_database.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history