From 57919ba7271a6c2b36173f2ba0f580b84f962b1b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 8 Feb 2021 12:29:58 -0600 Subject: Remove support for inst closure (#5874) This was a feature implemented for "Deciding Local Theory Extensions via E-matching" CAV 2015 that is not used anymore, and will be a burden to maintain further with potential changes to term database. It also simplifies the TermDatabase::addTerm method (which changed indentation). --- src/theory/quantifiers/equality_query.cpp | 5 ----- 1 file changed, 5 deletions(-) (limited to 'src/theory/quantifiers/equality_query.cpp') diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index c60c98d70..def27fe5a 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -172,11 +172,6 @@ int EqualityQueryQuantifiersEngine::getRepScore(Node n, return -2; }else if( !n.getType().isSubtypeOf( v_tn ) ){ //reject if incorrect type return -2; - } - else if (options::lteRestrictInstClosure() - && (!d_tdb->isInstClosure(n) || !d_tdb->hasTermCurrent(n, false))) - { - return -1; }else if( options::instMaxLevel()!=-1 ){ //score prefer lowest instantiation level if( n.hasAttribute(InstLevelAttribute()) ){ -- cgit v1.2.3