From 478b935ba5e2b9eda4eb21f7651747c5325229b1 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 14 May 2014 14:46:53 -0500 Subject: [PATCH] Finish --dump-instantiations option. Update scripts. --- contrib/run-script-cascj7-fof | 6 +++--- contrib/run-script-cascj7-tff | 8 ++++---- src/smt/smt_engine.cpp | 13 +++++++------ src/theory/quantifiers/inst_match.cpp | 12 ++++++------ src/theory/quantifiers/inst_match.h | 10 +++++----- src/theory/quantifiers_engine.cpp | 15 +++++++-------- 6 files changed, 32 insertions(+), 32 deletions(-) diff --git a/contrib/run-script-cascj7-fof b/contrib/run-script-cascj7-fof index 582a14952..be656b57a 100755 --- a/contrib/run-script-cascj7-fof +++ b/contrib/run-script-cascj7-fof @@ -15,7 +15,7 @@ echo "------- cvc4-fof $bench at $2..." function trywith { limit=$1; shift; echo "--- Run $@ at $limit..."; - (ulimit -t "$limit";$cvc4 --no-checking --no-interactive --dump-instantiations "$@" $bench) 2>/dev/null | + (ulimit -t "$limit";$cvc4 --no-checking --no-interactive --dump-instantiations --inst-format=szs "$@" $bench) 2>/dev/null | (read w1 w2 w3 result w4 w5; case "$result" in Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; @@ -25,11 +25,11 @@ function trywith { } function finishwith { echo "--- Run $@ at $limit..."; - $cvc4 --no-checking --no-interactive --dump-instantiations "$@" $bench + $cvc4 --no-checking --no-interactive --dump-instantiations --inst-format=szs "$@" $bench } +trywith 15 --quant-cf --pre-skolem-quant --full-saturate-quant trywith 30 --full-saturate-quant -trywith 15 --decision=internal --full-saturate-quant trywith 30 --finite-model-find --fmf-inst-engine --mbqi=gen-ev trywith 30 --relevant-triggers --full-saturate-quant trywith 15 --finite-model-find --decision=justification-stoponly diff --git a/contrib/run-script-cascj7-tff b/contrib/run-script-cascj7-tff index 8033bed1f..4506e511d 100755 --- a/contrib/run-script-cascj7-tff +++ b/contrib/run-script-cascj7-tff @@ -9,13 +9,13 @@ filename=${file%.*} echo "------- cvc4-tff $bench at $2..." # use: trywith [params..] -# to attempt a run. Only thing printed on stdout is "sat" or "unsat", in -# which case this run script terminates immediately. Otherwise, this +# to attempt a run. If an SZS ontology result is printed, then +# the run script terminates immediately. Otherwise, this # function returns normally. function trywith { limit=$1; shift; echo "--- Run $@ at $limit..."; - (ulimit -t "$limit";$cvc4 --no-checking --no-interactive --dump-instantiations "$@" $bench) 2>/dev/null | + (ulimit -t "$limit";$cvc4 --no-checking --no-interactive --dump-instantiations --inst-format=szs "$@" $bench) 2>/dev/null | (read w1 w2 w3 result w4 w5; case "$result" in Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; @@ -25,7 +25,7 @@ function trywith { } function finishwith { echo "--- Run $@ at $limit..."; - $cvc4 --no-checking --no-interactive --dump-instantiations "$@" $bench + $cvc4 --no-checking --no-interactive --dump-instantiations --inst-format=szs "$@" $bench } trywith 15 --cbqi-recurse --full-saturate-quant diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 4deb43f42..c6b76e850 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3801,15 +3801,16 @@ Proof* SmtEngine::getProof() throw(ModalException) { } void SmtEngine::printInstantiations( std::ostream& out ) { - //if( options::instFormatMode()==INST_FORMAT_MODE_SZS ){ - out << "% SZS CNF output start CNFRefutation for " << d_filename.c_str() << std::endl; - //} + SmtScope smts(this); + if( options::instFormatMode()==INST_FORMAT_MODE_SZS ){ + out << "% SZS CNF output start CNFRefutation for " << d_filename.c_str() << std::endl; + } if( d_theoryEngine ){ d_theoryEngine->printInstantiations( out ); } - //if( options::instFormatMode()==INST_FORMAT_MODE_SZS ){ - out << "% SZS CNF output end CNFRefutation for " << d_filename.c_str() << std::endl; - //} + if( options::instFormatMode()==INST_FORMAT_MODE_SZS ){ + out << "% SZS CNF output end CNFRefutation for " << d_filename.c_str() << std::endl; + } } vector SmtEngine::getAssertions() throw(ModalException) { diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 703a44d03..292190168 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -27,7 +27,7 @@ namespace CVC4 { namespace theory { namespace inst { -InstMatch::InstMatch( Node f ) { +InstMatch::InstMatch( TNode f ) { for( unsigned i=0; i& terms ) const { +void InstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms ) const { if( terms.size()==q[0].getNumChildren() ){ out << " ( "; for( unsigned i=0; i0 ) out << ", "; - //out << terms[i]; + if( i>0 ){ out << ", ";} + out << terms[i]; } out << " )" << std::endl; }else{ @@ -282,13 +282,13 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< } } -void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< Node >& terms ) const{ +void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms ) const{ if( d_valid.get() ){ if( terms.size()==q[0].getNumChildren() ){ out << " ( "; for( unsigned i=0; i0 ) out << ", "; - //out << terms[i]; + out << terms[i]; } out << " )" << std::endl; }else{ diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index accd3baed..d728d18a2 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -41,7 +41,7 @@ public: std::vector< Node > d_vals; public: InstMatch(){} - InstMatch( Node f ); + explicit InstMatch( TNode f ); InstMatch( InstMatch* m ); /** fill all unfilled values with m */ @@ -101,7 +101,7 @@ public: /** the data */ std::map< Node, InstMatchTrie > d_data; private: - void print( std::ostream& out, Node q, std::vector< Node >& terms ) const; + void print( std::ostream& out, Node q, std::vector< TNode >& terms ) const; public: InstMatchTrie(){} ~InstMatchTrie(){} @@ -129,7 +129,7 @@ public: bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false, bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ); void print( std::ostream& out, Node q ) const{ - std::vector< Node > terms; + std::vector< TNode > terms; print( out, q, terms ); } };/* class InstMatchTrie */ @@ -142,7 +142,7 @@ public: /** is valid */ context::CDO< bool > d_valid; private: - void print( std::ostream& out, Node q, std::vector< Node >& terms ) const; + void print( std::ostream& out, Node q, std::vector< TNode >& terms ) const; public: CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){} ~CDInstMatchTrie(){} @@ -170,7 +170,7 @@ public: bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false, bool modInst = false, int index = 0, bool onlyExist = false ); void print( std::ostream& out, Node q ) const{ - std::vector< Node > terms; + std::vector< TNode > terms; print( out, q, terms ); } };/* class CDInstMatchTrie */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 83733da42..3714ca4d0 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -623,19 +623,18 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){ } void QuantifiersEngine::printInstantiations( std::ostream& out ) { - //Trace("ajr-temp") << "QE print inst." << std::endl; - //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 ){ - // out << "Instantiations of " << it->first << " : " << std::endl; - // it->second->print( out, it->first ); - // } - //}else{ + 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 ){ + out << "Instantiations of " << it->first << " : " << std::endl; + it->second->print( out, it->first ); + } + }else{ for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){ out << "Instantiations of " << it->first << " : " << std::endl; it->second.print( out, it->first ); out << std::endl; } - //} + } } QuantifiersEngine::Statistics::Statistics(): -- 2.30.2