| 2013-05-14 |
Andrew Reynolds | Update casc24-fnt run script. Add casc24-fof run script.
|
commit | commitdiff | tree |
| 2013-05-14 |
Andrew Reynolds | Add support for quantifier patterns in smt2 printer.
|
commit | commitdiff | tree |
| 2013-05-14 |
Andrew Reynolds | Refactoring to separate old and new model building...
|
commit | commitdiff | tree |
| 2013-05-11 |
Andrew Reynolds | Preliminary version of finite model finding over bounded...
|
commit | commitdiff | tree |
| 2013-05-10 |
Andrew Reynolds | Update casc run script. Work on compliance for SZS...
|
commit | commitdiff | tree |
| 2013-05-10 |
Andrew Reynolds | Add simplification option --fo-prop-quant. Add model...
|
commit | commitdiff | tree |
| 2013-05-09 |
Andrew Reynolds | Add new method for checking candidate models, --fmf...
|
commit | commitdiff | tree |
| 2013-04-30 |
Andrew Reynolds | Add option in quantifiers for clause splitting
|
commit | commitdiff | tree |
| 2013-04-03 |
Andrew Reynolds | abort quantifiers check if master equality engine is...
|
commit | commitdiff | tree |
| 2013-03-30 |
Andrew Reynolds | do simple ite rewriting within quantifiers
|
commit | commitdiff | tree |
| 2013-03-15 |
Andrew Reynolds | changed default option for quantifier instantiation
|
commit | commitdiff | tree |
| 2013-03-11 |
Andrew Reynolds | ite removal option for quantifiers --ite-remove-quant...
|
commit | commitdiff | tree |
| 2013-03-06 |
Andrew Reynolds | fixed two bugs for the new E-matching implementation...
|
commit | commitdiff | tree |
| 2013-02-24 |
Andrew Reynolds | added option --model-u-dt-enum for outputting uninterpreted...
|
commit | commitdiff | tree |
| 2013-02-05 |
Andrew Reynolds | More improvements for E-matching
|
commit | commitdiff | tree |
| 2013-02-04 |
Andrew Reynolds | Model no longer adds subterms of quantifiers to equality...
|
commit | commitdiff | tree |
| 2013-01-29 |
Andrew Reynolds | currently disabling bug486 regression. we need to...
|
commit | commitdiff | tree |
| 2013-01-29 |
Andrew Reynolds | fix for finite model finding caused by new collectModelInfo...
|
commit | commitdiff | tree |
| 2013-01-28 |
Andrew Reynolds | made QuantifiersEngine::d_inst_match_trie and QuantifiersEng...
|
commit | commitdiff | tree |
| 2013-01-27 |
Andrew Reynolds | some fixes for Intel benchmarks regarding quantifiers...
|
commit | commitdiff | tree |
| 2012-12-11 |
Andrew Reynolds | adding cache for preprocessing datatypes terms to fix...
|
commit | commitdiff | tree |
| 2012-12-01 |
Andrew Reynolds | drastic simplification of quantifiers code regarding...
|
commit | commitdiff | tree |
| 2012-11-30 |
Andrew Reynolds | quantifiers now uses master equality engine, preparation...
|
commit | commitdiff | tree |
| 2012-11-30 |
Andrew Reynolds | parametric datatypes fix related to non-ascribed type...
|
commit | commitdiff | tree |
| 2012-11-29 |
Andrew Reynolds | require type ascriptions for parametric datatype constructor...
|
commit | commitdiff | tree |
| 2012-11-29 |
Andrew Reynolds | fixes bug 438, incorporate subtypes into type unification...
|
commit | commitdiff | tree |
| 2012-11-18 |
Andrew Reynolds | support for quantifiers macros, bug fix for bug 454...
|
commit | commitdiff | tree |
| 2012-11-14 |
Andrew Reynolds | replaced all static member data from rewrite rule triggers...
|
commit | commitdiff | tree |
| 2012-11-13 |
Andrew Reynolds | refactoring of quantifiers rewriter based on code review...
|
commit | commitdiff | tree |
| 2012-11-12 |
Andrew Reynolds | minor bug fixes for quantifiers, added sort inference...
|
commit | commitdiff | tree |
| 2012-11-08 |
Andrew Reynolds | added support for parametric datatypes in smt2 parser...
|
commit | commitdiff | tree |
| 2012-11-02 |
Andrew Reynolds | more minor updates to inst gen and representative selection...
|
commit | commitdiff | tree |
| 2012-10-31 |
Andrew Reynolds | cleaning up some of the equality query stuff, implemented...
|
commit | commitdiff | tree |
| 2012-10-29 |
Andrew Reynolds | more updates and minor bug fixes for fmf/inst-gen quantifier...
|
commit | commitdiff | tree |
| 2012-10-26 |
Andrew Reynolds | bug fix for parametric datatypes, previously datatypes...
|
commit | commitdiff | tree |
| 2012-10-26 |
Andrew Reynolds | fixed bug in datatypes decision procedure enforcing...
|
commit | commitdiff | tree |
| 2012-10-24 |
Andrew Reynolds | fixed assertion failures in efficient e-matching
|
commit | commitdiff | tree |
| 2012-10-24 |
Andrew Reynolds | efficient e-matching now specific to rewrite rules
|
commit | commitdiff | tree |
| 2012-10-23 |
Andrew Reynolds | more major cleanup of quantifiers code, separating...
|
commit | commitdiff | tree |
| 2012-10-23 |
Andrew Reynolds | fixed problem with datatypes giving incorrect explanations...
|
commit | commitdiff | tree |
| 2012-10-23 |
Andrew Reynolds | more updates to inst gen: fixed partial instantiations...
|
commit | commitdiff | tree |
| 2012-10-17 |
Andrew Reynolds | first working version of new inst-gen-style quantifier...
|
commit | commitdiff | tree |
| 2012-10-16 |
Andrew Reynolds | more cleanup of quantifiers code
|
commit | commitdiff | tree |
| 2012-10-16 |
Andrew Reynolds | first draft of new inst gen method (still with bugs...
|
commit | commitdiff | tree |
| 2012-10-10 |
Andrew Reynolds | cleanup up some static data members in the quantifiers...
|
commit | commitdiff | tree |
| 2012-10-09 |
Andrew Reynolds | fixed datatypes rewriter to detect clashes between...
|
commit | commitdiff | tree |
| 2012-10-09 |
Andrew Reynolds | made datatypes rewrite incorrect selectors to ground...
|
commit | commitdiff | tree |
| 2012-10-03 |
Andrew Reynolds | minor fix for mbqi in finite model finding
|
commit | commitdiff | tree |
| 2012-10-01 |
Andrew Reynolds | initial draft of skolemization during pre-processing...
|
commit | commitdiff | tree |
| 2012-09-26 |
Andrew Reynolds | updates to model generation : do not modify equality...
|
commit | commitdiff | tree |
| 2012-09-17 |
Andrew Reynolds | minor fix for models, added simple cliques option for...
|
commit | commitdiff | tree |
| 2012-09-16 |
Andrew Reynolds | store values returned by get-value in TheoryModel:...
|
commit | commitdiff | tree |
| 2012-09-13 |
Andrew Reynolds | ensure that get-value and get-model are consistent...
|
commit | commitdiff | tree |
| 2012-09-11 |
Andrew Reynolds | added getCardinality to model
|
commit | commitdiff | tree |
| 2012-09-10 |
Andrew Reynolds | modified getValue to return Expr instead of Node
|
commit | commitdiff | tree |
| 2012-09-03 |
Andrew Reynolds | minor cleanup leftover from fmf-devel
|
commit | commitdiff | tree |
| 2012-08-31 |
Andrew Reynolds | merge from fmf-devel branch. more updates to models...
|
commit | commitdiff | tree |
| 2012-07-27 |
Andrew Reynolds | removing unecessary files
|
commit | commitdiff | tree |
| 2012-07-27 |
Andrew Reynolds | merging fmf-devel branch, includes refactored datatype...
|
commit | commitdiff | tree |
| 2012-07-17 |
Andrew Reynolds | minor fix to prevent getValue from returning null
|
commit | commitdiff | tree |
| 2012-07-12 |
Andrew Reynolds | removing readme from fmf-devel
|
commit | commitdiff | tree |
| 2012-07-12 |
Andrew Reynolds | merged fmf-devel branch, includes support for SMT2...
|
commit | commitdiff | tree |
| 2012-06-18 |
Andrew Reynolds | fixed smt version 1 parser for quantifiers
|
commit | commitdiff | tree |
| 2012-02-04 |
Andrew Reynolds | support for isWellFounded/mkGroundTerm on uninterpretted...
|
commit | commitdiff | tree |
| 2012-01-17 |
Andrew Reynolds | updates to smt2 parser to support datatypes, minor...
|
commit | commitdiff | tree |
| 2011-12-14 |
Andrew Reynolds | added minor documentation for parametric datatypes...
|
commit | commitdiff | tree |
| 2011-06-03 |
Andrew Reynolds | fixed various bugs related to ambiguous parametric...
|
commit | commitdiff | tree |
| 2011-06-02 |
Andrew Reynolds | added (temporary) support for ensuring that all ambiguously...
|
commit | commitdiff | tree |
| 2011-05-13 |
Andrew Reynolds | added support for parametric datatypes, updated cvc...
|
commit | commitdiff | tree |
| 2011-05-06 |
Andrew Reynolds | added 10 benchmarks to regress/regress0/datatypes from...
|
commit | commitdiff | tree |
| 2011-05-06 |
Andrew Reynolds | significant revisions/improvements to code for theory...
|
commit | commitdiff | tree |
| 2011-05-02 |
Andrew Reynolds | minor updates to exp manager, fixed 32bit vs 64bit...
|
commit | commitdiff | tree |
| 2011-04-29 |
Andrew Reynolds | refactoring to datatypes theory, added working prototype...
|
commit | commitdiff | tree |
| 2011-04-28 |
Andrew Reynolds | more fixes/improvements to datatypes theory and transitive...
|
commit | commitdiff | tree |
| 2011-04-27 |
Andrew Reynolds | cleaned up some of the hacks in the datatypes theory...
|
commit | commitdiff | tree |
| 2011-04-22 |
Andrew Reynolds | added fixes for datatype theory solver to account for...
|
commit | commitdiff | tree |
|
projects / cvc5.git / search