summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2017-09-28Update symbol table to support operator overloading (#1154)Andrew Reynolds
2017-09-28Fix output of --show-config for readline. (#1159)Mathias Preiner
2017-09-28Cegqi refactor prep bv (#1155)Andrew Reynolds
2017-09-28Improve finite model finding for recursive predicates (#1150)Andrew Reynolds
2017-09-27Minor fixes for partial quantifier elimination. (#1147)Andrew Reynolds
2017-09-27CEGQI for BV: Add inverse for BITVECTOR_MULT. (#1153)Aina Niemetz
2017-09-27Fix seeking for buffered input (#1145)Andres Noetzli
2017-09-26Fix type checking of to_real (#1127)Martin Brain
2017-09-26Improve FP rewriter: const folding, other (#1126)Martin Brain
2017-09-26Fixing CIDs 1172014 and 1172013: Initializing members of GetProofCommand and ...Tim King
2017-09-26Fixing Cid 1172009 (#1141)Tim King
2017-09-26Fixing CID 1172020: Initializing CDHashMap::iterator::d_it to nullptr. (#1139)Tim King
2017-09-26Fixing CID 1362903: Initializing d_bvp to nullptr. (#1136)Tim King
2017-09-26CID 1362904: Initializing GetInstantiationsCommand::d_smtEngine to nullptr. (...Tim King
2017-09-26Fix build for old GMP version (#1114)Andres Noetzli
2017-09-25Fixing CIDs 1172012 and 1172011: Initiallzing d_exprManager to nullptr in con...Tim King
2017-09-25Cegqi refactor substitutions (#1129)Andrew Reynolds
2017-09-25Initializing BVMinisat Solver::notify to nullptr. (#1132)Tim King
2017-09-25Fix bug related to sort inference + subtypes. (#1125)Andrew Reynolds
2017-09-25Fixing CID 1362917: There was a branch where d_issup was not initialized. Swi...Tim King
2017-09-25Fixing CID 1362895: Initializing d_bvp to nullptr. (#1137)Tim King
2017-09-24CID 1362907: Initializing d_smtEngine to nullptr. (#1134)Tim King
2017-09-21Sygus inv templ refactor (#1110)Andrew Reynolds
2017-09-20Extend quantifier-free UF solver to higher-order. This includes an ex… (#1100)Andrew Reynolds
2017-09-20Fix issue #1081, memory leak in cmd executor (#1109)Andres Noetzli
2017-09-19Add FP type enumerator and cardinality computer (#1104)Martin
2017-09-19Fixing a null pointer dereference in the cvc3 compatibility layer. (#1089)Tim King
2017-09-19Removing a potentially invalid comparison in the TPTP parser. (#1091)Tim King
2017-09-19Fix issue #1074, improve non-fatal error handling (#1075)Andres Noetzli
2017-09-19Refactor cegqi instantiation infrastructure so that it is more independent of...Andrew Reynolds
2017-09-18Fix issue #1105 involving string to int (#1112)Andrew Reynolds
2017-09-18Floating point symfpu support (#1103)Martin
2017-09-17Moving the CVC4_PUBLIC attribute to the beginning of operator++. (#1107)Tim King
2017-09-14Make floating-point comparison operators chainable (#1101)Martin
2017-09-14Add missing CVC4_PUBLIC in kind_template (#1078)makaimann
2017-09-14Remove unhandled subtypes (#1098)Andrew Reynolds
2017-09-14Simplifying the throw specifier of SmtEngine::checkSat and related calls to C...Tim King
2017-09-13Floating point symfpu support (#1093)Martin
2017-09-13Add new kinds required for higher-order. (#1083)Andrew Reynolds
2017-09-13Add isConst check for lambda expressions. (#1084)Andrew Reynolds
2017-09-13Modify equality engine to allow operators to be marked as external terms (#1082)Andrew Reynolds
2017-09-13Remove unused RecordSelect and TupleSelect (#1087)Andres Noetzli
2017-09-12Initial infrastructure for BV instantiation via word-level inversions. (#1056)Andrew Reynolds
2017-09-11Adding reasonable breaks in switch statement in TheoryStrings::normalizeRegex...Tim King
2017-09-11Addressing a coverity scan complaint in theory_strings.cpp. I believe the roo...Tim King
2017-09-10Ensure that expand definitions is called on all non-variable expressi… (#1070)Andrew Reynolds
2017-09-07Properly handle user cardinality constraints for uf-ss=none. (#1068)Andrew Reynolds
2017-09-05Remove support for conversions between uint32/uint16 and string. (#1069)Andrew Reynolds
2017-08-31Replace CVC4_THREADLOCAL in interactive_shell (#1065)Andres Noetzli
2017-08-31Answer unknown when uf-ss=no-minimal is combined with cardinality constraints...Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback