Added preprocessing pass that propagates unconstrained values - solves all of

the unconstrained examples in QF_AUFBV/brummayerbiere3 - should also help
generally on at least BV and maybe others.
Off by default for now - results are mixed and it's hard to evaluate with so
many existing assertion failures and segfaults - will re-evaluate once those
are fixed

3 files changed, 32 insertions, 0 deletions

diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index ade887b23..b9db8dace 100644
--- a/src/parser/smt/smt.cpp
+++ b/src/parser/smt/smt.cpp
@@ -49,6 +49,8 @@ std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> Smt::newL
   logicMap["QF_UFNRA"] = QF_UFNRA;
   logicMap["QF_ABV"] = QF_ABV;
   logicMap["QF_AUFBV"] = QF_AUFBV;
+  logicMap["QF_AUFBVLIA"] = QF_AUFBVLIA;
+  logicMap["QF_AUFBVLRA"] = QF_AUFBVLRA;
   logicMap["QF_UFNIRA"] = QF_UFNIRA;
   logicMap["QF_AUFLIA"] = QF_AUFLIA;
   logicMap["QF_AUFLIRA"] = QF_AUFLIRA;
@@ -219,6 +221,20 @@ void Smt::setLogic(const std::string& name) {
     addTheory(THEORY_BITVECTORS);
     break;
 
+  case QF_AUFBVLIA:
+    addUf();
+    addTheory(THEORY_ARRAYS_EX);
+    addTheory(THEORY_BITVECTORS);
+    addTheory(THEORY_INTS);
+    break;
+
+  case QF_AUFBVLRA:
+    addUf();
+    addTheory(THEORY_ARRAYS_EX);
+    addTheory(THEORY_BITVECTORS);
+    addTheory(THEORY_REALS);
+    break;
+
   case QF_AUFLIA:
     addTheory(THEORY_INT_ARRAYS_EX);
     addUf();
diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h
index 1606d7bab..34ec624bc 100644
--- a/src/parser/smt/smt.h
+++ b/src/parser/smt/smt.h
@@ -42,6 +42,8 @@ public:
     LRA,
     QF_ABV,
     QF_AUFBV,
+    QF_AUFBVLIA,
+    QF_AUFBVLRA,
     QF_AUFLIA,
     QF_AUFLIRA,
     QF_AX,
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index dc1b47bde..3fa00baae 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -166,6 +166,20 @@ void Smt2::setLogic(const std::string& name) {
     addTheory(THEORY_BITVECTORS);
     break;
 
+  case Smt::QF_AUFBVLIA:
+    addOperator(kind::APPLY_UF);
+    addTheory(THEORY_ARRAYS);
+    addTheory(THEORY_BITVECTORS);
+    addTheory(THEORY_INTS);
+    break;
+
+  case Smt::QF_AUFBVLRA:
+    addOperator(kind::APPLY_UF);
+    addTheory(THEORY_ARRAYS);
+    addTheory(THEORY_BITVECTORS);
+    addTheory(THEORY_REALS);
+    break;
+
   case Smt::QF_AUFLIA:
     addTheory(THEORY_ARRAYS);
     addOperator(kind::APPLY_UF);