From 2cadfe31cfddaff7eff4cd220273d0bab3d2792d Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 31 Aug 2016 17:44:42 -0500 Subject: Updates to cbqi. New strategy --cbqi-nested-qe to do qe on nested quantifiers during instantiation. Decide on innermost ce lits first, register nested counterexample lemmas eagerly. --- src/theory/theory_engine.h | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'src/theory/theory_engine.h') diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index bb7946dd8..4366f8d3a 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -789,6 +789,12 @@ public: * Get instantiations */ void getInstantiations( std::map< Node, 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. -- cgit v1.2.3