return result;
}
+void AntlrParser::newFunction(std::string name,
+ const std::vector< std::string>& sorts) {
+ // FIXME: Need to actually create a function type
+ d_varSymbolTable.bindName(name, d_exprManager->mkVar());
+}
+
+void AntlrParser::newFunctions(const std::vector<std::string>& names,
+ const std::vector< std::string>& sorts) {
+ for(unsigned i = 0; i < names.size(); ++i) {
+ newFunction(names[i], sorts);
+ }
+}
+
void AntlrParser::newPredicate(std::string name,
const std::vector<std::string>& sorts) {
Debug("parser") << "newPredicate(" << name << ")" << std::endl;
}
}
+bool AntlrParser::isSort(std::string name) {
+ return d_sortTable.isBound(name);
+}
+
+void AntlrParser::newSort(std::string name) {
+ Assert( !isSort(name) ) ;
+ // Trivial binding
+ d_sortTable.bindName(name,name);
+ Assert( isSort(name) ) ;
+}
+
+void AntlrParser::newSorts(const std::vector<std::string>& names) {
+ for(unsigned i = 0; i < names.size(); ++i) {
+ newSort(names[i]);
+ }
+}
+
void AntlrParser::setExpressionManager(ExprManager* em) {
d_exprManager = em;
}
}
}
+bool AntlrParser::checkSort(std::string name, DeclarationCheck check) {
+ switch(check) {
+ case CHECK_DECLARED:
+ return isSort(name);
+ case CHECK_UNDECLARED:
+ return !isSort(name);
+ case CHECK_NONE:
+ return true;
+ default:
+ Unhandled("Unknown check type!");
+ }
+}
+
}/* CVC4::parser namespace */
}/* CVC4 namespace */
*/
bool checkDeclaration(std::string varName, DeclarationCheck check);
+ /**
+ * Return true if the the declaration policy we want to enforce is true
+ * on the given sort name.
+ * @param name the sort symbol to check
+ * @oaram check the kind of check to perform
+ * @return true if the check holds
+ */
+ bool checkSort(std::string name, DeclarationCheck check);
+
/**
* Types of symbols.
*/
*/
bool isDeclared(std::string var_name, SymbolType type = SYM_VARIABLE);
+ /**
+ * Checks if the sort has been declared.
+ * @param the sort name
+ */
+ bool isSort(std::string name);
+
/**
* Returns the true expression.
* @return the true expression
Expr mkExpr(Kind kind, const std::vector<Expr>& children);
/**
- * Creates a new predicate over the given sorts. The predicate
- * has arity sorts.size().
+ * Creates a new function over the given sorts. The function
+ * has arity sorts.size() - 1 and range type sorts[sorts.size() - 1].
+ * @param name the name of the function
+ * @param sorts the sorts
+ */
+ void newFunction(std::string name,
+ const std::vector<std::string>& sorts);
+
+ /**
+ * Creates new functions over the given sorts. Each function has
+ * arity sorts.size() - 1 and range type sorts[sorts.size() - 1].
+ * @param name the name of the function
+ * @param sorts the sorts
+ */
+ void newFunctions(const std::vector<std::string>& names,
+ const std::vector<std::string>& sorts);
+
+ /**
+ * Creates a new predicate over the given sorts. The predicate has
+ * arity sorts.size().
* @param name the name of the predicate
* @param sorts the sorts
*/
void newPredicates(const std::vector<std::string>& names, const std::vector<
std::string>& sorts);
+ /**
+ * Creates a new sort with the given name.
+ */
+ void newSort(std::string name);
+
+ /**
+ * Creates a new sorts with the given names.
+ */
+ void newSorts(const std::vector<std::string>& names);
+
/**
* Returns the precedence rank of the kind.
*/
/** The symbol table lookup */
SymbolTable<Expr> d_varSymbolTable;
+
+ /** The sort table */
+ SymbolTable<std::string> d_sortTable;
};
}/* CVC4::parser namespace */
{ smt_command = new AssertCommand(formula); }
| FORMULA_ATTR formula = annotatedFormula
{ smt_command = new CheckSatCommand(formula); }
- | STATUS_ATTR b_status = status
- { smt_command = new SetBenchmarkStatusCommand(b_status); }
- | EXTRAPREDS_ATTR LPAREN (predicateDeclaration)+ RPAREN
- | NOTES_ATTR STRING_LITERAL
+ | STATUS_ATTR b_status = status
+ { smt_command = new SetBenchmarkStatusCommand(b_status); }
+ | EXTRAFUNS_ATTR LPAREN (functionDeclaration)+ RPAREN
+ | EXTRAPREDS_ATTR LPAREN (predicateDeclaration)+ RPAREN
+ | EXTRASORTS_ATTR LPAREN (sortDeclaration)+ RPAREN
+ | NOTES_ATTR STRING_LITERAL
| annotation
;
Kind kind;
vector<Expr> children;
}
+<<<<<<< .mine
+ : formula = annotatedAtom
+ | LPAREN kind = boolConnective annotatedFormulas[children] RPAREN
+ { formula = mkExpr(kind, children); }
+ /* TODO: let, flet, quantifiers */
+=======
: formula = annotatedAtom
| LPAREN kind = boolConnective annotatedFormulas[children] RPAREN { formula = mkExpr(kind, children); }
+>>>>>>> .r150
;
/**
+<<<<<<< .mine
+ * Matches a sequence of annotaed formulas and puts them into the formulas
+ * vector.
+ * @param formulas the vector to fill with formulas
+ */
+annotatedFormulas[std::vector<Expr>& formulas]
+{
+ Expr f;
+}
+ : ( f = annotatedFormula { formulas.push_back(f); } )+
+ ;
+
+/**
+ * Matches an annotated proposition atom, which is either a propositional atom
+ * or built of other atoms using a predicate symbol.
+=======
* Matches an annotated proposition atom, which is either a propositional atom
* or built of other atoms using a predicate symbol.
+>>>>>>> .r150
* @return expression representing the atom
*/
+<<<<<<< .mine
+annotatedAtom returns [CVC4::Expr atom]
+{
+ Kind kind;
+ string predName;
+ Expr pred;
+ vector<Expr> children;
+}
+ : atom = propositionalAtom
+=======
annotatedAtom returns [CVC4::Expr atom]
: atom = propositionalAtom
+>>>>>>> .r150
+ | LPAREN kind = arithPredicate annotatedTerms[children] RPAREN
+ { atom = mkExpr(kind,children); }
+ | LPAREN pred = predicateSymbol
+ { children.push_back(pred); }
+ annotatedTerms[children] RPAREN
+ { atom = mkExpr(CVC4::APPLY,children); }
+ ;
+
+/**
+ * Matches an annotated term.
+ * @return the expression representing the term
+ */
+annotatedTerm returns [CVC4::Expr term]
+{
+ Kind kind;
+ Expr f, t1, t2;
+ vector<Expr> children;
+}
+ : term = baseTerm
+ | LPAREN f = functionSymbol
+ { children.push_back(f); }
+ annotatedTerms[children] RPAREN
+ { term = mkExpr(CVC4::APPLY, children); }
+ // | LPAREN kind = arithFunction annotatedTerms[children] RPAREN
+ // { term = mkExpr(kind,children); }
+ | LPAREN ITE
+ f = annotatedFormula
+ t1 = annotatedTerm
+ t2 = annotatedTerm RPAREN
+ { term = mkExpr(CVC4::ITE, f, t1, t2); }
+ ;
+
+/**
+ * Matches a sequence of annotaed formulas and puts them into the formulas
+ * vector.
+ * @param formulas the vector to fill with formulas
+ */
+annotatedTerms[std::vector<Expr>& terms]
+{
+ Expr t;
+}
+ : ( t = annotatedFormula { terms.push_back(t); } )+
+ ;
+
+baseTerm returns [CVC4::Expr term]
+{
+ string name;
+}
+ : name = identifier[CHECK_DECLARED] { term = getVariable(name); }
+ /* TODO: constants */
;
/**
;
/**
+<<<<<<< .mine
+=======
* Mathces a sequence of annotaed formulas and puts them into the formulas
* vector.
* @param formulas the vector to fill with formulas
;
/**
+>>>>>>> .r150
* Matches a propositional atom and returns the expression of the atom.
* @return atom the expression of the atom
*/
{
std::string p;
}
- : p = predicateName[CHECK_DECLARED] { atom = getVariable(p); }
+ : atom = predicateSymbol
| TRUE { atom = getTrueExpr(); }
| FALSE { atom = getFalseExpr(); }
;
+arithPredicate returns [CVC4::Kind kind]
+ : EQUAL { kind = CVC4::EQUAL; }
+ /* TODO: lt, gt */
+ ;
+
/**
+<<<<<<< .mine
+ * Matches a (possibly undeclared) predicate identifier (returning the string).
+=======
* Matches a predicate symbol.
+>>>>>>> .r150
* @param check what kind of check to do with the symbol
*/
predicateName[DeclarationCheck check = CHECK_NONE] returns [std::string p]
: p = identifier[check]
;
+<<<<<<< .mine
+
+/**
+ * Matches an previously declared predicate symbol (returning an Expr)
+ */
+predicateSymbol returns [CVC4::Expr pred]
+{
+ string name;
+}
+ : name = predicateName[CHECK_DECLARED]
+ { pred = getVariable(name); }
+ ;
+
+/**
+ * Matches a (possibly undeclared) function identifier (returning the string)
+ * @param check what kind of check to do with the symbol
+ */
+functionName[DeclarationCheck check = CHECK_NONE] returns [std::string name]
+ : name = identifier[check]
+ ;
+/**
+ * Matches an previously declared function symbol (returning an Expr)
+ */
+functionSymbol returns [CVC4::Expr fun]
+{
+ string name;
+}
+ : name = functionName[CHECK_DECLARED]
+ { fun = getVariable(name); }
+ ;
+
+=======
+
+>>>>>>> .r150
/**
* Matches an attribute name from the input (:attribute_name).
*/
* Matches the sort symbol, which can be an arbitrary identifier.
* @param check the check to perform on the name
*/
+<<<<<<< .mine
+sortName[DeclarationCheck check = CHECK_NONE] returns [std::string name]
+ : name = identifier[CHECK_NONE]
+ /* We pass CHECK_NONE to identifier, because identifier checks
+ in the variable namespace, not the sorts namespace. */
+ { checkSort(name,check) }?
+=======
sortName[DeclarationCheck check = CHECK_NONE] returns [std::string s]
: s = identifier[check]
+>>>>>>> .r150
;
+<<<<<<< .mine
+functionDeclaration
+{
+ string name;
+ vector<string> sorts;
+}
+ : LPAREN name = functionName[CHECK_UNDECLARED]
+ sortNames[sorts, CHECK_DECLARED] RPAREN
+ { newFunction(name, sorts); }
+ ;
+
+=======
+
+>>>>>>> .r150
/**
* Matches the declaration of a predicate and declares it
*/
string p_name;
vector<string> p_sorts;
}
+<<<<<<< .mine
+ : LPAREN p_name = predicateName[CHECK_UNDECLARED]
+ sortNames[p_sorts, CHECK_DECLARED] RPAREN
+ { newPredicate(p_name, p_sorts); }
+=======
: LPAREN p_name = predicateName[CHECK_UNDECLARED] sortNames[p_sorts] RPAREN { newPredicate(p_name, p_sorts); }
+>>>>>>> .r150
+ ;
+<<<<<<< .mine
+
+sortDeclaration
+{
+ string name;
+}
+ : name = sortName[CHECK_UNDECLARED]
+ { newSort(name); }
;
+
+=======
+>>>>>>> .r150
/**
* Matches a sequence of sort symbols and fills them into the given vector.
*/
-sortNames[std::vector<std::string>& sorts]
+sortNames[std::vector<std::string>& sorts,DeclarationCheck check = CHECK_NONE]
{
- std::string sort;
+ std::string name;
}
+<<<<<<< .mine
+ : ( name = sortName[check]
+ { sorts.push_back(name); })*
+=======
: ( sort = sortName[CHECK_UNDECLARED] { sorts.push_back(sort); })*
+>>>>>>> .r150
;
/**
projects / cvc5.git / commitdiff