From 0e3dc441641c64e6137d85f8d7eaeb78ee562e51 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 11 Dec 2012 18:29:31 -0500
Subject: [PATCH] SMT-LIB compliance fix to get-assignment; resolves bug 480

---
 src/smt/smt_engine.cpp            | 23 +++++++++++++++--------
 test/regress/regress0/Makefile.am |  3 ++-
 test/regress/regress0/bug480.smt2 | 11 +++++++++++
 3 files changed, 28 insertions(+), 9 deletions(-)
 create mode 100644 test/regress/regress0/bug480.smt2

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c82b7ca2c..77e43d518 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -631,6 +631,11 @@ void SmtEngine::finalOptionsAreSet() {
     }
   }
 
+  if(options::produceAssignments() && !options::produceModels()) {
+    Notice() << "SmtEngine: turning on produce-models to support produce-assignments" << std::endl;
+    setOption("produce-models", SExpr("true"));
+  }
+
   if(! d_logic.isLocked()) {
     // ensure that our heuristics are properly set up
     setLogicInternal();
@@ -2705,20 +2710,22 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) {
 
   vector<SExpr> sexprs;
   TypeNode boolType = d_nodeManager->booleanType();
+  TheoryModel* m = d_theoryEngine->getModel();
   for(AssignmentSet::const_iterator i = d_assignments->begin(),
         iend = d_assignments->end();
       i != iend;
       ++i) {
     Assert((*i).getType() == boolType);
 
-    // Normalize
-    Node n = Rewriter::rewrite(*i);
+    // Expand, then normalize
+    hash_map<Node, Node, NodeHashFunction> cache;
+    Node n = d_private->expandDefinitions(*i, cache);
+    n = Rewriter::rewrite(n);
 
     Trace("smt") << "--- getting value of " << n << endl;
-    TheoryModel* m = d_theoryEngine->getModel();
     Node resultNode;
-    if( m ){
-      resultNode = m->getValue( n );
+    if(m != NULL) {
+      resultNode = m->getValue(n);
     }
 
     // type-check the result we got
@@ -2727,12 +2734,12 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) {
     vector<SExpr> v;
     if((*i).getKind() == kind::APPLY) {
       Assert((*i).getNumChildren() == 0);
-      v.push_back((*i).getOperator().toString());
+      v.push_back(SExpr::Keyword((*i).getOperator().toString()));
     } else {
       Assert((*i).isVar());
-      v.push_back((*i).toString());
+      v.push_back(SExpr::Keyword((*i).toString()));
     }
-    v.push_back(resultNode.toString());
+    v.push_back(SExpr::Keyword(resultNode.toString()));
     sexprs.push_back(v);
   }
   return SExpr(sexprs);
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 0f6c11be9..3b30a8d9e 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -142,7 +142,8 @@ BUG_TESTS = \
 	bug411.smt2 \
 	bug421.smt2 \
 	bug421b.smt2 \
-	bug425.cvc
+	bug425.cvc \
+	bug480.smt2
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 
diff --git a/test/regress/regress0/bug480.smt2 b/test/regress/regress0/bug480.smt2
new file mode 100644
index 000000000..ba58f354b
--- /dev/null
+++ b/test/regress/regress0/bug480.smt2
@@ -0,0 +1,11 @@
+; EXPECT: sat
+; EXPECT: ((foo true) (bar false) (baz true))
+; EXIT: 10
+(set-logic QF_LIA)
+(set-option :produce-assignments true)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(assert (! (or (! (= x (+ y 5)) :named foo) (! (= x (- y 5)) :named bar)) :named baz))
+(assert (and (> x 0) (<= y 5)))
+(check-sat)
+(get-assignment)
-- 
2.30.2