summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
AgeCommit message (Expand)Author
2012-11-14replaced all static member data from rewrite rule triggers, added infrastruct...Andrew Reynolds
2012-11-13refactoring of quantifiers rewriter based on code review from yesterday, refa...Andrew Reynolds
2012-11-12minor bug fixes for quantifiers, added sort inference module (not ready to be...Andrew Reynolds
2012-11-10Fix 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-02more minor updates to inst gen and representative selection, clean up of equa...Andrew Reynolds
2012-10-31cleaning up some of the equality query stuff, implemented a new representativ...Andrew Reynolds
2012-10-29more updates and minor bug fixes for fmf/inst-gen quantifier instantiationAndrew Reynolds
2012-10-24efficient e-matching now specific to rewrite rulesAndrew Reynolds
2012-10-23more major cleanup of quantifiers code, separating rewrite-rules-specific cod...Andrew Reynolds
2012-10-23more updates to inst gen: fixed partial instantiations, recognize duplicate d...Andrew Reynolds
2012-10-19--fallback-sequential / --no-fallback-sequential optionKshitij Bansal
2012-10-17first working version of new inst-gen-style quantifier instantiation techniqu...Andrew Reynolds
2012-10-16more cleanup of quantifiers codeAndrew Reynolds
2012-10-16first draft of new inst gen method (still with bugs), some cleanup of quantif...Andrew Reynolds
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
2012-10-10cleanup up some static data members in the quantifiers codeAndrew Reynolds
2012-10-09fixed datatypes rewriter to detect clashes between non-datatype subfields. c...Andrew Reynolds
2012-10-05fix \fileMorgan Deters
2012-10-05Bug-related:Morgan Deters
2012-10-04disable model-generation by default in cvc3 compatibility layer. should fix ...Morgan Deters
2012-10-03minor fix for mbqi in finite model findingAndrew Reynolds
2012-10-01initial draft of skolemization during pre-processing, made simple cliques the...Andrew Reynolds
2012-09-28rename Assert.h/Assert.cpp to cvc4_assert.h/cvc4_assert.cpp -- we need to mak...Morgan Deters
2012-09-26updates to model generation : do not modify equality engine during getValue, ...Andrew Reynolds
2012-09-22Separate public-facing and internal-facing interfaces to Statistics.Morgan Deters
2012-09-19General subscriber infrastructure for NodeManager, as discussed in theMorgan Deters
2012-09-13ensure that get-value and get-model are consistent, rewrite function value bo...Andrew Reynolds
2012-09-10modified getValue to return Expr instead of NodeAndrew Reynolds
2012-08-31merge 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-20remove duplicate function TheoryEngine::getTheory(TheoryId). It was a duplic...Morgan Deters
2012-08-20minor cleanupMorgan Deters
2012-08-191. Fix for inst_match.cpp to allow compilation on fedoraClark Barrett
2012-08-16Replace propagateAsDecision() with Theory::getNextDecisionRequest():Morgan Deters
2012-08-03fix uses of getMetaKind() from outside the expr package. (they now use isCon...Morgan Deters
2012-07-31Moving some instantiation-related stuff from src/theory to src/theory/quantif...Morgan Deters
2012-07-31Options merge. This commit:Morgan Deters
2012-07-27Minor cleanup after today's commits:Morgan Deters
2012-07-27merging fmf-devel branch, includes refactored datatype theory, updates to mod...Andrew Reynolds
2012-07-27Merge quantifiers2-trunk:François Bobot
2012-07-12merged fmf-devel branch, includes support for SMT2 command get-value and (ext...Andrew Reynolds
2012-07-08another signed-ness warning fix for newer GCCMorgan Deters
2012-07-07Various fixes to documentation---typos, some incomplete documentation fixed, ...Morgan Deters
2012-06-14fix quantifier non-bugKshitij Bansal
2012-06-14* removing rewriteEquality from the rewriterDejan Jovanović
2012-06-11mark a quantifiers global var as "static" so we can find it easier laterMorgan Deters
2012-06-11Merge from quantifiers2-trunkmerge branch.Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback