From: ajreynol Date: Fri, 28 Oct 2016 22:14:04 +0000 (-0500) Subject: Add get instantiations utilities to API. X-Git-Tag: cvc5-1.0.0~6017 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b1dea08db5a965d8d9d6f38bd05c280a8a126352;p=cvc5.git Add get instantiations utilities to API. --- diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f288c6c0a..e3a0533af 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -5125,6 +5125,43 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) } } +void SmtEngine::getInstantiatedQuantifiedFormulas( std::vector< Expr >& qs ) { + SmtScope smts(this); + if( d_theoryEngine ){ + std::vector< Node > qs_n; + d_theoryEngine->getInstantiatedQuantifiedFormulas( qs_n ); + for( unsigned i=0; i& insts ) { + SmtScope smts(this); + if( d_theoryEngine ){ + std::vector< Node > insts_n; + d_theoryEngine->getInstantiations( Node::fromExpr( q ), insts_n ); + for( unsigned i=0; i >& tvecs ) { + SmtScope smts(this); + if( d_theoryEngine ){ + std::vector< std::vector< Node > > tvecs_n; + d_theoryEngine->getInstantiationTermVectors( Node::fromExpr( q ), tvecs_n ); + for( unsigned i=0; i tvec; + for( unsigned j=0; j SmtEngine::getAssertions() throw(ModalException) { SmtScope smts(this); finalOptionsAreSet(); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 2741cea85..760c7c071 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -565,6 +565,17 @@ public: */ Expr doQuantifierElimination(const Expr& e, bool doFull, bool strict=true) throw(TypeCheckingException, ModalException, LogicException); + /** + * Get list of quantified formulas that were instantiated + */ + void getInstantiatedQuantifiedFormulas( std::vector< Expr >& qs ); + + /** + * Get instantiations + */ + void getInstantiations( Expr q, std::vector< Expr >& insts ); + void getInstantiationTermVectors( Expr q, std::vector< std::vector< Expr > >& tvecs ); + /** * Get an unsatisfiable core (only if immediately preceded by an * UNSAT or VALID query). Only permitted if CVC4 was built with diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 67990ef69..95b01bc7b 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -1382,6 +1382,29 @@ bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas, } } +void QuantifiersEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) { + std::vector< Node > lemmas; + getInstantiations( q, lemmas ); + std::map< Node, Node > quant; + std::map< Node, std::vector< Node > > tvec; + getExplanationForInstLemmas( lemmas, quant, tvec ); + for( std::map< Node, std::vector< Node > >::iterator it = tvec.begin(); it != tvec.end(); ++it ){ + tvecs.push_back( it->second ); + } +} + +void QuantifiersEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) { + if( options::incrementalSolving() ){ + for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){ + getInstantiationTermVectors( it->first, insts[it->first] ); + } + }else{ + for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){ + getInstantiationTermVectors( it->first, insts[it->first] ); + } + } +} + void QuantifiersEngine::getExplanationForInstLemmas( std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) { if( d_trackInstLemmas ){ if( options::incrementalSolving() ){ @@ -1456,6 +1479,18 @@ void QuantifiersEngine::printSynthSolution( std::ostream& out ) { } } +void QuantifiersEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ) { + if( options::incrementalSolving() ){ + for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){ + qs.push_back( it->first ); + } + }else{ + for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){ + qs.push_back( it->first ); + } + } +} + void QuantifiersEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) { bool useUnsatCore = false; std::vector< Node > active_lemmas; diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 232d1d889..ff6a8a36c 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -374,9 +374,14 @@ public: void printInstantiations( std::ostream& out ); /** print solution for synthesis conjectures */ void printSynthSolution( std::ostream& out ); + /** get list of quantified formulas that were instantiated */ + void getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ); /** get instantiations */ void getInstantiations( Node q, std::vector< Node >& insts ); void getInstantiations( std::map< Node, std::vector< Node > >& insts ); + /** get instantiation term vectors */ + void getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ); + void getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ); /** get instantiated conjunction */ Node getInstantiatedConjunction( Node q ); /** get unsat core lemmas */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index a14534efe..c3e853ec0 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1445,6 +1445,30 @@ void TheoryEngine::printSynthSolution( std::ostream& out ) { } } +void TheoryEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ) { + if( d_quantEngine ){ + d_quantEngine->getInstantiatedQuantifiedFormulas( qs ); + }else{ + Assert( false ); + } +} + +void TheoryEngine::getInstantiations( Node q, std::vector< Node >& insts ) { + if( d_quantEngine ){ + d_quantEngine->getInstantiations( q, insts ); + }else{ + Assert( false ); + } +} + +void TheoryEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) { + if( d_quantEngine ){ + d_quantEngine->getInstantiationTermVectors( q, tvecs ); + }else{ + Assert( false ); + } +} + void TheoryEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) { if( d_quantEngine ){ d_quantEngine->getInstantiations( insts ); @@ -1453,6 +1477,14 @@ void TheoryEngine::getInstantiations( std::map< Node, std::vector< Node > >& ins } } +void TheoryEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) { + if( d_quantEngine ){ + d_quantEngine->getInstantiationTermVectors( insts ); + }else{ + Assert( false ); + } +} + Node TheoryEngine::getInstantiatedConjunction( Node q ) { if( d_quantEngine ){ return d_quantEngine->getInstantiatedConjunction( q ); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 4366f8d3a..fc98c6e3a 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -786,9 +786,20 @@ public: void printSynthSolution( std::ostream& out ); /** - * Get instantiations + * Get list of quantified formulas that were instantiated */ + void getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ); + + /** + * 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] ) , ... , 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.