summaryrefslogtreecommitdiff
path: root/test/regress/regress0/fmf/Makefile.am
AgeCommit message (Expand)Author
2018-03-21 Move regression tests to single Makefile.am (#1658)Andres Noetzli
2018-02-15Refactor regressions (#1581)Andrew Reynolds
2017-11-03Suppport SAT logic (#1310)Andrew Reynolds
2017-09-28Improve finite model finding for recursive predicates (#1150)Andrew Reynolds
2017-08-31Answer unknown when uf-ss=no-minimal is combined with cardinality constraints...Andrew Reynolds
2017-05-05Do not eliminate extended arithmetic symbols when finite model finding is on,...ajreynol
2017-04-28Do not eliminate non-standard arithmetic operators in recursive function defi...ajreynol
2017-04-24Fixes and simplifications for fmf mbqi.ajreynol
2017-04-14Fix for fmf-fun when the option is set by user command.ajreynol
2017-04-05Caching for fun def process, add regression.ajreynol
2017-03-22Minor fix for bounded integers.ajreynol
2017-03-15Allow 0 argument recursive functions. Fixes bug 782.ajreynol
2017-03-02Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boole...ajreynol
2017-02-07Generalize finite bound inference to unifiable variables in set membership li...ajreynol
2017-01-11Fix for when variables are (partially) bound in multiple ways, add regression...ajreynol
2016-12-07Fix boolean term conversion for INST_ATTRIBUTE, fixes bug 764.ajreynol
2016-12-07Refactoring, generalization of bounded inference module. Simplification of re...ajreynol
2016-12-02Refactor preprocessing of models in fmf. Fix options --fmf-empty-sorts and --...ajreynol
2016-11-17Fix Makefiles in testAndres Notzli
2016-10-21Move slow regress0 benchmarks to regress1, increment regress1 through regress3.ajreynol
2016-06-01Initial infrastructure for bounded set quantification (disabled). Refactoring...ajreynol
2016-05-23Fix related to parametric sorts whose interpretation is finite due to uninter...ajreynol
2016-04-11Minor fixes for inst match generators. Updates to qip.googleajreynol
2016-04-10More work on instantiation propagation. Enable external filtering of instanti...ajreynol
2016-03-07Minor change to F-Length inference in strings. No internal tracking of cardin...ajreynol
2016-02-23Fix term database for non-equal, congruent terms in master equality engine. D...ajreynol
2016-02-19Fixes and improvements for datatypes properties and splitting.ajreynol
2016-02-18Implement dynamic splitting for quantified formulas. Minor refactoring of re...ajreynol
2016-02-09Fix regression, minor change to output.ajreynol
2016-02-08Updates related to finite model finding and (co)datatypes. Bug fix enumerator...ajreynol
2016-02-01Simplify fmc model construction, add regression. Improve FMF debug assertions.ajreynol
2016-01-20Fix bug in fmc mbqi where modelscomputed for mbqi could involve non-constant ...ajreynol
2016-01-19Bug fixes for model construction with codatatypes, add regressions.ajreynol
2016-01-18Bug fix rewriter for fun defs.ajreynol
2016-01-15Ensure model construction for parametric sorts involving uninterpreted sorts ...ajreynol
2015-12-22Always split on constructor types for datatypes involving uninterpreted sorts...ajreynol
2015-11-04Better combination of UF with cbqi, refactor quantifiers intialization.ajreynol
2015-06-27Refactor various corner cases of fmf, quantifiers modules. Enable cbqi2 by de...ajreynol
2015-04-26Bug fixes and improvements for mbqi with theory symbols, TheoryModel fullMode...ajreynol
2014-11-07Properly distinguish which EQC to assign values in datatypes, use assertRepre...ajreynol
2014-11-06Reenable regression. Add (for now, disabled) changes to datatypes theory com...ajreynol
2014-11-05More work on datatypes theory combination: fix bug in care graph, do not assi...ajreynol
2014-04-14Fix bug in mbqi=fmc handling theory symbols. Fix mbqi=fmc models (Bug 557). ...Andrew Reynolds
2014-04-10Add support for cardinality constraints logic UFC. Add regressions in fmf/. ...Andrew Reynolds
2014-03-07Remove --ite-remove-quant; support pulling ground ITEs out of quantifier bodi...Morgan Deters
2013-12-23Proof-checking code; fixups of segfaults and missing functionality in proof g...Morgan Deters
2013-10-24Fix for bug515Clark Barrett
2013-09-18Support a personal build configuration and make rules.Morgan Deters
2013-09-13Documentation fixes, some code typo fixes, file perms, other minor things.Morgan Deters
2013-09-09Another minor fix for datatypes to repair my previous commit.Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback