summaryrefslogtreecommitdiff
path: root/src/options
AgeCommit message (Expand)Author
2018-02-05Statically eliminate redundant sygus constructors (#1560)Andrew Reynolds
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-02Option to check solutions produced by SyGuS solver (#1553)Haniel Barbosa
2018-02-01Use sygus to synthesize/verify rewrite rules (#1547)Andrew Reynolds
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-17Removes yet more throw specifiers. Updating the documentation as needed. (#1518)Tim King
2018-01-14Removing throw specifiers from OptionsHandler. (#1510)Tim King
2018-01-09Cleaning up throw specifiers on Exception and subclasses. (#1475)Tim King
2018-01-09Fix output of --trace=help. (#1500)Aina Niemetz
2018-01-08Removing more miscellaneous throw specifiers. (#1488)Tim King
2018-01-03Global negate (#1466)Andrew Reynolds
2017-12-29Cbqi repeat solve literal (#1458)Andrew Reynolds
2017-12-27Disable sygus PBE when sygus stream is enabled (#1451)Andrew Reynolds
2017-12-20Transcendental functions check model (#1443)Andrew Reynolds
2017-12-10Add new infrastructure for preprocessing passes (#1053)justinxu421
2017-12-08Add CEGQI BV linearization of additions and equalities over additions. (#1417)Mathias Preiner
2017-12-07Fixes related to SyGuS + real arithmetic (#1432)Andrew Reynolds
2017-12-05Fix output of --show-trace-tags. (#1430)Mathias Preiner
2017-12-03Normalize grammars - 2 (#1420)Haniel Barbosa
2017-11-30Add Gaussian Elimination as a preprocessing pass for BV. (#1342)Aina Niemetz
2017-11-29Minor improvements and changes to defaults for cbqi bv (#1406)Andrew Reynolds
2017-11-24Implement tangent and secant planes for transcendental functions (#1401)Andrew Reynolds
2017-11-22Sygus Lambda Grammars (#1390)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-18Ho instantiation (#1204)Andrew Reynolds
2017-11-17Add random number generator. (#1370)Aina Niemetz
2017-11-13Disable sygus qe preprocessing by default (#1353)Andrew Reynolds
2017-11-03Fix bv help message. (#1315)Andrew Reynolds
2017-11-03Sygus clean main (#1297)Andrew Reynolds
2017-10-27Cbqi multiple instantiation (#1289)Andrew Reynolds
2017-10-24Cbqi bv ineq mode (#1273)Andrew Reynolds
2017-10-23CBQI BV: Add ULT/SLT inverse handling. (#1268)Aina Niemetz
2017-10-20SyGuS term size limit (#1262)Andrew Reynolds
2017-10-12CBQI BV quick heuristics (#1239)Andrew Reynolds
2017-10-10Add copyright information. (#1201)Aina Niemetz
2017-10-04Ho quant util (#1119)Andrew Reynolds
2017-10-03Add Cryptominisat and LFSC to --show-config output. (#1194)Mathias Preiner
2017-09-30SyGuS streaming solution mode (#1131)Andrew Reynolds
2017-09-29Initial working version of BV word-level instantiation (#1158)Andrew Reynolds
2017-09-20Extend quantifier-free UF solver to higher-order. This includes an ex… (#1100)Andrew Reynolds
2017-08-30Use thread_local instead of compiler extensions (#210)Andres Noetzli
2017-08-25Move LFSC checker out of the CVC repository. (#222)Aina Niemetz
2017-08-17Add mbqi interleave option, change option fs-inst to fs-interleave.ajreynol
2017-08-10Fix line numbers in options_templateAndres Noetzli
2017-08-04Set default language to smt lib 2.6 (including as a base language for sygus),...ajreynol
2017-07-14Removing BOOST_FOREACH usage.Tim King
2017-07-10Merge ntExt branch. Adds support for transcendental functions. Refactoring of...ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback