projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ee0701f) | patch
Simple variable elimination for single inv properties. Relax conditions for partial...
authorajreynol <andrew.j.reynolds@gmail.com>
Tue, 3 Feb 2015 10:39:03 +0000 (11:39 +0100)
committerajreynol <andrew.j.reynolds@gmail.com>
Tue, 3 Feb 2015 10:39:03 +0000 (11:39 +0100)
commit3df24b6e0480799e8f400d15778ed5d3fb2ba7ae
tree8f1b68d934257de16e5e5ddf3db5c129869758d2tree
parentee0701f8c94b659594b033fa218b588a0d23acd7commit | diff
Simple variable elimination for single inv properties.  Relax conditions for partial inst variables for LTE.
src/theory/quantifiers/ce_guided_instantiation.cpp diff | blob | history
src/theory/quantifiers/ce_guided_single_inv.cpp diff | blob | history
src/theory/quantifiers/ce_guided_single_inv.h diff | blob | history
src/theory/quantifiers/local_theory_ext.cpp diff | blob | history