summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/smt_engine.cpp37
-rw-r--r--src/smt/smt_engine.h11
-rw-r--r--src/theory/quantifiers_engine.cpp35
-rw-r--r--src/theory/quantifiers_engine.h5
-rw-r--r--src/theory/theory_engine.cpp32
-rw-r--r--src/theory/theory_engine.h13
6 files changed, 132 insertions, 1 deletions
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<qs_n.size(); i++ ){
+ qs.push_back( qs_n[i].toExpr() );
+ }
+ }
+}
+
+void SmtEngine::getInstantiations( Expr q, std::vector< Expr >& 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<insts_n.size(); i++ ){
+ insts.push_back( insts_n[i].toExpr() );
+ }
+ }
+}
+
+void SmtEngine::getInstantiationTermVectors( Expr q, std::vector< std::vector< Expr > >& 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<tvecs_n.size(); i++ ){
+ std::vector< Expr > tvec;
+ for( unsigned j=0; j<tvecs_n[i].size(); j++ ){
+ tvec.push_back( tvecs_n[i][j].toExpr() );
+ }
+ tvecs.push_back( tvec );
+ }
+ }
+}
+
vector<Expr> 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
@@ -566,6 +566,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
* unsat-core support and produce-unsat-cores is on.
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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback