projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: df88bab) | patch
Accelerate sygus solution reconstruction for constants and id functions. Minor chang...
authorajreynol <andrew.j.reynolds@gmail.com>
Fri, 12 Jun 2015 12:15:14 +0000 (14:15 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Fri, 12 Jun 2015 12:15:14 +0000 (14:15 +0200)
commitad0863ae8333c4dcd950153e0db8cd4565a250b3
tree96d265ac59ce48f5bb90f0d041b1a4ffe57539a4tree
parentdf88bab0da253bb00056a25b4f7603d9ac6f3d66commit | diff
Accelerate sygus solution reconstruction for constants and id functions.  Minor changes to sygus type registration.  Print sygus let solutions assuming fixed variable names.
src/parser/smt2/smt2.cpp diff | blob | history
src/theory/quantifiers/ce_guided_single_inv_sol.cpp diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers/term_database.h diff | blob | history
src/util/datatype.cpp diff | blob | history
src/util/datatype.h diff | blob | history