From fa53ae111cd314f455456a884f1247bb9b8e2c7b Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Mon, 30 Jun 2014 10:53:52 -0400
Subject: [PATCH] Use FS as the set-logic string for theory of sets

---
 examples/api/sets.cpp                                       | 4 ++++
 src/theory/logic_info.cpp                                   | 6 +++---
 test/regress/regress0/sets/copy_check_heap_access_33_4.smt2 | 2 +-
 test/regress/regress0/sets/error1.smt2                      | 2 +-
 test/regress/regress0/sets/fuzz14418.smt2                   | 2 +-
 test/regress/regress0/sets/fuzz15201.smt2                   | 2 +-
 test/regress/regress0/sets/fuzz31811.smt2                   | 2 +-
 test/regress/regress0/sets/insert.smt2                      | 2 +-
 test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2 | 2 +-
 .../regress/regress0/sets/jan24/remove_check_free_31_6.smt2 | 2 +-
 test/regress/regress0/sets/mar2014/sharing-preregister.smt2 | 2 +-
 test/regress/regress0/sets/mar2014/small.smt2               | 2 +-
 test/regress/regress0/sets/mar2014/smaller.smt2             | 2 +-
 .../regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 | 2 +-
 test/regress/regress0/sets/setofsets-disequal.smt2          | 2 +-
 test/regress/regress0/sets/sets-disequal.smt2               | 2 +-
 test/regress/regress0/sets/sets-testlemma-ints.smt2         | 2 +-
 test/regress/regress0/sets/sets-testlemma-reals.smt2        | 2 +-
 test/regress/regress0/sets/sets-testlemma.smt2              | 2 +-
 test/regress/regress0/sets/sharingbug.smt2                  | 2 +-
 20 files changed, 25 insertions(+), 21 deletions(-)

diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp
index 79168e06a..7390eefe0 100644
--- a/examples/api/sets.cpp
+++ b/examples/api/sets.cpp
@@ -26,6 +26,10 @@ int main() {
   ExprManager em;
   SmtEngine smt(&em);
 
+  // Optionally, set the logic. We need at least UF for equality predicate,
+  // integers (LIA) and sets (FS).
+  smt.setLogic("QF_UFLIAFS");
+
   // Produce models
   smt.setOption("produce-models", true);
 
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 78f4996b8..bc2f1286b 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -129,7 +129,7 @@ std::string LogicInfo::getLogicString() const {
         ++seen;
       }
       if(d_theories[THEORY_SETS]) {
-        ss << "_SETS";
+        ss << "FS";
         ++seen;
       }
 
@@ -272,9 +272,9 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc
         arithNonLinear();
         p += 4;
       }
-      if(!strncmp(p, "_SETS", 5)) {
+      if(!strncmp(p, "FS", 2)) {
         enableTheory(THEORY_SETS);
-        p += 5;
+        p += 2;
       }
     }
   }
diff --git a/test/regress/regress0/sets/copy_check_heap_access_33_4.smt2 b/test/regress/regress0/sets/copy_check_heap_access_33_4.smt2
index b4ddfec41..9af45c2dd 100644
--- a/test/regress/regress0/sets/copy_check_heap_access_33_4.smt2
+++ b/test/regress/regress0/sets/copy_check_heap_access_33_4.smt2
@@ -1,7 +1,7 @@
 ; COMMAND-LINE: --full-saturate-quant
 ; EXPECT: unsat
 (set-option :print-success false)
-(set-logic AUFLIA_SETS)
+(set-logic AUFLIAFS)
 (set-info :status unsat)
 (declare-sort Loc 0)
 (define-sort SetLoc () (Set Loc))
diff --git a/test/regress/regress0/sets/error1.smt2 b/test/regress/regress0/sets/error1.smt2
index 1241b117f..bf1822305 100644
--- a/test/regress/regress0/sets/error1.smt2
+++ b/test/regress/regress0/sets/error1.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: sat
-(set-logic QF_UFLIA_SETS)
+(set-logic QF_UFLIAFS)
 (set-info :status sat)
 (declare-fun A () (Set Int))
 (declare-fun C () (Set Int))
diff --git a/test/regress/regress0/sets/fuzz14418.smt2 b/test/regress/regress0/sets/fuzz14418.smt2
index e7a7be97a..24679749c 100644
--- a/test/regress/regress0/sets/fuzz14418.smt2
+++ b/test/regress/regress0/sets/fuzz14418.smt2
@@ -11,7 +11,7 @@
 (set-info :smt-lib-version 2.0)
 (set-info :category "random")
 (set-info :status sat)
-(set-logic QF_UFLIA_SETS)
+(set-logic QF_UFLIAFS)
 (define-sort Element () Int)
 (declare-fun f0 ( Int) Int)
 (declare-fun f1 ( (Set Element) (Set Element) (Set Element)) (Set Element))
diff --git a/test/regress/regress0/sets/fuzz15201.smt2 b/test/regress/regress0/sets/fuzz15201.smt2
index 650c0ead1..e12b74d18 100644
--- a/test/regress/regress0/sets/fuzz15201.smt2
+++ b/test/regress/regress0/sets/fuzz15201.smt2
@@ -4,7 +4,7 @@
 (set-info :smt-lib-version 2.0)
 (set-info :category "random")
 (set-info :status sat)
-(set-logic QF_UFLIA_SETS)
+(set-logic QF_UFLIAFS)
 (define-sort Element () Int)
 (declare-fun f0 ( Int) Int)
 (declare-fun f1 ( (Set Element)) (Set Element))
diff --git a/test/regress/regress0/sets/fuzz31811.smt2 b/test/regress/regress0/sets/fuzz31811.smt2
index 536d62d3d..5e7c032ea 100644
--- a/test/regress/regress0/sets/fuzz31811.smt2
+++ b/test/regress/regress0/sets/fuzz31811.smt2
@@ -9,7 +9,7 @@
 (set-info :smt-lib-version 2.0)
 (set-info :category "random")
 (set-info :status sat)
-(set-logic QF_UFLIA_SETS)
+(set-logic QF_UFLIAFS)
 (define-sort Element () Int)
 (declare-fun f0 ( Int Int Int) Int)
 (declare-fun f1 ( (Set Element) (Set Element)) (Set Element))
diff --git a/test/regress/regress0/sets/insert.smt2 b/test/regress/regress0/sets/insert.smt2
index 3a7b18179..b4936a32b 100644
--- a/test/regress/regress0/sets/insert.smt2
+++ b/test/regress/regress0/sets/insert.smt2
@@ -1,5 +1,5 @@
 (set-option :produce-models true)
-(set-logic QF_UFLIA_SETS)
+(set-logic QF_UFLIAFS)
 (set-info :status sat)
 (declare-fun X () (Set Int))
 (assert (= X (insert 1 2 (singleton 3))))
diff --git a/test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2 b/test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2
index 4a588aeb6..2ef07f920 100644
--- a/test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2
+++ b/test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2
@@ -1,5 +1,5 @@
 (set-option :print-success false)
-(set-logic AUFLIA_SETS)
+(set-logic AUFLIAFS)
 (set-info :status unsat)
 (declare-sort Loc 0)
 (define-sort SetLoc () (Set Loc))
diff --git a/test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2 b/test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2
index c10b14f2b..2bf2d4c62 100644
--- a/test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2
+++ b/test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2
@@ -1,5 +1,5 @@
 (set-option :print-success false)
-(set-logic AUFLIA_SETS)
+(set-logic AUFLIAFS)
 (set-info :status unsat)
 (declare-sort Loc 0)
 (define-sort SetLoc () (Set Loc))
diff --git a/test/regress/regress0/sets/mar2014/sharing-preregister.smt2 b/test/regress/regress0/sets/mar2014/sharing-preregister.smt2
index 61af2124d..d851ca35e 100644
--- a/test/regress/regress0/sets/mar2014/sharing-preregister.smt2
+++ b/test/regress/regress0/sets/mar2014/sharing-preregister.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-(set-logic QF_UFLIA_SETS)
+(set-logic QF_UFLIAFS)
 (set-info :status sat)
 (declare-fun a () Int)
 (declare-fun b () Int)
diff --git a/test/regress/regress0/sets/mar2014/small.smt2 b/test/regress/regress0/sets/mar2014/small.smt2
index 896b13219..635c7959d 100644
--- a/test/regress/regress0/sets/mar2014/small.smt2
+++ b/test/regress/regress0/sets/mar2014/small.smt2
@@ -4,7 +4,7 @@
 ; demostrates core issue with UniqueZipper.hs.1030minimized.cvc4.smt2
 ; unlike original benchmark, this is unsat.
 
-(set-logic QF_UFLIA_SETS)
+(set-logic QF_UFLIAFS)
 (declare-fun x () Int)
 (declare-fun y () Int)
 (declare-fun z () Int)
diff --git a/test/regress/regress0/sets/mar2014/smaller.smt2 b/test/regress/regress0/sets/mar2014/smaller.smt2
index 22e029b69..d6565205b 100644
--- a/test/regress/regress0/sets/mar2014/smaller.smt2
+++ b/test/regress/regress0/sets/mar2014/smaller.smt2
@@ -4,7 +4,7 @@
 ; demostrates core issue with UniqueZipper.hs.1030minimized.cvc4.smt2
 ; fails check-model, even though answer is correct
 
