summaryrefslogtreecommitdiff
path: root/src/options
AgeCommit message (Expand)Author
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
2017-07-10Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes ...ajreynol
2017-07-07Update copyright headers.Mathias Preiner
2017-06-28Enable non-linear solve by default, update regressions.ajreynol
2017-05-30print only labeled assertions as part of the unsat coreguykatzz
2017-05-12Adding VPATH back inmakaimann
2017-05-12Conditional coverage buildmakaimann
2017-05-05Do not eliminate extended arithmetic symbols when finite model finding is on,...ajreynol
2017-04-21Handle subtypes in sets. Bug fixes for tuples with subtypes.ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback