Support uninterpreted constants in the evaluator (#4777)

4 files changed, 48 insertions, 3 deletions

diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index 7a4940328..a7228658d 100644
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -43,6 +43,10 @@ EvalResult::EvalResult(const EvalResult& other)
       new (&d_str) String;
       d_str = other.d_str;
       break;
+    case UCONST:
+      new (&d_uc)
+          UninterpretedConstant(other.d_uc.getType(), other.d_uc.getIndex());
+      break;
     case INVALID: break;
   }
 }
@@ -67,6 +71,10 @@ EvalResult& EvalResult::operator=(const EvalResult& other)
         new (&d_str) String;
         d_str = other.d_str;
         break;
+      case UCONST:
+        new (&d_uc)
+            UninterpretedConstant(other.d_uc.getType(), other.d_uc.getIndex());
+        break;
       case INVALID: break;
     }
   }
@@ -91,9 +99,13 @@ EvalResult::~EvalResult()
     {
       d_str.~String();
       break;
-
-      default: break;
     }
+    case UCONST:
+    {
+      d_uc.~UninterpretedConstant();
+      break;
+    }
+    default: break;
   }
 }
 
@@ -106,6 +118,7 @@ Node EvalResult::toNode() const
     case EvalResult::BITVECTOR: return nm->mkConst(d_bv);
     case EvalResult::RATIONAL: return nm->mkConst(d_rat);
     case EvalResult::STRING: return nm->mkConst(d_str);
+    case EvalResult::UCONST: return nm->mkConst(d_uc);
     default:
     {
       Trace("evaluator") << "Missing conversion from " << d_tag << " to node"
@@ -389,7 +402,13 @@ EvalResult Evaluator::evalInternal(
           results[currNode] = EvalResult(r);
           break;
         }
-
+        case kind::UNINTERPRETED_CONSTANT:
+        {
+          const UninterpretedConstant& uc =
+              currNodeVal.getConst<UninterpretedConstant>();
+          results[currNode] = EvalResult(uc);
+          break;
+        }
         case kind::PLUS:
         {
           Rational res = results[currNode[0]].d_rat;
@@ -824,6 +843,11 @@ EvalResult Evaluator::evalInternal(
               results[currNode] = EvalResult(lhs.d_str == rhs.d_str);
               break;
             }
+            case EvalResult::UCONST:
+            {
+              results[currNode] = EvalResult(lhs.d_uc == rhs.d_uc);
+              break;
+            }
 
             default:
             {
diff --git a/src/theory/evaluator.h b/src/theory/evaluator.h
index e986edf1f..059d21e56 100644
--- a/src/theory/evaluator.h
+++ b/src/theory/evaluator.h
@@ -25,6 +25,7 @@
 
 #include "base/output.h"
 #include "expr/node.h"
+#include "expr/uninterpreted_constant.h"
 #include "util/bitvector.h"
 #include "util/rational.h"
 #include "util/string.h"
@@ -45,6 +46,7 @@ struct EvalResult
     BITVECTOR,
     RATIONAL,
     STRING,
+    UCONST,
     INVALID
   } d_tag;
 
@@ -55,6 +57,7 @@ struct EvalResult
     BitVector d_bv;
     Rational d_rat;
     String d_str;
+    UninterpretedConstant d_uc;
   };
 
   EvalResult(const EvalResult& other);
@@ -63,6 +66,7 @@ struct EvalResult
   EvalResult(const BitVector& bv) : d_tag(BITVECTOR), d_bv(bv) {}
   EvalResult(const Rational& i) : d_tag(RATIONAL), d_rat(i) {}
   EvalResult(const String& str) : d_tag(STRING), d_str(str) {}
+  EvalResult(const UninterpretedConstant& u) : d_tag(UCONST), d_uc(u) {}
 
   EvalResult& operator=(const EvalResult& other);
 
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 4e79b5dbe..8118d8d79 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1910,6 +1910,7 @@ set(regress_1_tests
   regress1/sygus/dt-test-ns.sy
   regress1/sygus/dup-op.sy
   regress1/sygus/error1-dt.sy
+  regress1/sygus/eval-uc.sy
   regress1/sygus/extract.sy
   regress1/sygus/fast-enum-backtrack.sy
   regress1/sygus/fg_polynomial3.sy
diff --git a/test/regress/regress1/sygus/eval-uc.sy b/test/regress/regress1/sygus/eval-uc.sy
new file mode 100644
index 000000000..e2bf9d144
--- /dev/null
+++ b/test/regress/regress1/sygus/eval-uc.sy
@@ -0,0 +1,16 @@
+; EXPECT: unsat
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --uf-ho
+(set-logic ALL)
+(declare-sort S 0)
+(declare-var f Bool)
+(declare-var u (-> S Bool))
+(declare-var new_f Bool)
+(declare-var new_u (-> S Bool))
+(define-fun init ((f Bool) (u (-> S Bool))) Bool (and f (forall ((x S)) (not (u x)))))
+(define-fun trans ((f Bool) (u (-> S Bool)) (new_f Bool) (new_u (-> S Bool))) Bool (and (not new_f) (exists ((x S)) (forall ((y S)) (= (new_u y) (or (u y) (= y x)))))))
+;(define-fun trans ((f Bool) (u (-> S Bool)) (new_f Bool) (new_u (-> S Bool))) Bool (and new_f (exists ((x S)) (forall ((y S)) (= (new_u y) (or (u y) (= y x)))))))
+(synth-fun inv_matrix ((f Bool) (u (-> S Bool)) (x S)) Bool ((Start Bool)) ((Start Bool ( (or (not 
+(u x)) (not f))))))
+(define-fun inv ((f Bool) (u (-> S Bool))) Bool (forall ((x S)) (inv_matrix f u x)))
+(constraint (=> (and (inv f u) (trans f u new_f new_u)) (inv new_f new_u)))
+(check-synth)