diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-16 09:29:15 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-16 09:29:15 +0100 |
| commit | 338ec2ee86e16423b265ba9bfc036606223f846f (patch) | |
| tree | 22f92c46fc4c70b839e74b13611c38f6277c3682 /src/parser/smt2 | |
| parent | 0042f301908763cf1edb8a2d56b3f373a0055908 (diff) | |
Minor: Ensure indexed terms are in EE. Add support for bv constants in sygus parser.
Diffstat (limited to 'src/parser/smt2')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 17 |
1 files changed, 16 insertions, 1 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 320fead5f..67f26533e 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -640,7 +640,8 @@ sygusCommand returns [CVC4::Command* cmd = NULL] const DatatypeConstructor& ctor = dt[j]; std::vector<Expr> bvs, extraArgs; for(size_t k = 0; k < ctor.getNumArgs(); ++k) { - Expr bv = EXPR_MANAGER->mkBoundVar(ctor[k].getName(), SelectorType(ctor[k].getType()).getRangeType()); + std::string vname = "v_" + ctor[k].getName(); + Expr bv = EXPR_MANAGER->mkBoundVar(vname, SelectorType(ctor[k].getType()).getRangeType()); bvs.push_back(bv); extraArgs.push_back(bv); } @@ -757,11 +758,25 @@ sygusGTerm[CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops] { assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 ); std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2); ops.push_back(MK_CONST( BitVector(hexString, 16) )); + name = dt.getName() + "_" + AntlrInput::tokenText($HEX_LITERAL); + std::string testerId("is-"); + testerId.append(name); + PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); + PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); + CVC4::DatatypeConstructor c(name, testerId); + dt.addConstructor(c); } | BINARY_LITERAL { assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 ); std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2); ops.push_back(MK_CONST( BitVector(binString, 2) )); + name = dt.getName() + "_" + AntlrInput::tokenText($BINARY_LITERAL); + std::string testerId("is-"); + testerId.append(name); + PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); + PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); + CVC4::DatatypeConstructor c(name, testerId); + dt.addConstructor(c); } | symbol[name,CHECK_DECLARED,SYM_VARIABLE] { Expr bv = PARSER_STATE->getVariable(name); |