From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 18 Sep 2019 20:03:12 +0000 (-0500)
Subject: Decouple fmf-bound and finite-model-find (#3297)
X-Git-Tag: cvc5-1.0.0~3940
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a9c40f60e4b36494e10520dcc3a3985b4700342f;p=cvc5.git

Decouple fmf-bound and finite-model-find (#3297)
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 6d80207a6..fa318aaf1 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1215,43 +1215,39 @@ void SmtEngine::setDefaults() {
     d_logic = LogicInfo("QF_BV");
   }
 
-  // set strings-exp
-  /* - disabled for 1.4 release [MGD 2014.06.25]
-  if(!d_logic.hasEverything() && d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
-    if(! options::stringExp.wasSetByUser()) {
-      options::stringExp.set( true );
-      Trace("smt") << "turning on strings-exp, for the theory of strings" << std::endl;
-    }
-  }
-  */
-  // for strings
-  if(options::stringExp()) {
-    if( !d_logic.isQuantified() ) {
+  // set default options associated with strings-exp
+  if (options::stringExp())
+  {
+    // We require quantifiers since extended functions reduce using them
+    if (!d_logic.isQuantified())
+    {
       d_logic = d_logic.getUnlockedCopy();
       d_logic.enableQuantifiers();
       d_logic.lock();
       Trace("smt") << "turning on quantifier logic, for strings-exp"
                    << std::endl;
     }
-    if(! options::fmfBound.wasSetByUser()) {
+    // We require bounded quantifier handling.
+    if (!options::fmfBound.wasSetByUser())
+    {
       options::fmfBound.set( true );
       Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
     }
-    if(! options::fmfInstEngine.wasSetByUser()) {
-      options::fmfInstEngine.set( true );
-      Trace("smt") << "turning on fmf-inst-engine, for strings-exp" << std::endl;
+    // Turn off E-matching, since some bounded quantifiers introduced by strings
+    // (e.g. for replaceall) admit matching loops.
+    if (!options::eMatching.wasSetByUser())
+    {
+      options::eMatching.set(false);
+      Trace("smt") << "turning off E-matching, for strings-exp" << std::endl;
     }
-    /*
-    if(! options::rewriteDivk.wasSetByUser()) {
-      options::rewriteDivk.set( true );
-      Trace("smt") << "turning on rewrite-divk, for strings-exp" << std::endl;
-    }*/
-    /*
-    if(! options::stringFMF.wasSetByUser()) {
-      options::stringFMF.set( true );
-      Trace("smt") << "turning on strings-fmf, for strings-exp" << std::endl;
+    // Do not eliminate extended arithmetic symbols from quantified formulas,
+    // since some strategies, e.g. --re-elim-agg, introduce them.
+    if (!options::elimExtArithQuant.wasSetByUser())
+    {
+      options::elimExtArithQuant.set(false);
+      Trace("smt") << "turning off elim-ext-arith-quant, for strings-exp"
+                   << std::endl;
     }
-    */
   }
 
   // sygus inference may require datatypes
@@ -1808,8 +1804,6 @@ void SmtEngine::setDefaults() {
   //now have determined whether fmfBoundInt is on/off
   //apply fmfBoundInt options
   if( options::fmfBound() ){
-    //must have finite model finding on
-    options::finiteModelFind.set( true );
     if (!options::mbqiMode.wasSetByUser()
         || (options::mbqiMode() != quantifiers::MBQI_NONE
             && options::mbqiMode() != quantifiers::MBQI_FMC))
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 1eb62945b..e399af71d 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -138,13 +138,13 @@ class QuantifiersEnginePrivate
       modules.push_back(d_synth_e.get());
     }
     // finite model finding
-    if (options::finiteModelFind())
+    if (options::fmfBound())
+    {
+      d_bint.reset(new quantifiers::BoundedIntegers(c, qe));
+      modules.push_back(d_bint.get());
+    }
+    if (options::finiteModelFind() || options::fmfBound())
     {
-      if (options::fmfBound())
-      {
-        d_bint.reset(new quantifiers::BoundedIntegers(c, qe));
-        modules.push_back(d_bint.get());
-      }
       d_model_engine.reset(new quantifiers::ModelEngine(c, qe));
       modules.push_back(d_model_engine.get());
       // finite model finder has special ways of building the model
diff --git a/test/regress/regress0/fmf/fmf-strange-bounds-2.smt2 b/test/regress/regress0/fmf/fmf-strange-bounds-2.smt2
index f1c53c4ef..1e289d94f 100644
--- a/test/regress/regress0/fmf/fmf-strange-bounds-2.smt2
+++ b/test/regress/regress0/fmf/fmf-strange-bounds-2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fmf-bound
+; COMMAND-LINE: --finite-model-find --fmf-bound
 ; EXPECT: unsat
 (set-logic ALL)
 (set-info :status unsat)
diff --git a/test/regress/regress1/fmf/bound-int-alt.smt2 b/test/regress/regress1/fmf/bound-int-alt.smt2
index 146487925..57fbe66bb 100644
--- a/test/regress/regress1/fmf/bound-int-alt.smt2
+++ b/test/regress/regress1/fmf/bound-int-alt.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fmf-bound-int
+; COMMAND-LINE: --finite-model-find --fmf-bound-int
 ; EXPECT: sat
 (set-logic UFLIA)
 (set-info :status sat)
diff --git a/test/regress/regress2/quantifiers/net-policy-no-time.smt2 b/test/regress/regress2/quantifiers/net-policy-no-time.smt2
index 6dcb47201..938aa01ea 100644
--- a/test/regress/regress2/quantifiers/net-policy-no-time.smt2
+++ b/test/regress/regress2/quantifiers/net-policy-no-time.smt2
@@ -1,5 +1,6 @@
 (set-logic UFDTLIRA)
 (set-option :fmf-bound true)
+(set-option :finite-model-find true)
 (set-option :produce-models true)
 (set-info :status sat)