Age | Commit message (Expand) | Author |
2017-10-09 | Split term database (#1206) | Andrew Reynolds |
2017-10-05 | Ho model (#1120) | Andrew Reynolds |
2017-07-07 | Update copyright headers. | Mathias Preiner |
2017-04-24 | Fixes and simplifications for fmf mbqi. | ajreynol |
2017-03-24 | Add some regressions. Minor. | ajreynol |
2017-03-24 | Refactor model building for quantifiers to be a single pass, simplification. ... | ajreynol |
2016-12-07 | Refactoring, generalization of bounded inference module. Simplification of re... | ajreynol |
2016-12-02 | Refactor preprocessing of models in fmf. Fix options --fmf-empty-sorts and --... | ajreynol |
2016-10-13 | Revert "Merge branch 'origin' of https://github.com/CVC4/CVC4.git" | Tim King |
2016-10-11 | Merge branch 'origin' of https://github.com/CVC4/CVC4.git | Paul Meng |
2016-09-15 | Refactor setIncomplete in quantifiers. | ajreynol |
2016-08-24 | Merge remote-tracking branch 'origin/master' | PaulMeng |
2016-08-15 | Enable bounded set membership with --fmf-bound. Map to term models for bounde... | ajreynol |
2016-07-05 | Merge branch 'master' of https://github.com/CVC4/CVC4.git | PaulMeng |
2016-06-01 | Initial infrastructure for bounded set quantification (disabled). Refactoring... | ajreynol |
2016-05-02 | Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, ... | ajreynol |
2016-04-20 | update from the master | PaulMeng |
2016-04-13 | Minor improvements for alpha equivalence and partial quantifier elimination i... | ajreynol |
2016-04-12 | Optimizations for QCF to check relevant domain of variable argument positions... | ajreynol |
2016-04-10 | More work on instantiation propagation. Enable external filtering of instanti... | ajreynol |
2016-04-03 | Updating the copyright headers and scripts. | Tim King |
2016-03-16 | Change internal representative selection for finite domains that do not invol... | ajreynol |
2016-03-07 | Minor change to F-Length inference in strings. No internal tracking of cardin... | ajreynol |
2016-02-23 | Fix term database for non-equal, congruent terms in master equality engine. D... | ajreynol |
2016-02-11 | More aggressive conditional rewriting for quantified formulas. Bug fix set in... | ajreynol |
2016-02-08 | Updates related to finite model finding and (co)datatypes. Bug fix enumerator... | ajreynol |
2016-01-20 | Fix bug in fmc mbqi where modelscomputed for mbqi could involve non-constant ... | ajreynol |
2015-12-14 | Refactoring Options Handler & Library Cycle Breaking | Tim King |
2015-04-28 | Fix smt2 printing of fun-def. Simplification of mbqi interface. | ajreynol |
2015-04-26 | Bug fixes and improvements for mbqi with theory symbols, TheoryModel fullMode... | ajreynol |
2015-04-21 | Fix bug in fmf mbqi=fmc with arrays. Add two datatypes regressions. | ajreynol |
2014-10-13 | Model building into quantifiers engine. Simplify axiom-inst mode. | ajreynol |
2014-07-26 | Minor bug fix for exhaustive instantiation in model_engine. | ajreynol |
2014-07-19 | Minor fix for explanations for co-datatypes. Bug fix for explanations in FMF... | ajreynol |
2014-07-01 | Update copyrights. | Morgan Deters |
2014-05-12 | Minor updates/fix to --cbqi-recurse | Andrew Reynolds |
2014-05-11 | More preparation for CASC proofs. Minor fix for sort inference (rewrite new ... | Andrew Reynolds |
2014-04-28 | Merge remote-tracking branch 'upstream/master' into sets | Kshitij Bansal |
2014-04-17 | simplify mkSkolem naming system: don't use $$ | Kshitij Bansal |
2014-04-14 | Fix bug in mbqi=fmc handling theory symbols. Fix mbqi=fmc models (Bug 557). ... | Andrew Reynolds |
2014-03-11 | Initial refactor of rewrite rules, make theory_rewriterules empty theory. Pu... | Andrew Reynolds |
2014-01-27 | More optimization of QCF and instantiation caching. Fix CDInstMatchTrie. | Andrew Reynolds |
2014-01-03 | Removing and consolidating options for uf-ss and quantifiers. Bug fix for in... | Andrew Reynolds |
2014-01-03 | Added support for proof production in Equality Engine. Cleaned up existing p... | Andrew Reynolds |
2013-12-05 | Update copyrights, add missing file-level documentation; fix perms. | Morgan Deters |
2013-11-06 | Bug fixes for bounded integer quantification. Current best strategy is to tu... | Andrew Reynolds |
2013-09-27 | Add new symmetry breaking technique for finite model finding. Improvements t... | Andrew Reynolds |
2013-09-15 | Change default option of simple ite lifting within quantifier bodies. add so... | Andrew Reynolds |
2013-09-13 | Documentation fixes, some code typo fixes, file perms, other minor things. | Morgan Deters |
2013-08-13 | Minor cleanup. | Morgan Deters |