diff options
Diffstat (limited to 'src/theory/quantifiers/skolemize.h')
| -rw-r--r-- | src/theory/quantifiers/skolemize.h | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h index 8cf3e3176..b28854baf 100644 --- a/src/theory/quantifiers/skolemize.h +++ b/src/theory/quantifiers/skolemize.h @@ -108,15 +108,18 @@ class Skolemize Node getSkolemizedBody(Node q); /** is n a variable that we can apply inductive strenghtening to? */ static bool isInductionTerm(Node n); - /** print all skolemizations + /** + * Get skolemization vectors, where for each quantified formula that was + * skolemized, this is the list of skolems that were used to witness the + * negation of that quantified formula (which is equivalent to an existential + * one). + * * This is used for the command line option * --dump-instantiations - * which prints an informal justification - * of steps taken by the quantifiers module. - * Returns true if we printed at least one - * skolemization. + * which prints an informal justification of steps taken by the quantifiers + * module. */ - bool printSkolemization(std::ostream& out); + void getSkolemTermVectors(std::map<Node, std::vector<Node> >& sks) const; private: /** Are proofs enabled? */ |