Use FS as the set-logic string for theory of sets

diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp
index 79168e06a84db2de86d354d8fc5b9a6448c68cd2..7390eefe0d1b31dfc78f51d20eef9ae6e2351e06 100644 (file)
--- 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 78f4996b8ddaf728083844213984d5bd2dfb26bb..bc2f1286b26d44ae90053c4f9f5789b0da10c3c8 100644 (file)
--- 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 b4ddfec41e29623a258710575a07829fc9d8c469..9af45c2ddd7df16b340fbbd2cae4a492e8b8144a 100644 (file)
--- 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 1241b117ffc1e116842838ff029bed1d3ed04b28..bf1822305cd94cc1266b385d0b51b766d8db78a4 100644 (file)
--- 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 e7a7be97ac872ae2cea300982050061eb2cd1de6..24679749c3cd0c43b4675001bbf942153b6aace7 100644 (file)
--- 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 650c0ead16ae1fc53da8099f7a29adf87359579a..e12b74d18b72536029d64143aa6f493d6256704a 100644 (file)
--- 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 536d62d3d3a1823294fb46e2e320654fb6b35526..5e7c032eaec6f7888b4c5e1851a2d826f60a1d13 100644 (file)
--- 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 3a7b18179e150a2d9a0c29858abac00b805c904f..b4936a32b94f59c5137cca066c696cda46c850dd 100644 (file)
--- 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 4a588aeb6e8330c9ddfc8e72595192cbe33d7489..2ef07f9200d635ae768982ec16ed4103b742ffc6 100644 (file)
--- 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 c10b14f2b14aff137df272840d47c119141c98e7..2bf2d4c62a921b22a3389bf4213b018741832d38 100644 (file)
--- 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 61af2124d54154c44fd14c7c697f7c1bb22fa5a0..d851ca35e832cb239022f00b0bc75eded5c2abb6 100644 (file)
--- 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 896b13219c0cb2ff601628bd9a6fa3b7853b84e4..635c7959d5823c8b9b0fbae19f33021f73b72906 100644 (file)
--- 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 22e029b69ddf3654d8bb647448748977bf12dd19..d6565205b33472565b939852433acc57300904c5 100644 (file)
--- 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 e5defb2accf21915f748085f0ca52efc23cb1469..61fbee11d5fd6a973c7092ddd95f21226dbff9ee 100644 (file)
--- 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 18ad053d6234213ffccd29bc018fef7d01fc456d..1702aab2789feefea25532105c27d1cf916ab13f 100644 (file)
--- 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 65f55f3a6a71e0fed1a1002310fe560106845dd5..3acf77108b03e5ebef963ed98f97bfcadcd28aa1 100644 (file)
--- 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 9dd25740115f526ebe68c76ddf193f666eac957e..e68520cbf826f8e24675ddec5ed2e06d55e3447e 100644 (file)
--- 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 16e7780b4f882d7704c0c1e434e39c27d9c6b98d..bc18235f030ea7772ad44572afd80742d3ea6380 100644 (file)
--- 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 183f542425d37a6a29963c35a3213b963a2fbe46..aee8c5937b4012682d37b58d6718d66eb4ad1d03 100644 (file)
--- 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 b388bb534dbd2bedc30ba44da1d95f6aa8e86af4..b875798167dd1d8a5b18637ae789887ff43747df 100644 (file)
--- 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))