summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/ce_guided_single_inv.h
AgeCommit message (Expand)Author
2016-10-11Merge branch 'origin' of https://github.com/CVC4/CVC4.gitPaul Meng
2016-09-25Adding a destructor to CegqiOutputSingleInv.Tim King
2016-08-24Merge remote-tracking branch 'origin/master'PaulMeng
2016-07-26Add option to minimize sygus solutions based on using weakest implicants of i...ajreynol
2016-07-05Merge branch 'master' of https://github.com/CVC4/CVC4.gitPaulMeng
2016-04-20update from the masterPaulMeng
2016-04-10More work on instantiation propagation. Enable external filtering of instanti...ajreynol
2016-04-03Updating the copyright headers and scripts.Tim King
2016-03-24Freeing CegConjecture::d_ceg_si. Also making d_ceg_si a provate member of Ceg...Tim King
2016-03-08Extend synthesis solver to handle single invocation with additional universal...ajreynol
2016-03-01Shorter explanations for strings based on tracking which parts of normal form...ajreynol
2015-12-02Minor fixes for cegqi-si-partial.ajreynol
2015-12-01More work on --cegqi-si-partial, incomplete.ajreynol
2015-11-28Initial work on --cegqi-si-partial, refactoring.ajreynol
2015-11-26Update to new implementation of single invocation partition by default.ajreynol
2015-11-26Front-end support for get-value of sort cardinality, minor fixes for sygus so...ajreynol
2015-11-25Infrastructure for partially single invocation properties. Bug fix for uncons...ajreynol
2015-08-28Improvements to sygus, register equivalent terms based on rewrites of origina...ajreynol
2015-08-27Do ITE term bookkeeping when solving Sygus inputs. Add missing script from S...ajreynol
2015-08-24Improvements to vts in cbqi, bug fix vts for non-atomic terms containing vts ...ajreynol
2015-08-19Implementation of model-based projection in cbqi, cleanup, add regressions.ajreynol
2015-07-30Implement virtual term substitution for non-nested quantifiers. Fix soundnes...ajreynol
2015-07-25Add option --sygus-inv-templ for synthesizing strengthening/weakening of pre/...ajreynol
2015-07-20Squashed merge of SygusComp 2015 branch.ajreynol
2015-07-05Add options --partial-triggers, --elim-taut-quant, improve robustness of --pu...ajreynol
2015-07-02On-demand upper bound lemmas for deltas in quantified LRA (for casc). Force n...ajreynol
2015-05-29Do not enforce dt fairness when single invocation sygus.ajreynol
2015-04-21Changes needed to compile at Google, plus some bug fixes from Google.Clark Barrett
2015-04-01Improvements and bug fixes related to cbqi/cegqi. Minor fix for fmf with fun...ajreynol
2015-03-23Decouple counter-example guided quantifier instantiation from Sygus.ajreynol
2015-03-11Minor fixes and improvements to cegqi-si for linear arithmetic.ajreynol
2015-03-05Minor fixes. Extend cegqi-si to real arithmetic.ajreynol
2015-03-04More work on arithmetic single invocation synthesis conjectures.ajreynol
2015-02-26Robust strategy for single invocation LIA synthesis conjectures. Add regress...ajreynol
2015-02-11Better support for solving multiple functions with cegqi-si. Minor cleanup.ajreynol
2015-02-11Move si solution reconstruction to own file, make more robust. Other refactor...ajreynol
2015-02-06Handle missing cases for single inv solution reconstruction. Minor fixes. Re...ajreynol
2015-02-05Working version of sygus solution reconstruction from single inv cegqi. Heur...ajreynol
2015-02-04Initial draft of solution reconstruction into syntax for single inv cegqi.ajreynol
2015-02-04Work on solution reconstruction for single inv. Fix compiler error found by ...ajreynol
2015-02-04Refactor sygus_util to TermDb. Initial work on solution reconstruction into ...ajreynol
2015-02-04Start work on simplifying single inv solutions. Minor.ajreynol
2015-02-03Simple variable elimination for single inv properties. Relax conditions for ...ajreynol
2015-02-03Solutions for single invocation conjectures.ajreynol
2015-02-02Single invocation module for counterexample guided quantifier instantiation -...ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback