From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 16 Oct 2014 15:48:08 +0000 (+0200)
Subject: Use n-ary splits instead of binary splits in theory datatypes.
X-Git-Tag: cvc5-1.0.0~6559
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=135b3d1521df59813293f1242c360c488b17958d;p=cvc5.git

Use n-ary splits instead of binary splits in theory datatypes.
---

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 4c37e8889..f717e7701 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -222,15 +222,15 @@ void TheoryDatatypes::check(Effort e) {
                 Trace("datatypes-infer") << "DtInfer : 1-cons : " << t << std::endl;
                 d_infer.push_back( t );
               }else{
-                  Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[consIndex].getTester() ), n );
-                  Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n <<  endl;
-                  test = Rewriter::rewrite( test );
-                  NodeBuilder<> nb(kind::OR);
-                  nb << test << test.notNode();
-                  Node lemma = nb;
-                  d_out->lemma( lemma );
-                  d_out->requirePhase( test, true );
-                  return;
+                Trace("dt-split") << "*************Split for constructors on " << n <<  endl;
+                std::vector< Node > children;
+                for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+                  Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), n );
+                  children.push_back( test );
+                }
+                Node lemma = NodeManager::currentNM()->mkNode( kind::OR, children );
+                d_out->lemma( lemma );
+                return;
               }
             }else{
               Trace("dt-split-debug") << "Do not split constructor for " << n << " : " << n.getType() << " " << dt.getNumConstructors() << std::endl;