This makes INST_ATTRIBUTE (optionally) take multiple children, giving a way for the user to set attributes on quantified formulas, which does not require a new API command.
This is a special case of term annotations that occur as the body of a quantified formula.
If we need to extend our API to support further user-provided attributes, we should use a similar approach, e.g. a new kind ANNOTATE.
* Specifies a custom property for a quantified formula given by a
* term that is ascribed a user attribute.
*
- * Parameters:
- * - 1: Term with a user attribute.
+ * Parameters: n >= 1
+ * - 1: The keyword of the attribute (a term with kind CONST_STRING).
+ * - 2...n: The values of the attribute.
*
* Create with:
- * - `Solver::mkTerm(Kind kind, const Term& child) const`
+ * - `mkTerm(Kind kind, Term child1, Term child2)
+ * - `mkTerm(Kind kind, Term child1, Term child2, Term child3)
+ * - `mkTerm(Kind kind, const std::vector<Term>& children)
*/
INST_ATTRIBUTE,
/**
{
std::stringstream sIntLit;
sIntLit << $INTEGER_LITERAL;
+ api::Term keyword = SOLVER->mkString("quant-inst-max-level");
api::Term n = SOLVER->mkInteger(sIntLit.str());
- std::vector<api::Term> values;
- values.push_back( n );
- std::string attr_name(AntlrInput::tokenText($tok));
- attr_name.erase( attr_name.begin() );
- api::Sort boolType = SOLVER->getBooleanSort();
- api::Term avar = PARSER_STATE->bindVar(attr_name, boolType);
- retExpr = MK_TERM(api::INST_ATTRIBUTE, avar);
- Command* c = new SetUserAttributeCommand(attr_name, avar, values);
- c->setMuted(true);
- PARSER_STATE->preemptCommand(c);
+ retExpr = MK_TERM(api::INST_ATTRIBUTE, keyword, n);
}
| tok=( ATTRIBUTE_QUANTIFIER_ID_TOK ) symbolicExpr[sexpr]
{
- api::Sort boolType = SOLVER->getBooleanSort();
- api::Term avar = SOLVER->mkConst(boolType, sexprToString(sexpr));
- retExpr = MK_TERM(api::INST_ATTRIBUTE, avar);
- Command* c = new SetUserAttributeCommand("qid", avar);
- c->setMuted(true);
- PARSER_STATE->preemptCommand(c);
+ api::Term keyword = SOLVER->mkString("qid");
+ api::Term name = SOLVER->mkString(sexprToString(sexpr));
+ retExpr = MK_TERM(api::INST_ATTRIBUTE, keyword, name);
}
| ATTRIBUTE_NAMED_TOK symbolicExpr[sexpr]
{
out, sortToTypeNode(d_locSort), sortToTypeNode(d_dataSort));
}
-/* -------------------------------------------------------------------------- */
-/* class SetUserAttributeCommand */
-/* -------------------------------------------------------------------------- */
-
-SetUserAttributeCommand::SetUserAttributeCommand(
- const std::string& attr,
- api::Term term,
- const std::vector<api::Term>& termValues,
- const std::string& strValue)
- : d_attr(attr), d_term(term), d_termValues(termValues), d_strValue(strValue)
-{
-}
-
-SetUserAttributeCommand::SetUserAttributeCommand(const std::string& attr,
- api::Term term)
- : SetUserAttributeCommand(attr, term, {}, "")
-{
-}
-
-SetUserAttributeCommand::SetUserAttributeCommand(
- const std::string& attr,
- api::Term term,
- const std::vector<api::Term>& values)
- : SetUserAttributeCommand(attr, term, values, "")
-{
-}
-
-SetUserAttributeCommand::SetUserAttributeCommand(const std::string& attr,
- api::Term term,
- const std::string& value)
- : SetUserAttributeCommand(attr, term, {}, value)
-{
-}
-
-void SetUserAttributeCommand::invoke(api::Solver* solver, SymbolManager* sm)
-{
- try
- {
- if (!d_term.isNull())
- {
- solver->getSmtEngine()->setUserAttribute(d_attr,
- termToNode(d_term),
- termVectorToNodes(d_termValues),
- d_strValue);
- }
- d_commandStatus = CommandSuccess::instance();
- }
- catch (exception& e)
- {
- d_commandStatus = new CommandFailure(e.what());
- }
-}
-
-Command* SetUserAttributeCommand::clone() const
-{
- return new SetUserAttributeCommand(d_attr, d_term, d_termValues, d_strValue);
-}
-
-std::string SetUserAttributeCommand::getCommandName() const
-{
- return "set-user-attribute";
-}
-
-void SetUserAttributeCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- OutputLanguage language) const
-{
- Printer::getPrinter(language)->toStreamCmdSetUserAttribute(
- out, d_attr, termToNode(d_term));
-}
-
/* -------------------------------------------------------------------------- */
/* class SimplifyCommand */
/* -------------------------------------------------------------------------- */
api::Sort d_dataSort;
};
-/**
- * The command when an attribute is set by a user. In SMT-LIBv2 this is done
- * via the syntax (! expr :attr)
- */
-class CVC5_EXPORT SetUserAttributeCommand : public Command
-{
- public:
- SetUserAttributeCommand(const std::string& attr, api::Term term);
- SetUserAttributeCommand(const std::string& attr,
- api::Term term,
- const std::vector<api::Term>& values);
- SetUserAttributeCommand(const std::string& attr,
- api::Term term,
- const std::string& value);
-
- void invoke(api::Solver* solver, SymbolManager* sm) override;
- Command* clone() const override;
- std::string getCommandName() const override;
- void toStream(
- std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- OutputLanguage language = language::output::LANG_AUTO) const override;
-
- private:
- SetUserAttributeCommand(const std::string& attr,
- api::Term term,
- const std::vector<api::Term>& termValues,
- const std::string& strValue);
-
- const std::string d_attr;
- const api::Term d_term;
- const std::vector<api::Term> d_termValues;
- const std::string d_strValue;
-}; /* class SetUserAttributeCommand */
-
/**
* The command when parsing check-sat.
* This command will check satisfiability of the input formula.
{
public:
GetModelCommand();
-
- // Model is private to the library -- for now
- // Model* getResult() const ;
void invoke(api::Solver* solver, SymbolManager* sm) override;
void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
Command* clone() const override;
#include "theory/quantifiers_engine.h"
#include "theory/rewriter.h"
#include "theory/theory_engine.h"
+#include "util/string.h"
using namespace cvc5::theory;
using namespace cvc5::kind;
"Expecting a quantified formula as argument to get-qe.");
}
NodeManager* nm = NodeManager::currentNM();
- SkolemManager* sm = nm->getSkolemManager();
// ensure the body is rewritten
q = nm->mkNode(q.getKind(), q[0], Rewriter::rewrite(q[1]));
// do nested quantifier elimination if necessary
<< q << std::endl;
// tag the quantified formula with the quant-elim attribute
TypeNode t = nm->booleanType();
- Node n_attr = sm->mkDummySkolem("qe", t, "Auxiliary variable for qe attr.");
- std::vector<Node> node_values;
TheoryEngine* te = d_smtSolver.getTheoryEngine();
Assert(te != nullptr);
- te->setUserAttribute(
- doFull ? "quant-elim" : "quant-elim-partial", n_attr, node_values, "");
- QuantifiersEngine* qe = te->getQuantifiersEngine();
- n_attr = nm->mkNode(INST_ATTRIBUTE, n_attr);
+ Node keyword =
+ nm->mkConst(String(doFull ? "quant-elim" : "quant-elim-partial"));
+ Node n_attr = nm->mkNode(INST_ATTRIBUTE, keyword);
n_attr = nm->mkNode(INST_PATTERN_LIST, n_attr);
std::vector<Node> children;
children.push_back(q[0]);
// failed, return original
return q;
}
+ QuantifiersEngine* qe = te->getQuantifiersEngine();
// must use original quantified formula to compute QE, which ensures that
// e.g. term formula removal is not run on the body. Notice that we assume
// that the (single) quantified formula is preprocessed, rewritten
d_env->getStatisticsRegistry().storeSnapshot();
}
-void SmtEngine::setUserAttribute(const std::string& attr,
- Node expr,
- const std::vector<Node>& expr_values,
- const std::string& str_value)
-{
- SmtScope smts(this);
- finishInit();
- TheoryEngine* te = getTheoryEngine();
- Assert(te != nullptr);
- te->setUserAttribute(attr, expr, expr_values, str_value);
-}
-
void SmtEngine::setOption(const std::string& key, const std::string& value)
{
NodeManagerScope nms(getNodeManager());
*/
void printStatisticsDiff() const;
- /**
- * Set user attribute.
- * This function is called when an attribute is set by a user.
- * In SMT-LIBv2 this is done via the syntax (! expr :attr)
- */
- void setUserAttribute(const std::string& attr,
- Node expr,
- const std::vector<Node>& expr_values,
- const std::string& str_value);
-
/** Get the options object (const and non-const versions) */
Options& getOptions();
const Options& getOptions() const;
d_engine->spendResource(r);
}
-void EngineOutputChannel::handleUserAttribute(const char* attr,
- theory::Theory* t)
-{
- d_engine->handleUserAttribute(attr, t);
-}
-
void EngineOutputChannel::trustedConflict(TrustNode pconf)
{
Assert(pconf.getKind() == TrustNodeKind::CONFLICT);
void spendResource(Resource r) override;
- void handleUserAttribute(const char* attr, theory::Theory* t) override;
-
/**
* Let pconf be the pair (Node conf, ProofGenerator * pfg). This method
* sends conf on the output channel of this class whose proof can be generated
# An instantiation pattern may have more than 1 child, in which case it specifies a multi-trigger.
operator INST_PATTERN 1: "instantiation pattern"
operator INST_NO_PATTERN 1 "instantiation no-pattern"
-operator INST_ATTRIBUTE 1 "instantiation attribute"
+operator INST_ATTRIBUTE 1: "instantiation attribute"
operator INST_POOL 1: "instantiation pool"
operator INST_ADD_TO_POOL 2 "instantiation add to pool"
operator SKOLEM_ADD_TO_POOL 2 "skolemization add to pool"
QuantAttributes::QuantAttributes() {}
-void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::vector< Node >& node_values, std::string str_value ){
+void QuantAttributes::setUserAttribute(const std::string& attr,
+ TNode n,
+ const std::vector<Node>& nodeValues)
+{
Trace("quant-attr-debug") << "Set " << attr << " " << n << std::endl;
if (attr == "fun-def")
{
QuantNameAttribute qna;
n.setAttribute(qna, true);
}else if( attr=="quant-inst-max-level" ){
- Assert(node_values.size() == 1);
- uint64_t lvl = node_values[0].getConst<Rational>().getNumerator().getLong();
+ Assert(nodeValues.size() == 1);
+ uint64_t lvl = nodeValues[0].getConst<Rational>().getNumerator().getLong();
Trace("quant-attr-debug") << "Set instantiation level " << n << " to " << lvl << std::endl;
QuantInstLevelAttribute qila;
n.setAttribute( qila, lvl );
void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){
Trace("quant-attr-debug") << "Compute attributes for " << q << std::endl;
if( q.getNumChildren()==3 ){
+ NodeManager* nm = NodeManager::currentNM();
qa.d_ipl = q[2];
for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
Kind k = q[2][i].getKind();
}
else if (k == INST_ATTRIBUTE)
{
- Node avar = q[2][i][0];
+ Node avar;
+ // We support two use cases of INST_ATTRIBUTE:
+ // (1) where the user constructs a term of the form
+ // (INST_ATTRIBUTE "keyword" [nodeValues])
+ // (2) where we internally generate nodes of the form
+ // (INST_ATTRIBUTE v) where v has an internal attribute set on it.
+ // We distinguish these two cases by checking the kind of the first
+ // child.
+ if (q[2][i][0].getKind() == CONST_STRING)
+ {
+ // make a dummy variable to be used below
+ avar = nm->mkBoundVar(nm->booleanType());
+ std::vector<Node> nodeValues(q[2][i].begin() + 1, q[2][i].end());
+ // set user attribute on the dummy variable
+ setUserAttribute(
+ q[2][i][0].getConst<String>().toString(), avar, nodeValues);
+ }
+ else
+ {
+ // assume the dummy variable has already had its attributes set
+ avar = q[2][i][0];
+ }
if( avar.getAttribute(FunDefAttribute()) ){
Trace("quant-attr") << "Attribute : function definition : " << q << std::endl;
//get operator directly from pattern
}
if (avar.getAttribute(QuantNameAttribute()))
{
- Trace("quant-attr") << "Attribute : quantifier name : " << avar
- << " for " << q << std::endl;
- qa.d_name = avar;
+ // only set the name if there is a value
+ if (q[2][i].getNumChildren() > 1)
+ {
+ Trace("quant-attr") << "Attribute : quantifier name : "
+ << q[2][i][1].getConst<String>().toString()
+ << " for " << q << std::endl;
+ // assign the name to a variable with the given name (to avoid
+ // enclosing the name in quotes)
+ qa.d_name = nm->mkBoundVar(q[2][i][1].getConst<String>().toString(),
+ nm->booleanType());
+ }
+ else
+ {
+ Warning() << "Missing name for qid attribute";
+ }
}
if( avar.hasAttribute(QuantInstLevelAttribute()) ){
qa.d_qinstLevel = avar.getAttribute(QuantInstLevelAttribute());
QuantAttributes();
~QuantAttributes(){}
/** set user attribute
- * This function applies an attribute
- * This can be called when we mark expressions with attributes, e.g. (! q
- * :attribute attr [node_values, str_value...]),
- * It can also be called internally in various ways (for SyGus, quantifier
- * elimination, etc.)
- */
+ * This function applies an attribute
+ * This can be called when we mark expressions with attributes, e.g. (! q
+ * :attribute attr [nodeValues]),
+ * It can also be called internally in various ways (for SyGus, quantifier
+ * elimination, etc.)
+ */
static void setUserAttribute(const std::string& attr,
- Node q,
- std::vector<Node>& node_values,
- std::string str_value);
+ TNode q,
+ const std::vector<Node>& nodeValues);
/** compute quantifier attributes */
static void computeQuantAttributes(Node q, QAttributes& qa);
d_qim(*this, d_qstate, d_qreg, d_treg, d_pnm),
d_qengine(nullptr)
{
- out.handleUserAttribute( "fun-def", this );
- out.handleUserAttribute("qid", this);
- out.handleUserAttribute( "quant-inst-max-level", this );
- out.handleUserAttribute( "quant-elim", this );
- out.handleUserAttribute( "quant-elim-partial", this );
-
// construct the quantifiers engine
d_qengine.reset(
new QuantifiersEngine(d_qstate, d_qreg, d_treg, d_qim, d_pnm));
return true;
}
-void TheoryQuantifiers::setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value){
- QuantAttributes::setUserAttribute( attr, n, node_values, str_value );
-}
-
} // namespace quantifiers
} // namespace theory
} // namespace cvc5
{
return std::string("TheoryQuantifiers");
}
- void setUserAttribute(const std::string& attr,
- Node n,
- std::vector<Node> node_values,
- std::string str_value) override;
private:
/** The theory rewriter for this theory. */
TNode n,
bool check)
{
+ if (n.getKind() == kind::INST_ATTRIBUTE)
+ {
+ if (n.getNumChildren() > 1)
+ {
+ // first must be a keyword
+ if (n[0].getKind() != kind::CONST_STRING)
+ {
+ throw TypeCheckingExceptionPrivate(
+ n[0], "Expecting a keyword at the head of INST_ATTRIBUTE.");
+ }
+ }
+ }
return nodeManager->instPatternType();
}
*/
virtual std::string identify() const = 0;
- /** Set user attribute
- * This function is called when an attribute is set by a user. In SMT-LIBv2 this is done
- * via the syntax (! n :attr)
- */
- virtual void setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value) {
- Unimplemented() << "Theory " << identify()
- << " doesn't support Theory::setUserAttribute interface";
- }
-
typedef context::CDList<Assertion>::const_iterator assertions_iterator;
/**
d_false(),
d_interrupted(false),
d_inPreregister(false),
- d_factsAsserted(d_env.getContext(), false),
- d_attr_handle()
+ d_factsAsserted(d_env.getContext(), false)
{
for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST;
++ theoryId)
bool TheoryEngine::isProofEnabled() const { return d_pnm != nullptr; }
-void TheoryEngine::setUserAttribute(const std::string& attr,
- Node n,
- const std::vector<Node>& node_values,
- const std::string& str_value)
-{
- Trace("te-attr") << "set user attribute " << attr << " " << n << endl;
- if( d_attr_handle.find( attr )!=d_attr_handle.end() ){
- for( size_t i=0; i<d_attr_handle[attr].size(); i++ ){
- d_attr_handle[attr][i]->setUserAttribute(attr, n, node_values, str_value);
- }
- } else {
- //unhandled exception?
- }
-}
-
-void TheoryEngine::handleUserAttribute(const char* attr, Theory* t) {
- Trace("te-attr") << "Handle user attribute " << attr << " " << t << endl;
- std::string str( attr );
- d_attr_handle[ str ].push_back( t );
-}
-
void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) {
for(TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
Theory* theory = d_theoryTable[theoryId];
/** Prints the assertions to the debug stream */
void printAssertions(const char* tag);
-private:
-
- std::map< std::string, std::vector< theory::Theory* > > d_attr_handle;
-
public:
- /** Set user attribute.
- *
- * This function is called when an attribute is set by a user. In SMT-LIBv2
- * this is done via the syntax (! n :attr)
- */
- void setUserAttribute(const std::string& attr,
- Node n,
- const std::vector<Node>& node_values,
- const std::string& str_value);
-
- /** Handle user attribute.
- *
- * Associates theory t with the attribute attr. Theory t will be
- * notified whenever an attribute of name attr is set.
- */
- void handleUserAttribute(const char* attr, theory::Theory* t);
/**
* Check that the theory assertions are satisfied in the model.
void requirePhase(TNode, bool) override {}
void setIncomplete(theory::IncompleteId id) override {}
- void handleUserAttribute(const char* attr, theory::Theory* t) override {}
void clear() { d_callHistory.clear(); }
projects / cvc5.git / commitdiff