Do not solve for 0-ary non-constant symbols (for which isVar returns true), add regre...

diff --git a/src/expr/node.h b/src/expr/node.h
index 6dbb5aa2bba26ee4041ac9c0e9c98fe8cea46833..31721b2ef1ce6df495811ebfd22a5f5b21555a8c 100644 (file)
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -464,6 +464,12 @@ public:
     assertTNodeNotExpired();
     return getMetaKind() == kind::metakind::VARIABLE;
   }
+  inline bool isUninterpretedVar() const {
+    assertTNodeNotExpired();
+    return getMetaKind() == kind::metakind::VARIABLE &&
+           getKind() != kind::UNIVERSE_SET && 
+           getKind() != kind::SEP_NIL;
+  }
 
   inline bool isClosure() const {
     assertTNodeNotExpired();

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 37d65972e95e00acb7fcdbf1ce9264d08d247471..2b2ebbf5e9d53dbf87d3344a6e29f3136520ed6b 100644 (file)
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -271,12 +271,12 @@ Theory::PPAssertStatus Theory::ppAssert(TNode in,
     // 1) x is a variable
     // 2) x is not in the term t
     // 3) x : T and t : S, then S <: T
-    if (in[0].isVar() && !in[1].hasSubterm(in[0]) &&
+    if (in[0].isUninterpretedVar() && !in[1].hasSubterm(in[0]) &&
         (in[1].getType()).isSubtypeOf(in[0].getType()) ){
       outSubstitutions.addSubstitution(in[0], in[1]);
       return PP_ASSERT_STATUS_SOLVED;
     }
-    if (in[1].isVar() && !in[0].hasSubterm(in[1]) &&
+    if (in[1].isUninterpretedVar() && !in[0].hasSubterm(in[1]) &&
         (in[0].getType()).isSubtypeOf(in[1].getType())){
       outSubstitutions.addSubstitution(in[1], in[0]);
       return PP_ASSERT_STATUS_SOLVED;

diff --git a/test/regress/regress0/rels/Makefile.am b/test/regress/regress0/rels/Makefile.am
index 06658e9887003630a03a6fc801c809c9f6388ddb..7c9dca8dd2d450aa64fdf518bdc1cdacc01c2403 100644 (file)
--- a/test/regress/regress0/rels/Makefile.am
+++ b/test/regress/regress0/rels/Makefile.am
@@ -100,7 +100,8 @@ TESTS =     \
   rel_tp_join_1.cvc \
   rel_transpose_0.cvc \
   set-strat.cvc \
-  rel_tc_8.cvc
+  rel_tc_8.cvc \
+  atom_univ2.cvc
 
 # unsolved : garbage_collect.cvc
 

diff --git a/test/regress/regress0/rels/atom_univ2.cvc b/test/regress/regress0/rels/atom_univ2.cvc
new file mode 100644 (file)
index 0000000..9901ce6
--- /dev/null
+++ b/test/regress/regress0/rels/atom_univ2.cvc
@@ -0,0 +1,23 @@
+% EXPECT: unsat\r
+OPTION "logic" "ALL_SUPPORTED";\r
+Atom: TYPE;\r
+\r
+a : SET OF [Atom];\r
+b : SET OF [Atom, Atom];\r
+\r
+x : Atom;\r
+y : Atom;\r
+\r
+ASSERT NOT(x = y);\r
+\r
+ASSERT TUPLE(y) IS_IN a;\r
+ASSERT (x, y) IS_IN b;\r
+\r
+ASSERT UNIVERSE::SET OF [Atom, Atom] = (UNIVERSE::SET OF [Atom] PRODUCT UNIVERSE::SET OF [Atom]);\r
+\r
+u : SET OF [Atom, Atom];\r
+ASSERT u = UNIVERSE::SET OF [Atom, Atom];\r
+\r
+ASSERT NOT (x, y) IS_IN u;\r
+\r
+CHECKSAT;\r

diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am
index f731bd15eaad954b05f05eb05b4d83fc616f7950..692390ddec4e1cfd1de431e2f7677367a44bd69d 100644 (file)
--- a/test/regress/regress0/sep/Makefile.am
+++ b/test/regress/regress0/sep/Makefile.am
@@ -56,7 +56,8 @@ TESTS =       \
   emp2-quant-unsat.smt2 \
   dispose-1.smt2 \
   finite-witness-sat.smt2 \
-  sep-fmf-priority.smt2
+  sep-fmf-priority.smt2 \
+  nil-no-elim.smt2
 
 
 FAILING_TESTS =

diff --git a/test/regress/regress0/sep/nil-no-elim.smt2 b/test/regress/regress0/sep/nil-no-elim.smt2
new file mode 100644 (file)
index 0000000..e9aa380
--- /dev/null
+++ b/test/regress/regress0/sep/nil-no-elim.smt2
@@ -0,0 +1,11 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-sort U 0)
+(declare-fun f (U) U)
+(declare-fun a () U)
+
+(assert (= (as sep.nil U) (f a)))
+
+(assert (pto (f a) 0))
+
+(check-sat)