From 4d7329f72720e884a6161dcdeb8d377d19031930 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 24 Sep 2014 14:35:39 +0200 Subject: [PATCH] Refactor option for uf+cardinality constraints solver. --- src/theory/quantifiers/model_engine.cpp | 3 +- src/theory/quantifiers_engine.cpp | 10 ++--- src/theory/uf/options | 4 +- src/theory/uf/options_handlers.h | 41 +++++++++++++++++++- src/theory/uf/theory_uf.cpp | 2 +- src/theory/uf/theory_uf_strong_solver.cpp | 46 +++-------------------- src/theory/uf/theory_uf_strong_solver.h | 6 --- 7 files changed, 54 insertions(+), 58 deletions(-) diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index f3d3e4bc9..9e5a8997b 100644 --- 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 c1ad62cd9..5dd3816c5 100644 --- 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 26f87da79..d9e4c9477 100644 --- 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 a885a10d2..8c072e232 100644 --- 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 4fcf4166b..2b9fc3daf 100644 --- 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 001b21d0a..cddaace3e 100644 --- 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 1e5a361a7..333f1717e 100644 --- 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 ); -- 2.30.2