Smtlib goal annotation

Parse/SMTLIB2.cpp

@@ -1802,9 +1802,11 @@ void SMTLIB2::parseAnnotatedTerm(LExpr* exp)
 
   auto toParse = lRdr.readExpr();
 
-  // we only consider :named annotations
   if(lRdr.tryAcceptAtom(":named")){
     _todo.push(make_pair(PO_LABEL,lRdr.readExpr()));
+  } else if(env.options->parseGoalAnnotations() && lRdr.tryAcceptAtom(":goal")){
+    (void) lRdr.readExpr(); /* we ignore the goal name */
+    _todo.push(make_pair(PO_MAKE_GOAL,nullptr));
   }
 
   _todo.push(make_pair(PO_PARSE,toParse));
@@ -2758,6 +2760,13 @@ SMTLIB2::ParseResult SMTLIB2::parseTermOrFormula(LExpr* body, bool isSort)
         _results.push(res);
         continue;
       }
+      case PO_MAKE_GOAL: {
+        ASS_GE(_results.size(),1);
+        ParseResult res =  _results.pop();
+        res.isGoal = true;
+        _results.push(res);
+        continue;
+      }
       case PO_LET_PREPARE_LOOKUP:
         parseLetPrepareLookup(exp);
         continue;
@@ -2802,7 +2811,7 @@ void SMTLIB2::readAssert(LExpr* body)
     USER_ERROR_EXPR("Asserted expression of non-boolean sort "+body->toString());
   }
 
-  FormulaUnit* fu = new FormulaUnit(fla, FromInput(UnitInputType::ASSUMPTION));
+  FormulaUnit* fu = new FormulaUnit(fla, FromInput(res.isGoal ? UnitInputType::NEGATED_CONJECTURE : UnitInputType::ASSUMPTION));
   _formulas.pushBack(fu);
 }
 

Parse/SMTLIB2.hpp

@@ -296,6 +296,7 @@ class SMTLIB2 {
       Formula* frm;
       TermList trm;
     };
+    bool isGoal = false;
 
     /**
      * Try interpreting ParseResult as a formula
@@ -431,6 +432,7 @@ class SMTLIB2 {
     PO_QUANT,              // takes LExpr* (the whole quantified expression again)
     PO_POP_LOOKUP,         // takes nothing
     PO_AS_END,             // takes LExpr* (the whole as expression again)
+    PO_MAKE_GOAL,          // takes nullptr
   };
   /**
    * Main smtlib term parsing stack.

Shell/Options.cpp

@@ -495,6 +495,13 @@ void Options::init()
        "This also ensures a symbol is not used as a function and predicate.";
     _lookup.insert(&_arityCheck);
     _arityCheck.tag(OptionTag::DEVELOPMENT);
+
+    _parseGoalAnnotations = BoolOptionValue("parse_goal_annotations","",true);
+    _parseGoalAnnotations.description="Enable parsing :goal annotations in smtlib problems."
+       "They can be used like this: (assert (! <formula> :goal <goal-name>))";
+    _lookup.insert(&_parseGoalAnnotations);
+    _parseGoalAnnotations.tag(OptionTag::INPUT);
+
     _functionDefinitionElimination = ChoiceOptionValue<FunctionDefinitionElimination>("function_definition_elimination","fde",
                                                                                       FunctionDefinitionElimination::ALL,{"all","none","unused"});
     _functionDefinitionElimination.description=

Shell/Options.hpp

@@ -2083,6 +2083,7 @@ bool _hard;
   bool partialRedundancyAvatarConstraints() const { return _partialRedundancyAvatarConstraints.actualValue; }
   bool partialRedundancyLiteralConstraints() const { return _partialRedundancyLiteralConstraints.actualValue; }
   bool arityCheck() const { return _arityCheck.actualValue; }
+  bool parseGoalAnnotations() const { return _parseGoalAnnotations.actualValue; }
   //void setArityCheck(bool newVal) { _arityCheck=newVal; }
   Demodulation backwardDemodulation() const { return _backwardDemodulation.actualValue; }
   DemodulationRedundancyCheck demodulationRedundancyCheck() const { return _demodulationRedundancyCheck.actualValue; }
@@ -2425,6 +2426,7 @@ bool _hard;
 	BoolOptionValue _randomAWR;
   BoolOptionValue _literalMaximalityAftercheck;
   BoolOptionValue _arityCheck;
+  BoolOptionValue _parseGoalAnnotations;
 
   BoolOptionValue _randomTraversals;