diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-27 10:32:32 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-27 10:32:32 -0600 |
| commit | 8795787c2ef337e73b46778b99f5bfa6c2a19f93 (patch) | |
| tree | 0989e95f24c2eeedd177d2281069d266b31d971d /src/theory/quantifiers_engine.h | |
| parent | a6d3c9e7fb765704f34815900712b10e85687edc (diff) | |
(proof-new) Improvements to quantifiers engine and instantiate interfaces (#5814)
This makes printing instantiations done at the SmtEngine level instead of deeply embedded within the Instantiate module. This provides much better flexibility for future uses of instantiations (e.g. how they are minimized in the new proof infrastructure).
Note this PR breaks the functionality that instantiations are minimized based on the old unsat cores infrastructure (see the disabled regression). This will be fixed once proof-new is fully merged.
Diffstat (limited to 'src/theory/quantifiers_engine.h')
| -rw-r--r-- | src/theory/quantifiers_engine.h | 18 |
1 files changed, 16 insertions, 2 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index d09090da3..126fca01f 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -258,11 +258,19 @@ public: * guided instantiation. */ Node getInternalRepresentative(Node a, Node q, int index); + /** + * Get quantifiers name, which returns a variable corresponding to the name of + * quantified formula q if q has a name, or otherwise returns q itself. + */ + Node getNameForQuant(Node q) const; + /** + * Get name for quantified formula. Returns true if q has a name or if req + * is false. Sets name to the result of the above method. + */ + bool getNameForQuant(Node q, Node& name, bool req = true) const; public: //----------user interface for instantiations (see quantifiers/instantiate.h) - /** print instantiations */ - void printInstantiations(std::ostream& out); /** print solution for synthesis conjectures */ void printSynthSolution(std::ostream& out); /** get list of quantified formulas that were instantiated */ @@ -272,6 +280,12 @@ public: std::vector<std::vector<Node> >& tvecs); void getInstantiationTermVectors( std::map<Node, std::vector<std::vector<Node> > >& insts); + /** + * 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. + */ + void getSkolemTermVectors(std::map<Node, std::vector<Node> >& sks) const; /** get synth solutions * |