summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2017-10-13CBQI BV: Added EXTRACT handling. (#1240)Aina Niemetz
2017-10-12CBQI BV quick heuristics (#1239)Andrew Reynolds
2017-10-12Initial support for solving bit-vector inequalities (#1229)Andrew Reynolds
2017-10-12Sygus logics (#1226)Andrew Reynolds
2017-10-11Enable regressions for CBQI BV and fix inverse for LSHR. (#1234)Aina Niemetz
2017-10-11Add side conditions for UDIV_TOTAL, SHL, CONCAT. (#1224)Mathias Preiner
2017-10-11Cleaning up ProofArray class. (#1208)Tim King
2017-10-11Ho Lambda Lifting (#1116)Andrew Reynolds
2017-10-11Adds infrastructure for a rewriting pass in BvInstantiator::processAssertion ...Andrew Reynolds
2017-10-11Move unsat core names to smt engine (#1192)Andrew Reynolds
2017-10-10Ho node manager types (#1203)Andrew Reynolds
2017-10-10Add copyright information. (#1201)Aina Niemetz
2017-10-10Fix memory leak in quantifiers engine (#1219)Andres Noetzli
2017-10-09Add skeleton of the FP theory solver (#1130)Martin
2017-10-09Split term database (#1206)Andrew Reynolds
2017-10-09CBQI BV: Add inverse for more operators. (#1213)Aina Niemetz
2017-10-05Fix typo in comment.Clark Barrett
2017-10-05Minor change to how SyGus commands are translated to SmtEngine commands. This...Andrew Reynolds
2017-10-05Ho model (#1120)Andrew Reynolds
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 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-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-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-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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback