projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4a00ff2) | patch
Implement equality inference module for arithmetic terms. Optimization for entailmen...
authorajreynol <andrew.j.reynolds@gmail.com>
Mon, 28 Mar 2016 17:32:58 +0000 (12:32 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Mon, 28 Mar 2016 17:33:07 +0000 (12:33 -0500)
commit358e453bda62923fd0be94af5317b24a7281014b
treef2fdb4efc7a97341c2b77dca0fce96b28e7f591btree
parent4a00ff296240ff81ee909937ade8cc8aa88561dfcommit | diff
Implement equality inference module for arithmetic terms.  Optimization for entailment checks.  Other minor infrastructure.
src/Makefile.am diff | blob | history
src/theory/quantifiers/equality_infer.cpp [new file with mode: 0644] blob
src/theory/quantifiers/equality_infer.h [new file with mode: 0644] blob
src/theory/quantifiers/quant_util.cpp diff | blob | history
src/theory/quantifiers/quant_util.h 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
src/theory/theory_engine.cpp diff | blob | history