From 0b13f748c7a6f2cb5ee61404e0864667e9a931b9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 22 Jul 2013 16:04:39 -0500 Subject: [PATCH] Add option --cbqi-recurse. --- src/theory/quantifiers/options | 2 ++ src/theory/quantifiers/theory_quantifiers.cpp | 4 ++-- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index d44f2e770..1c5e52869 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -77,6 +77,8 @@ option cbqi --enable-cbqi/--disable-cbqi bool :default false turns on counterexample-based quantifier instantiation [off by default] /turns off counterexample-based quantifier instantiation +option recurseCbqi --cbqi-recurse bool :default false + turns on recursive counterexample-based quantifier instantiation option userPatternsQuant /--ignore-user-patterns bool :default true ignore user-provided patterns for quantifier instantiation diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 52c9e34f3..066282c2c 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -149,7 +149,7 @@ Node TheoryQuantifiers::getNextDecisionRequest(){ void TheoryQuantifiers::assertUniversal( Node n ){ Assert( n.getKind()==FORALL ); - if( !TermDb::hasInstConstAttr(n) ){ + if( options::recurseCbqi() || !TermDb::hasInstConstAttr(n) ){ getQuantifiersEngine()->registerQuantifier( n ); getQuantifiersEngine()->assertNode( n ); } @@ -157,7 +157,7 @@ void TheoryQuantifiers::assertUniversal( Node n ){ void TheoryQuantifiers::assertExistential( Node n ){ Assert( n.getKind()== NOT && n[0].getKind()==FORALL ); - if( !TermDb::hasInstConstAttr(n[0]) ){ + if( options::recurseCbqi() || !TermDb::hasInstConstAttr(n[0]) ){ if( d_skolemized.find( n )==d_skolemized.end() ){ Node body = getQuantifiersEngine()->getTermDatabase()->getSkolemizedBody( n[0] ); NodeBuilder<> nb(kind::OR); -- 2.30.2