From 1f4b954a2cc7667a56a3007fa75c125fba93ed23 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 2 Mar 2017 14:45:21 -0600 Subject: Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions. --- src/theory/quantifiers_engine.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'src/theory/quantifiers_engine.cpp') diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 573c97f00..ba50f9ead 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -1275,8 +1275,7 @@ bool QuantifiersEngine::addSplit( Node n, bool reqPhase, bool reqPhasePol ){ bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool reqPhasePol ){ //Assert( !areEqual( n1, n2 ) ); //Assert( !areDisequal( n1, n2 ) ); - Kind knd = n1.getType()==NodeManager::currentNM()->booleanType() ? IFF : EQUAL; - Node fm = NodeManager::currentNM()->mkNode( knd, n1, n2 ); + Node fm = NodeManager::currentNM()->mkNode( EQUAL, n1, n2 ); return addSplit( fm ); } -- cgit v1.2.3