Skip to content

Commit

Permalink
Add new utility methods to smt2 parser state (cvc5#9360)
Browse files Browse the repository at this point in the history 
This adds new methods to the smt2 parser state class in preparation for the flex parser.

In particular, since no theory-specific operators will be lexed, we will not have custom parsing rules for e.g. set.comprehension. Thus, we require a new notion of a "closure kind".

We also will parse indexed symbols that are indexed by symbols in a uniform way, requiring new variants for mkIndexedConstant and mkIndexedOp.
  • Loading branch information
@ajreynol
ajreynol committed Dec 20, 2022
1 parent 89f34c8 commit 5e8ea0a
Show file tree
Hide file tree
Showing 2 changed files with 147 additions and 0 deletions.
121 changes: 121 additions & 0 deletions src/parser/smt2/smt2.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -292,6 +292,8 @@ void Smt2State::addCoreSymbols()
addOperator(NOT, "not");
addOperator(OR, "or");
addOperator(XOR, "xor");
addClosureKind(FORALL, "forall");
addClosureKind(EXISTS, "exists");
}

void Smt2State::addOperator(Kind kind, const std::string& name)
Expand All @@ -308,6 +310,13 @@ void Smt2State::addIndexedOperator(Kind tKind, const std::string& name)
d_indexedOpKindMap[name] = tKind;
}

void Smt2State::addClosureKind(Kind tKind, const std::string& name)
{
// also include it as a normal operator
addOperator(tKind, name);
d_closureKindMap[name] = tKind;
}

bool Smt2State::isIndexedOperatorEnabled(const std::string& name) const
{
return d_indexedOpKindMap.find(name) != d_indexedOpKindMap.end();
Expand Down Expand Up @@ -462,6 +471,98 @@ Term Smt2State::mkIndexedConstant(const std::string& name,
return Term();
}

Term Smt2State::mkIndexedConstant(const std::string& name,
const std::vector<std::string>& symbols)
{
if (d_logic.isTheoryEnabled(internal::theory::THEORY_STRINGS))
{
if (name == "char")
{
if (symbols.size() != 1)
{
parseError("Unexpected number of indices for char");
}
if (symbols[0].length() <= 2 || symbols[0].substr(0, 2) != "#x")
{
parseError(std::string("Unexpected index for char: `") + symbols[0]
+ "'");
}
return mkCharConstant(symbols[0].substr(2));
}
}
else if (d_logic.hasCardinalityConstraints())
{
if (name == "fmf.card")
{
if (symbols.size() != 2)
{
parseError("Unexpected number of indices for fmf.card");
}
Sort t = getSort(symbols[0]);
// convert second symbol back to a numeral
uint32_t ubound = stringToUnsigned(symbols[1]);
return d_solver->mkCardinalityConstraint(t, ubound);
}
}
parseError(std::string("Unknown indexed literal `") + name + "'");
return Term();
}

Term Smt2State::mkIndexedOp(const std::string& name,
const std::vector<std::string>& symbols)
{
if (d_logic.isTheoryEnabled(internal::theory::THEORY_DATATYPES))
{
if (name == "is" || name == "update")
{
if (symbols.size() != 1)
{
parseError(std::string("Unexpected number of indices for " + name));
}
const std::string& cname = symbols[0];
// must be declared
checkDeclaration(cname, CHECK_DECLARED, SYM_VARIABLE);
Term f = getExpressionForName(cname);
if (f.getKind() == APPLY_CONSTRUCTOR && f.getNumChildren() == 1)
{
// for nullary constructors, must get the operator
f = f[0];
}
if (name == "is")
{
if (!f.getSort().isDatatypeConstructor())
{
parseError("Bad syntax for (_ is X), X must be a constructor.");
}
// get the datatype that f belongs to
Sort sf = f.getSort().getDatatypeConstructorCodomainSort();
Datatype d = sf.getDatatype();
// lookup by name
DatatypeConstructor dc = d.getConstructor(f.toString());
return dc.getTesterTerm();
}
else
{
Assert(name == "update");
if (!f.getSort().isDatatypeSelector())
{
parseError("Bad syntax for (_ update X), X must be a selector.");
}
std::string sname = f.toString();
// get the datatype that f belongs to
Sort sf = f.getSort().getDatatypeSelectorDomainSort();
Datatype d = sf.getDatatype();
// find the selector
DatatypeSelector ds = d.getSelector(f.toString());
// get the updater term
return ds.getUpdaterTerm();
}
}
}
parseError(std::string("Unknown indexed literal `") + name + "'");
return Term();
}

Kind Smt2State::getIndexedOpKind(const std::string& name)
{
const auto& kIt = d_indexedOpKindMap.find(name);
Expand All @@ -473,6 +574,17 @@ Kind Smt2State::getIndexedOpKind(const std::string& name)
return UNDEFINED_KIND;
}

Kind Smt2State::getClosureKind(const std::string& name)
{
const auto& kIt = d_closureKindMap.find(name);
if (kIt != d_closureKindMap.end())
{
return (*kIt).second;
}
parseError(std::string("Unknown closure `") + name + "'");
return UNDEFINED_KIND;
}

Term Smt2State::bindDefineFunRec(
const std::string& fname,
const std::vector<std::pair<std::string, Sort>>& sortedVarNames,
Expand Down Expand Up @@ -592,6 +704,8 @@ Command* Smt2State::setLogic(std::string name, bool fromCommand)
if (d_logic.isHigherOrder())
{
addOperator(HO_APPLY, "@");
// lambda is a closure kind
addClosureKind(LAMBDA, "lambda");
}

if (d_logic.isTheoryEnabled(internal::theory::THEORY_ARITH))
Expand Down Expand Up @@ -704,6 +818,8 @@ Command* Smt2State::setLogic(std::string name, bool fromCommand)
addIndexedOperator(RELATION_GROUP, "rel.group");
addIndexedOperator(RELATION_AGGREGATE, "rel.aggr");
addIndexedOperator(RELATION_PROJECT, "rel.project");
// set.comprehension is a closure kind
addClosureKind(SET_COMPREHENSION, "set.comprehension");
}

if (d_logic.isTheoryEnabled(internal::theory::THEORY_BAGS))
Expand Down Expand Up @@ -1470,6 +1586,11 @@ Sort Smt2State::getIndexedSort(const std::string& name,
return ret;
}

bool Smt2State::isClosure(const std::string& name)
{
return d_closureKindMap.find(name) != d_closureKindMap.end();
}

std::unique_ptr<Command> Smt2State::handlePush(std::optional<uint32_t> nscopes)
{
checkThatLogicIsSet();
Expand Down
26 changes: 26 additions & 0 deletions src/parser/smt2/smt2.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,14 @@ class Smt2State : public ParserState
* @param name The name of the symbol (e.g. "extract")
*/
void addIndexedOperator(Kind tKind, const std::string& name);
/**
* Registers a closure kind
*
* @param tKind The kind of the term that uses the operator kind (e.g.
* LAMBDA).
* @param name The name of the symbol (e.g. "lambda")
*/
void addClosureKind(Kind tKind, const std::string& name);
/**
* Checks whether an indexed operator is enabled. All indexed operators in
* the current logic are considered to be enabled. This includes operators
Expand Down Expand Up @@ -111,6 +119,12 @@ class Smt2State : public ParserState
*/
Term mkIndexedConstant(const std::string& name,
const std::vector<uint32_t>& numerals);
/** Same as above, for constants indexed by symbols. */
Term mkIndexedConstant(const std::string& name,
const std::vector<std::string>& symbols);
/** Same as above, for constants indexed by symbols. */
Term mkIndexedOp(const std::string& name,
const std::vector<std::string>& symbols);

/**
* Creates an indexed operator kind, e.g. BITVECTOR_EXTRACT for "extract".
Expand All @@ -120,6 +134,14 @@ class Smt2State : public ParserState
* error if the name is not valid.
*/
Kind getIndexedOpKind(const std::string& name);
/**
* Creates the closure kind, e.g. FORALL for "forall".
*
* @param name The name of the operator (e.g. "forall")
* @return The kind corresponding to the closure or a parse
* error if the name is not valid.
*/
Kind getClosureKind(const std::string& name);

/**
* If we are in a version < 2.6, this updates name to the tester name of cons,
Expand Down Expand Up @@ -375,6 +397,8 @@ class Smt2State : public ParserState
*/
Sort getIndexedSort(const std::string& name,
const std::vector<std::string>& numerals);
/** is closure? */
bool isClosure(const std::string& name);
//------------------------- end processing parse operators

/**
Expand Down Expand Up @@ -437,6 +461,8 @@ class Smt2State : public ParserState
* BITVECTOR_EXTRACT).
*/
std::unordered_map<std::string, Kind> d_indexedOpKindMap;
/** Closure map */
std::unordered_map<std::string, Kind> d_closureKindMap;
/** The last named term and its name */
std::pair<Term, std::string> d_lastNamedTerm;
/**
Expand Down

0 comments on commit 5e8ea0a

Please sign in to comment.