-(set-logic QF_UFLIA_SETS)
+(set-logic QF_UFLIAFS)
 (declare-fun x () Int)
 (declare-fun y () Int)
 (declare-fun a () (Set Int))
diff --git a/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 b/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2
index e5defb2ac..61fbee11d 100644
--- a/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2
+++ b/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2
@@ -1,5 +1,5 @@
 (set-option :print-success false)
-(set-logic AUFLIA_SETS)
+(set-logic AUFLIAFS)
 (set-info :status unsat)
 (declare-sort Loc 0)
 (define-sort SetLoc () (Set Loc))
diff --git a/test/regress/regress0/sets/setofsets-disequal.smt2 b/test/regress/regress0/sets/setofsets-disequal.smt2
index 18ad053d6..1702aab27 100644
--- a/test/regress/regress0/sets/setofsets-disequal.smt2
+++ b/test/regress/regress0/sets/setofsets-disequal.smt2
@@ -1,7 +1,7 @@
 ; On a production build (as of 2014-05-16), takes several minutes
 ; to finish (2967466 decisions).
 
-(set-logic QF_BV_SETS)
+(set-logic QF_BVFS)
 (set-info :status unsat)
 
 (define-sort myset () (Set (Set (_ BitVec 1))))
diff --git a/test/regress/regress0/sets/sets-disequal.smt2 b/test/regress/regress0/sets/sets-disequal.smt2
index 65f55f3a6..3acf77108 100644
--- a/test/regress/regress0/sets/sets-disequal.smt2
+++ b/test/regress/regress0/sets/sets-disequal.smt2
@@ -3,7 +3,7 @@
 ; EXPECT: sat
 ; EXPECT: unsat
 ; EXIT: 0
-(set-logic QF_BV_SETS)
+(set-logic QF_BVFS)
 (declare-fun S1 () (Set (_ BitVec 1)))
 (declare-fun S2 () (Set (_ BitVec 1)))
 (declare-fun S3 () (Set (_ BitVec 1)))
diff --git a/test/regress/regress0/sets/sets-testlemma-ints.smt2 b/test/regress/regress0/sets/sets-testlemma-ints.smt2
index 9dd257401..e68520cbf 100644
--- a/test/regress/regress0/sets/sets-testlemma-ints.smt2
+++ b/test/regress/regress0/sets/sets-testlemma-ints.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: sat
-(set-logic QF_UFLIA_SETS)
+(set-logic QF_UFLIAFS)
 (set-info :status sat)
 (declare-fun x () (Set Int))
 (declare-fun y () (Set Int))
diff --git a/test/regress/regress0/sets/sets-testlemma-reals.smt2 b/test/regress/regress0/sets/sets-testlemma-reals.smt2
index 16e7780b4..bc18235f0 100644
--- a/test/regress/regress0/sets/sets-testlemma-reals.smt2
+++ b/test/regress/regress0/sets/sets-testlemma-reals.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: sat
-(set-logic QF_UFLRA_SETS)
+(set-logic QF_UFLRAFS)
 (set-info :status sat)
 (declare-fun x () (Set Real))
 (declare-fun y () (Set Real))
diff --git a/test/regress/regress0/sets/sets-testlemma.smt2 b/test/regress/regress0/sets/sets-testlemma.smt2
index 183f54242..aee8c5937 100644
--- a/test/regress/regress0/sets/sets-testlemma.smt2
+++ b/test/regress/regress0/sets/sets-testlemma.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: sat
-(set-logic QF_UFBV_SETS)
+(set-logic QF_UFBVFS)
 (set-info :status sat)
 (declare-fun x () (Set (_ BitVec 2)))
 (declare-fun y () (Set (_ BitVec 2)))
diff --git a/test/regress/regress0/sets/sharingbug.smt2 b/test/regress/regress0/sets/sharingbug.smt2
index b388bb534..b87579816 100644
--- a/test/regress/regress0/sets/sharingbug.smt2
+++ b/test/regress/regress0/sets/sharingbug.smt2
@@ -2,7 +2,7 @@
 (set-info :smt-lib-version 2.0)
 (set-info :category "random")
 (set-info :status sat)
-(set-logic QF_UFLIA_SETS)
+(set-logic QF_UFLIAFS)
 (define-sort Element () Int)
 (declare-fun f0 ( Int Int Int) Int)
 (declare-fun f1 ( (Set Element)) (Set Element))
-- 
2.30.2