summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rwxr-xr-xcontrib/run-script-cascj7-fof6
-rwxr-xr-xcontrib/run-script-cascj7-tff8
-rw-r--r--src/smt/smt_engine.cpp13
-rw-r--r--src/theory/quantifiers/inst_match.cpp12
-rw-r--r--src/theory/quantifiers/inst_match.h10
-rw-r--r--src/theory/quantifiers_engine.cpp15
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<Expr> 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<f[0].getNumChildren(); i++ ){
d_vals.push_back( Node::null() );
}
@@ -198,12 +198,12 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No
}
}
-void InstMatchTrie::print( std::ostream& out, Node q, std::vector< Node >& 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; i<terms.size(); i++ ){
- if( i>0 ) 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; i<terms.size(); i++ ){
if( i>0 ) 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():
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback