diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-19 16:53:48 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-19 16:53:48 -0600 |
| commit | f2ed7b1aebc175b971e3cebf4c0b2fff6e4e895f (patch) | |
| tree | 9d67467344399282909475f3cf891639f8abbaf8 /src/theory/theory_engine.h | |
| parent | 7191e58e5561a159c0cd3b81fddbe311ba70a45b (diff) | |
Enable new implementation of CEGQI based on nested quantifier elimination (#5477)
This replaces the old implementation of CEGQI based on nested quantifier elimination (--cegqi-nested-qe) with the new implementation.
The previous implementation used some convoluted internal attributes to manage dependencies between quantified formulas, the new implementation is much simpler: it simply eliminates nested quantification eagerly.
Fixes #5365, fixes #5279, fixes #4849, fixes #4433.
This PR also required fixes related to how quantifier elimination is computed.
Diffstat (limited to 'src/theory/theory_engine.h')
| -rw-r--r-- | src/theory/theory_engine.h | 13 |
1 files changed, 2 insertions, 11 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index ee3611a53..1412d7464 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -686,23 +686,14 @@ class TheoryEngine { /** * Get instantiation methods - * first inputs forall x.q[x] and returns ( q[a], ..., q[z] ) - * second inputs forall x.q[x] and returns ( a, ..., z ) - * third and fourth return mappings e.g. forall x.q1[x] -> ( q1[a]...q1[z] ) + * the first given forall x.q[x] returns ( a, ..., z ) + * the second returns mappings e.g. forall x.q1[x] -> ( q1[a]...q1[z] ) * , ... , forall x.qn[x] -> ( qn[a]...qn[z] ) */ - void getInstantiations( Node q, std::vector< Node >& insts ); void getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ); - void getInstantiations( std::map< Node, std::vector< Node > >& insts ); void getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ); /** - * Get instantiated conjunction, returns q[t1] ^ ... ^ q[tn] where t1...tn are current set of instantiations for q. - * Can be used for quantifier elimination when satisfiable and q[t1] ^ ... ^ q[tn] |= q - */ - Node getInstantiatedConjunction( Node q ); - - /** * Forwards an entailment check according to the given theoryOfMode. * See theory.h for documentation on entailmentCheck(). */ |