summaryrefslogtreecommitdiff
path: root/src/options/quantifiers_options
AgeCommit message (Expand)Author
2018-03-21Refactor mkoptions (#1631)Mathias Preiner
2018-02-27Improvements to sygus sampling (#1621)Andrew Reynolds
2018-02-08Minor improvements to sygus sampling. (#1577)Andrew Reynolds
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-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-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-03Normalize grammars - 2 (#1420)Haniel Barbosa
2017-11-29Minor improvements and changes to defaults for cbqi bv (#1406)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-13Disable sygus qe preprocessing by default (#1353)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-12CBQI BV quick heuristics (#1239)Andrew Reynolds
2017-10-04Ho quant util (#1119)Andrew Reynolds
2017-09-30SyGuS streaming solution mode (#1131)Andrew Reynolds
2017-09-29Initial working version of BV word-level instantiation (#1158)Andrew Reynolds
2017-08-17Add mbqi interleave option, change option fs-inst to fs-interleave.ajreynol
2017-07-10Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes ...ajreynol
2017-05-05Do not eliminate extended arithmetic symbols when finite model finding is on,...ajreynol
2017-04-20Minor fixes.ajreynol
2017-04-04Enable multi-trigger-linear by default, add option.ajreynol
2017-03-31Add option multi-trigger-linear, minor optimization to E-matching.ajreynol
2017-03-29Add quantifiers options related to model and master equality engine.ajreynol
2017-03-24Refactor model building for quantifiers to be a single pass, simplification. ...ajreynol
2017-03-22Work on new approach for sygus involving conditional solutions. Refactoring o...ajreynol
2017-02-15Minimization modes for fmf bound.ajreynol
2016-12-07Refactoring, generalization of bounded inference module. Simplification of re...ajreynol
2016-11-21Refactoring related to track instantiation option.ajreynol
2016-09-20More refactoring of cbqi. Add a few regressions. Add option for qcf.ajreynol
2016-09-16Use matching heuristics for EPR instantiation.ajreynol
2016-09-15Begin refactoring of cbqi, remove a few dead options. Pre-skolemize by defaul...ajreynol
2016-09-12Refactor prenex modes.ajreynol
2016-09-12Remove old implementation of cbqiajreynol
2016-09-09Support for separation logic + EPR. Refactor preprocessing of sep.nil, only a...ajreynol
2016-09-03Option for prenex normal formajreynol
2016-09-01Fix boolean term issue in invariants from sygus. Minor default options change...ajreynol
2016-09-01Updates to cbqi. New strategy --cbqi-nested-qe to do qe on nested quantifier...ajreynol
2016-08-26Basic support for EPR+CBQI. Minor cleanup.ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback