projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Minor improvements for alpha equivalence and partial quantifier elimination in increm...
[cvc5.git]
/
src
/
theory
/
quantifiers
/
full_model_check.cpp
2016-04-13
ajreynol
Minor improvements for alpha equivalence and partial...
blob
|
commitdiff
|
raw
2016-04-12
ajreynol
Optimizations for QCF to check relevant domain of varia...
blob
|
commitdiff
|
raw
|
diff to current
2016-04-10
ajreynol
More work on instantiation propagation. Enable external...
blob
|
commitdiff
|
raw
|
diff to current
2016-04-09
Guy
Merge branch 'master' of https://github.com/CVC4/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2016-04-04
Tim King
Updating the copyright headers and scripts.
blob
|
commitdiff
|
raw
|
diff to current
2016-03-16
ajreynol
Change internal representative selection for finite...
blob
|
commitdiff
|
raw
|
diff to current
2016-03-07
ajreynol
Minor change to F-Length inference in strings. No inter...
blob
|
commitdiff
|
raw
|
diff to current
2016-02-23
ajreynol
Fix term database for non-equal, congruent terms in...
blob
|
commitdiff
|
raw
|
diff to current
2016-02-11
ajreynol
More aggressive conditional rewriting for quantified...
blob
|
commitdiff
|
raw
|
diff to current
2016-02-08
ajreynol
Updates related to finite model finding and (co)datatyp...
blob
|
commitdiff
|
raw
|
diff to current
2016-01-20
ajreynol
Fix bug in fmc mbqi where modelscomputed for mbqi could...
blob
|
commitdiff
|
raw
|
diff to current
2015-12-15
Tim King
Refactoring Options Handler & Library Cycle Breaking
blob
|
commitdiff
|
raw
|
diff to current
2015-05-12
barrettcw
Merge pull request #74 from finnhaedicke/namespace_minisat
blob
|
commitdiff
|
raw
|
diff to current
2015-04-28
ajreynol
Fix smt2 printing of fun-def. Simplification of mbqi...
blob
|
commitdiff
|
raw
|
diff to current
2015-04-26
ajreynol
Bug fixes and improvements for mbqi with theory symbols...
blob
|
commitdiff
|
raw
|
diff to current
2015-04-22
Kshitij Bansal
Merge pull request #73 from kbansal/parser-dont-tokenize
blob
|
commitdiff
|
raw
|
diff to current
2015-04-21
ajreynol
Fix bug in fmf mbqi=fmc with arrays. Add two datatypes...
blob
|
commitdiff
|
raw
|
diff to current
2014-11-10
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-11-07
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-11-07
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-11-07
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-11-05
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-10-17
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-10-16
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-10-13
ajreynol
Model building into quantifiers engine. Simplify axiom...
blob
|
commitdiff
|
raw
|
diff to current
2014-10-11
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-10-10
Kshitij Bansal
Merge remote-tracking branch 'origin/1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-10-09
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-10-07
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-10-06
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-10-06
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-10-03
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-10-03
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-10-02
Morgan Deters
Merge branch '1.4.x'.
blob
|
commitdiff
|
raw
|
diff to current
2014-09-30
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-09-27
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-09-26
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-09-17
Kshitij Bansal
Merge branch '1.4.x' while ignoring commit 8d5eb49.
blob
|
commitdiff
|
raw
|
diff to current
2014-09-17
Kshitij Bansal
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-08-22
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-08-22
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-08-19
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-08-18
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-07-25
ajreynol
Minor bug fix for exhaustive instantiation in model_engine.
blob
|
commitdiff
|
raw
|
diff to current
2014-07-19
ajreynol
Minor fix for explanations for co-datatypes. Bug fix...
blob
|
commitdiff
|
raw
|
diff to current
2014-07-10
Kshitij Bansal
Merge remote-tracking branch 'origin/master' into segfa...
blob
|
commitdiff
|
raw
|
diff to current
2014-07-01
Morgan Deters
Update copyrights.
blob
|
commitdiff
|
raw
|
diff to current
2014-05-13
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2014-05-12
Andrew Reynolds
Minor updates/fix to --cbqi-recurse
blob
|
commitdiff
|
raw
|
diff to current
2014-05-12
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2014-05-11
Andrew Reynolds
More preparation for CASC proofs. Minor fix for sort...
blob
|
commitdiff
|
raw
|
diff to current
2014-04-28
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2014-04-28
Kshitij Bansal
Merge pull request #25 from kbansal/sets
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-17
Kshitij Bansal
simplify mkSkolem naming system: don't use $$
blob
|
commitdiff
|
raw
|
diff to current
2014-04-14
Andrew Reynolds
Fix bug in mbqi=fmc handling theory symbols. Fix mbqi...
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-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-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-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-27
Andrew Reynolds
More optimization of QCF and instantiation caching...
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
Kshitij Bansal
Merge branch '1.3.x'
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-12-05
Morgan Deters
Update copyrights, add missing file-level documentation...
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-09-30
Liana Hadarean
merged golden
blob
|
commitdiff
|
raw
|
diff to current
2013-09-27
Morgan Deters
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2013-09-27
Andrew Reynolds
Add new symmetry breaking technique for finite model...
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-09-13
Morgan Deters
Documentation fixes, some code typo fixes, file perms...
blob
|
commitdiff
|
raw
|
diff to current
2013-08-26
Kshitij Bansal
Merge branch '1.2.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-08-13
Morgan Deters
Minor cleanup.
blob
|
commitdiff
|
raw
|
diff to current
2013-08-13
Andrew Reynolds
Minor fixes for --fmf-fmc for quantifiers containing...
blob
|
commitdiff
|
raw
|
diff to current
2013-07-29
Morgan Deters
Fix numerous compiler warnings on various platforms
blob
|
commitdiff
|
raw
|
diff to current
2013-07-22
Andrew Reynolds
Bug fix for --fmf-fmc for non-uninterpreted sort quanti...
blob
|
commitdiff
|
raw
|
diff to current
2013-07-02
Andrew Reynolds
Minor fixes for bounded integers, rewrite engine.
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-26
Andrew Reynolds
Add support for interval models in bounded integers...
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-05
Andrew Reynolds
Fix bug in --fmf-fmc for producing models of functions...
blob
|
commitdiff
|
raw
|
diff to current
2013-06-04
Morgan Deters
Merge branch '1.2.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-06-04
Andrew Reynolds
Add partial support for MBQI with arrays when using...
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-23
Andrew Reynolds
Refactoring to prepare for MBQI with integer quantifica...
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
next