summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-10-05Allow CDHashMaps for objects without default constructors (#1092)Martin
2017-10-04Add mkZero, mkOne and mkUmulo to bv utils. (#1200)Aina Niemetz
2017-10-04Ho quant util (#1119)Andrew Reynolds
2017-10-04Removing the throw specifier from ArrayStoreAll constructor. (#1182)Tim King
2017-10-03Add regression from #50 regarding "as" parsing in smt2 (#1188)Andrew Reynolds
2017-10-03Add Cryptominisat and LFSC to --show-config output. (#1194)Mathias Preiner
2017-10-03Move sygus grammar utilities to separate file. (#1184)Andrew Reynolds
2017-10-03Op overload parser (#1162)Andrew Reynolds
2017-10-03Add initial version of the SMTCOMP2018 run scripts (#1185)Andres Noetzli
2017-10-02Unify hash functions for pairs (#1161)Andres Noetzli
2017-10-02Add 5 FP kinds for partial to total fn conversion (#1128)Martin
2017-10-02Address comments from PR #1164. (#1174)Mathias Preiner
2017-10-02Removing throw specifiers from SymbolTable::Implementation. (#1183)Tim King
2017-10-01Removing throw specifiers from TypeEnumeratorBase's operator* and isFinished....Tim King
2017-10-01CID 1457268: Initializing CegConjecture::d_syntax_guided to false. (#1181)Tim King
2017-10-01Refactor check function in last call effort of non-linear extension. (#1175)Andrew Reynolds
2017-09-30SyGuS streaming solution mode (#1131)Andrew Reynolds
2017-09-29Move BvInverter class into separate file. (#1173)Mathias Preiner
2017-09-29A few updates to license files.Clark Barrett
2017-09-29Add license information for GMPAndres Noetzli
2017-09-29Simplify representation of inversion Skolems for bv cegqi (#1164)Andrew Reynolds
2017-09-29Initial working version of BV word-level instantiation (#1158)Andrew Reynolds
2017-09-29Better hash function for pairs (#1157)Andres Noetzli
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-27Add quantifiers API example, fixes #879 (#1146)Andrew Reynolds
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback