diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-13 14:21:47 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-13 14:21:47 -0500 |
| commit | 4b86268a71d0d6fd179134889f7d15304623b130 (patch) | |
| tree | 9a736babe6e79286b20641f7c056390c9108c66a /src/parser | |
| parent | df642ec7d4eef0e2f994751be53e66201f2b92f9 (diff) | |
Statistics on instantiations per quantified formula. (#4719)
This adds a new print format for instantiations --print-instantiations=num, which prints the total number of instantations of quantified formulas. This count is user-context-dependent, which is in sync with the existing print-instantiation format (list).
It also simplifies and improves printing of Instantiation Tries.
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index cc87306e3..62ea4e4fa 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1898,6 +1898,16 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr] c->setMuted(true); PARSER_STATE->preemptCommand(c); } + | tok=( ATTRIBUTE_QUANTIFIER_ID_TOK ) symbolicExpr[sexpr] + { + api::Sort boolType = SOLVER->getBooleanSort(); + api::Term avar = SOLVER->mkVar(boolType, sexpr.toString()); + attr = std::string(":qid"); + retExpr = MK_TERM(api::INST_ATTRIBUTE, avar); + Command* c = new SetUserAttributeCommand("qid", avar.getExpr()); + c->setMuted(true); + PARSER_STATE->preemptCommand(c); + } | ATTRIBUTE_NAMED_TOK symbolicExpr[sexpr] { attr = std::string(":named"); @@ -2351,6 +2361,7 @@ ATTRIBUTE_PATTERN_TOK : ':pattern'; ATTRIBUTE_NO_PATTERN_TOK : ':no-pattern'; ATTRIBUTE_NAMED_TOK : ':named'; ATTRIBUTE_INST_LEVEL : ':quant-inst-max-level'; +ATTRIBUTE_QUANTIFIER_ID_TOK : ':qid'; // operators (NOTE: theory symbols go here) EXISTS_TOK : 'exists'; |