git.libre-soc.org Git - cvc5.git/history - src/theory/quantifiers/full_model

[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

RSS Atom