diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/datatypes/datatypes_rewriter.h | 28 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_match.cpp | 26 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_match.h | 18 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 12 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 2 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 11 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 5 |
7 files changed, 90 insertions, 12 deletions
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 0c00ed8df..ffec86477 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -200,20 +200,24 @@ public: } } - if(in.getKind() == kind::EQUAL && in[0] == in[1]) { - return RewriteResponse(REWRITE_DONE, - NodeManager::currentNM()->mkConst(true)); - } if(in.getKind() == kind::EQUAL ) { - std::vector< Node > rew; - if( checkClash(in[0], in[1], rew) ){ - Trace("datatypes-rewrite") << "Rewrite clashing equality " << in << " to false" << std::endl; - return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(false)); - }else if( rew.size()==1 && rew[0]!=in ){ - Trace("datatypes-rewrite") << "Rewrite equality " << in << " to " << rew[0] << std::endl; - return RewriteResponse(REWRITE_AGAIN_FULL, rew[0] ); + if(in[0] == in[1]) { + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); }else{ - Trace("datatypes-rewrite-debug") << "Did not rewrite equality " << in << " " << in[0].getKind() << " " << in[1].getKind() << std::endl; + std::vector< Node > rew; + if( checkClash(in[0], in[1], rew) ){ + Trace("datatypes-rewrite") << "Rewrite clashing equality " << in << " to false" << std::endl; + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(false)); + }else if( rew.size()==1 && rew[0]!=in ){ + Trace("datatypes-rewrite") << "Rewrite equality " << in << " to " << rew[0] << std::endl; + return RewriteResponse(REWRITE_AGAIN_FULL, rew[0] ); + }else if( in[1]<in[0] ){ + Node ins = NodeManager::currentNM()->mkNode(in.getKind(), in[1], in[0]); + Trace("datatypes-rewrite") << "Swap equality " << in << " to " << ins << std::endl; + return RewriteResponse(REWRITE_DONE, ins); + }else{ + Trace("datatypes-rewrite-debug") << "Did not rewrite equality " << in << " " << in[0].getKind() << " " << in[1].getKind() << std::endl; + } } } diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 5eca87903..f2d5c640d 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -212,6 +212,18 @@ void InstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& term } } +void InstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< TNode >& vars, std::vector< TNode >& terms ) const { + if( terms.size()==q[0].getNumChildren() ){ + insts.push_back( q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ) ); + }else{ + for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){ + terms.push_back( it->first ); + it->second.getInstantiations( insts, q, vars, terms ); + terms.pop_back(); + } + } +} + bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq, bool modInst, int index, bool onlyExist ){ @@ -298,6 +310,20 @@ void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& te } } +void CDInstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< TNode >& vars, std::vector< TNode >& terms ) const{ + if( d_valid.get() ){ + if( terms.size()==q[0].getNumChildren() ){ + insts.push_back( q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ) ); + }else{ + for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){ + terms.push_back( it->first ); + it->second->getInstantiations( insts, q, vars, terms ); + terms.pop_back(); + } + } + } +} + }/* CVC4::theory::inst namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index f1c1c952a..abe31b48d 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -101,6 +101,7 @@ public: std::map< Node, InstMatchTrie > d_data; private: void print( std::ostream& out, Node q, std::vector< TNode >& terms ) const; + void getInstantiations( std::vector< Node >& insts, Node q, std::vector< TNode >& vars, std::vector< TNode >& terms ) const; public: InstMatchTrie(){} ~InstMatchTrie(){} @@ -131,6 +132,14 @@ public: std::vector< TNode > terms; print( out, q, terms ); } + void getInstantiations( std::vector< Node >& insts, Node q ) { + std::vector< TNode > terms; + std::vector< TNode > vars; + for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ + vars.push_back( q[0][i] ); + } + getInstantiations( insts, q, vars, terms ); + } void clear() { d_data.clear(); } };/* class InstMatchTrie */ @@ -143,6 +152,7 @@ public: context::CDO< bool > d_valid; private: void print( std::ostream& out, Node q, std::vector< TNode >& terms ) const; + void getInstantiations( std::vector< Node >& insts, Node q, std::vector< TNode >& vars, std::vector< TNode >& terms ) const; public: CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){} ~CDInstMatchTrie(){} @@ -173,6 +183,14 @@ public: std::vector< TNode > terms; print( out, q, terms ); } + void getInstantiations( std::vector< Node >& insts, Node q ) { + std::vector< TNode > terms; + std::vector< TNode > vars; + for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ + vars.push_back( q[0][i] ); + } + getInstantiations( insts, q, vars, terms ); + } };/* class CDInstMatchTrie */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 6fedc14f0..f3201bd60 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -1106,6 +1106,18 @@ void QuantifiersEngine::printSynthSolution( std::ostream& out ) { } } +void QuantifiersEngine::getInstantiations( std::map< Node, 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 ){ + it->second->getInstantiations( insts[it->first], it->first ); + } + }else{ + for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){ + it->second.getInstantiations( insts[it->first], it->first ); + } + } +} + QuantifiersEngine::Statistics::Statistics() : d_time("theory::QuantifiersEngine::time"), d_num_quant("QuantifiersEngine::Num_Quantifiers", 0), diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index aa770ad67..49c9eeff8 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -342,6 +342,8 @@ public: void printInstantiations( std::ostream& out ); /** print solution for synthesis conjectures */ void printSynthSolution( std::ostream& out ); + /** get instantiations */ + void getInstantiations( std::map< Node, std::vector< Node > >& insts ); /** statistics class */ class Statistics { public: diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 45f7506de..dcb3fec0a 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1212,6 +1212,8 @@ Node TheoryEngine::ensureLiteral(TNode n) { void TheoryEngine::printInstantiations( std::ostream& out ) { if( d_quantEngine ){ d_quantEngine->printInstantiations( out ); + }else{ + out << "Internal error : instantiations not available when quantifiers are not present." << std::endl; } } @@ -1223,6 +1225,15 @@ void TheoryEngine::printSynthSolution( std::ostream& out ) { } } +void TheoryEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) { + if( d_quantEngine ){ + d_quantEngine->getInstantiations( insts ); + }else{ + Assert( false ); + } +} + + static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) { std::set<TNode> all; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 886aa6863..5061f3cb7 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -783,6 +783,11 @@ public: */ void printSynthSolution( std::ostream& out ); + /** + * Get instantiations + */ + void getInstantiations( std::map< Node, std::vector< Node > >& insts ); + /** * Forwards an entailment check according to the given theoryOfMode. * See theory.h for documentation on entailmentCheck(). |