summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.h
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2014-08-18 12:47:07 +0200
committerajreynol <andrew.j.reynolds@gmail.com>2014-08-18 12:47:07 +0200
commitfe7a5119d5b48a2546ece43574bc4d07e86c14a7 (patch)
treee64192933867061c3b215ee02e0d3aafad6b419e /src/theory/theory_engine.h
parent18da2141dcddf221f0a40782b02a24766f0ed2c7 (diff)
Add support for quantifier-specific instantiation levels. Add option for setting inst-level 0 only for input terms.
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r--src/theory/theory_engine.h2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index e6684d56e..eec4f1168 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -820,7 +820,7 @@ public:
* 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);
+ void setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value);
/**
* Handle user attribute.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback