Sync Q6 updates

app.py

@@ -15,23 +15,53 @@ def process(corpus_desc, query_desc, query):
     corpus = CORPUS_BY_DESC[corpus_desc]
     query_type = QUERY_TYPE_BY_DESC[query_desc]
     timestamp = datetime.datetime.now().strftime('%Y%m%d-%H%M%S')
-    print(json.dumps({'timestamp': timestamp, 'corpus': corpus, 'query_type': query_type, 'query': query}))
     data = {
+        'timestamp': timestamp,
         'corpus': corpus,
         'query_type': query_type,
         'query': query,
     }
+    print(json.dumps(data))
     if API_IPADDR is None:
         raise ValueError(f'API_IPADDR envvar is not set!')
     response = requests.post(f'http://{API_IPADDR}:5000/', json=data)
     if response.status_code == 200:
         result = response.json()
     else:
-        raise ValueError(f'Invalid response: {response.status_code}')
+        raise ValueError(f'HTTP error {response.status_code}: {response.json()}')
     if debug:
         print(result)
     return result
 
+def process_ard_cnf_multi(corpus_desc, query_desc, query, maxnum):
+    corpus = CORPUS_BY_DESC[corpus_desc]
+    query_type = QUERY_TYPE_BY_DESC[query_desc]
+    timestamp = datetime.datetime.now().strftime('%Y%m%d-%H%M%S')
+    data = {
+        'timestamp': timestamp,
+        'corpus': corpus,
+        'query_type': query_type,
+        'query': query,
+        'maxnum': maxnum,
+    }
+    print(json.dumps(data))
+    if API_IPADDR is None:
+        raise ValueError(f'API_IPADDR envvar is not set!')
+    response = requests.post(f'http://{API_IPADDR}:5000/', json=data)
+    if response.status_code == 200:
+        result = response.json()
+    else:
+        raise ValueError(f'HTTP error {response.status_code}: {response.json()}')
+    if debug:
+        print(result)
+    if len(result) != 3:
+        raise ValueError(f'Invalid result: {result}')
+    outputs, output_tokens, message = result[0], result[1], result[2]
+    outputs = outputs[:maxnum]
+    while len(outputs) < 10:
+        outputs.append([])
+    return output_tokens, message, outputs[0], outputs[1], outputs[2], outputs[3], outputs[4], outputs[5], outputs[6], outputs[7], outputs[8], outputs[9]
+
 with gr.Blocks() as demo:
     with gr.Column():
         gr.HTML(
@@ -88,13 +118,13 @@ with gr.Blocks() as demo:
                 gr.HTML(f'<p style="font-size: 16px;">Note: The (n-1)-gram needs to exist in the corpus. If the (n-1)-gram is not found in the corpus, an error message will appear. If the (n-1)-gram appears more than {MAX_CNT_FOR_NTD} times in the corpus, the result will be approximate.</p>')
                 with gr.Row():
                     with gr.Column(scale=1):
-                        a_ntd_input = gr.Textbox(placeholder='Enter a string (an (n-1)-gram) here', label='Query', interactive=True)
+                        ntd_input = gr.Textbox(placeholder='Enter a string (an (n-1)-gram) here', label='Query', interactive=True)
                         with gr.Row():
-                            a_ntd_clear = gr.ClearButton(value='Clear', variant='secondary', visible=True)
-                            a_ntd_submit = gr.Button(value='Submit', variant='primary', visible=True)
-                        a_ntd_output_tokens = gr.Textbox(label='Tokenized', lines=2, interactive=False)
+                            ntd_clear = gr.ClearButton(value='Clear', variant='secondary', visible=True)
+                            ntd_submit = gr.Button(value='Submit', variant='primary', visible=True)
+                        ntd_output_tokens = gr.Textbox(label='Tokenized', lines=2, interactive=False)
                     with gr.Column(scale=1):
-                        a_ntd_output = gr.Label(label='Distribution', num_top_classes=10)
+                        ntd_output = gr.Label(label='Distribution', num_top_classes=10)
 
         with gr.Row(visible=False) as row_4:
             with gr.Column():
@@ -120,46 +150,98 @@ with gr.Blocks() as demo:
                 gr.HTML('<p style="font-size: 16px;">Example query: <b>I love natural language</b> (the output is P(* | natural language), for the top-10 tokens *)</p>')
                 with gr.Row():
                     with gr.Column(scale=1):
-                        a_infntd_input = gr.Textbox(placeholder='Enter a string here', label='Query', interactive=True)
+                        infntd_input = gr.Textbox(placeholder='Enter a string here', label='Query', interactive=True)
                         with gr.Row():
-                            a_infntd_clear = gr.ClearButton(value='Clear', variant='secondary', visible=True)
-                            a_infntd_submit = gr.Button(value='Submit', variant='primary', visible=True)
-                        a_infntd_output_tokens = gr.Textbox(label='Tokenized', lines=2, interactive=False)
-                        a_infntd_longest_suffix = gr.Textbox(label='Longest Found Suffix', interactive=False)
+                            infntd_clear = gr.ClearButton(value='Clear', variant='secondary', visible=True)
+                            infntd_submit = gr.Button(value='Submit', variant='primary', visible=True)
+                        infntd_output_tokens = gr.Textbox(label='Tokenized', lines=2, interactive=False)
+                        infntd_longest_suffix = gr.Textbox(label='Longest Found Suffix', interactive=False)
                     with gr.Column(scale=1):
-                        a_infntd_output = gr.Label(label='Distribution', num_top_classes=10)
+                        infntd_output = gr.Label(label='Distribution', num_top_classes=10)
+
+        # with gr.Row(visible=False) as row_6:
+        #     with gr.Column():
+        #         gr.HTML(f'''<h2>6. Searching for document containing n-gram(s)</h2>
+        #                     <p style="font-size: 16px;">This displays a random document in the corpus that satisfies your query. You can simply enter an n-gram, in which case the document displayed would contain your n-gram. You can also connect multiple n-gram terms with the AND/OR operators, in the <a href="https://en.wikipedia.org/wiki/Conjunctive_normal_form">CNF format</a>, in which case the displayed document contains n-grams such that it satisfies this logical constraint.</p>
+        #                     <p style="font-size: 16px;">Example queries:</p>
+        #                     <ul style="font-size: 16px;">
+        #                         <li><b>natural language processing</b> (the displayed document would contain "natural language processing")</li>
+        #                         <li><b>natural language processing AND deep learning</b> (the displayed document would contain both "natural language processing" and "deep learning")</li>
+        #                         <li><b>natural language processing OR artificial intelligence AND deep learning OR machine learning</b> (the displayed document would contain at least one of "natural language processing" / "artificial intelligence", and also at least one of "deep learning" / "machine learning")</li>
+        #                     </ul>
+        #                     <p style="font-size: 16px;">If you want another random document, simply hit the Submit button again :)</p>
+        #                     <p style="font-size: 16px;">A few notes:</p>
+        #                     <ul style="font-size: 16px;">
+        #                         <li>When you write a query in CNF, note that <b>OR has higher precedence than AND</b> (which is contrary to conventions in boolean algebra).</li>
+        #                         <li>If the document is too long, it will be truncated to {MAX_OUTPUT_DOC_TOKENS} tokens.</li>
+        #                         <li>We can only include documents where all terms (or clauses) are separated by no more than {MAX_DIFF_TOKENS} tokens.</li>
+        #                         <li>If you query for two or more clauses, and a clause has more than {MAX_CLAUSE_FREQ_FAST_APPROX_PER_SHARD} matches (per shard), we will estimate the count from a random subset of all documents containing that clause. This might cause a zero count on conjuction of some simple n-grams (e.g., <b>birds AND oil</b>).</li>
+        #                         <li>The number of found documents may contain duplicates (e.g., if a document contains your query term twice, it may be counted twice).</li>
+        #                     </ul>
+        #                     <p style="font-size: 16px;">❗️WARNING: Corpus may contain problematic contents such as PII, toxicity, hate speech, and NSFW text. This tool is merely presenting selected text from the corpus, without any post-hoc safety filtering. It is NOT creating new text. This is a research prototype through which we can expose and examine existing problems with massive text corpora. Please use with caution. Don't be evil :)</p>
+        #                 ''')
+        #         with gr.Row():
+        #             with gr.Column(scale=1):
+        #                 ard_cnf_input = gr.Textbox(placeholder='Enter a query here', label='Query', interactive=True)
+        #                 with gr.Row():
+        #                     ard_cnf_clear = gr.ClearButton(value='Clear', variant='secondary', visible=True)
+        #                     ard_cnf_submit = gr.Button(value='Submit', variant='primary', visible=True)
+        #                 ard_cnf_output_tokens = gr.Textbox(label='Tokenized', lines=2, interactive=False)
+        #             with gr.Column(scale=1):
+        #                 ard_cnf_output_message = gr.Label(label='Message', num_top_classes=0)
+        #                 ard_cnf_output = gr.HighlightedText(label='Document', show_legend=False, color_map={"-": "red", "0": "green", "1": "cyan", "2": "blue", "3": "magenta"})
 
-        with gr.Row(visible=False) as row_6:
+        with gr.Row(visible=False) as row_6a:
             with gr.Column():
-                gr.HTML(f'''<h2>6. Searching for document containing n-gram(s)</h2>
-                            <p style="font-size: 16px;">This displays a random document in the corpus that satisfies your query. You can simply enter an n-gram, in which case the document displayed would contain your n-gram. You can also connect multiple n-gram terms with the AND/OR operators, in the <a href="https://en.wikipedia.org/wiki/Conjunctive_normal_form">CNF format</a>, in which case the displayed document contains n-grams such that it satisfies this logical constraint.</p>
+                gr.HTML(f'''<h2>6. Searching for documents containing n-gram(s)</h2>
+                            <p style="font-size: 16px;">This displays a few random documents in the corpus that satisfies your query. You can simply enter an n-gram, in which case the document displayed would contain your n-gram. You can also connect multiple n-gram terms with the AND/OR operators, in the <a href="https://en.wikipedia.org/wiki/Conjunctive_normal_form">CNF format</a>, in which case the displayed document contains n-grams such that it satisfies this logical constraint.</p>
                             <p style="font-size: 16px;">Example queries:</p>
                             <ul style="font-size: 16px;">
                                 <li><b>natural language processing</b> (the displayed document would contain "natural language processing")</li>
                                 <li><b>natural language processing AND deep learning</b> (the displayed document would contain both "natural language processing" and "deep learning")</li>
                                 <li><b>natural language processing OR artificial intelligence AND deep learning OR machine learning</b> (the displayed document would contain at least one of "natural language processing" / "artificial intelligence", and also at least one of "deep learning" / "machine learning")</li>
                             </ul>
-                            <p style="font-size: 16px;">If you want another random document, simply hit the Submit button again :)</p>
+                            <p style="font-size: 16px;">If you want another batch of random documents, simply hit the Submit button again :)</p>
                             <p style="font-size: 16px;">A few notes:</p>
                             <ul style="font-size: 16px;">
                                 <li>When you write a query in CNF, note that <b>OR has higher precedence than AND</b> (which is contrary to conventions in boolean algebra).</li>
                                 <li>If the document is too long, it will be truncated to {MAX_OUTPUT_DOC_TOKENS} tokens.</li>
                                 <li>We can only include documents where all terms (or clauses) are separated by no more than {MAX_DIFF_TOKENS} tokens.</li>
-                                <li>If you query for two or more clauses, and a clause has more than {MAX_CLAUSE_FREQ_FAST_APPROX_PER_SHARD} matches (per shard), we will search within a random subset of all documents containing that clause.</li>
+                                <li>If you query for two or more clauses, and a clause has more than {MAX_CLAUSE_FREQ_FAST_APPROX_PER_SHARD} matches (per shard), we will estimate the count from a random subset of all documents containing that clause. This might cause a zero count on conjuction of some simple n-grams (e.g., <b>birds AND oil</b>).</li>
                                 <li>The number of found documents may contain duplicates (e.g., if a document contains your query term twice, it may be counted twice).</li>
                             </ul>
                             <p style="font-size: 16px;">❗️WARNING: Corpus may contain problematic contents such as PII, toxicity, hate speech, and NSFW text. This tool is merely presenting selected text from the corpus, without any post-hoc safety filtering. It is NOT creating new text. This is a research prototype through which we can expose and examine existing problems with massive text corpora. Please use with caution. Don't be evil :)</p>
                         ''')
                 with gr.Row():
                     with gr.Column(scale=1):
-                        a_ard_cnf_input = gr.Textbox(placeholder='Enter a query here', label='Query', interactive=True)
+                        ard_cnf_multi_input = gr.Textbox(placeholder='Enter a query here', label='Query', interactive=True)
+                        ard_cnf_multi_maxnum = gr.Slider(minimum=1, maximum=10, value=1, step=1, label='Number of documents to Display')
                         with gr.Row():
-                            a_ard_cnf_clear = gr.ClearButton(value='Clear', variant='secondary', visible=True)
-                            a_ard_cnf_submit = gr.Button(value='Submit', variant='primary', visible=True)
-                        a_ard_cnf_output_tokens = gr.Textbox(label='Tokenized', lines=2, interactive=False)
+                            ard_cnf_multi_clear = gr.ClearButton(value='Clear', variant='secondary', visible=True)
+                            ard_cnf_multi_submit = gr.Button(value='Submit', variant='primary', visible=True)
+                        ard_cnf_multi_output_tokens = gr.Textbox(label='Tokenized', lines=2, interactive=False)
                     with gr.Column(scale=1):
-                        a_ard_cnf_output_message = gr.Label(label='Message', num_top_classes=0)
-                        a_ard_cnf_output = gr.HighlightedText(label='Document', show_legend=False, color_map={"-": "red", "0": "green", "1": "cyan", "2": "blue", "3": "magenta"})
+                        ard_cnf_multi_output_message = gr.Label(label='Message', num_top_classes=0)
+                        with gr.Tab(label='1'):
+                            ard_cnf_multi_output_0 = gr.HighlightedText(label='Document', show_legend=False, color_map={"-": "red", "0": "green", "1": "cyan", "2": "blue", "3": "magenta"})
+                        with gr.Tab(label='2'):
+                            ard_cnf_multi_output_1 = gr.HighlightedText(label='Document', show_legend=False, color_map={"-": "red", "0": "green", "1": "cyan", "2": "blue", "3": "magenta"})
+                        with gr.Tab(label='3'):
+                            ard_cnf_multi_output_2 = gr.HighlightedText(label='Document', show_legend=False, color_map={"-": "red", "0": "green", "1": "cyan", "2": "blue", "3": "magenta"})
+                        with gr.Tab(label='4'):
+                            ard_cnf_multi_output_3 = gr.HighlightedText(label='Document', show_legend=False, color_map={"-": "red", "0": "green", "1": "cyan", "2": "blue", "3": "magenta"})
+                        with gr.Tab(label='5'):
+                            ard_cnf_multi_output_4 = gr.HighlightedText(label='Document', show_legend=False, color_map={"-": "red", "0": "green", "1": "cyan", "2": "blue", "3": "magenta"})
+                        with gr.Tab(label='6'):
+                            ard_cnf_multi_output_5 = gr.HighlightedText(label='Document', show_legend=False, color_map={"-": "red", "0": "green", "1": "cyan", "2": "blue", "3": "magenta"})
+                        with gr.Tab(label='7'):
+                            ard_cnf_multi_output_6 = gr.HighlightedText(label='Document', show_legend=False, color_map={"-": "red", "0": "green", "1": "cyan", "2": "blue", "3": "magenta"})
+                        with gr.Tab(label='8'):
+                            ard_cnf_multi_output_7 = gr.HighlightedText(label='Document', show_legend=False, color_map={"-": "red", "0": "green", "1": "cyan", "2": "blue", "3": "magenta"})
+                        with gr.Tab(label='9'):
+                            ard_cnf_multi_output_8 = gr.HighlightedText(label='Document', show_legend=False, color_map={"-": "red", "0": "green", "1": "cyan", "2": "blue", "3": "magenta"})
+                        with gr.Tab(label='10'):
+                            ard_cnf_multi_output_9 = gr.HighlightedText(label='Document', show_legend=False, color_map={"-": "red", "0": "green", "1": "cyan", "2": "blue", "3": "magenta"})
 
         with gr.Row(visible=False) as row_7:
             with gr.Column():
@@ -185,18 +267,20 @@ If you find this tool useful, please kindly cite our paper:
 
     count_clear.add([count_input, count_output, count_output_tokens])
     ngram_clear.add([ngram_input, ngram_output, ngram_output_tokens])
-    a_ntd_clear.add([a_ntd_input, a_ntd_output, a_ntd_output_tokens])
+    ntd_clear.add([ntd_input, ntd_output, ntd_output_tokens])
     infgram_clear.add([infgram_input, infgram_output, infgram_output_tokens])
-    a_infntd_clear.add([a_infntd_input, a_infntd_output, a_infntd_output_tokens, a_infntd_longest_suffix])
-    a_ard_cnf_clear.add([a_ard_cnf_input, a_ard_cnf_output, a_ard_cnf_output_tokens, a_ard_cnf_output_message])
+    infntd_clear.add([infntd_input, infntd_output, infntd_output_tokens, infntd_longest_suffix])
+    # ard_cnf_clear.add([ard_cnf_input, ard_cnf_output, ard_cnf_output_tokens, ard_cnf_output_message])
+    ard_cnf_multi_clear.add([ard_cnf_multi_input, ard_cnf_multi_output_tokens, ard_cnf_multi_output_message, ard_cnf_multi_output_0, ard_cnf_multi_output_1, ard_cnf_multi_output_2, ard_cnf_multi_output_3, ard_cnf_multi_output_4, ard_cnf_multi_output_5, ard_cnf_multi_output_6, ard_cnf_multi_output_7, ard_cnf_multi_output_8, ard_cnf_multi_output_9])
     doc_analysis_clear.add([doc_analysis_input, doc_analysis_output])
 
     count_submit.click(process, inputs=[corpus_desc, query_desc, count_input], outputs=[count_output, count_output_tokens])
     ngram_submit.click(process, inputs=[corpus_desc, query_desc, ngram_input], outputs=[ngram_output, ngram_output_tokens])
-    a_ntd_submit.click(process, inputs=[corpus_desc, query_desc, a_ntd_input], outputs=[a_ntd_output, a_ntd_output_tokens])
+    ntd_submit.click(process, inputs=[corpus_desc, query_desc, ntd_input], outputs=[ntd_output, ntd_output_tokens])
     infgram_submit.click(process, inputs=[corpus_desc, query_desc, infgram_input], outputs=[infgram_output, infgram_output_tokens, infgram_longest_suffix])
-    a_infntd_submit.click(process, inputs=[corpus_desc, query_desc, a_infntd_input], outputs=[a_infntd_output, a_infntd_output_tokens, a_infntd_longest_suffix])
-    a_ard_cnf_submit.click(process, inputs=[corpus_desc, query_desc, a_ard_cnf_input], outputs=[a_ard_cnf_output, a_ard_cnf_output_tokens, a_ard_cnf_output_message])
+    infntd_submit.click(process, inputs=[corpus_desc, query_desc, infntd_input], outputs=[infntd_output, infntd_output_tokens, infntd_longest_suffix])
+    # ard_cnf_submit.click(process, inputs=[corpus_desc, query_desc, ard_cnf_input], outputs=[ard_cnf_output, ard_cnf_output_tokens, ard_cnf_output_message])
+    ard_cnf_multi_submit.click(process_ard_cnf_multi, inputs=[corpus_desc, query_desc, ard_cnf_multi_input, ard_cnf_multi_maxnum], outputs=[ard_cnf_multi_output_tokens, ard_cnf_multi_output_message, ard_cnf_multi_output_0, ard_cnf_multi_output_1, ard_cnf_multi_output_2, ard_cnf_multi_output_3, ard_cnf_multi_output_4, ard_cnf_multi_output_5, ard_cnf_multi_output_6, ard_cnf_multi_output_7, ard_cnf_multi_output_8, ard_cnf_multi_output_9])
     doc_analysis_submit.click(process, inputs=[corpus_desc, query_desc, doc_analysis_input], outputs=[doc_analysis_output])
 
     def update_query_desc(selection):
@@ -206,7 +290,8 @@ If you find this tool useful, please kindly cite our paper:
             row_3: gr.Row(visible=(selection == QUERY_DESC_BY_TYPE['get_next_token_distribution_approx'])),
             row_4: gr.Row(visible=(selection == QUERY_DESC_BY_TYPE['compute_infgram_prob'])),
             row_5: gr.Row(visible=(selection == QUERY_DESC_BY_TYPE['get_infgram_next_token_distribution_approx'])),
-            row_6: gr.Row(visible=(selection == QUERY_DESC_BY_TYPE['get_a_random_document_from_cnf_query_fast_approx'])),
+            # row_6: gr.Row(visible=(selection == QUERY_DESC_BY_TYPE['get_a_random_document_from_cnf_query_fast_approx'])),
+            row_6a: gr.Row(visible=(selection == QUERY_DESC_BY_TYPE['get_random_documents_from_cnf_query_fast_approx'])),
             # row_7: gr.Row(visible=(selection == QUERY_DESC_BY_TYPE['analyze_document'])),
         }
     query_desc.change(fn=update_query_desc, inputs=query_desc, outputs=[
@@ -215,7 +300,8 @@ If you find this tool useful, please kindly cite our paper:
         row_3,
         row_4,
         row_5,
-        row_6,
+        # row_6,
+        row_6a,
         # row_7,
     ])
 

constants.py

@@ -12,20 +12,21 @@ QUERY_TYPE_BY_DESC = {
     '3. Compute the next-token distribution of an (n-1)-gram': 'get_next_token_distribution_approx',
     '4. Compute the ∞-gram probability of the last token': 'compute_infgram_prob',
     '5. Compute the ∞-gram next-token distribution': 'get_infgram_next_token_distribution_approx',
-    '6. Searching for document containing n-gram(s)': 'get_a_random_document_from_cnf_query_fast_approx',
+    # '6. Searching for document containing n-gram(s)': 'get_a_random_document_from_cnf_query_fast_approx',
+    '6. Searching for documents containing n-gram(s)': 'get_random_documents_from_cnf_query_fast_approx',
     # '7. Analyze an (AI-generated) document using ∞-gram': 'analyze_document',
 }
 QUERY_DESC_BY_TYPE = {v: k for k, v in QUERY_TYPE_BY_DESC.items()}
 QUERY_DESCS = list(QUERY_TYPE_BY_DESC.keys())
 
-MAX_QUERY_CHARS = os.environ.get('MAX_QUERY_CHARS', 1000)
-MAX_INPUT_DOC_TOKENS = os.environ.get('MAX_INPUT_DOC_TOKENS', 1000)
-MAX_OUTPUT_DOC_TOKENS = os.environ.get('MAX_OUTPUT_DOC_TOKENS', 5000)
-MAX_CNT_FOR_NTD = os.environ.get('MAX_CNT_FOR_NTD', 1000)
-MAX_CLAUSE_FREQ = os.environ.get('MAX_CLAUSE_FREQ', 10000)
-MAX_CLAUSE_FREQ_FAST = os.environ.get('MAX_CLAUSE_FREQ_FAST', 1000000)
-MAX_CLAUSE_FREQ_FAST_APPROX_PER_SHARD = os.environ.get('MAX_CLAUSE_FREQ_FAST_APPROX_PER_SHARD', 50000)
-MAX_DIFF_TOKENS = os.environ.get('MAX_DIFF_TOKENS', 100)
+MAX_QUERY_CHARS = int(os.environ.get('MAX_QUERY_CHARS', 1000))
+MAX_INPUT_DOC_TOKENS = int(os.environ.get('MAX_INPUT_DOC_TOKENS', 1000))
+MAX_OUTPUT_DOC_TOKENS = int(os.environ.get('MAX_OUTPUT_DOC_TOKENS', 5000))
+MAX_CNT_FOR_NTD = int(os.environ.get('MAX_CNT_FOR_NTD', 1000))
+MAX_CLAUSE_FREQ = int(os.environ.get('MAX_CLAUSE_FREQ', 10000))
+MAX_CLAUSE_FREQ_FAST = int(os.environ.get('MAX_CLAUSE_FREQ_FAST', 1000000))
+MAX_CLAUSE_FREQ_FAST_APPROX_PER_SHARD = int(os.environ.get('MAX_CLAUSE_FREQ_FAST_APPROX_PER_SHARD', 50000))
+MAX_DIFF_TOKENS = int(os.environ.get('MAX_DIFF_TOKENS', 100))
 MAX_DIFF_BYTES = 2 * MAX_DIFF_TOKENS
-MAX_CLAUSES_IN_CNF = os.environ.get('MAX_CLAUSES_IN_CNF', 4)
-MAX_TERMS_IN_DISJ_CLAUSE = os.environ.get('MAX_TERMS_IN_DISJ_CLAUSE', 4)
+MAX_CLAUSES_IN_CNF = int(os.environ.get('MAX_CLAUSES_IN_CNF', 4))
+MAX_TERMS_IN_DISJ_CLAUSE = int(os.environ.get('MAX_TERMS_IN_DISJ_CLAUSE', 4))