projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Fixes to quantifiers rewriter to prevent miniscoping nested quantifiers. Minor fixes...
[cvc5.git]
/
src
/
theory
/
quantifiers
/
options
2014-05-08
Andrew Reynolds
Fixes to quantifiers rewriter to prevent miniscoping...
blob
|
commitdiff
|
raw
2014-05-02
Andrew Reynolds
Add option --dt-stc-ind for strengthening skolemization...
blob
|
commitdiff
|
raw
|
diff to current
2014-05-01
Kshitij Bansal
Merge remote-tracking branch 'upstream/master' into...
blob
|
commitdiff
|
raw
|
diff to current
2014-04-30
Tim King
T-entailment work, and QCF (quant conflict find) work...
blob
|
commitdiff
|
raw
|
diff to current
2014-04-28
Kshitij Bansal
Merge remote-tracking branch 'upstream/master' into...
blob
|
commitdiff
|
raw
|
diff to current
2014-04-24
Andrew Reynolds
Add --inst-max-level=N option for Kshitij. Support...
blob
|
commitdiff
|
raw
|
diff to current
2014-04-17
Morgan Deters
Allow fmf-bound-int to be set with set-option and via...
blob
|
commitdiff
|
raw
|
diff to current
2014-04-10
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2014-04-10
Andrew Reynolds
Add support for cardinality constraints logic UFC....
blob
|
commitdiff
|
raw
|
diff to current
2014-04-01
Tim King
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-03-26
Morgan Deters
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-03-21
Kshitij Bansal
Merge pull request #22 from kbansal/sets-model
blob
|
commitdiff
|
raw
|
diff to current
2014-03-12
Andrew Reynolds
Work on array pf signature, add working example. Add...
blob
|
commitdiff
|
raw
|
diff to current
2014-03-11
Morgan Deters
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-03-11
Morgan Deters
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-03-11
Andrew Reynolds
Initial refactor of rewrite rules, make theory_rewriter...
blob
|
commitdiff
|
raw
|
diff to current
2014-03-10
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2014-03-08
Tim King
Merge remote-tracking branch 'CVC4root/master'
blob
|
commitdiff
|
raw
|
diff to current
2014-03-08
Morgan Deters
Remove --ite-remove-quant; support pulling ground ITEs...
blob
|
commitdiff
|
raw
|
diff to current
2014-03-07
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2014-03-04
Morgan Deters
Don't theory-preprocess under quantifiers; but DO theor...
blob
|
commitdiff
|
raw
|
diff to current
2014-03-01
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2014-02-27
Andrew Reynolds
Bug fix for QCF algorithm, was missing instantiations...
blob
|
commitdiff
|
raw
|
diff to current
2014-02-26
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2014-02-25
Andrew Reynolds
Add options --full-saturate-quant and --mbqi=trust...
blob
|
commitdiff
|
raw
|
diff to current
2014-02-21
Morgan Deters
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-02-21
Morgan Deters
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-02-20
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2014-02-20
Andrew Reynolds
Fix ite and iff handling in QCF. Add option for heuris...
blob
|
commitdiff
|
raw
|
diff to current
2014-02-19
Tim King
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-01-27
Morgan Deters
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-01-26
Andrew Reynolds
More optimization of QCF. Fixed InstMatchTrie for...
blob
|
commitdiff
|
raw
|
diff to current
2014-01-24
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2014-01-24
Andrew Reynolds
Simplify the QCF algorithm by more aggressive flattenin...
blob
|
commitdiff
|
raw
|
diff to current
2014-01-22
Tianyi Liang
Smarter options, but still have a bug
blob
|
commitdiff
|
raw
|
diff to current
2014-01-21
Tianyi Liang
Smarter options, but still have a bug
blob
|
commitdiff
|
raw
|
diff to current
2014-01-18
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2014-01-18
Morgan Deters
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-01-17
Andrew Reynolds
More optimizations for quantifiers conflict find. ...
blob
|
commitdiff
|
raw
|
diff to current
2014-01-17
Kshitij Bansal
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-01-10
Andrew Reynolds
Add stats to quantifiers conflict find. Added option...
blob
|
commitdiff
|
raw
|
diff to current
2014-01-10
Andrew Reynolds
Add new method --quant-cf for finding conflicts eagerly...
blob
|
commitdiff
|
raw
|
diff to current
2014-01-09
Morgan Deters
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-01-08
Morgan Deters
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-01-04
Andrew Reynolds
Removing and consolidating options for uf-ss and quanti...
blob
|
commitdiff
|
raw
|
diff to current
2014-01-03
Andrew Reynolds
Added support for proof production in Equality Engine...
blob
|
commitdiff
|
raw
|
diff to current
2013-11-06
Andrew Reynolds
Bug fixes for bounded integer quantification. Current...
blob
|
commitdiff
|
raw
|
diff to current
2013-11-06
Andrew Reynolds
Bug fixes for bounded integer quantification. Current...
blob
|
commitdiff
|
raw
|
diff to current
2013-10-07
Liana Hadarean
merged golden
blob
|
commitdiff
|
raw
|
diff to current
2013-10-07
Andrew Reynolds
Multiple fixes for datatypes theory solver: add support...
blob
|
commitdiff
|
raw
|
diff to current
2013-09-30
Liana Hadarean
merged golden
blob
|
commitdiff
|
raw
|
diff to current
2013-09-15
Andrew Reynolds
Change default option of simple ite lifting within...
blob
|
commitdiff
|
raw
|
diff to current
2013-08-26
Kshitij Bansal
Merge branch '1.2.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-07-22
Andrew Reynolds
Add option --cbqi-recurse.
blob
|
commitdiff
|
raw
|
diff to current
2013-06-28
Andrew Reynolds
More bug fixes for interval models.
blob
|
commitdiff
|
raw
|
diff to current
2013-06-25
Morgan Deters
Merge branch '1.2.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-06-25
Andrew Reynolds
Refactoring of model engine to separate individual...
blob
|
commitdiff
|
raw
|
diff to current
2013-06-24
Andrew Reynolds
Add options for symmetry breaking in uf+ss totality...
blob
|
commitdiff
|
raw
|
diff to current
2013-06-19
Morgan Deters
Merge branch '1.2.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-06-17
Andrew Reynolds
Make --var-elim-quant true by default. Add rewrite...
blob
|
commitdiff
|
raw
|
diff to current
2013-06-04
Morgan Deters
Merge branch '1.2.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-06-03
Morgan Deters
Merge tag 'casc24'
blob
|
commitdiff
|
raw
|
diff to current
2013-05-29
Morgan Deters
Merge branch '1.2.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-05-22
Andrew Reynolds
Merge branch 'master' of https://github.com/CVC4/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2013-05-22
Andrew Reynolds
Significant work on bounded integer quantification...
blob
|
commitdiff
|
raw
|
diff to current
2013-05-21
Morgan Deters
Merge branch '1.2.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-05-21
Morgan Deters
Merge branch '1.2.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-05-20
Morgan Deters
Merge branch '1.2.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-05-10
Morgan Deters
Add documentation for --disable-fmf-inst-gen, which...
blob
|
commitdiff
|
raw
|
diff to current
2013-05-10
Andrew Reynolds
Add simplification option --fo-prop-quant. Add model...
blob
|
commitdiff
|
raw
|
diff to current
2013-05-09
Kshitij Bansal
Merge branch 'master' of ssh://github.com/CVC4/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2013-05-09
Andrew Reynolds
Add new method for checking candidate models, --fmf...
blob
|
commitdiff
|
raw
|
diff to current
2013-05-03
Tim King
Merging branch 'soiquickexplain'.
blob
|
commitdiff
|
raw
|
diff to current
2013-05-03
Tim King
Merge branch 'fcexplanations'
blob
|
commitdiff
|
raw
|
diff to current
2013-04-30
lianah
fixed merge conflicts
blob
|
commitdiff
|
raw
|
diff to current
2013-04-30
Andrew Reynolds
Add option in quantifiers for clause splitting
blob
|
commitdiff
|
raw
|
diff to current
2013-03-20
Liana Hadarean
merged master with dejan's constant evaluating equality...
blob
|
commitdiff
|
raw
|
diff to current
2013-03-15
Morgan Deters
Merge branch '1.0.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-03-15
Andrew Reynolds
changed default option for quantifier instantiation
blob
|
commitdiff
|
raw
|
diff to current
2013-03-14
Morgan Deters
Merge branch '1.0.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-03-13
lianah
post failed attempts at getting the incremental solver...
blob
|
commitdiff
|
raw
|
diff to current
2013-03-11
Andrew Reynolds
ite removal option for quantifiers --ite-remove-quant...
blob
|
commitdiff
|
raw
|
diff to current
2013-03-06
Andrew Reynolds
fixed two bugs for the new E-matching implementation...
blob
|
commitdiff
|
raw
|
diff to current
2013-03-05
Morgan Deters
Merge branch '1.0.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-03-01
Morgan Deters
Merge branch '1.0.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-02-26
lianah
Merge branch '1.0.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-02-24
Andrew Reynolds
added option --model-u-dt-enum for outputting uninterpr...
blob
|
commitdiff
|
raw
|
diff to current
2013-02-17
Kshitij Bansal
Merge branch '1.0.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-02-16
Morgan Deters
Merge branch '1.0.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-02-15
Kshitij Bansal
Merge branch '1.0.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-02-15
Kshitij Bansal
Merge branch '1.0.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-02-15
Morgan Deters
Merge branch '1.0.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-02-15
Tim King
Merge branch '1.0.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-02-08
Morgan Deters
Merge branch '1.0.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-02-05
Morgan Deters
Merge branch '1.0.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-02-05
Kshitij Bansal
Merge remote-tracking branch 'origin/1.0.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-02-05
Morgan Deters
Merge branch '1.0.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-02-04
Morgan Deters
Merge branch '1.0.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-02-04
Morgan Deters
Merge branch '1.0.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-02-04
Andrew Reynolds
Model no longer adds subterms of quantifiers to equalit...
blob
|
commitdiff
|
raw
|
diff to current
next