summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/datatypes/datatypes_rewriter.h28
-rw-r--r--src/theory/quantifiers/inst_match.cpp26
-rw-r--r--src/theory/quantifiers/inst_match.h18
-rw-r--r--src/theory/quantifiers_engine.cpp12
-rw-r--r--src/theory/quantifiers_engine.h2
-rw-r--r--src/theory/theory_engine.cpp11
-rw-r--r--src/theory/theory_engine.h5
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().
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback