projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Merge pull request #73 from kbansal/parser-dont-tokenize
[cvc5.git] / src / theory / quantifiers /
2015-04-22 Kshitij BansalMerge pull request #73 from kbansal/parser-dont-tokenize tree | commitdiff
2015-04-21 ajreynolFix bug in fmf mbqi=fmc with arrays. Add two datatypes... tree | commitdiff
2015-04-17 Kshitij BansalMerge pull request #72 from kbansal/decision-requirephase tree | commitdiff
2015-04-16 ajreynolFix option --quant-fun-wd. Add mk_starexec script... tree | commitdiff
2015-04-16 ajreynolHandle (degenerate) case of synthesis conjectures for... tree | commitdiff
2015-04-13 Tim KingMaking CVC4::theory::quantifiers::PrenexQuantMode publi... tree | commitdiff
2015-04-09 ajreynolFix unsat-core issues related to rewrite rules, quantif... tree | commitdiff
2015-04-09 ajreynolFix performance issue with variable triggers + instanti... tree | commitdiff
2015-04-08 ajreynolMake fun-def quantifiers carry the function app they... tree | commitdiff
2015-04-07 ajreynolMinor fixes for cegqi. tree | commitdiff
2015-04-02 Kshitij BansalMerge pull request #71 from kbansal/const-are-triggers tree | commitdiff
2015-04-01 ajreynolImprovements and bug fixes related to cbqi/cegqi. ... tree | commitdiff
2015-03-31 Kshitij Bansalfix no return value warning tree | commitdiff
2015-03-23 ajreynolDecouple counter-example guided quantifier instantiatio... tree | commitdiff
2015-03-11 ajreynolMinor fixes and improvements to cegqi-si for linear... tree | commitdiff
2015-03-05 ajreynolMinor fixes. Extend cegqi-si to real arithmetic. tree | commitdiff
2015-03-04 ajreynolMore work on arithmetic single invocation synthesis... tree | commitdiff
2015-02-26 ajreynolRobust strategy for single invocation LIA synthesis... tree | commitdiff
2015-02-22 ajreynolNew trigger options. --inst-no-entail on by default... tree | commitdiff
2015-02-13 ajreynolHandle recursive singleton case for codatatypes, add... tree | commitdiff
2015-02-11 ajreynolBetter support for solving multiple functions with... tree | commitdiff
2015-02-11 ajreynolMove si solution reconstruction to own file, make more... tree | commitdiff
2015-02-06 ajreynolHandle missing cases for single inv solution reconstruc... tree | commitdiff
2015-02-06 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4 tree | commitdiff
2015-02-05 ajreynolWorking version of sygus solution reconstruction from... tree | commitdiff
2015-02-04 ajreynolInitial draft of solution reconstruction into syntax... tree | commitdiff
2015-02-04 ajreynolWork on solution reconstruction for single inv. Fix... tree | commitdiff
2015-02-04 ajreynolRefactor sygus_util to TermDb. Initial work on solutio... tree | commitdiff
2015-02-04 ajreynolStart work on simplifying single inv solutions. Minor. tree | commitdiff
2015-02-03 ajreynolSimple variable elimination for single inv properties... tree | commitdiff
2015-02-02 ajreynolSolutions for single invocation conjectures. tree | commitdiff
2015-02-02 ajreynolSingle invocation module for counterexample guided... tree | commitdiff
2015-02-01 ajreynolGeneralization of sygus lemmas based on arguments and... tree | commitdiff
2015-01-31 ajreynolBug fix fairness for commutative operators in sygus... tree | commitdiff
2015-01-31 ajreynolLemmas instead of conflicts in sygus sym break (do... tree | commitdiff
2015-01-30 ajreynolGeneralize conflict clauses in sygus sym break, merge... tree | commitdiff
2015-01-29 ajreynolRestrict LtePartialInst instantiations based on E-match... tree | commitdiff
2015-01-29 ajreynolApply global search space narrowing for multiple synth... tree | commitdiff
2015-01-28 ajreynolMinor refactor CEGQI. tree | commitdiff
2015-01-27 ajreynolAlways miniscope nested quantifiers. Disable miniscopi... tree | commitdiff
2015-01-27 ajreynolRecognize when synthesis conjectures are in single... tree | commitdiff
2015-01-26 ajreynolOutput solutions for synthesis conjectures with --dump... tree | commitdiff
2015-01-24 ajreynolVariable patterns only look at eligible terms. Minor... tree | commitdiff
2015-01-24 ajreynolAdd --lte-restrict-inst-closure option. Push dt.size... tree | commitdiff
2015-01-23 ajreynolCEGQI fairness based on term height. Fix sygus-nf... tree | commitdiff
2015-01-23 ajreynolRework inst-closure. tree | commitdiff
2015-01-22 ajreynolNarrow sygus search space based on NNF and rewriting... tree | commitdiff
2015-01-22 ajreynolAdd option --lte-partial-inst. Remove inst-closure. tree | commitdiff
2015-01-22 ajreynolDo not drop patterns during boolean term rewriting... tree | commitdiff
2015-01-21 ajreynolInitial work on sygusNormalForm. tree | commitdiff
2015-01-20 ajreynolMark datatypes as sygus. Add option to normalize sygus... tree | commitdiff
2015-01-20 ajreynolHandle miniscoping of conjunctions in synthesis propert... tree | commitdiff
2015-01-16 ajreynolAllow uninterpreted/defined functions in Sygus grammars... tree | commitdiff
2015-01-16 ajreynolMinor: Ensure indexed terms are in EE. Add support... tree | commitdiff
2015-01-14 Morgan Deterssygus input language and benchmark tree | commitdiff
2015-01-07 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4 tree | commitdiff
2014-12-28 ajreynolDisable prenex by default when using fmf bound int... tree | commitdiff
2014-12-27 Dejan JovanovicAdding an option to the equality engine constructor... tree | commitdiff
2014-12-21 ajreynolAdd misc trigger options. tree | commitdiff
2014-12-03 Kshitij BansalMerge branch 'master' of https://github.com/CVC4/CVC4 tree | commitdiff
2014-11-28 ajreynolSynchronize conjecture generation with E-matching.... tree | commitdiff
2014-11-27 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4 tree | commitdiff
2014-11-25 ajreynolFix bug in --term-db-mode=relevant with variable trigge... tree | commitdiff
2014-11-21 ajreynolThrow error when pattern is not list of terms. tree | commitdiff
2014-11-21 ajreynolChange default option to --inst-when=full-last-call... tree | commitdiff
2014-11-18 ajreynolCompute model basis only for fmf. Add another co-datat... tree | commitdiff
2014-11-18 ajreynolAdd local theory extensions instantiation strategy... tree | commitdiff
2014-11-17 Morgan DetersNew, uniform checkTime statistic for all theories ... tree | commitdiff
2014-11-16 ajreynolAdd term db mode. Minor changes to quantifiers rewrite... tree | commitdiff
2014-11-14 ajreynolBe lazier to consider EQC in UF+cardinality solver... tree | commitdiff
2014-11-13 Morgan DetersMerge pull request #69 from mdeters/bug594 tree | commitdiff
2014-11-13 ajreynolRemove two obsolete versions of MBQI. tree | commitdiff
2014-11-13 ajreynolMore preparation for filtering relevant terms in TermDb. tree | commitdiff
2014-11-11 Kshitij BansalMerge pull request #64 from mdeters/theorysets-hashset... tree | commitdiff
2014-11-11 ajreynolWork on synchronizing decision=justification and E... tree | commitdiff
2014-11-10 Tianyi LiangMerge pull request #63 from mdeters/theorystrings-hashs... tree | commitdiff
2014-11-10 ajreynolDo not eliminate variables only occurring in patterns... tree | commitdiff
2014-11-10 Morgan DetersMerge branch '1.4.x' tree | commitdiff
2014-11-07 Morgan DetersMerge branch '1.4.x' tree | commitdiff
2014-11-07 Morgan DetersMerge branch '1.4.x' tree | commitdiff
2014-11-07 ajreynolEnable --quant-cf by default. Fix bug in qcf for mixed... tree | commitdiff
2014-11-07 Morgan DetersMerge branch '1.4.x' tree | commitdiff
2014-11-07 ajreynolProperly distinguish which EQC to assign values in... tree | commitdiff
2014-11-05 ajreynolFix model bug in --mbqi=fmc. Minor cleanup in datatypes. tree | commitdiff
2014-11-05 Morgan DetersMerge branch '1.4.x' tree | commitdiff
2014-11-05 ajreynolMore work on datatypes theory combination: fix bug... tree | commitdiff
2014-11-01 ajreynolFix cegqi for synthesis without syntax. tree | commitdiff
2014-11-01 ajreynolFix some mistakes in datatypes theory combination,... tree | commitdiff
2014-10-31 ajreynolDo not allow duplication of function definitions. ... tree | commitdiff
2014-10-28 ajreynolPreprocessing step for finding finite runs of well... tree | commitdiff
2014-10-28 ajreynolInitial infrastructure for function definition quantifi... tree | commitdiff
2014-10-28 ajreynolImprove stats in conjecture generator, minor cleanup. tree | commitdiff
2014-10-25 ajreynolMinor fix for --user-pat=resort tree | commitdiff
2014-10-24 Morgan DetersFix typo. tree | commitdiff
2014-10-24 ajreynolAdd --user-pat=resort. Minor cleanup of options. tree | commitdiff
2014-10-18 ajreynolFix for bounded integers when incremental, fixes bug... tree | commitdiff
2014-10-17 Morgan DetersMerge branch '1.4.x' tree | commitdiff
2014-10-16 ajreynolMake --user-pat=trust default. Fix a few warnings... tree | commitdiff
2014-10-16 Morgan DetersMerge branch '1.4.x' tree | commitdiff
2014-10-16 ajreynolAdd dt.size to datatypes theory. Add option for fairne... tree | commitdiff
next