summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2012-11-08Improved support for division by zero. This adds the *_TOTAL kinds and ↵Tim King
uninterpreted functions for division by 0.
2012-11-08exception fixMorgan Deters
2012-11-08Fixed two small bugs in model generationClark Barrett
2012-11-08Added getBaseType - Morgan please checkClark Barrett
2012-11-08added support for parametric datatypes in smt2 parser, includes support for ↵Andrew Reynolds
'as' qualifier
2012-11-07* Type ascription bug fixed (resolves bug 432), but there are others I ↵Morgan Deters
discovered (still outstanding). :-( * Fix a documentation-building problem when building from tarballs (fixes distcheck build failure last night) * Provide expected output for arith regression 'mod.01.smt2' * Also, fix a compiler warning in inst_gen.cpp (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-07Fix to a bug in integer mod lemmas.Tim King
2012-11-06fix issue in compatibility layer that could segfaultMorgan Deters
2012-11-05Fix to the context dependent static learning code.Tim King
2012-11-05fixes for replacement function libraryMorgan Deters
2012-11-02more minor updates to inst gen and representative selection, clean up of ↵Andrew Reynolds
equality query
2012-10-31cleaning up some of the equality query stuff, implemented a new ↵Andrew Reynolds
representative selection strategy for quantifier instantiation
2012-10-29more updates and minor bug fixes for fmf/inst-gen quantifier instantiationAndrew Reynolds
2012-10-29Tweak to options configuration for turning off minisat elimination when ↵Clark Barrett
models are on
2012-10-29Disable minisat elimination when models are onClark Barrett
2012-10-29Disable some array optimizations when models are onClark Barrett
2012-10-26Fix to subrange type enumerator, and its unit test. Resolves bug 436.Morgan Deters
(this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-26bug fix for parametric datatypes, previously datatypes theory/rewriter was ↵Andrew Reynolds
not recognizing parametric datatype types as being datatype types
2012-10-26Fix for bug 430. d_delta in PartialModel was never being computed. (Delta ↵Tim King
remained at its initial non-sensical value of -1.) There was a problem with guarding d_delta with d_deltaIsSafe in PartialModel.
2012-10-26build options sources into distribution tarballs (in the same way that antlr ↵Morgan Deters
grammars are pre-generated for tarballs). this speeds up user builds by not requiring them to run the mkoptions script (unless they change an options meta-file). i've tested this, but let me know if there are any problems you encounter.
2012-10-26better parametric datatype arity checking; fixes bug 433Morgan Deters
2012-10-26Fixed a failing datatype regression with check-modelsClark Barrett
2012-10-26fixed bug in datatypes decision procedure enforcing rewriting of incorrectly ↵Andrew Reynolds
applied selector terms, this effects two regression test where TCC fails, using --disable-dt-rewrite-error-sel changes answer of both regression tests
2012-10-26More bug fixes and more checks for modelsClark Barrett
2012-10-25more minor fixes to build systemACSYS
2012-10-24fixed assertion failures in efficient e-matchingAndrew Reynolds
2012-10-24Includes many fixes to build system for Solaris (thanks Tim!), and alsoMorgan Deters
just in general, and some documentation adjustments.
2012-10-24Updated the ArithStaticLearner to be user context dependent.Tim King
2012-10-24Fix for systems that do not have the MAP_FILE macro defined.Tim King
2012-10-24fix for bug 429 Dejan Jovanović
* not all asserted units were tracked in the user trail, moved the tracking into uncheckedEnqueue
2012-10-24efficient e-matching now specific to rewrite rulesAndrew Reynolds
2012-10-23more major cleanup of quantifiers code, separating rewrite-rules-specific ↵Andrew Reynolds
code from quantifiers-specific code
2012-10-23fixed problem with datatypes giving incorrect explanations, now corrected ↵Andrew Reynolds
and improved. this update fixes bug 428, also changes the result for 2 benchmarks where tcc in cvc3 fails (cvc4 had previously had been answering correctly by accident).
2012-10-23More debugging info, small changes to model builderClark Barrett
2012-10-23Added reads that were missing in collectModelInfoClark Barrett
2012-10-23fixed TheoryBV collectModel info to check for shared terms; this seems to ↵Liana Hadarean
fix bug424
2012-10-23more updates to inst gen: fixed partial instantiations, recognize duplicate ↵Andrew Reynolds
defaults for uf
2012-10-22fix parser generation in distributed tarballs (should fix bug #427)Morgan Deters
2012-10-22one more incorrect #line fixedMorgan Deters
2012-10-22fix installation of certain header filesMorgan Deters
2012-10-19Fix for model building with shared terms for arithmetic.Tim King
(this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-19Fix problem with incremental with portfolio. Fixes bug 420.Kshitij Bansal
(this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-19BV theory model fixLiana Hadarean
2012-10-19--fallback-sequential / --no-fallback-sequential optionKshitij Bansal
closes bug 419, fix typo, fix warning (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-17first working version of new inst-gen-style quantifier instantiation ↵Andrew Reynolds
technique for fmf (--fmf-new-inst-gen), minor cleanup
2012-10-16more cleanup of quantifiers codeAndrew Reynolds
2012-10-16first draft of new inst gen method (still with bugs), some cleanup of ↵Andrew Reynolds
quantifiers code
2012-10-14fix #line number warnings (sorry!)Morgan Deters
2012-10-12Added assertions and tracing code for collectModelInfo phaseClark Barrett
2012-10-12Latest changes to model codeClark Barrett
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback