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

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index a699528855931f596efa1158b298bfa81da5a25d..19bfe3ca549d3c3e0a7145c72943a906e9320c6d 100644 (file)
--- 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 dddbee73b34082dbbd4715290e88f95ddab5202c..69e8cc4e090e79a040aec6db2730f113aa04b0d8 100644 (file)
--- 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 53c04cfe8df8f5a6c9fd647d0f0ec6d9b18d6fb0..53842b373ae8e2dd15d6c52d817da5288545fb2d 100644 (file)
--- 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 1cab2f9d89ad5dbb1b15339423e88d18d11b55d8..dc2102ffae20b22f70b8c188a9d96cf84117dd76 100644 (file)
--- 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 be74fffab16e863691a858576be48c58b538e41a..461dbafe9571307c1c38e49e6a8ac98fe3ba9eba 100644 (file)
--- 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 8136bf11e854fb92b7de787fb1b458db1d0f4551..f976a0dbf30863a4c974ab6028693e67b6e04a91 100755 (executable)
--- 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 ) {\r
   //return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT ||\r
   //       n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER;\r
-  return inst::Trigger::isAtomicTriggerKind( n.getKind() );  \r
+  return inst::Trigger::isAtomicTriggerKind( n.getKind() );\r
 }\r
 \r
 Node MatchGen::getOperator( QuantConflictFind * p, Node n ) {\r
@@ -1683,7 +1683,6 @@ bool MatchGen::isHandled( TNode n ) {
 \r
 QuantConflictFind::QuantConflictFind( QuantifiersEngine * qe, context::Context* c ) :\r
 QuantifiersModule( qe ),\r
-d_c( c ),\r
 d_conflict( c, false ),\r
 d_qassert( c ) {\r
   d_fid_count = 0;\r

diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 81f31fa900b9b5e5fd59ba4e5bb88ac3931ce017..93e1f72a66a7548ae1e7ff7fb4aea545d489250d 100755 (executable)
--- 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;\r
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;\r
 private:\r
-  context::Context* d_c;\r
   context::CDO< bool > d_conflict;\r
   std::vector< Node > d_quant_order;\r
   std::map< Kind, Node > d_zero;\r