From 32b0aba2c2c27ad038d34c8554a4bae76e8dd363 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 21 Nov 2014 09:42:07 +0100 Subject: [PATCH] Change default option to --inst-when=full-last-call (interleave instantiation and theory combination). Fix inefficiency in NNF, enable by default. Set best defaults for --mbqi=abs. --- src/smt/smt_engine.cpp | 9 ++++++- src/theory/quantifiers/options | 6 ++--- src/theory/quantifiers/options_handlers.h | 10 ++++---- .../quantifiers/quantifiers_rewriter.cpp | 24 +++++++++++++++---- test/regress/regress0/quantifiers/burns4.smt2 | 2 ++ 5 files changed, 38 insertions(+), 13 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 86b0faaf6..74cdee0b7 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1319,7 +1319,6 @@ void SmtEngine::setDefaults() { if( !options::quantConflictFind.wasSetByUser() ){ options::quantConflictFind.set( false ); } - //for finite model finding if( ! options::instWhenMode.wasSetByUser()){ //instantiate only on last call if( options::eMatching() ){ @@ -1327,6 +1326,14 @@ void SmtEngine::setDefaults() { options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL ); } } + if( options::mbqiMode()==quantifiers::MBQI_ABS ){ + if( !options::preSkolemQuant.wasSetByUser() ){ + options::preSkolemQuant.set( true ); + } + if( !options::fmfOneInstPerRound.wasSetByUser() ){ + options::fmfOneInstPerRound.set( true ); + } + } } //implied options... diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index dad173ff5..a428633cc 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -41,7 +41,7 @@ option simpleIteLiftQuant /--disable-ite-lift-quant bool :default true option cnfQuant --cnf-quant bool :default false apply CNF conversion to quantified formulas # Whether to NNF quantifier bodies -option nnfQuant --nnf-quant bool :default false +option nnfQuant --nnf-quant bool :default true apply NNF conversion to quantified formulas option clauseSplit --clause-split bool :default false @@ -88,7 +88,7 @@ option fmfFunWellDefined --fmf-fun bool :default false option registerQuantBodyTerms --register-quant-body-terms bool :default false consider ground terms within bodies of quantified formulas for matching -option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h" +option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h" when to apply instantiation option instMaxLevel --inst-max-level=N int :read-write :default -1 maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default) @@ -127,7 +127,7 @@ option finiteModelFind finite-model-find --finite-model-find bool :default false option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_FMC :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h" choose mode for model-based quantifier instantiation -option fmfOneInstPerRound --mbqi-one-inst-per-round bool :default false +option fmfOneInstPerRound --mbqi-one-inst-per-round bool :read-write :default false only add one instantiation per quantifier per round for mbqi option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false only add instantiations for one quantifier per round for mbqi diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index 08fcf319d..e9f85d454 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -29,17 +29,17 @@ namespace quantifiers { static const std::string instWhenHelp = "\ Modes currently supported by the --inst-when option:\n\ \n\ -full (default)\n\ +full-last-call (default)\n\ ++ Alternate running instantiation rounds at full effort and last\n\ + call. In other words, interleave instantiation and theory combination.\n\ +\n\ +full\n\ + Run instantiation round at full effort, before theory combination.\n\ \n\ full-delay \n\ + Run instantiation round at full effort, before theory combination, after\n\ all other theories have finished.\n\ \n\ -full-last-call\n\ -+ Alternate running instantiation rounds at full effort and last\n\ - call. In other words, interleave instantiation and theory combination.\n\ -\n\ last-call\n\ + Run instantiation at last call effort, after theory combination and\n\ and theories report sat.\n\ diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 0ed175393..1e6ec3a02 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -309,11 +309,19 @@ Node QuantifiersRewriter::computeNNF( Node body ){ }else{ std::vector< Node > children; Kind k = body[0].getKind(); + if( body[0].getKind()==OR || body[0].getKind()==AND ){ + k = body[0].getKind()==AND ? OR : AND; for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ - children.push_back( computeNNF( body[0][i].notNode() ) ); + Node nc = computeNNF( body[0][i].notNode() ); + if( nc.getKind()==k ){ + for( unsigned j=0; j children; bool childrenChanged = false; + bool isAssoc = body.getKind()==AND || body.getKind()==OR; for( int i=0; i<(int)body.getNumChildren(); i++ ){ Node nc = computeNNF( body[i] ); - children.push_back( nc ); - childrenChanged = childrenChanged || nc!=body[i]; + if( isAssoc && nc.getKind()==body.getKind() ){ + for( unsigned j=0; jmkNode( body.getKind(), children ); diff --git a/test/regress/regress0/quantifiers/burns4.smt2 b/test/regress/regress0/quantifiers/burns4.smt2 index 886d6f5c8..72023fd4f 100644 --- a/test/regress/regress0/quantifiers/burns4.smt2 +++ b/test/regress/regress0/quantifiers/burns4.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --full-saturate-quant +; EXPECT: unsat (set-logic AUFLIA) (set-info :source | Burns mutual exclusion protocol. This is a benchmark of the haRVey theorem prover. It was translated to SMT-LIB by Leonardo de Moura |) (set-info :smt-lib-version 2.0) -- 2.30.2