From: ajreynol Date: Thu, 16 Oct 2014 20:16:49 +0000 (+0200) Subject: Make --user-pat=trust default. Fix a few warnings found by Morgan. Minor changes... X-Git-Tag: cvc5-1.0.0~6557 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9d7378688486cb0dbad207482932dfb4b5d91f95;p=cvc5.git Make --user-pat=trust default. Fix a few warnings found by Morgan. Minor changes to options. --- diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index a69952885..19bfe3ca5 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1342,6 +1342,13 @@ void SmtEngine::setDefaults() { options::conjectureFilterModel.set( false ); } } + if( options::conjectureGenPerRound.wasSetByUser() ){ + if( options::conjectureGenPerRound()>0 ){ + options::conjectureGen.set( true ); + }else{ + options::conjectureGen.set( false ); + } + } //until bugs 371,431 are fixed if( ! options::minisatUseElim.wasSetByUser()){ diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index dddbee73b..69e8cc4e0 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -44,7 +44,8 @@ void CegInstantiation::CegConjecture::initializeGuard( QuantifiersEngine * qe ){ if( d_guard.isNull() ){ d_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) ); //specify guard behavior - qe->getValuation().ensureLiteral( d_guard ); + d_guard = qe->getValuation().ensureLiteral( d_guard ); + AlwaysAssert( !d_guard.isNull() ); qe->getOutputChannel().requirePhase( d_guard, true ); } } @@ -338,7 +339,7 @@ void CegInstantiation::getMeasureLemmas( Node n, Node v, std::vector< Node >& le Node lem = lhs.eqNode( rhs ); Node cond = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[index].getTester() ), n ); lem = NodeManager::currentNM()->mkNode( OR, cond.negate(), lem ); - + d_size_term_lemma[n][index] = lem; Trace("cegqi-lemma-debug") << "...constructed lemma " << lem << std::endl; lems.push_back( lem ); diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index 53c04cfe8..53842b373 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -99,9 +99,9 @@ typedef enum { } QcfMode; typedef enum { - /** default, use but do not trust */ - USER_PAT_MODE_DEFAULT, - /** if patterns are supplied for a quantifier, use only those */ + /** use but do not trust */ + USER_PAT_MODE_USE, + /** default, if patterns are supplied for a quantifier, use only those */ USER_PAT_MODE_TRUST, /** ignore user patterns */ USER_PAT_MODE_IGNORE, diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 1cab2f9d8..dc2102ffa 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -101,7 +101,7 @@ option cbqi --enable-cbqi bool :read-write :default false option recurseCbqi --cbqi-recurse bool :default false turns on recursive counterexample-based quantifier instantiation -option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToUserPatMode :handler-include "theory/quantifiers/options_handlers.h" +option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_TRUST :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToUserPatMode :handler-include "theory/quantifiers/options_handlers.h" policy for handling user-provided patterns for quantifier instantiation option flipDecision --flip-decision/ bool :default false @@ -178,7 +178,7 @@ option conjectureUeeIntro --conjecture-gen-uee-intro bool :default false option ceGuidedInst --cegqi bool :default false counterexample guided quantifier instantiation -option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_UF_DT_SIZE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToCegqiFairMode :handler-include "theory/quantifiers/options_handlers.h" +option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToCegqiFairMode :handler-include "theory/quantifiers/options_handlers.h" if and how to apply fairness for cegqi endmodule diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index be74fffab..461dbafe9 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -141,13 +141,13 @@ mc \n\ static const std::string userPatModeHelp = "\ User pattern modes currently supported by the --user-pat option:\n\ \n\ -default \n\ -+ Default, use both user-provided and auto-generated patterns when patterns\n\ - are provided for a quantified formula.\n\ -\n\ trust \n\ + When provided, use only user-provided patterns for a quantified formula.\n\ \n\ +use \n\ ++ Use both user-provided and auto-generated patterns when patterns\n\ + are provided for a quantified formula.\n\ +\n\ ignore \n\ + Ignore user-provided patterns. \n\ \n\ @@ -322,9 +322,9 @@ inline QcfMode stringToQcfMode(std::string option, std::string optarg, SmtEngine } inline UserPatMode stringToUserPatMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "default") { - return USER_PAT_MODE_DEFAULT; - } else if(optarg == "trust") { + if(optarg == "use") { + return USER_PAT_MODE_USE; + } else if(optarg == "default" || optarg == "trust") { return USER_PAT_MODE_TRUST; } else if(optarg == "ignore") { return USER_PAT_MODE_IGNORE; diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 8136bf11e..f976a0dbf 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1655,7 +1655,7 @@ bool MatchGen::isHandledBoolConnective( TNode n ) { bool MatchGen::isHandledUfTerm( TNode n ) { //return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT || // n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER; - return inst::Trigger::isAtomicTriggerKind( n.getKind() ); + return inst::Trigger::isAtomicTriggerKind( n.getKind() ); } Node MatchGen::getOperator( QuantConflictFind * p, Node n ) { @@ -1683,7 +1683,6 @@ bool MatchGen::isHandled( TNode n ) { QuantConflictFind::QuantConflictFind( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ), -d_c( c ), d_conflict( c, false ), d_qassert( c ) { d_fid_count = 0; diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 81f31fa90..93e1f72a6 100755 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -164,7 +164,6 @@ class QuantConflictFind : public QuantifiersModule typedef context::CDChunkList NodeList; typedef context::CDHashMap NodeBoolMap; private: - context::Context* d_c; context::CDO< bool > d_conflict; std::vector< Node > d_quant_order; std::map< Kind, Node > d_zero;