summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2014-08-29Set instantiation level on skolemized bodies of quantifiers. Rename ↵ajreynol
inst-level attribute to quant-inst-max-level
2014-08-29Do not use pure theory terms as single triggers. Minor cleanup.ajreynol
2014-08-28fixing bug580 caused by bad bv inequality explanationlianah
2014-08-27Fix assertion in rep_set.cpp, avoid full check in datatypes when in conflict.ajreynol
2014-08-26Improved SMT-LIBv2 language support for unsat cores.Morgan Deters
2014-08-26Bug fixes for --purify-triggers, --dt-force-assignment.ajreynol
2014-08-25Fix build rule.Morgan Deters
2014-08-25Fix Win32 builds.Morgan Deters
2014-08-25New option --purify-triggers. Refactoring of InstMatchGenerator.ajreynol
2014-08-24remove some debugging codeKshitij Bansal
(it can be brought back from version control, if needed)
2014-08-24improvements to sets sharingKshitij Bansal
* Add TheorySets::getEqualityStatus(TNode, TNode) * Add TheorySets::getModelValue(TNode)
2014-08-24fix option alias (minor)Kshitij Bansal
2014-08-24fix type in sets_translateKshitij Bansal
2014-08-23Unsat core printing.Morgan Deters
2014-08-23Some fixes for dump- and get-unsat-core.Morgan Deters
2014-08-23Quieter finish to build.Morgan Deters
2014-08-22Unit test fix.Morgan Deters
2014-08-22One small thing forgotten in core commit.Morgan Deters
2014-08-22Java-side interface improvements for unsat cores.Morgan Deters
2014-08-22Unsat core infrastruture and API (SMT-LIB compliance to come).Morgan Deters
2014-08-22Merge branch '1.4.x'Morgan Deters
2014-08-22Fix incorrectly-labeled test.Morgan Deters
2014-08-22Merge branch '1.4.x'Morgan Deters
2014-08-22Fix operator-printing issue in SMT2.Morgan Deters
2014-08-22Fix SMT1 parser :extrasorts/:extrapreds.Morgan Deters
2014-08-21Avoid doing work in quantifiers engine when no quantifiers are asserted.ajreynol
2014-08-21Fix --inst-max-level for strategies that use arbitrary representative terms.ajreynol
2014-08-20Update bv proof signature and example, after discussions with Liana.ajreynol
2014-08-20Add option for inductive strengthening based on well-founded induction for ↵ajreynol
integers (default schema).
2014-08-19Merge branch '1.4.x'Morgan Deters
2014-08-19Produce error for bad indexed function names in SMT-LIB, remove antlr warning.Morgan Deters
2014-08-18Making getEqualityStatus more powerful for bit-vector theory.lianah
2014-08-18Merge branch '1.4.x'Morgan Deters
Conflicts: test/regress/regress0/Makefile.am
2014-08-18Revert a8e0ce67 and add test case (resolves bug #578).Morgan Deters
This reverts commit a8e0ce673ba00533a663804cf74500e4d9a3a5cb.
2014-08-18Add support for quantifier-specific instantiation levels. Add option for ↵ajreynol
setting inst-level 0 only for input terms.
2014-08-15Update smt_engine.cppKshitij Bansal
Code changed but comment didn't, might as well get rid of it.
2014-08-12To avoid confusion, permit --enable-staticbinary as an alias for ↵Morgan Deters
--enable-static-binary.
2014-08-09Fix a build issue for some configurations, thanks Tianyi.Morgan Deters
2014-08-08Add draft of BV proof signature (incomplete) and example proof.ajreynol
2014-08-07Another build fix.Morgan Deters
2014-08-07Fix win32 build.Morgan Deters
2014-08-06Fix double-linking issue (I think) by simplifying builds/ structure.Morgan Deters
2014-08-06First crack at fixing double-linking issues in build system.Morgan Deters
2014-08-05Fix for manpages.Morgan Deters
2014-08-05fixed bug575 for bv modelslianah
2014-08-05fixed bug575 for bv modelslianah
2014-08-05Minor fix : do not drop instantiation patterns when merging quantifiers.ajreynol
2014-08-04Some fixes to symmetry breaker (resolves bug 576).Morgan Deters
2014-08-04Some fixes to symmetry breaker (resolves bug 576).Morgan Deters
2014-08-04Better support for resource-limiting when there aren't any actual conflicts.Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback