SMT-LIB compliance fix to get-assignment; resolves bug 480

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c82b7ca2c0268306d4000d1f784ac225aa730d40..77e43d518fde80c224ed3b9703472c436ad294a4 100644 (file)
--- 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 0f6c11be96d4881eb1bda2c441a3fd0b6ad346cb..3b30a8d9ee846c11deef58a2420ca7aa74773f60 100644 (file)
--- 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 (file)
index 0000000..ba58f35
--- /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)