summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2013-09-12fix bug 534: portfolio define-fun duplicate modelKshitij Bansal
2013-09-09Add support for check-sat with argument.Morgan Deters
2013-09-09Fix declare-datatypes dumping bug (bug 385).Morgan Deters
2013-09-09Support per-command verbosity settings.Morgan Deters
2013-09-09Support empty (and 1-ary) tuples and records.Morgan Deters
2013-09-09Fix some line-numbering in auto-generated metakind.h. Thanks to Martin ↵Morgan Deters
Brain for reporting this.
2013-09-09Fix portfolio on bug411.smt2. (get-model command should only go to last winner)Morgan Deters
2013-09-09Ensure no cost for datatypes debugging when not tracing it.Morgan Deters
2013-09-06Fix datatypes for bug 503Andrew Reynolds
2013-09-05Fix FLOOR and DISTINCT in CVC language parser.Morgan Deters
2013-09-05Fix lambda handling in CVC parserMorgan Deters
2013-09-05Permit setOption(decision-mode)Morgan Deters
2013-09-05Fix bugs/issues with missed-t-prop dump outputMorgan Deters
2013-09-05Fix declare-fun/define-fun in dumps; resolves bugs 408 and 385; also fix a ↵Morgan Deters
segfault in smt2 printer
2013-08-30Add ability to mkConst(TupleSelect) and friends in language bindingsMorgan Deters
2013-08-26Merge branch '1.2.x'Kshitij Bansal
2013-08-26bug 374 fix: assert litVal=desiredVal only for leaf nodes1.2.xKshitij Bansal
2013-08-20Change recursive expandDefinitions() to an interative worklist-based one; we ↵Morgan Deters
were blowing the stack. Fixes a segfault reported by Pantazis Deligiannis.
2013-08-13--segv-nospin is now default.Morgan Deters
2013-08-13Minor cleanup.Morgan Deters
2013-08-13Minor fixes for --fmf-fmc for quantifiers containing datatypesAndrew Reynolds
2013-08-13initial modifications for per-ic cbqiAndrew Reynolds
2013-08-09Clean up "make install"-produced intermediate files (resolves bug 526)Morgan Deters
2013-08-08Fix a serious bug in the preprocessor; problem inputs reported by Pantazis ↵Morgan Deters
Deligiannis.
2013-08-08Parameterized, uninterpreted sorts need no Boolean-term conversionMorgan Deters
2013-07-30Minor fixes to build system.Morgan Deters
2013-07-29Fix numerous compiler warnings on various platformsMorgan Deters
2013-07-24Regressions now checking models on unknown too. But quantifiers don't have ↵Morgan Deters
to be simplified by check-model in that case.
2013-07-24Fixes for building with mingw win64.Morgan Deters
2013-07-24Don't allow --stats if not a statistics-enabled buildMorgan Deters
2013-07-24some portfolio driver cleanupMorgan Deters
2013-07-23Some fixes for (get-info :all-options)Morgan Deters
2013-07-23fix for win32 option parsing via mingw32Morgan Deters
2013-07-23(get-info :all-options) to get option values; also command-line option ↵Morgan Deters
suggestions
2013-07-22Allow BV and DT in either order in the logic stringMorgan Deters
2013-07-22Add option --cbqi-recurse.Andrew Reynolds
2013-07-22Bug fix for --fmf-fmc for non-uninterpreted sort quantifiers, added ↵Andrew Reynolds
infrastructure to BV collectModelInfo in preparation for bug fix.
2013-07-19possible fix for bug 521Dejan Jovanovic
2013-07-19Minor fix for --no-condense-function-valuesMorgan Deters
2013-07-18Fix quantifier instantiation bug in cbqi, add default priorities in rewrite ↵Andrew Reynolds
engine.
2013-07-17Fix bug 516; include some bug testcases.Morgan Deters
2013-07-16fixed seg fault when bv equality is turned offLiana Hadarean
2013-07-16fixed bug520Liana Hadarean
2013-07-16"Tabular"-style function definitions in models with ↵Morgan Deters
--no-condense-function-values
2013-07-16Minor bugfixes to model-buildingMorgan Deters
2013-07-13Remove now-unused language bindings interface file.Morgan Deters
2013-07-13Fix language bindings and portfolio builds.Morgan Deters
2013-07-12Fix for curious GCC 4.8 translation with -O.Morgan Deters
2013-07-11Remove auto-aritization from TPTP parserMorgan Deters
2013-07-11Support for TPTP's TFF0 (with arithmetic)Morgan Deters
This commit reverses an "SZS ontology compliance hack" that was done for CASC-24 this year, and adds a TPTP pretty-printer which is capable of outputting results in the TPTP way (rather than the SMT way). This commit includes minor changes to the Expr package to add obvious missing functionality, and to fix the way expressions with builtin operators are made. These changes are truly a _fix_, the implementation had not been properly aligned with the design vision for some corner cases.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback