diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-16 22:16:49 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-16 22:16:55 +0200 |
commit | 9d7378688486cb0dbad207482932dfb4b5d91f95 (patch) | |
tree | 11762aa3a877de82f3b578699c40ba37016efb79 /src/theory/quantifiers | |
parent | 6d279143db69b153815165c752eae1432538ec2e (diff) |
Make --user-pat=trust default. Fix a few warnings found by Morgan. Minor changes to options.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/modes.h | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/options | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/options_handlers.h | 14 | ||||
-rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.cpp | 3 | ||||
-rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.h | 1 |
6 files changed, 16 insertions, 17 deletions
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<Node> NodeList;
typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
private:
- context::Context* d_c;
context::CDO< bool > d_conflict;
std::vector< Node > d_quant_order;
std::map< Kind, Node > d_zero;
|