summaryrefslogtreecommitdiff
path: root/src/expr/command.h
AgeCommit message (Expand)Author
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
2015-01-26Output solutions for synthesis conjectures with --dump-synth. Minor refactor...ajreynol
2014-11-17Resource-limiting work.Liana Hadarean
2014-10-23Parsing and infrastructure support for SMT-LIBv2.5 input and output languages.Morgan Deters
2014-10-06Support for RESET command in CVC native language (and infrastructure for supp...Morgan Deters
2014-08-26Improved SMT-LIBv2 language support for unsat cores.Morgan Deters
2014-08-22Unsat core infrastruture and API (SMT-LIB compliance to come).Morgan Deters
2014-08-18Add support for quantifier-specific instantiation levels. Add option for set...ajreynol
2014-07-01Update copyrights.Morgan Deters
2014-06-19For casc : print models of functions rewritten by sort inference.ajreynol
2014-05-11More preparation for CASC proofs. Minor fix for sort inference (rewrite new ...Andrew Reynolds
2014-05-09Add variable ordering to ambqi. Bug fix to macros. More preparation for CASC...Andrew Reynolds
2013-12-24Better automatic handling of output language setting.Morgan Deters
2013-09-09Support per-command verbosity settings.Morgan Deters
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-03-21Add the ability to "mute" commands, needed for SMT-LIB compliance.Morgan Deters
2013-02-16Some cleanup and copyright updatingMorgan Deters
2012-11-12* Fix language bindings: various issuesMorgan Deters
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
2012-10-09* make Model class private (as discussed at meeting today)Morgan Deters
2012-10-05BoolExpr removed and replaced with ExprDejan Jovanović
2012-10-04Implemented array type enumerator, more fixes for modelsClark Barrett
2012-09-28Some fixes to portfolioKshitij Bansal
2012-09-15minor interface improvements, compliance fixesMorgan Deters
2012-09-08Some minor changes after reviewing the portfolio "unified driver" commit.Morgan Deters
2012-09-08Single driver for both sequential and portfolioKshitij Bansal
2012-09-04Accepted some patches from the Multicore Programming Group at Imperial Colleg...Morgan Deters
2012-08-31merge from fmf-devel branch. more updates to models: now with collectModelIn...Andrew Reynolds
2012-08-24fix get-value output in a couple ways; this fixes bug #378Morgan Deters
2012-08-06Cleanup of some command stuff, fixes broken Java build.Morgan Deters
2012-07-27Merge quantifiers2-trunk:François Bobot
2012-07-12merged fmf-devel branch, includes support for SMT2 command get-value and (ext...Andrew Reynolds
2012-06-09Dagification of output expressions.Morgan Deters
2012-06-07Adding EchoCommand and associated printer and parser rules:Morgan Deters
2012-04-06* Fix ITEs and functions in CVC language printer.Morgan Deters
2012-03-09Some work on the dump infrastructure to support portfolio work.Morgan Deters
2012-02-22Fixes to documentation / fixes for MacOSMorgan Deters
2012-02-20portfolio mergeMorgan Deters
2011-11-22More language bindings work:Morgan Deters
2011-10-29Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF command, SmtEngine::g...Morgan Deters
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
2011-07-11merge from symmetry branchMorgan Deters
2011-05-05Merge from nonclausal-simplification-v2 branch:Morgan Deters
2011-05-01minor fixes, plus experimental readline support in InteractiveShellMorgan Deters
2011-04-18Partial merge from datatypes-merge branch:Morgan Deters
2010-11-08cleanup, documentation, SMT-LIBv2 complianceMorgan Deters
2010-10-10additional model gen and SMT-LIBv2 compliance work: (get-assignment) now supp...Morgan Deters
2010-10-07SMT-LIBv2 (define-fun...) command now functional; does eager expansion at pre...Morgan Deters
2010-10-05parser and core support for SMT-LIBv2 commands get-info, set-option, get-opti...Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback