summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-02-06Resolving warnings from -Winconsistent-missing-override on clang. (#1563)Tim King
2018-02-06Fix two multiply-by-constant corner cases for bv rewriter (#1562)Andrew Reynolds
2018-02-06Updated authors listAina Niemetz
2018-02-06Fix rewrite for string replace (#1537)Andrew Reynolds
2018-02-05Using getOperator() directly instead of using -1. CID 1172262. (#1559)Tim King
2018-02-05Aborting on errors in StatisticsRegistry::unregisterStat() instead of throwin...Tim King
2018-02-05Statically eliminate redundant sygus constructors (#1560)Andrew Reynolds
2018-02-05Cleaning up the printing of theory model representative sets. (#1538)Tim King
2018-02-05Removing references to __gnu_cxx. (#1541)Tim King
2018-02-04Sample based on sygus grammar by default (#1558)Andrew Reynolds
2018-02-02Option to use sampling for CEGIS (#1555)Andrew Reynolds
2018-02-02Restoring ostream format. Resolves a few CIDs 1362780. (#1543)Tim King
2018-02-02Fix remaining synthesis solution regressions (#1557)Andrew Reynolds
2018-02-02Option to check solutions produced by SyGuS solver (#1553)Haniel Barbosa
2018-02-01Add interface in sygus to get synthesis solution Nodes (#1552)Andrew Reynolds
2018-02-01Use sygus to synthesize/verify rewrite rules (#1547)Andrew Reynolds
2018-01-30Further clean and document datatypes rewriter (#1548)Andrew Reynolds
2018-01-29Generalize explanations for PBE sygus strings based on negative contains when...Andrew Reynolds
2018-01-28Sort children of all commutative operators for sygus. (#1544)Andrew Reynolds
2018-01-27Removing an unused variable. Resolves CID 1172257. (#1542)Tim King
2018-01-26Removing structurally dead code. (#1540)Tim King
2018-01-24Commenting out throw specifiers on SmtEngine. These can later be refined into...Tim King
2018-01-24Added unit tests for PLUS, NEG, NOT ICs for CBQI BV. (#1534)Aina Niemetz
2018-01-23Fix MULT handling for CBQI BV. (#1531)Aina Niemetz
2018-01-23Commenting out throw specifiers for DeltaRationExceptions. These functions ca...Tim King
2018-01-22Add previous concat handling for CBQI BV as heuristic for EQ. (#1528)Aina Niemetz
2018-01-21Refactor and fix solveBvLit for CBQI BV. (#1526)Aina Niemetz
2018-01-21Only push/pop around check-sat if it is associated with an assertion (#1525)Andrew Reynolds
2018-01-17Removes yet more throw specifiers. Updating the documentation as needed. (#1518)Tim King
2018-01-15Removing more miscellaneous throw specifiers. (#1509)Tim King
2018-01-14Removing throw specifiers from Type. (#1511)Tim King
2018-01-14Removing throw specifiers from OptionsHandler. (#1510)Tim King
2018-01-13Remove BITVECTOR_SUB from isInvertible(). (#1513)Aina Niemetz
2018-01-12Improvements for CBQI BV (#1504)Andrew Reynolds
2018-01-10Removed division by constant handling for CBQI BV (unsound). (#1508)Aina Niemetz
2018-01-10Removing throw specifiers for TypeRules. (#1501)Tim King
2018-01-10Removing throw specifiers from type enumerators. (#1502)Tim King
2018-01-09Cleaning up throw specifiers on Exception and subclasses. (#1475)Tim King
2018-01-09Fix linearization for terms where the solve variable does not occur. (#1506)Mathias Preiner
2018-01-09Reorganized bitvector.h. (#1505)Aina Niemetz
2018-01-09Fix output of --trace=help. (#1500)Aina Niemetz
2018-01-09Removing throw specifiers from miscellaneous src/expr/ classes. (#1503)Tim King
2018-01-08Removing more miscellaneous throw specifiers. (#1488)Tim King
2018-01-08Add bv util mkConst(unsigned, Integer&). (#1499)Aina Niemetz
2018-01-08Remove throw specifiers from symbol table. (#1490)Tim King
2018-01-08Added division by constant handling for CBQI BV. (#1498)Aina Niemetz
2018-01-08Remove portfolio option from builds. (#1496)Aina Niemetz
2018-01-08Removes throw specifiers from command.{h,cpp}. (#1485)Tim King
2018-01-08Improvements to quant+BV/Bool variable elimination (#1495)Andrew Reynolds
2018-01-08Fix broken GMP URL in get-win-dependencies script (#1493)Andres Noetzli
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback