diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-04 14:45:21 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-09-04 14:45:21 -0500 |
| commit | d9ee2ae563b031547e76245d9f01fb24b95bc8cb (patch) | |
| tree | 5e26cc4d7997869f7faf1325bda6debb6d6b8c62 /src/theory/quantifiers/term_util.h | |
| parent | 599e788f249e478b5817b6cf45584d8e43458df4 (diff) | |
Move getCounterexampleLiteral out of term utilities (#3238)
Diffstat (limited to 'src/theory/quantifiers/term_util.h')
| -rw-r--r-- | src/theory/quantifiers/term_util.h | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index 302901625..b39a4e129 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -125,8 +125,6 @@ public: std::map< Node, std::map< Node, unsigned > > d_var_num; /** map from universal quantifiers to their inst constant body */ std::map< Node, Node > d_inst_const_body; - /** map from universal quantifiers to their counterexample literals */ - std::map< Node, Node > d_ce_lit; /** instantiation constants to universal quantifiers */ std::map< Node, Node > d_inst_constants_map; public: @@ -140,8 +138,6 @@ public: unsigned getNumInstantiationConstants( Node q ) const; /** get the ce body q[e/x] */ Node getInstConstantBody( Node q ); - /** get counterexample literal (for cbqi) */ - Node getCounterexampleLiteral( Node q ); /** returns node n with bound vars of q replaced by instantiation constants of q node n : is the future pattern node q : is the quantifier containing which bind the variable |