Fix to consider leafs of theory sets to be variables (#8305)

Fixes cvc5/cvc5-projects#494.

With this fix, we now properly consider terms that belong to other theories that are of set type, e.g. (select x (as set.universe (Set RoundingMode)) in this example to be "variables" according to the theory of sets procedure.

The benchmark is unsat because there are 5 rounding modes and we are selecting an index in a sequence storing "false" at the first 6 indices.

diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp
index 3f619dcade2f24b75a571e0c562c5ed2e8225e78..62ae32a145f6639ca0db730e9ab7824094e9acc0 100644 (file)
--- a/src/theory/sets/solver_state.cpp
+++ b/src/theory/sets/solver_state.cpp
@@ -141,10 +141,12 @@ void SolverState::registerTerm(Node r, TypeNode tnn, Node n)
     d_allCompSets.push_back(n);
     Trace("sets-debug2") << "Comp-set[" << r << "] : " << n << std::endl;
   }
-  else if (n.isVar() && !d_skCache.isSkolem(n))
+  else if (Theory::isLeafOf(n, THEORY_SETS) && !d_skCache.isSkolem(n))
   {
-    // it is important that we check it is a variable, but not an internally
-    // introduced skolem, due to the semantics of the universe set.
+    // It is important that we check it is a leaf, due to parametric theories
+    // that may be used to construct terms of set type. It is also important to
+    // exclude internally introduced skolems, due to the semantics of the
+    // universe set.
     if (tnn.isSet())
     {
       if (d_var_set.find(r) == d_var_set.end())

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 84aebd5ae52a02d309c87441ea3e880066f6e1cb..398c08cbbc5636f328d5b0de8497727fa60c84db 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2411,6 +2411,7 @@ set(regress_1_tests
   regress1/sets/lemmabug-ListElts317minimized.smt2
   regress1/sets/proj-issue164.smt2
   regress1/sets/proj-issue178.smt2
+  regress1/sets/proj-issue494-finite-leafof.smt2
   regress1/sets/remove_check_free_31_6.smt2
   regress1/sets/sets-disequal.smt2
   regress1/sets/sets-tuple-poly.cvc.smt2

diff --git a/test/regress/regress1/sets/proj-issue494-finite-leafof.smt2 b/test/regress/regress1/sets/proj-issue494-finite-leafof.smt2
new file mode 100644 (file)
index 0000000..24f0a51
--- /dev/null
+++ b/test/regress/regress1/sets/proj-issue494-finite-leafof.smt2
@@ -0,0 +1,9 @@
+(set-logic ALL)
+(set-info :status unsat)
+(set-option :strings-exp true)
+(set-option :sets-ext true)
+(declare-const x (Array (Set RoundingMode) (Set RoundingMode)))
+(check-sat-assuming (
+(seq.nth 
+(seq.++ (seq.++ (seq.unit false) (seq.unit false)) (seq.++ (seq.unit false) (seq.unit false)) (seq.++ (seq.unit false) (seq.unit false))) 
+(set.card (select x (as set.universe (Set RoundingMode)))))))