Unsat core infrastruture and API (SMT-LIB compliance to come).

2 files changed, 19 insertions, 6 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index bd7c96dce..e1547d23d 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -378,7 +378,9 @@ command returns [CVC4::Command* cmd = NULL]
   | /* assertion */
     ASSERT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     term[expr, expr2]
-    { cmd = new AssertCommand(expr); }
+    { cmd = new AssertCommand(expr, /* inUnsatCore */ PARSER_STATE->lastNamedTerm() == expr);
+      PARSER_STATE->setLastNamedTerm(Expr());
+    }
   | /* check-sat */
     CHECKSAT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     ( term[expr, expr2]
@@ -684,7 +686,7 @@ rewriterulesCommand[CVC4::Command*& cmd]
       };
       args.push_back(expr);
       expr = MK_EXPR(CVC4::kind::REWRITE_RULE, args);
-      cmd = new AssertCommand(expr); }
+      cmd = new AssertCommand(expr, false); }
     /* propagation rule */
   | rewritePropaKind[kind]
     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
@@ -735,7 +737,7 @@ rewriterulesCommand[CVC4::Command*& cmd]
       };
       args.push_back(expr);
       expr = MK_EXPR(CVC4::kind::REWRITE_RULE, args);
-      cmd = new AssertCommand(expr); }
+      cmd = new AssertCommand(expr, false); }
   ;
 
 rewritePropaKind[CVC4::Kind& kind]
@@ -1035,8 +1037,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
 
     /* attributed expressions */
   | LPAREN_TOK ATTRIBUTE_TOK term[expr, f2]
-    ( attribute[expr, attexpr,attr]
-      { if( attr == ":pattern" && ! attexpr.isNull()) {
+    ( attribute[expr, attexpr, attr]
+      { if(attr == ":pattern" && ! attexpr.isNull()) {
           patexprs.push_back( attexpr );
         }
       }
@@ -1074,7 +1076,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
           }
         }
         expr2 = MK_EXPR(kind::INST_PATTERN_LIST, patexprs);
-      }else{
+      } else {
         expr2 = f2;
       }
     }
@@ -1210,6 +1212,8 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
       PARSER_STATE->reserveSymbolAtAssertionLevel(name);
       // define it
       Expr func = PARSER_STATE->mkFunction(name, expr.getType());
+      // remember the last term to have been given a :named attribute
+      PARSER_STATE->setLastNamedTerm(expr);
       // bind name to expr with define-fun
       Command* c =
         new DefineNamedFunctionCommand(name, func, std::vector<Expr>(), expr);
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 71161be94..7ecd2e5b1 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -54,6 +54,7 @@ private:
   bool d_logicSet;
   LogicInfo d_logic;
   std::hash_map<std::string, Kind, StringHashFunction> operatorKindMap;
+  Expr d_lastNamedTerm;
 
 protected:
   Smt2(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false);
@@ -105,6 +106,14 @@ public:
 
   void includeFile(const std::string& filename);
 
+  void setLastNamedTerm(Expr e) {
+    d_lastNamedTerm = e;
+  }
+
+  Expr lastNamedTerm() {
+    return d_lastNamedTerm;
+  }
+
   bool isAbstractValue(const std::string& name) {
     return name.length() >= 2 && name[0] == '@' && name[1] != '0' &&
       name.find_first_not_of("0123456789", 1) == std::string::npos;