projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 958b0b5) | patch
1. Fix for inst_match.cpp to allow compilation on fedora
authorClark Barrett <barrett@cs.nyu.edu>
Sun, 19 Aug 2012 02:08:15 +0000 (02:08 +0000)
committerClark Barrett <barrett@cs.nyu.edu>
Sun, 19 Aug 2012 02:08:15 +0000 (02:08 +0000)
commite8e85053afba60bd6060cb07c52c88c316d73b30
tree05b0d8c37ab667cb8f22d2159bf5079557405a9btree
parent958b0b56aad79df431376344420106115ab23778commit | diff
1. Fix for inst_match.cpp to allow compilation on fedora
2. Initial implementation of computeIsConst for arrays - still needs
   additional checks based on cardinality
3. Finally fixed pre-competition bug in array rewriter
4. Still to come: array rewrites for constants and STORE_ALL
src/theory/arrays/theory_arrays_rewriter.h diff | blob | history
src/theory/arrays/theory_arrays_type_rules.h diff | blob | history
src/theory/quantifiers/inst_match.cpp diff | blob | history