Make --user-pat=trust default. Fix a few warnings found by Morgan. Minor changes to options.

7 files changed, 23 insertions, 17 deletions

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<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;