diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_repair_const.h')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_repair_const.h | 24 |
1 files changed, 2 insertions, 22 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h index 6be5ce5e6..e02ca1f3e 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.h +++ b/src/theory/quantifiers/sygus/sygus_repair_const.h @@ -2,9 +2,9 @@ /*! \file sygus_repair_const.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa + ** Andrew Reynolds, Haniel Barbosa, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 @@ -209,26 +209,6 @@ class SygusRepairConst * If n is in the given logic, this method returns true. */ bool getFitToLogicExcludeVar(LogicInfo& logic, Node n, Node& exvar); - /** initialize checker - * - * This function initializes the smt engine checker to check the - * satisfiability of the argument "query" - * - * The arguments em and varMap are used for supporting cases where we - * want checker to use a different expression manager instead of the current - * expression manager. The motivation for this so that different options can - * be set for the subcall. - * - * We update the flag needExport to true if checker is using the expression - * manager em. In this case, subsequent expressions extracted from smte - * (for instance, model values) must be exported to the current expression - * manager. - */ - void initializeChecker(std::unique_ptr<SmtEngine>& checker, - ExprManager& em, - ExprManagerMapCollection& varMap, - Node query, - bool& needExport); }; } /* CVC4::theory::quantifiers namespace */ |