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.cpp | |
parent | 599e788f249e478b5817b6cf45584d8e43458df4 (diff) |
Move getCounterexampleLiteral out of term utilities (#3238)
Diffstat (limited to 'src/theory/quantifiers/term_util.cpp')
-rw-r--r-- | src/theory/quantifiers/term_util.cpp | 20 |
1 files changed, 0 insertions, 20 deletions
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 94bc2c3f8..ffd808ed3 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -200,26 +200,6 @@ Node TermUtil::getInstConstantBody( Node q ){ } } -Node TermUtil::getCounterexampleLiteral( Node q ){ - if( d_ce_lit.find( q )==d_ce_lit.end() ){ - /* - Node ceBody = getInstConstantBody( f ); - //check if any variable are of bad types, and fail if so - for( size_t i=0; i<d_inst_constants[f].size(); i++ ){ - if( d_inst_constants[f][i].getType().isBoolean() ){ - d_ce_lit[ f ] = Node::null(); - return Node::null(); - } - } - */ - Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() ); - //otherwise, ensure literal - Node ceLit = d_quantEngine->getValuation().ensureLiteral( g ); - d_ce_lit[ q ] = ceLit; - } - return d_ce_lit[ q ]; -} - Node TermUtil::substituteBoundVariablesToInstConstants(Node n, Node q) { registerQuantifier( q ); |