diff options
Diffstat (limited to 'src/theory/quantifiers/inst_strategy_cbqi.h')
| -rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.h | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 5511af209..8ed59778b 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -1,13 +1,13 @@ /********************* */ /*! \file inst_strategy_cbqi.h ** \verbatim - ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): Tim King + ** Top contributors (to current version): + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 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 counterexample-guided quantifier instantiation **/ @@ -39,6 +39,8 @@ protected: bool d_incomplete_check; /** whether we have added cbqi lemma */ NodeSet d_added_cbqi_lemma; + /** whether we have instantiated quantified formulas */ + //NodeSet d_added_inst; /** whether to do cbqi for this quantified formula */ std::map< Node, bool > d_do_cbqi; /** register ce lemma */ @@ -120,7 +122,7 @@ class CegqiOutputInstStrategy : public CegqiOutput { public: CegqiOutputInstStrategy( InstStrategyCegqi * out ) : d_out( out ){} InstStrategyCegqi * d_out; - bool addInstantiation( std::vector< Node >& subs ); + bool doAddInstantiation( std::vector< Node >& subs ); bool isEligibleForInstantiation( Node n ); bool addLemma( Node lem ); }; @@ -141,7 +143,7 @@ public: InstStrategyCegqi( QuantifiersEngine * qe ); ~InstStrategyCegqi() throw(); - bool addInstantiation( std::vector< Node >& subs ); + bool doAddInstantiation( std::vector< Node >& subs ); bool isEligibleForInstantiation( Node n ); bool addLemma( Node lem ); /** identify */ |