From 6cb3f49d3933061000fe63d2ee7e004cae06d6ba Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 4 Apr 2017 09:59:45 -0500
Subject: [PATCH] Do not solve for 0-ary non-constant symbols (for which isVar
 returns true), add regressions.

---
 src/expr/node.h                            |  6 ++++++
 src/theory/theory.cpp                      |  4 ++--
 test/regress/regress0/rels/Makefile.am     |  3 ++-
 test/regress/regress0/rels/atom_univ2.cvc  | 23 ++++++++++++++++++++++
 test/regress/regress0/sep/Makefile.am      |  3 ++-
 test/regress/regress0/sep/nil-no-elim.smt2 | 11 +++++++++++
 6 files changed, 46 insertions(+), 4 deletions(-)
 create mode 100644 test/regress/regress0/rels/atom_univ2.cvc
 create mode 100644 test/regress/regress0/sep/nil-no-elim.smt2

diff --git a/src/expr/node.h b/src/expr/node.h
index 6dbb5aa2b..31721b2ef 100644
--- 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 37d65972e..2b2ebbf5e 100644
--- 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 06658e988..7c9dca8dd 100644
--- 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
index 000000000..9901ce630
--- /dev/null
+++ b/test/regress/regress0/rels/atom_univ2.cvc
@@ -0,0 +1,23 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+Atom: TYPE;
+
+a : SET OF [Atom];
+b : SET OF [Atom, Atom];
+
+x : Atom;
+y : Atom;
+
+ASSERT NOT(x = y);
+
+ASSERT TUPLE(y) IS_IN a;
+ASSERT (x, y) IS_IN b;
+
+ASSERT UNIVERSE::SET OF [Atom, Atom] = (UNIVERSE::SET OF [Atom] PRODUCT UNIVERSE::SET OF [Atom]);
+
+u : SET OF [Atom, Atom];
+ASSERT u = UNIVERSE::SET OF [Atom, Atom];
+
+ASSERT NOT (x, y) IS_IN u;
+
+CHECKSAT;
diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am
index f731bd15e..692390dde 100644
--- 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
index 000000000..e9aa3807a
--- /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)
-- 
2.30.2