diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-14 10:42:39 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-14 10:42:39 -0500 |
| commit | beb73911f71daa6711390264221e7b4de7dc8c6c (patch) | |
| tree | dc102dfca7f3ac87944af7760de759fe56a2b648 /src/theory/quantifiers_engine.h | |
| parent | 5887766342258361d3635a5b29a015dadb9ebe83 (diff) | |
Lemma cache in theory sep. Minor optimization for sets. Minor improvements to EPR
Diffstat (limited to 'src/theory/quantifiers_engine.h')
| -rw-r--r-- | src/theory/quantifiers_engine.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index bcc33327e..25542e49e 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -333,6 +333,8 @@ public: bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true ); /** add split equality */ bool addSplitEquality( Node n1, Node n2, bool reqPhase = false, bool reqPhasePol = true ); + /** add EPR axiom */ + bool addEPRAxiom( TypeNode tn ); /** mark relevant quantified formula, this will indicate it should be checked before the others */ void markRelevant( Node q ); /** has added lemma */ |