Refactor option for uf+cardinality constraints solver.

diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index f3d3e4bc9eabda20a380337ed3a357ef2fae410a..9e5a8997b9307428b51714c0363523678422d8b0 100644 (file)
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -103,7 +103,8 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){
             Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl;
             //let the strong solver verify that the model is minimal
             //for debugging, this will if there are terms in the model that the strong solver was not notified of
-            if( ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->debugModel( fm ) ){
+            uf::StrongSolverTheoryUF * ufss = ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver();
+            if( !ufss || ufss->debugModel( fm ) ){
               Trace("model-engine-debug") << "Check model..." << std::endl;
               d_incomplete_check = false;
               //print debug

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index c1ad62cd995692c27c5a51d4fb03d4fee35ba79e..5dd3816c533340a4a86bf064ac78670fe44f3524 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -215,12 +215,10 @@ void QuantifiersEngine::check( Theory::Effort e ){
     Trace("quant-engine-debug") << "Done resetting all modules." << std::endl;
 
     if( e==Theory::EFFORT_LAST_CALL ){
-      //if effort is last call, try to minimize model first
-      if( options::finiteModelFind() ){
-        //first, check if we can minimize the model further  FIXME: remove?
-        if( !((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->minimize() ){
-          return;
-        }
+      //if effort is last call, try to minimize model first FIXME: remove?
+      uf::StrongSolverTheoryUF * ufss = ((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver();
+      if( ufss && !ufss->minimize() ){
+        return;
       }
       ++(d_statistics.d_instantiation_rounds_lc);
     }else if( e==Theory::EFFORT_FULL ){

diff --git a/src/theory/uf/options b/src/theory/uf/options
index 26f87da79c06383ee63cfdc73916cc3255b4e326..d9e4c94770258e726747dedb8036d957e378d2ce 100644 (file)
--- a/src/theory/uf/options
+++ b/src/theory/uf/options
@@ -29,8 +29,8 @@ option ufssSimpleCliques --uf-ss-simple-cliques bool :default true
  always use simple clique lemmas for uf strong solver
 option ufssDiseqPropagation --uf-ss-deq-prop bool :default false
  eagerly propagate disequalities for uf strong solver
-option ufssMinimalModel /--disable-uf-ss-min-model bool :default true
- disable finding a minimal model in uf strong solver
+option ufssMode --uf-ss=MODE CVC4::theory::uf::UfssMode :default CVC4::theory::uf::UF_SS_FULL :include "theory/uf/options_handlers.h" :handler CVC4::theory::uf::stringToUfssMode :handler-include "theory/uf/options_handlers.h"
+ mode of operation for uf strong solver.
 option ufssCliqueSplits --uf-ss-clique-splits bool :default false
  use cliques instead of splitting on demand to shrink model
 

diff --git a/src/theory/uf/options_handlers.h b/src/theory/uf/options_handlers.h
index a885a10d203a4dc82de8d8403cea76486dfe087a..8c072e2321f05251f7d6ef0296c324208c68bf1b 100644 (file)
--- a/src/theory/uf/options_handlers.h
+++ b/src/theory/uf/options_handlers.h
@@ -2,7 +2,7 @@
 /*! \file options_handlers.h
  ** \verbatim
  ** Original author: Morgan Deters
- ** Major contributors: none
+ ** Major contributors: Andrew Reynolds
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2014  New York University and The University of Iowa
@@ -22,6 +22,45 @@
 namespace CVC4 {
 namespace theory {
 namespace uf {
+  
+typedef enum {
+  /** default, use uf strong solver to find minimal models for uninterpreted sorts */
+  UF_SS_FULL,
+  /** use uf strong solver to shrink model sizes, but do no enforce minimality */
+  UF_SS_NO_MINIMAL,
+  /** do not use uf strong solver */
+  UF_SS_NONE,
+} UfssMode;
+  
+static const std::string ufssModeHelp = "\
+UF strong solver options currently supported by the --uf-ss option:\n\
+\n\
+full \n\
++ Default, use uf strong solver to find minimal models for uninterpreted sorts.\n\
+\n\
+no-minimal \n\
++ Use uf strong solver to shrink model sizes, but do no enforce minimality.\n\
+\n\
+none \n\
++ Do not use uf strong solver to shrink model sizes. \n\
+\n\
+";
+
+inline UfssMode stringToUfssMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg ==  "default" || optarg == "full" ) {
+    return UF_SS_FULL;
+  } else if(optarg == "no-minimal") {
+    return UF_SS_NO_MINIMAL;
+  } else if(optarg == "none") {
+    return UF_SS_NONE;
+  } else if(optarg ==  "help") {
+    puts(ufssModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --uf-ss: `") +
+                          optarg + "'.  Try --uf-ss help.");
+  }
+}
 
 }/* CVC4::theory::uf namespace */
 }/* CVC4::theory namespace */

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 4fcf4166b6eb32088acfbd1ebec898b63ce03867..2b9fc3daf8ce98f902914606ad25d36fdfc2d6d2 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -61,7 +61,7 @@ void TheoryUF::setMasterEqualityEngine(eq::EqualityEngine* eq) {
 
 void TheoryUF::finishInit() {
   // initialize the strong solver
-  if (options::finiteModelFind()) {
+  if (options::finiteModelFind() && options::ufssMode()!=UF_SS_NONE) {
     d_thss = new StrongSolverTheoryUF(getSatContext(), getUserContext(), *d_out, this);
   }
 }

diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 001b21d0afd35a0acb3be479374fb8188230a2f7..cddaace3edf51bc5a92e76d7aed24ec4155d7c0a 100644 (file)
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -339,16 +339,6 @@ bool StrongSolverTheoryUF::SortModel::Region::getCandidateClique( int cardinalit
   return false;
 }
 
-
-void StrongSolverTheoryUF::SortModel::Region::getRepresentatives( std::vector< Node >& reps ){
-  for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){
-    RegionNodeInfo* rni = it->second;
-    if( rni->d_valid ){
-      reps.push_back( it->first );
-    }
-  }
-}
-
 void StrongSolverTheoryUF::SortModel::Region::getNumExternalDisequalities( std::map< Node, int >& num_ext_disequalities ){
   for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){
     RegionNodeInfo* rni = it->second;
@@ -624,7 +614,7 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel
           if( d_regions[i]->d_valid ){
             std::vector< Node > clique;
             if( d_regions[i]->check( level, d_cardinality, clique ) ){
-              if( options::ufssMinimalModel() ){
+              if( options::ufssMode()==UF_SS_FULL ){
                 //add clique lemma
                 addCliqueLemma( clique, out );
                 return;
@@ -695,7 +685,7 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel
                 if( d_regions[i]->d_valid ){
                   int fcr = forceCombineRegion( i, false );
                   Trace("uf-ss-debug") << "Combined regions " << i << " " << fcr << std::endl;
-                  if( options::ufssMinimalModel() || fcr!=-1 ){
+                  if( options::ufssMode()==UF_SS_FULL || fcr!=-1 ){
                     recheck = true;
                     break;
                   }
@@ -921,7 +911,7 @@ void StrongSolverTheoryUF::SortModel::checkRegion( int ri, bool checkCombine ){
     //now check if region is in conflict
     std::vector< Node > clique;
     if( d_regions[ri]->check( Theory::EFFORT_STANDARD, d_cardinality, clique ) ){
-      if( options::ufssMinimalModel() ){
+      if( options::ufssMode()==UF_SS_FULL ){
         //explain clique
         addCliqueLemma( clique, &d_thss->getOutputChannel() );
       }
@@ -1085,7 +1075,7 @@ int StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){
     }
     Assert( s!=Node::null() );
   }else{
-    if( !options::ufssMinimalModel() ){
+    if( options::ufssMode()!=UF_SS_FULL ){
       //since candidate clique is not reported, we may need to find splits manually
       for ( std::map< Node, Region::RegionNodeInfo* >::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it ){
         if ( it->second->d_valid ){
@@ -1480,19 +1470,6 @@ int StrongSolverTheoryUF::SortModel::getNumRegions(){
   return count;
 }
 
-void StrongSolverTheoryUF::SortModel::getRepresentatives( std::vector< Node >& reps ){
-  for( int i=0; i<(int)d_regions_index; i++ ){
-    //should not have multiple regions at this point
-    //if( foundRegion ){
-    //  Assert( !d_regions[i]->d_valid );
-    //}
-    if( d_regions[i]->d_valid ){
-      //this is the only valid region
-      d_regions[i]->getRepresentatives( reps );
-    }
-  }
-}
-
 Node StrongSolverTheoryUF::SortModel::getCardinalityLiteral( int c ) {
   if( d_cardinality_literal.find( c )==d_cardinality_literal.end() ){
     d_cardinality_literal[c] = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, d_cardinality_term,
@@ -1661,7 +1638,7 @@ bool StrongSolverTheoryUF::areDisequal( Node a, Node b ) {
 void StrongSolverTheoryUF::check( Theory::Effort level ){
   if( !d_conflict ){
     Trace("uf-ss-solver") << "StrongSolverTheoryUF: check " << level << std::endl;
-    if( level==Theory::EFFORT_FULL ){
+    if( level==Theory::EFFORT_FULL && Debug.isOn( "uf-ss-debug" ) ){
       debugPrint( "uf-ss-debug" );
     }
     for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
@@ -1801,19 +1778,6 @@ int StrongSolverTheoryUF::getCardinality( TypeNode tn ) {
   return -1;
 }
 
-/*
-void StrongSolverTheoryUF::getRepresentatives( Node n, std::vector< Node >& reps ){
-  SortModel* c = getSortModel( n );
-  if( c ){
-    c->getRepresentatives( reps );
-    if( (int)reps.size()!=c->getCardinality() ){
-      Trace("uf-ss-warn") << "Sort " << n.getType() << " has cardinality " << c->getCardinality();
-      Trace("uf-ss-warn") << ", but provided " << reps.size() << " representatives!!!" << std::endl;
-    }
-  }
-}
-*/
-
 bool StrongSolverTheoryUF::minimize( TheoryModel* m ){
   for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
     if( !it->second->minimize( d_out, m ) ){

diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index 1e5a361a7f1e826ec87ca3ac578ea7eda8db9686..333f1717e5527e7bd77af4a79492b7874b91d53d 100644 (file)
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -146,8 +146,6 @@ public:
       bool getMustCombine( int cardinality );
       /** has splits */
       bool hasSplits() { return d_splitsSize>0; }
-      /** get representatives */
-      void getRepresentatives( std::vector< Node >& reps );
       /** get external disequalities */
       void getNumExternalDisequalities( std::map< Node, int >& num_ext_disequalities );
     public:
@@ -280,8 +278,6 @@ public:
     bool isConflict() { return d_conflict; }
     /** get cardinality */
     int getCardinality() { return d_cardinality; }
-    /** get representatives */
-    void getRepresentatives( std::vector< Node >& reps );
     /** has cardinality */
     bool hasCardinalityAsserted() { return d_hasCard; }
     /** get cardinality term */
@@ -381,8 +377,6 @@ public:
   int getCardinality( Node n );
   /** get cardinality for type */
   int getCardinality( TypeNode tn );
-  /** get representatives */
-  //void getRepresentatives( Node n, std::vector< Node >& reps );
   /** minimize */
   bool minimize( TheoryModel* m = NULL );