diff options
Diffstat (limited to 'src/theory/quantifiers/fmf/full_model_check.h')
-rw-r--r-- | src/theory/quantifiers/fmf/full_model_check.h | 23 |
1 files changed, 21 insertions, 2 deletions
diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h index 7dd1991f5..4a6c62827 100644 --- a/src/theory/quantifiers/fmf/full_model_check.h +++ b/src/theory/quantifiers/fmf/full_model_check.h @@ -2,9 +2,9 @@ /*! \file full_model_check.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Mathias Preiner + ** Andrew Reynolds, Mathias Preiner, Morgan Deters ** 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 @@ -86,7 +86,16 @@ protected: Node d_false; std::map<TypeNode, std::map< Node, int > > d_rep_ids; std::map<Node, Def > d_quant_models; + /** + * The predicate for the quantified formula. This is used to express + * conditions under which the quantified formula is false in the model. + * For example, for quantified formula (forall x:Int, y:U. P), this is + * a predicate of type (Int x U) -> Bool. + */ std::map<Node, Node > d_quant_cond; + /** A set of quantified formulas that cannot be handled by model-based + * quantifier instantiation */ + std::unordered_set<Node, NodeHashFunction> d_unhandledQuant; std::map< TypeNode, Node > d_array_cond; std::map< Node, Node > d_array_term_cond; std::map< Node, std::vector< int > > d_star_insts; @@ -155,6 +164,16 @@ public: bool processBuildModel(TheoryModel* m) override; bool useSimpleModels(); + + private: + /** + * Register quantified formula. + * This checks whether q can be handled by model-based instantiation and + * initializes the necessary information if so. + */ + void registerQuantifiedFormula(Node q); + /** Is quantified formula q handled by model-based instantiation? */ + bool isHandled(Node q) const; };/* class FullModelChecker */ }/* CVC4::theory::quantifiers::fmcheck namespace */ |