8000 Commits · tml/CVC4 · GitHub

More Web Proxy on the site http://driver.im/

Commits

Commits on Dec 11, 2012

adding cache for preprocessing datatypes terms to fix bug 475, fix for handling user attributes in quantifiers (was broken)

ajreynol
authored and
mdeters
committed
adding cache for preprocessing datatypes terms to fix bug 475, fix for handling user attributes in quantifiers (was broken)
ajreynol
committed

Commits on Dec 1, 2012

drastic simplification of quantifiers code regarding equality queries, instantiation strategies moved from instantiators to central instantiation engine, removed instantiator objects, simplified re…
ajreynol
committed

Commits on Nov 30, 2012

Commits on Nov 29, 2012

Commits on Nov 18, 2012

support for quantifiers macros, bug fix for bug 454 involving E-matching Array select terms (thanks for the bug report Francois)
ajreynol
committed

Commits on Nov 14, 2012

replaced all static member data from rewrite rule triggers, added infrastructure for recognizing quantifier macros
ajreynol
committed

Commits on Nov 13, 2012

refactoring of quantifiers rewriter based on code review from yesterday, refactoring code out of instantiators in preparation for quantifiers equality engine
ajreynol
committed

Commits on Nov 12, 2012

minor bug fixes for quantifiers, added sort inference module (not ready to be used yet), added new totality lemma option for uf strong solver
ajreynol
committed

Commits on Nov 8, 2012

added support for parametric datatypes in smt2 parser, includes support for 'as' qualifier
ajreynol
committed

Commits on Nov 2, 2012

more minor updates to inst gen and representative selection, clean up of equality query
ajreynol
committed

Commits on Oct 31, 2012

cleaning up some of the equality query stuff, implemented a new representative selection strategy for quantifier instantiation
ajreynol
committed

Commits on Oct 29, 2012

more updates and minor bug fixes for fmf/inst-gen quantifier instantiation
ajreynol
committed

Commits on Oct 26, 2012

Commits on Oct 24, 2012

Commits on Oct 23, 2012

Commits on Oct 17, 2012

first working version of new inst-gen-style quantifier instantiation technique for fmf (--fmf-new-inst-gen), minor cleanup
ajreynol
committed

Commits on Oct 16, 2012

Commits on Oct 10, 2012

cleanup up some static data members in the quantifiers code
ajreynol
committed

Commits on Oct 9, 2012

Commits on Oct 3, 2012

minor fix for mbqi in finite model finding
ajreynol
committed

Commits on Oct 1, 2012

initial draft of skolemization during pre-processing, made simple cliques the default option for uf strong solver
ajreynol
committed

Commits on Sep 26, 2012

updates to model generation : do not modify equality engine during getValue, other minor changes, still problems with constants not being specified for some eq classes
ajreynol
committed

Commits on Sep 17, 2012

minor fix for models, added simple cliques option for uf strong solver
ajreynol
committed

Commits on Sep 16, 2012

store values returned by get-value in TheoryModel::d_reps if necessary, fixes bug 382.
ajreynol
committed

Commits on Sep 13, 2012

ensure that get-value and get-model are consistent, rewrite function value bodies, do not dag-ify model output
ajreynol
committed

Commits on Sep 11, 2012

added getCardinality to model
ajreynol
committed

0