diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-08-25 13:50:45 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-08-25 13:50:45 -0500 |
| commit | dce53c4de6dd7482d9784388cc61753352f241d8 (patch) | |
| tree | d1df5306b02e61cde0cc6d6280fb7cd8efb16494 /src/theory/quantifiers/inst_strategy_cbqi.h | |
| parent | 6b355496aaf27d46d6a33402814753589b755842 (diff) | |
Options for counterexample guided instantiation.
Diffstat (limited to 'src/theory/quantifiers/inst_strategy_cbqi.h')
| -rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.h | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 8ed59778b..20d872c36 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -39,6 +39,10 @@ protected: bool d_incomplete_check; /** whether we have added cbqi lemma */ NodeSet d_added_cbqi_lemma; + /** parent guards */ + std::map< Node, std::vector< Node > > d_parent_quant; + std::map< Node, std::vector< Node > > d_children_quant; + std::map< Node, bool > d_active_quant; /** whether we have instantiated quantified formulas */ //NodeSet d_added_inst; /** whether to do cbqi for this quantified formula */ |