projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
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 Bansal
Merge pull request #73 from kbansal/parser-dont-tokenize
tree
|
commitdiff
2015-04-21
ajreynol
Fix bug in fmf mbqi=fmc with arrays. Add two datatypes...
tree
|
commitdiff
2015-04-17
Kshitij Bansal
Merge pull request #72 from kbansal/decision-requirephase
tree
|
commitdiff
2015-04-16
ajreynol
Fix option --quant-fun-wd. Add mk_starexec script...
tree
|
commitdiff
2015-04-16
ajreynol
Handle (degenerate) case of synthesis conjectures for...
tree
|
commitdiff
2015-04-13
Tim King
Making CVC4::theory::quantifiers::PrenexQuantMode publi...
tree
|
commitdiff
2015-04-09
ajreynol
Fix unsat-core issues related to rewrite rules, quantif...
tree
|
commitdiff
2015-04-09
ajreynol
Fix performance issue with variable triggers + instanti...
tree
|
commitdiff
2015-04-08
ajreynol
Make fun-def quantifiers carry the function app they...
tree
|
commitdiff
2015-04-07
ajreynol
Minor fixes for cegqi.
tree
|
commitdiff
2015-04-02
Kshitij Bansal
Merge pull request #71 from kbansal/const-are-triggers
tree
|
commitdiff
2015-04-01
ajreynol
Improvements and bug fixes related to cbqi/cegqi. ...
tree
|
commitdiff
2015-03-31
Kshitij Bansal
fix no return value warning
tree
|
commitdiff
2015-03-23
ajreynol
Decouple counter-example guided quantifier instantiatio...
tree
|
commitdiff
2015-03-11
ajreynol
Minor fixes and improvements to cegqi-si for linear...
tree
|
commitdiff
2015-03-05
ajreynol
Minor fixes. Extend cegqi-si to real arithmetic.
tree
|
commitdiff
2015-03-04
ajreynol
More work on arithmetic single invocation synthesis...
tree
|
commitdiff
2015-02-26
ajreynol
Robust strategy for single invocation LIA synthesis...
tree
|
commitdiff
2015-02-22
ajreynol
New trigger options. --inst-no-entail on by default...
tree
|
commitdiff
2015-02-13
ajreynol
Handle recursive singleton case for codatatypes, add...
tree
|
commitdiff
2015-02-11
ajreynol
Better support for solving multiple functions with...
tree
|
commitdiff
2015-02-11
ajreynol
Move si solution reconstruction to own file, make more...
tree
|
commitdiff
2015-02-06
ajreynol
Handle missing cases for single inv solution reconstruc...
tree
|
commitdiff
2015-02-06
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
tree
|
commitdiff
2015-02-05
ajreynol
Working version of sygus solution reconstruction from...
tree
|
commitdiff
2015-02-04
ajreynol
Initial draft of solution reconstruction into syntax...
tree
|
commitdiff
2015-02-04
ajreynol
Work on solution reconstruction for single inv. Fix...
tree
|
commitdiff
2015-02-04
ajreynol
Refactor sygus_util to TermDb. Initial work on solutio...
tree
|
commitdiff
2015-02-04
ajreynol
Start work on simplifying single inv solutions. Minor.
tree
|
commitdiff
2015-02-03
ajreynol
Simple variable elimination for single inv properties...
tree
|
commitdiff
2015-02-02
ajreynol
Solutions for single invocation conjectures.
tree
|
commitdiff
2015-02-02
ajreynol
Single invocation module for counterexample guided...
tree
|
commitdiff
2015-02-01
ajreynol
Generalization of sygus lemmas based on arguments and...
tree
|
commitdiff
2015-01-31
ajreynol
Bug fix fairness for commutative operators in sygus...
tree
|
commitdiff
2015-01-31
ajreynol
Lemmas instead of conflicts in sygus sym break (do...
tree
|
commitdiff
2015-01-30
ajreynol
Generalize conflict clauses in sygus sym break, merge...
tree
|
commitdiff
2015-01-29
ajreynol
Restrict LtePartialInst instantiations based on E-match...
tree
|
commitdiff
2015-01-29
ajreynol
Apply global search space narrowing for multiple synth...
tree
|
commitdiff
2015-01-28
ajreynol
Minor refactor CEGQI.
tree
|
commitdiff
2015-01-27
ajreynol
Always miniscope nested quantifiers. Disable miniscopi...
tree
|
commitdiff
2015-01-27
ajreynol
Recognize when synthesis conjectures are in single...
tree
|
commitdiff
2015-01-26
ajreynol
Output solutions for synthesis conjectures with --dump...
tree
|
commitdiff
2015-01-24
ajreynol
Variable patterns only look at eligible terms. Minor...
tree
|
commitdiff
2015-01-24
ajreynol
Add --lte-restrict-inst-closure option. Push dt.size...
tree
|
commitdiff
2015-01-23
ajreynol
CEGQI fairness based on term height. Fix sygus-nf...
tree
|
commitdiff
2015-01-23
ajreynol
Rework inst-closure.
tree
|
commitdiff
2015-01-22
ajreynol
Narrow sygus search space based on NNF and rewriting...
tree
|
commitdiff
2015-01-22
ajreynol
Add option --lte-partial-inst. Remove inst-closure.
tree
|
commitdiff
2015-01-22
ajreynol
Do not drop patterns during boolean term rewriting...
tree
|
commitdiff
2015-01-21
ajreynol
Initial work on sygusNormalForm.
tree
|
commitdiff
2015-01-20
ajreynol
Mark datatypes as sygus. Add option to normalize sygus...
tree
|
commitdiff
2015-01-20
ajreynol
Handle miniscoping of conjunctions in synthesis propert...
tree
|
commitdiff
2015-01-16
ajreynol
Allow uninterpreted/defined functions in Sygus grammars...
tree
|
commitdiff
2015-01-16
ajreynol
Minor: Ensure indexed terms are in EE. Add support...
tree
|
commitdiff
2015-01-14
Morgan Deters
sygus input language and benchmark
tree
|
commitdiff
2015-01-07
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
tree
|
commitdiff
2014-12-28
ajreynol
Disable prenex by default when using fmf bound int...
tree
|
commitdiff
2014-12-27
Dejan Jovanovic
Adding an option to the equality engine constructor...
tree
|
commitdiff
2014-12-21
ajreynol
Add misc trigger options.
tree
|
commitdiff
2014-12-03
Kshitij Bansal
Merge branch 'master' of https://github.com/CVC4/CVC4
tree
|
commitdiff
2014-11-28
ajreynol
Synchronize conjecture generation with E-matching....
tree
|
commitdiff
2014-11-27
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
tree
|
commitdiff
2014-11-25
ajreynol
Fix bug in --term-db-mode=relevant with variable trigge...
tree
|
commitdiff
2014-11-21
ajreynol
Throw error when pattern is not list of terms.
tree
|
commitdiff
2014-11-21
ajreynol
Change default option to --inst-when=full-last-call...
tree
|
commitdiff
2014-11-18
ajreynol
Compute model basis only for fmf. Add another co-datat...
tree
|
commitdiff
2014-11-18
ajreynol
Add local theory extensions instantiation strategy...
tree
|
commitdiff
2014-11-17
Morgan Deters
New, uniform checkTime statistic for all theories ...
tree
|
commitdiff
2014-11-16
ajreynol
Add term db mode. Minor changes to quantifiers rewrite...
tree
|
commitdiff
2014-11-14
ajreynol
Be lazier to consider EQC in UF+cardinality solver...
tree
|
commitdiff
2014-11-13
Morgan Deters
Merge pull request #69 from mdeters/bug594
tree
|
commitdiff
2014-11-13
ajreynol
Remove two obsolete versions of MBQI.
tree
|
commitdiff
2014-11-13
ajreynol
More preparation for filtering relevant terms in TermDb.
tree
|
commitdiff
2014-11-11
Kshitij Bansal
Merge pull request #64 from mdeters/theorysets-hashset...
tree
|
commitdiff
2014-11-11
ajreynol
Work on synchronizing decision=justification and E...
tree
|
commitdiff
2014-11-10
Tianyi Liang
Merge pull request #63 from mdeters/theorystrings-hashs...
tree
|
commitdiff
2014-11-10
ajreynol
Do not eliminate variables only occurring in patterns...
tree
|
commitdiff
2014-11-10
Morgan Deters
Merge branch '1.4.x'
tree
|
commitdiff
2014-11-07
Morgan Deters
Merge branch '1.4.x'
tree
|
commitdiff
2014-11-07
Morgan Deters
Merge branch '1.4.x'
tree
|
commitdiff
2014-11-07
ajreynol
Enable --quant-cf by default. Fix bug in qcf for mixed...
tree
|
commitdiff
2014-11-07
Morgan Deters
Merge branch '1.4.x'
tree
|
commitdiff
2014-11-07
ajreynol
Properly distinguish which EQC to assign values in...
tree
|
commitdiff
2014-11-05
ajreynol
Fix model bug in --mbqi=fmc. Minor cleanup in datatypes.
tree
|
commitdiff
2014-11-05
Morgan Deters
Merge branch '1.4.x'
tree
|
commitdiff
2014-11-05
ajreynol
More work on datatypes theory combination: fix bug...
tree
|
commitdiff
2014-11-01
ajreynol
Fix cegqi for synthesis without syntax.
tree
|
commitdiff
2014-11-01
ajreynol
Fix some mistakes in datatypes theory combination,...
tree
|
commitdiff
2014-10-31
ajreynol
Do not allow duplication of function definitions. ...
tree
|
commitdiff
2014-10-28
ajreynol
Preprocessing step for finding finite runs of well...
tree
|
commitdiff
2014-10-28
ajreynol
Initial infrastructure for function definition quantifi...
tree
|
commitdiff
2014-10-28
ajreynol
Improve stats in conjecture generator, minor cleanup.
tree
|
commitdiff
2014-10-25
ajreynol
Minor fix for --user-pat=resort
tree
|
commitdiff
2014-10-24
Morgan Deters
Fix typo.
tree
|
commitdiff
2014-10-24
ajreynol
Add --user-pat=resort. Minor cleanup of options.
tree
|
commitdiff
2014-10-18
ajreynol
Fix for bounded integers when incremental, fixes bug...
tree
|
commitdiff
2014-10-17
Morgan Deters
Merge branch '1.4.x'
tree
|
commitdiff
2014-10-16
ajreynol
Make --user-pat=trust default. Fix a few warnings...
tree
|
commitdiff
2014-10-16
Morgan Deters
Merge branch '1.4.x'
tree
|
commitdiff
2014-10-16
ajreynol
Add dt.size to datatypes theory. Add option for fairne...
tree
|
commitdiff
next