summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2017-12-04Fix side condition for BITVECTOR_MULT. (#1422)Mathias Preiner
2017-12-03Normalize grammars - 2 (#1420)Haniel Barbosa
2017-12-02Minor improvements to inst match generator (#1415)Andrew Reynolds
2017-12-01Improve rewriter for string replace (#1416)Andrew Reynolds
2017-12-01Fix reset-assertions (#1413)Andres Noetzli
2017-12-01Minor additions for sygus (#1419)Andrew Reynolds
2017-12-01Refactor and generalize PBE strategies (#1410)Andrew Reynolds
2017-12-01Fix build when Valgrind instrumentation enabledAndres Noetzli
2017-11-30Add debugging tools for ContextMemoryManager (#1407)Andres Noetzli
2017-11-30Add Gaussian Elimination as a preprocessing pass for BV. (#1342)Aina Niemetz
2017-11-30Fixes for issue 1404 (#1409)Andrew Reynolds
2017-11-30Remove remaining references to QuantArith (#1408)Andrew Reynolds
2017-11-29Minor improvements and changes to defaults for cbqi bv (#1406)Andrew Reynolds
2017-11-29Improve caching in term formula removal (#1398)Andrew Reynolds
2017-11-29Adding missing break statements. CID 1362756. (#1394)Tim King
2017-11-29Simplifying the conditions in checkLetBinding to avoid using iterator… (#1372)Tim King
2017-11-28Improve the rewriter for SINE. (#1221)Andrew Reynolds
2017-11-28Improve rewrite for string substr (#1337)Andrew Reynolds
2017-11-28Improve trigger filter instances (#1402)Andrew Reynolds
2017-11-28Removing throw specifiers from internal Printer hierarchy. (#1393)Tim King
2017-11-27Fix models for --solve-real-as-int. (#1371)Andrew Reynolds
2017-11-25Fixes for higher-order (#1405)Andrew Reynolds
2017-11-24(Refactor) Instantiate utility (#1387)Andrew Reynolds
2017-11-24Implement tangent and secant planes for transcendental functions (#1401)Andrew Reynolds
2017-11-23Ho parsing and regressions (#1350)Andrew Reynolds
2017-11-22Converting defined functions and let expressions from Sygus grammars to lambd...Haniel Barbosa
2017-11-22Sygus Lambda Grammars (#1390)Andrew Reynolds
2017-11-22Transcendental tangent planes utilities (#1288)Andrew Reynolds
2017-11-21Adding infrastructure for normalizing SyGuS grammars (#1397)Haniel Barbosa
2017-11-21Cegqi bv remove extract terms preprocess pass (#1376)Andrew Reynolds
2017-11-20Initializes members of QuantInfo. Resolves CID 1362929. (#1391)Tim King
2017-11-19Removing an unused variable from SygusInput. Resolves CID 1362932. (#1392)Tim King
2017-11-18Ho instantiation (#1204)Andrew Reynolds
2017-11-18Names the Effort enum of QuantConflictFind class. (#1354)Tim King
2017-11-17(Refactor) Document and clean single invocation partition. (#1364)Andrew Reynolds
2017-11-17Add random number generator. (#1370)Aina Niemetz
2017-11-16(Refactor) Arithmetic monomial sum (#1381)Andrew Reynolds
2017-11-15Initializes BitVectorProof::d_isAssumptionConflict. Resolves CID 1362898. (#1...Tim King
2017-11-15Sygus print callbacks (#1348)Andrew Reynolds
2017-11-15Removes an unused variable from Theory. (#1375)Tim King
2017-11-15Initializing members of Datatype. Addresses CIDs 1362897, 1362912, 1362923 an...Tim King
2017-11-15Adding garbage collection for Proof objects. (#1294)Tim King
2017-11-14Make QEffort an enum (#1366)Andrew Reynolds
2017-11-14(Refactor) Split sygus term db (#1335)Andrew Reynolds
2017-11-14Clean Ceg Instantiators (#1365)Andrew Reynolds
2017-11-14Cleaning up exporting vectors within commands. Resolves CID 1172285 and 11722...Tim King
2017-11-14Initializes InstPropagator::d_has_relevant_inst. Resolves 1362891. (#1360)Tim King
2017-11-13Initializes RegExpOpr::d_char_start and d_char_end. (#1359)Tim King
2017-11-13Initializes TriggerInfo::polarity. Resolves CID 1172054. (#1358)Tim King
2017-11-13Initializes NodeTheoryPair::timestamp in the default constructor. (#1356)Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback