Age | Commit message (Expand) | Author |
2012-11-12 | minor bug fixes for quantifiers, added sort inference module (not ready to be... | Andrew Reynolds |
2012-11-10 | Fix to quantifier rewritting not being idempotent. See bug 441. | Tim King |
2012-11-07 | * Type ascription bug fixed (resolves bug 432), but there are others I discov... | Morgan Deters |
2012-11-02 | more minor updates to inst gen and representative selection, clean up of equa... | Andrew Reynolds |
2012-10-31 | cleaning up some of the equality query stuff, implemented a new representativ... | Andrew Reynolds |
2012-10-29 | more updates and minor bug fixes for fmf/inst-gen quantifier instantiation | Andrew Reynolds |
2012-10-24 | efficient e-matching now specific to rewrite rules | Andrew Reynolds |
2012-10-23 | more major cleanup of quantifiers code, separating rewrite-rules-specific cod... | Andrew Reynolds |
2012-10-23 | more updates to inst gen: fixed partial instantiations, recognize duplicate d... | Andrew Reynolds |
2012-10-19 | --fallback-sequential / --no-fallback-sequential option | Kshitij Bansal |
2012-10-17 | first working version of new inst-gen-style quantifier instantiation techniqu... | Andrew Reynolds |
2012-10-16 | more cleanup of quantifiers code | Andrew Reynolds |
2012-10-16 | first draft of new inst gen method (still with bugs), some cleanup of quantif... | Andrew Reynolds |
2012-10-11 | Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it's | Morgan Deters |
2012-10-10 | cleanup up some static data members in the quantifiers code | Andrew Reynolds |
2012-10-09 | fixed datatypes rewriter to detect clashes between non-datatype subfields. c... | Andrew Reynolds |
2012-10-05 | fix \file | Morgan Deters |
2012-10-05 | Bug-related: | Morgan Deters |
2012-10-04 | disable model-generation by default in cvc3 compatibility layer. should fix ... | Morgan Deters |
2012-10-03 | minor fix for mbqi in finite model finding | Andrew Reynolds |
2012-10-01 | initial draft of skolemization during pre-processing, made simple cliques the... | Andrew Reynolds |
2012-09-28 | rename Assert.h/Assert.cpp to cvc4_assert.h/cvc4_assert.cpp -- we need to mak... | Morgan Deters |
2012-09-26 | updates to model generation : do not modify equality engine during getValue, ... | Andrew Reynolds |
2012-09-22 | Separate public-facing and internal-facing interfaces to Statistics. | Morgan Deters |
2012-09-19 | General subscriber infrastructure for NodeManager, as discussed in the | Morgan Deters |
2012-09-13 | ensure that get-value and get-model are consistent, rewrite function value bo... | Andrew Reynolds |
2012-09-10 | modified getValue to return Expr instead of Node | Andrew Reynolds |
2012-08-31 | merge from fmf-devel branch. more updates to models: now with collectModelIn... | Andrew Reynolds |
2012-08-27 | * Reversing commit r4258 (which disabled failing regressions). Fixed the pro... | Morgan Deters |
2012-08-24 | * disallow internal uses of mkVar() (you have to mkSkolem()) | Morgan Deters |
2012-08-20 | remove duplicate function TheoryEngine::getTheory(TheoryId). It was a duplic... | Morgan Deters |
2012-08-20 | minor cleanup | Morgan Deters |
2012-08-19 | 1. Fix for inst_match.cpp to allow compilation on fedora | Clark Barrett |
2012-08-16 | Replace propagateAsDecision() with Theory::getNextDecisionRequest(): | Morgan Deters |
2012-08-03 | fix uses of getMetaKind() from outside the expr package. (they now use isCon... | Morgan Deters |
2012-07-31 | Moving some instantiation-related stuff from src/theory to src/theory/quantif... | Morgan Deters |
2012-07-31 | Options merge. This commit: | Morgan Deters |
2012-07-27 | Minor cleanup after today's commits: | Morgan Deters |
2012-07-27 | merging fmf-devel branch, includes refactored datatype theory, updates to mod... | Andrew Reynolds |
2012-07-27 | Merge quantifiers2-trunk: | François Bobot |
2012-07-12 | merged fmf-devel branch, includes support for SMT2 command get-value and (ext... | Andrew Reynolds |
2012-07-08 | another signed-ness warning fix for newer GCC | Morgan Deters |
2012-07-07 | Various fixes to documentation---typos, some incomplete documentation fixed, ... | Morgan Deters |
2012-06-14 | fix quantifier non-bug | Kshitij Bansal |
2012-06-14 | * removing rewriteEquality from the rewriter | Dejan Jovanović |
2012-06-11 | mark a quantifiers global var as "static" so we can find it easier later | Morgan Deters |
2012-06-11 | Merge from quantifiers2-trunkmerge branch. | Morgan Deters |