diff options
Diffstat (limited to 'src/decision/justification_heuristic.h')
| -rw-r--r-- | src/decision/justification_heuristic.h | 39 |
1 files changed, 20 insertions, 19 deletions
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 0356650ae..5d83ed9fd 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -1,22 +1,23 @@ -/********************* */ -/*! \file justification_heuristic.h - ** \verbatim - ** Top contributors (to current version): - ** Kshitij Bansal, Gereon Kremer, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Justification heuristic for decision making - ** - ** A ATGP-inspired justification-based decision heuristic. See - ** [insert reference] for more details. This code is, or not, based - ** on the CVC3 implementation of the same heuristic. - ** - ** It needs access to the simplified but non-clausal formula. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Kshitij Bansal, Gereon Kremer, Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Justification heuristic for decision making + * + * A ATGP-inspired justification-based decision heuristic. See + * [insert reference] for more details. This code is, or not, based + * on the CVC3 implementation of the same heuristic. + * + * It needs access to the simplified but non-clausal formula. + */ #include "cvc4_private.h" |