class Context {
/**
- * Pointer to the ContextMemoryManager fot this Context.
+ * Pointer to the ContextMemoryManager for this Context.
*/
ContextMemoryManager* d_pCMM;
/**
* Doubly-linked list of objects to notify before every pop. See
- * ContextNotifyObj for sturcture of linked list.
+ * ContextNotifyObj for structure of linked list.
*/
ContextNotifyObj* d_pCNOpre;
/**
* Doubly-linked list of objects to notify after every pop. See
- * ContextNotifyObj for sturcture of linked list.
+ * ContextNotifyObj for structure of linked list.
*/
ContextNotifyObj* d_pCNOpost;
{ if (pScopePrev != NULL) d_level = pScopePrev->getLevel() + 1; }
/**
- * Destructor: Restore all of the objects in CotextObjList. Defined inline
+ * Destructor: Restore all of the objects in ContextObjList. Defined inline
* below.
*/
~Scope();
namespace CVC4 {
namespace parser {
-unsigned AntlrParser::getPrecedence(Kind kind) {
- switch(kind) {
- // Boolean operators
- case IFF:
- return 1;
- case IMPLIES:
- return 2;
- case OR:
- return 3;
- case XOR:
- return 4;
- case AND:
- return 5;
- default:
- Unhandled("Undefined precedence - necessary for proper parsing of CVC files!");
- }
- return 0;
-}
-
AntlrParser::AntlrParser(const antlr::ParserSharedInputState& state, int k) :
antlr::LLkParser(state, k) {
}
LT(0).get()->getColumn());
}
-Expr AntlrParser::createPrecedenceExpr(const vector<Expr>& exprs, const vector<
- Kind>& kinds) {
- Assert( exprs.size() > 0, "Expected non-empty vector expr");
- Assert( kinds.size() + 1 == exprs.size(), "Expected kinds to match exprs");
- return createPrecedenceExpr(exprs, kinds, 0, exprs.size() - 1);
-}
-
- /* Find the index of the kind with the lowest precedence. */
-unsigned AntlrParser::findPivot(const std::vector<Kind>& kinds,
- unsigned start_index, unsigned end_index) const {
- Assert( start_index >= 0, "Expected start_index >= 0. ");
- Assert( end_index < kinds.size(), "Expected end_index < kinds.size(). ");
- Assert( start_index <= end_index, "Expected start_index <= end_index. ");
-
- int pivot = start_index;
- unsigned pivot_precedence = getPrecedence(kinds[pivot]);
-
- for(unsigned i = start_index + 1; i <= end_index; ++i) {
- unsigned current_precedence = getPrecedence(kinds[i]);
- if(current_precedence < pivot_precedence) {
- pivot = i;
- pivot_precedence = current_precedence;
- }
- }
-
- return pivot;
-}
-
- /* "Tree-ify" an unparenthesized expression:
- e_1 op_1 e_2 op_2 ... e_(n-1) op_(n-1) e_n
- represented as a vector of exprs <e_1,e_2,...,e_n> and
- kinds <k_1,k_2,...,k_(n-1)>.
-
- This works by finding the lowest precedence operator op_i,
- then recursively tree-ifying lhs = (e1 op_1 ... op_(i-1) e_i),
- rhs = (e_(i+1) op_(i+1) ... op_(n-1) e_N), and forming the
- expression (lhs op_i rhs).
- */
-Expr AntlrParser::createPrecedenceExpr(const std::vector<Expr>& exprs,
- const std::vector<Kind>& kinds,
- unsigned start_index, unsigned end_index) {
- Assert( exprs.size() > 0, "Expected non-empty vector expr");
- Assert( kinds.size() + 1 == exprs.size(), "Expected kinds to match exprs.");
- Assert( start_index >= 0, "Expected start_index >= 0. ");
- Assert( end_index < exprs.size(), "Expected end_index < exprs.size. ");
- Assert( start_index <= end_index, "Expected start_index <= end_index. ");
-
- if(start_index == end_index) {
- return exprs[start_index];
- }
-
- unsigned pivot = findPivot(kinds, start_index, end_index - 1);
-
- Expr child_1 = createPrecedenceExpr(exprs, kinds, start_index, pivot);
- Expr child_2 = createPrecedenceExpr(exprs, kinds, pivot + 1, end_index);
- return d_exprManager->mkExpr(kinds[pivot], child_1, child_2);
-}
-
bool AntlrParser::checkDeclation(string varName, DeclarationCheck check) {
switch(check) {
case CHECK_DECLARED:
*/
Expr mkExpr(Kind kind, const std::vector<Expr>& children);
- /**
- * Creates a new expression based on the given string of expressions and kinds,
- * where kinds[i] is the operator to place between exprs[i] and exprs[i+1].
- * The expression is created so that it respects the kinds precedence table.
- * The exprs vector should be non-empty. If the length of exprs is N, then the
- * length of kinds should be N-1 (kinds may be empty).
- */
- Expr createPrecedenceExpr(const std::vector<Expr>& exprs, const std::vector<Kind>& kinds);
-
/**
* Creates a new predicated over the given sorts.
* @param p_name the name of the predicate
private:
-
- unsigned findPivot(const std::vector<Kind>& kinds, unsigned start_index, unsigned end_index) const;
-
- /**
- * Creates a new expression based on the given string of expressions and kinds
- * The expression is created so that it respects the kinds precedence table.
- * The exprs vector should be non-empty. The kinds vector should have one less
- * element than the exprs vector. start_index and end_index should be valid
- * indices into exprs.
- */
- Expr createPrecedenceExpr(const std::vector<Expr>& exprs, const std::vector<Kind>& kinds, unsigned start_index, unsigned end_index);
-
/** The expression manager */
ExprManager* d_exprManager;
* and associativity of the operators.
* @return the expression representing the formula
*/
-boolFormula returns [CVC4::Expr formula]
+boolFormula returns [CVC4::Expr formula]
+ : formula = boolAndFormula
+ ;
+
+/**
+ * Matches a Boolean AND formula of a given kind by doing a recursive descent.
+ */
+boolAndFormula returns [CVC4::Expr andFormula]
{
- vector<Expr> formulas;
- vector<Kind> kinds;
- Expr f;
- Kind k;
+ Expr e;
+ vector<Expr> exprs;
+}
+ : e = boolXorFormula { exprs.push_back(e); }
+ ( AND e = boolXorFormula { exprs.push_back(e); } )*
+ {
+ andFormula = (exprs.size() > 1 ? mkExpr(CVC4::AND, exprs) : exprs[0]);
+ }
+ ;
+
+/**
+ * Matches a Boolean XOR formula of a given kind by doing a recursive descent.
+ */
+boolXorFormula returns [CVC4::Expr xorFormula]
+{
+ Expr e;
+ vector<Expr> exprs;
+}
+ : e = boolOrFormula { exprs.push_back(e); }
+ ( XOR e = boolOrFormula { exprs.push_back(e); } )*
+ {
+ xorFormula = (exprs.size() > 1 ? mkExpr(CVC4::XOR, exprs) : exprs[0]);
+ }
+ ;
+
+/**
+ * Matches a Boolean OR formula of a given kind by doing a recursive descent.
+ */
+boolOrFormula returns [CVC4::Expr orFormula]
+{
+ Expr e;
+ vector<Expr> exprs;
}
- : f = primaryBoolFormula { formulas.push_back(f); }
- ( k = boolOperator { kinds.push_back(k); } f = primaryBoolFormula { formulas.push_back(f); } )*
+ : e = boolImpliesFormula { exprs.push_back(e); }
+ ( OR e = boolImpliesFormula { exprs.push_back(e); } )*
{
- // Create the expression based on precedences
- formula = createPrecedenceExpr(formulas, kinds);
+ orFormula = (exprs.size() > 1 ? mkExpr(CVC4::OR, exprs) : exprs[0]);
+ }
+ ;
+
+/**
+ * Matches a Boolean IMPLIES formula of a given kind by doing a recursive descent.
+ */
+boolImpliesFormula returns [CVC4::Expr impliesFormula]
+{
+ vector<Expr> exprs;
+ Expr e;
+}
+ : e = boolIffFormula { exprs.push_back(e); }
+ ( IMPLIES e = boolIffFormula { exprs.push_back(e); }
+ )*
+ {
+ impliesFormula = exprs.back();
+ for (int i = exprs.size() - 2; i >= 0; -- i) {
+ impliesFormula = mkExpr(CVC4::IMPLIES, exprs[i], impliesFormula);
+ }
}
;
+
+/**
+ * Matches a Boolean IFF formula of a given kind by doing a recursive descent.
+ */
+boolIffFormula returns [CVC4::Expr iffFormula]
+{
+ Expr e;
+}
+ : iffFormula = primaryBoolFormula
+ ( IFF e = primaryBoolFormula
+ { iffFormula = mkExpr(CVC4::IFF, iffFormula, e); }
+ )*
+ ;
/**
* Parses a primary Boolean formula. A primary Boolean formula is either a
| LPAREN formula = boolFormula RPAREN
;
-/**
- * Parses the Boolean operators and returns the corresponding CVC4 expression
- * kind.
- * @param the kind of the Boolean operator
- */
-boolOperator returns [CVC4::Kind kind]
- : IMPLIES { kind = CVC4::IMPLIES; }
- | AND { kind = CVC4::AND; }
- | OR { kind = CVC4::OR; }
- | XOR { kind = CVC4::XOR; }
- | IFF { kind = CVC4::IFF; }
- ;
-
/**
* Parses the Boolean atoms (variables and predicates).
* @return the expression representing the atom.
}
Parser::Parser(istream* input, AntlrParser* antlrParser, CharScanner* antlrLexer, bool deleteInput) :
- d_done(false), d_input(input), d_antlrParser(antlrParser), d_antlrLexer(antlrLexer), d_deleteInput(deleteInput) {
+ d_done(false), d_antlrParser(antlrParser), d_antlrLexer(antlrLexer), d_input(input), d_deleteInput(deleteInput) {
}
Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang,
std::istream* d_input;
/** Wherther to de-allocate the input */
- bool d_deleteInput;}; // end of class Parser
+ bool d_deleteInput;
+}; // end of class Parser
}/* CVC4::parser namespace */
}/* CVC4 namespace */
*/
parseExpr returns [CVC4::Expr expr]
: expr = annotatedFormula
+ | EOF
;
/**
const string goodSmtExprs[] = {
"(and a b)",
"(or (and a b) c)",
- "(implies (and (implies a b) a) b))",
+ "(implies (and (implies a b) a) b)",
"(and (iff a b) (not a))",
"(iff (xor a b) (and (or a b) (not (and a b))))"
};
projects / cvc5.git / commitdiff