From 3fbe87912dbffe70cf01fdf0b4652960998ea480 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 9 Jun 2015 11:45:14 +0200 Subject: [PATCH] Bug fix instantiations for fmf-bound-int. Disable nested pre-skolemization for non-UF logics. Update SMT COMP scripts accordingly. --- contrib/run-script-smtcomp2015 | 8 +++----- contrib/run-script-smtcomp2015-assertions | 4 +--- contrib/run-script-smtcomp2015-experimental | 6 ++---- src/smt/smt_engine.cpp | 8 +++++++- src/theory/quantifiers/bounded_integers.cpp | 1 + src/theory/quantifiers/quantifiers_rewriter.cpp | 2 +- src/theory/quantifiers_engine.cpp | 1 + src/theory/rep_set.cpp | 4 +++- 8 files changed, 19 insertions(+), 15 deletions(-) diff --git a/contrib/run-script-smtcomp2015 b/contrib/run-script-smtcomp2015 index c46671c08..8eb19a24f 100755 --- a/contrib/run-script-smtcomp2015 +++ b/contrib/run-script-smtcomp2015 @@ -54,7 +54,7 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) trywith 30 --no-inst-no-entail --no-quant-cf --full-saturate-quant trywith 30 --finite-model-find --mbqi=gen-ev --uf-ss-totality trywith 30 --inst-when=full --full-saturate-quant - trywith 30 --fmf-bound-int --macros-quant + #trywith 30 --fmf-bound-int --macros-quant # recently bug fixed trywith 30 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant trywith 30 --decision=justification-stoponly --full-saturate-quant # large runs 3min @@ -67,12 +67,10 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) finishwith --full-saturate-quant ;; LIA|LRA|NIA|NRA) - trywith 60 --cbqi --no-cbqi-sat --full-saturate-quant + trywith 180 --cbqi --no-cbqi-sat --full-saturate-quant trywith 60 --full-saturate-quant - trywith 60 --cbqi --no-cbqi-sat --cbqi-recurse --full-saturate-quant trywith 180 --qcf-tconstraint --full-saturate-quant - trywith 240 --cbqi --no-cbqi-sat --cbqi-recurse --full-saturate-quant - finishwith --cbqi --no-cbqi-sat --cbqi-recurse --pre-skolem-quant --full-saturate-quant + finishwith --cbqi --no-cbqi-sat --cbqi-recurse --full-saturate-quant ;; QF_AUFBV) trywith 600 diff --git a/contrib/run-script-smtcomp2015-assertions b/contrib/run-script-smtcomp2015-assertions index 3292e29fb..c4f9fc6cc 100755 --- a/contrib/run-script-smtcomp2015-assertions +++ b/contrib/run-script-smtcomp2015-assertions @@ -74,10 +74,8 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) LIA|LRA|NIA|NRA) trywith 30 --cbqi --no-cbqi-sat --full-saturate-quant trywith 30 --full-saturate-quant - trywith 30 --cbqi --no-cbqi-sat --cbqi-recurse --full-saturate-quant trywith 30 --qcf-tconstraint --full-saturate-quant - trywith 30 --cbqi --no-cbqi-sat --cbqi-recurse --full-saturate-quant - finishwith --cbqi --no-cbqi-sat --cbqi-recurse --pre-skolem-quant --full-saturate-quant + finishwith --cbqi --no-cbqi-sat --cbqi-recurse --full-saturate-quant ;; QF_AUFBV) trywith 30 diff --git a/contrib/run-script-smtcomp2015-experimental b/contrib/run-script-smtcomp2015-experimental index 9b8a0ba38..3480a8e3c 100755 --- a/contrib/run-script-smtcomp2015-experimental +++ b/contrib/run-script-smtcomp2015-experimental @@ -67,12 +67,10 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) finishwith --full-saturate-quant ;; LIA|LRA|NIA|NRA) - trywith 60 --cbqi --full-saturate-quant + trywith 180 --cbqi --full-saturate-quant trywith 60 --full-saturate-quant - trywith 60 --cbqi --cbqi-recurse --full-saturate-quant trywith 180 --qcf-tconstraint --full-saturate-quant - trywith 240 --cbqi --cbqi-recurse --full-saturate-quant - finishwith --cbqi --cbqi-recurse --pre-skolem-quant --full-saturate-quant + finishwith --cbqi --cbqi-recurse --full-saturate-quant ;; QF_AUFBV) trywith 600 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 9fe3a115d..5d5bb93dc 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1480,7 +1480,13 @@ void SmtEngine::setDefaults() { options::conjectureGen.set( false ); } } - + //can't pre-skolemize nested quantifiers without UF theory + if( !d_logic.isTheoryEnabled(THEORY_UF) && options::preSkolemQuant() ){ + if( !options::preSkolemQuantNested.wasSetByUser() ){ + options::preSkolemQuantNested.set( false ); + } + } + //until bugs 371,431 are fixed if( ! options::minisatUseElim.wasSetByUser()){ if( d_logic.isQuantified() || options::produceModels() || options::produceAssignments() || options::checkModels() ){ diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index 0ba8008aa..2fd595a9f 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -372,6 +372,7 @@ Node BoundedIntegers::getNextDecisionRequest() { } } } + Trace("bound-int-dec-debug") << "No decision request." << std::endl; return Node::null(); } diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 991043157..0afdece82 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1210,7 +1210,7 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v return nn.negate(); }else if( n.getKind()==kind::FORALL ){ if( polarity ){ - if( options::preSkolemQuant() && ( options::preSkolemQuantNested() || fvs.empty() ) ){ + if( options::preSkolemQuant() && options::preSkolemQuantNested() ){ vector< Node > children; children.push_back( n[0] ); //add children to current scope diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 6a4998016..88aea6c75 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -770,6 +770,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo getOutputChannel().safePoint(options::quantifierStep()); Assert( terms.size()==f[0].getNumChildren() ); + Trace("inst-add-debug") << "For quantified formula " << f << "..." << std::endl; Trace("inst-add-debug") << "Add instantiation: "; for( unsigned i=0; i0 ) Trace("inst-add-debug") << ", "; diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index 5580dc3d7..4ab8df72f 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -370,7 +370,9 @@ bool RepSetIterator::isFinished(){ } Node RepSetIterator::getTerm( int i ){ - int index = d_index_order[i]; + Trace("rsi-debug") << "rsi : get term " << i << ", index order = " << d_index_order[i] << std::endl; + //int index = d_index_order[i]; + int index = i; if( d_enum_type[index]==ENUM_DOMAIN_ELEMENTS ){ TypeNode tn = d_types[index]; Assert( d_rep_set->d_type_reps.find( tn )!=d_rep_set->d_type_reps.end() ); -- 2.30.2