summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/api/cpp/cvc5_kind.h9
-rw-r--r--src/parser/smt2/Smt2.g21
-rw-r--r--src/smt/command.cpp72
-rw-r--r--src/smt/command.h39
-rw-r--r--src/smt/quant_elim_solver.cpp12
-rw-r--r--src/smt/smt_engine.cpp12
-rw-r--r--src/smt/smt_engine.h10
-rw-r--r--src/theory/engine_output_channel.cpp6
-rw-r--r--src/theory/engine_output_channel.h2
-rw-r--r--src/theory/quantifiers/kinds2
-rw-r--r--src/theory/quantifiers/quantifiers_attributes.cpp51
-rw-r--r--src/theory/quantifiers/quantifiers_attributes.h17
-rw-r--r--src/theory/quantifiers/theory_quantifiers.cpp10
-rw-r--r--src/theory/quantifiers/theory_quantifiers.h4
-rw-r--r--src/theory/quantifiers/theory_quantifiers_type_rules.cpp12
-rw-r--r--src/theory/theory.h9
-rw-r--r--src/theory/theory_engine.cpp24
-rw-r--r--src/theory/theory_engine.h20
-rw-r--r--test/unit/test_smt.h1
19 files changed, 82 insertions, 251 deletions
diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index 2c5d2873e..e8b876b55 100644
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -3348,11 +3348,14 @@ enum CVC5_EXPORT Kind : int32_t
* 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,
/**
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 577aeb0a9..c3cf3ea66 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1815,26 +1815,15 @@ attribute[cvc5::api::Term& expr, cvc5::api::Term& retExpr]
{
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]
{
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 7aa05dde1..1981f1063 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1531,78 +1531,6 @@ void DeclareHeapCommand::toStream(std::ostream& out,
}
/* -------------------------------------------------------------------------- */
-/* 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 */
/* -------------------------------------------------------------------------- */
diff --git a/src/smt/command.h b/src/smt/command.h
index 5a67e6685..b83da5825 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -616,42 +616,6 @@ class CVC5_EXPORT DeclareHeapCommand : public Command
};
/**
- * 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.
*/
@@ -1000,9 +964,6 @@ class CVC5_EXPORT GetModelCommand : public Command
{
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;
diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp
index 185a60e46..e675feaa0 100644
--- a/src/smt/quant_elim_solver.cpp
+++ b/src/smt/quant_elim_solver.cpp
@@ -24,6 +24,7 @@
#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;
@@ -47,7 +48,6 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as,
"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
@@ -56,14 +56,11 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as,
<< 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]);
@@ -87,6 +84,7 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as,
// 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
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 61aed2009..f55bfa88b 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1921,18 +1921,6 @@ void SmtEngine::printStatisticsDiff() const
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());
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index df8346de7..208c83db8 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -824,16 +824,6 @@ class CVC5_EXPORT SmtEngine
*/
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;
diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp
index ee07dcd57..218175ee9 100644
--- a/src/theory/engine_output_channel.cpp
+++ b/src/theory/engine_output_channel.cpp
@@ -116,12 +116,6 @@ void EngineOutputChannel::spendResource(Resource r)
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);
diff --git a/src/theory/engine_output_channel.h b/src/theory/engine_output_channel.h
index cc1d8ece7..468825a7e 100644
--- a/src/theory/engine_output_channel.h
+++ b/src/theory/engine_output_channel.h
@@ -61,8 +61,6 @@ class EngineOutputChannel : public theory::OutputChannel
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
diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds
index 4561226e1..250082952 100644
--- a/src/theory/quantifiers/kinds
+++ b/src/theory/quantifiers/kinds
@@ -34,7 +34,7 @@ sort INST_PATTERN_TYPE \
# 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"
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index 33ed6f536..7204a60e1 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -35,7 +35,10 @@ bool QAttributes::isStandard() const
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")
{
@@ -50,8 +53,8 @@ void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::ve
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 );
@@ -183,6 +186,7 @@ void QuantAttributes::computeAttributes( Node q ) {
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();
@@ -199,7 +203,28 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){
}
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
@@ -222,9 +247,21 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){
}
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());
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index 910dbab5b..48fb4f159 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -179,16 +179,15 @@ class QuantAttributes
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);
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index a108d4614..2ad475f01 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -40,12 +40,6 @@ TheoryQuantifiers::TheoryQuantifiers(Env& env,
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));
@@ -188,10 +182,6 @@ bool TheoryQuantifiers::preNotifyFact(
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
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 0ef5cfcbb..1d721a0ae 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -77,10 +77,6 @@ class TheoryQuantifiers : public Theory {
{
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. */
diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.cpp b/src/theory/quantifiers/theory_quantifiers_type_rules.cpp
index 6fb377a56..14f066ce1 100644
--- a/src/theory/quantifiers/theory_quantifiers_type_rules.cpp
+++ b/src/theory/quantifiers/theory_quantifiers_type_rules.cpp
@@ -106,6 +106,18 @@ TypeNode QuantifierAnnotationTypeRule::computeType(NodeManager* nodeManager,
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();
}
diff --git a/src/theory/theory.h b/src/theory/theory.h
index bde00b908..44a0e597b 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -775,15 +775,6 @@ class Theory {
*/
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;
/**
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index bd621126c..6bec3dc8f 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -253,8 +253,7 @@ TheoryEngine::TheoryEngine(Env& env)
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)
@@ -1833,27 +1832,6 @@ TrustNode TheoryEngine::getExplanation(
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];
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 3f2e589b3..e610adcf7 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -660,27 +660,7 @@ public:
/** 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.
diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h
index f1644dfcd..1cc6b0507 100644
--- a/test/unit/test_smt.h
+++ b/test/unit/test_smt.h
@@ -136,7 +136,6 @@ class DummyOutputChannel : public cvc5::theory::OutputChannel
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(); }
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback