From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 22 Jul 2013 21:04:39 +0000 (-0500)
Subject: Add option --cbqi-recurse.
X-Git-Tag: cvc5-1.0.0~7287^2~52
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0b13f748c7a6f2cb5ee61404e0864667e9a931b9;p=cvc5.git

Add option --cbqi-recurse.
---

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);