Age | Commit message (Expand) | Author |
2017-10-10 | Add copyright information. (#1201) | Aina Niemetz |
2017-10-04 | Ho quant util (#1119) | Andrew Reynolds |
2017-10-03 | Add Cryptominisat and LFSC to --show-config output. (#1194) | Mathias Preiner |
2017-09-30 | SyGuS streaming solution mode (#1131) | Andrew Reynolds |
2017-09-29 | Initial working version of BV word-level instantiation (#1158) | Andrew Reynolds |
2017-09-20 | Extend quantifier-free UF solver to higher-order. This includes an ex… (#1100) | Andrew Reynolds |
2017-08-30 | Use thread_local instead of compiler extensions (#210) | Andres Noetzli |
2017-08-25 | Move LFSC checker out of the CVC repository. (#222) | Aina Niemetz |
2017-08-17 | Add mbqi interleave option, change option fs-inst to fs-interleave. | ajreynol |
2017-08-10 | Fix line numbers in options_template | Andres Noetzli |
2017-08-04 | Set default language to smt lib 2.6 (including as a base language for sygus),... | ajreynol |
2017-07-14 | Removing BOOST_FOREACH usage. | Tim King |
2017-07-10 | Merge ntExt branch. Adds support for transcendental functions. Refactoring of... | ajreynol |
2017-07-10 | Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes ... | ajreynol |
2017-07-07 | Update copyright headers. | Mathias Preiner |
2017-06-28 | Enable non-linear solve by default, update regressions. | ajreynol |
2017-05-30 | print only labeled assertions as part of the unsat core | guykatzz |
2017-05-12 | Adding VPATH back in | makaimann |
2017-05-12 | Conditional coverage build | makaimann |
2017-05-05 | Do not eliminate extended arithmetic symbols when finite model finding is on,... | ajreynol |
2017-04-21 | Handle subtypes in sets. Bug fixes for tuples with subtypes. | ajreynol |
2017-04-20 | Minor fixes. | ajreynol |
2017-04-18 | Coverage fix | makaimann |
2017-04-07 | Change option names for nl. | ajreynol |
2017-04-05 | Merge pull request #143 from FabianWolff/master | Clark Barrett |
2017-04-05 | Add non-linear regressions, disable nlAlgSubs, do not do rep checking for NON... | ajreynol |
2017-04-05 | Fix several spelling errors | Fabian Wolff |
2017-04-04 | Enable multi-trigger-linear by default, add option. | ajreynol |
2017-04-02 | Adding a model based axiom instantiation scheme for multiplication. Merge com... | Tim King |
2017-03-31 | Add option multi-trigger-linear, minor optimization to E-matching. | ajreynol |
2017-03-29 | Add quantifiers options related to model and master equality engine. | ajreynol |
2017-03-24 | Refactor model building for quantifiers to be a single pass, simplification. ... | ajreynol |
2017-03-22 | Work on new approach for sygus involving conditional solutions. Refactoring o... | ajreynol |
2017-03-16 | Parsing support for SMT LIB 2.6. Minor fixes for printing datatypes. Fix for ... | ajreynol |
2017-03-06 | Adding support for bool-to-bv | Clark Barrett |
2017-03-02 | Minor cleanup and reorganization related to last commit. | ajreynol |
2017-03-02 | Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boole... | ajreynol |
2017-02-15 | Minimization modes for fmf bound. | ajreynol |
2017-02-07 | Generalize finite bound inference to unifiable variables in set membership li... | ajreynol |
2016-12-29 | Changing getTearDownIncremental() to return the type of options::tearDownIncr... | Tim King |
2016-12-07 | Refactoring, generalization of bounded inference module. Simplification of re... | ajreynol |
2016-11-21 | Refactoring related to track instantiation option. | ajreynol |
2016-11-11 | Add simple inferences for extended bitvector functions, add a few related opt... | ajreynol |
2016-11-10 | Add option for enabling/disabling lazy extended function reduction in bitvect... | ajreynol |
2016-11-08 | Add a few options to separation logic and sets. Minor changes to separation l... | ajreynol |
2016-10-26 | New implementation of sets+cardinality. Merge Paul Meng's relation solver as... | ajreynol |
2016-10-05 | Added an option that allow empty dependencies when attempting to minimize pre... | guykatzz |
2016-09-20 | More refactoring of cbqi. Add a few regressions. Add option for qcf. | ajreynol |
2016-09-16 | Use matching heuristics for EPR instantiation. | ajreynol |
2016-09-15 | Begin refactoring of cbqi, remove a few dead options. Pre-skolemize by defaul... | ajreynol |