d_context->push();
d_definedFunctions = new(true) DefinedFunctionMap(d_userContext);
- if( options::fmfFunWellDefined() ){
+ if( options::fmfFunWellDefined() || options::fmfFunWellDefinedRelevant() ){
d_fmfRecFunctionsAbs = new(true) TypeNodeMap(d_userContext);
d_fmfRecFunctionsConcrete = new(true) NodeListMap(d_userContext);
}
if( options::ufssSymBreak() ){
options::sortInference.set( true );
}
+ if( options::fmfFunWellDefinedRelevant() ){
+ if( !options::fmfFunWellDefined.wasSetByUser() ){
+ options::fmfFunWellDefined.set( true );
+ }
+ }
if( options::fmfFunWellDefined() ){
if( !options::finiteModelFind.wasSetByUser() ){
options::finiteModelFind.set( true );
FirstOrderModel::FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name ) :
TheoryModel( c, name, true ),
-d_qe( qe ), d_axiom_asserted( c, false ), d_forall_asserts( c ), d_isModelSet( c, false ){
+d_qe( qe ), d_forall_asserts( c ), d_isModelSet( c, false ){
}
if( !reduced ){
if( n.getKind()==FORALL ){
d_forall_asserts.push_back( n );
- if( n.getAttribute(AxiomAttribute()) ){
- d_axiom_asserted = true;
- }
}else if( n.getKind()==NOT ){
Assert( n[0].getKind()==FORALL );
}
protected:
/** quant engine */
QuantifiersEngine * d_qe;
- /** whether an axiom is asserted */
- context::CDO< bool > d_axiom_asserted;
/** list of quantifiers asserted in the current context */
context::CDList<Node> d_forall_asserts;
/** list of quantifiers that have been marked to reduce */
Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; }
/** get number to reduce quantifiers */
unsigned getNumToReduceQuantifiers() { return d_forall_to_reduce.size(); }
- /** bool axiom asserted */
- bool isAxiomAsserted() { return d_axiom_asserted; }
/** initialize model for term */
void initializeModelForTerm( Node n );
virtual void processInitializeModelForTerm( Node n ) = 0;
std::stringstream ss;
ss << "I_" << f;
TypeNode iType = NodeManager::currentNM()->mkSort( ss.str() );
+ AbsTypeFunDefAttribute atfda;
+ iType.setAttribute(atfda,true);
d_sorts[f] = iType;
//create functions f1...fn mapping from this sort to concrete elements
}
unsigned ModelEngine::needsModel( Theory::Effort e ) {
- return QuantifiersEngine::QEFFORT_MODEL;
+ return QuantifiersEngine::QEFFORT_MODEL;
}
void ModelEngine::reset_round( Theory::Effort e ) {
int addedLemmas = 0;
FirstOrderModel* fm = d_quantEngine->getModel();
- //the following will test that the model satisfies all asserted universal quantifiers by
+ //the following will test that the model satisfies all asserted universal quantifiers by
// (model-based) exhaustive instantiation.
double clSet = 0;
if( Trace.isOn("model-engine") ){
}else{
addedLemmas++;
}
-
+
if( Trace.isOn("model-engine") ){
double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
int ModelEngine::checkModel(){
FirstOrderModel* fm = d_quantEngine->getModel();
- quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder();
- Assert( mb!=NULL );
//flatten the representatives
//Trace("model-engine-debug") << "Flattening representatives...." << std::endl;
}
Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
- //default : 1 : conj,axiom
- //priority : 0 : conj, 1 : axiom
- //trust : 0 : conj
- int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0;
- for( int effort=startEffort; effort<2; effort++ ){
- // FMC uses two sub-effort levels
- int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : ( options::mbqiMode()==MBQI_TRUST ? 0 : 1 );
- for( int e=0; e<e_max; e++) {
- if (d_addedLemmas==0) {
- for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
- Node f = fm->getAssertedQuantifier( i );
- bool isAx = getTermDatabase()->isQAttrAxiom( f );
- Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << f << ", effort = " << e << "..." << std::endl;
- //determine if we should check this quantifier
- if( ( ( effort==1 && ( options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT || isAx ) ) || ( effort==0 && !isAx ) ) && mb->isQuantifierActive( f ) ){
- exhaustiveInstantiate( f, e );
- if( Trace.isOn("model-engine-warn") ){
- if( d_addedLemmas>10000 ){
- Debug("fmf-exit") << std::endl;
- debugPrint("fmf-exit");
- exit( 0 );
- }
+ // FMC uses two sub-effort levels
+ int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : ( options::mbqiMode()==MBQI_TRUST ? 0 : 1 );
+ for( int e=0; e<e_max; e++) {
+ if (d_addedLemmas==0) {
+ for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+ Node f = fm->getAssertedQuantifier( i );
+ Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << f << ", effort = " << e << "..." << std::endl;
+ //determine if we should check this quantifier
+ if( considerQuantifiedFormula( f ) ){
+ exhaustiveInstantiate( f, e );
+ if( Trace.isOn("model-engine-warn") ){
+ if( d_addedLemmas>10000 ){
+ Debug("fmf-exit") << std::endl;
+ debugPrint("fmf-exit");
+ exit( 0 );
}
- if( optOneQuantPerRound() && d_addedLemmas>0 ){
- break;
- }
- }else{
- Trace("fmf-exh-inst") << "-> Inactive : " << f << std::endl;
}
+ if( optOneQuantPerRound() && d_addedLemmas>0 ){
+ break;
+ }
+ }else{
+ Trace("fmf-exh-inst") << "-> Inactive : " << f << std::endl;
}
}
}
- if( d_addedLemmas==0 && options::axiomInstMode()==AXIOM_INST_MODE_TRUST ){
- //set incomplete
- if( effort==0 ){
- d_incomplete_check = true;
- }
- break;
- }
}
+
//print debug information
Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / ";
Trace("model-engine") << d_totalLemmas << std::endl;
return d_addedLemmas;
}
+bool ModelEngine::considerQuantifiedFormula( Node q ) {
+ if( !d_quantEngine->getModelBuilder()->isQuantifierActive( q ) ){ //!d_quantEngine->getModel()->isQuantifierActive( q );
+ return false;
+ }else{
+ if( options::fmfFunWellDefinedRelevant() ){
+ if( q[0].getNumChildren()==1 ){
+ TypeNode tn = q[0][0].getType();
+ if( tn.getAttribute(AbsTypeFunDefAttribute()) ){
+ //we are allowed to assume the introduced type is empty
+ if( d_quantEngine->getModel()->d_rep_set.getNumRelevantGroundReps( tn )==0 ){
+ Trace("model-engine-debug") << "Irrelevant function definition : " << q << std::endl;
+ return false;
+ }
+ }
+ }
+ }
+ return true;
+ }
+}
+
void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
//first check if the builder can do the exhaustive instantiation
quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder();
private:
//check model
int checkModel();
+ //consider quantified formula
+ bool considerQuantifiedFormula( Node q );
//exhaustively instantiate quantifier (possibly using mbqi)
void exhaustiveInstantiate( Node f, int effort = 0 );
private:
return out;
}
-std::ostream& operator<<(std::ostream& out, theory::quantifiers::AxiomInstMode mode) {
- switch(mode) {
- case theory::quantifiers::AXIOM_INST_MODE_DEFAULT:
- out << "AXIOM_INST_MODE_DEFAULT";
- break;
- case theory::quantifiers::AXIOM_INST_MODE_TRUST:
- out << "AXIOM_INST_MODE_TRUST";
- break;
- case theory::quantifiers::AXIOM_INST_MODE_PRIORITY:
- out << "AXIOM_INST_MODE_PRIORITY";
- break;
- default:
- out << "AxiomInstMode!UNKNOWN";
- }
-
- return out;
-}
-
std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode) {
switch(mode) {
case theory::quantifiers::MBQI_GEN_EVAL:
LITERAL_MATCH_EQUALITY,
} LiteralMatchMode;
-typedef enum {
- /** default, use all methods for axioms */
- AXIOM_INST_MODE_DEFAULT,
- /** only use heuristic methods for axioms, return unknown in the case no instantiations are produced */
- AXIOM_INST_MODE_TRUST,
- /** only use heuristic methods for axioms, resort to all methods when no instantiations are produced */
- AXIOM_INST_MODE_PRIORITY,
-} AxiomInstMode;
-
typedef enum {
/** mbqi from CADE 24 paper */
MBQI_GEN_EVAL,
option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h"
choose literal matching mode
-option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h"
- policy for instantiating axioms
-
### finite model finding options
option finiteModelFind finite-model-find --finite-model-find bool :default false :read-write
option quantFunWellDefined --quant-fun-wd bool :default false
assume that function defined by quantifiers are well defined
-option fmfFunWellDefined --fmf-fun bool :default false
- find models for finite runs of defined functions, assumes functions are well-defined
+option fmfFunWellDefined --fmf-fun bool :default false :read-write
+ find models for recursively defined functions, assumes functions are admissible
+option fmfFunWellDefinedRelevant --fmf-fun-rlv bool :default false
+ find models for recursively defined functions, assumes functions are admissible, allows empty type when function is irrelevant
option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_FMC :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h"
choose mode for model-based quantifier instantiation
Q( x ) with Q( s ) where Q( s ) is in the equivalence class of true.\n\
\n\
";
-
-static const std::string axiomInstModeHelp = "\
-Axiom instantiation modes currently supported by the --axiom-inst option:\n\
-\n\
-default \n\
-+ Treat axioms the same as usual quantifiers, i.e. use all available methods for\n\
- instantiating axioms.\n\
-\n\
-trust \n\
-+ Treat axioms only using heuristic instantiation. Return unknown if in the case\n\
- that no instantiations are produced.\n\
-\n\
-priority \n\
-+ Treat axioms only using heuristic instantiation. Resort to using all methods\n\
- in the case that no instantiations are produced.\n\
-\n\
-";
-
static const std::string mbqiModeHelp = "\
Model-based quantifier instantiation modes currently supported by the --mbqi option:\n\
\n\
}
}
-inline AxiomInstMode stringToAxiomInstMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
- if(optarg == "default") {
- return AXIOM_INST_MODE_DEFAULT;
- } else if(optarg == "trust") {
- return AXIOM_INST_MODE_TRUST;
- } else if(optarg == "priority") {
- return AXIOM_INST_MODE_PRIORITY;
- } else if(optarg == "help") {
- puts(axiomInstModeHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --axiom-inst: `") +
- optarg + "'. Try --axiom-inst help.");
- }
-}
-
inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
if(optarg == "gen-ev") {
return MBQI_GEN_EVAL;
struct SygusProxyAttributeId {};
typedef expr::Attribute<SygusProxyAttributeId, Node> SygusProxyAttribute;
+//attribute for fun-def abstraction type
+struct AbsTypeFunDefAttributeId {};
+typedef expr::Attribute<AbsTypeFunDefAttributeId, bool> AbsTypeFunDefAttribute;
+
class QuantifiersEngine;
namespace inst{
d_type_complete.clear();
d_tmap.clear();
d_values_to_terms.clear();
+ d_type_rlv_rep.clear();
}
bool RepSet::hasRep( TypeNode tn, Node n ) {
bool RepSet::complete( TypeNode t ){
std::map< TypeNode, bool >::iterator it = d_type_complete.find( t );
if( it==d_type_complete.end() ){
- //remove all previous
+ //remove all previous
for( unsigned i=0; i<d_type_reps[t].size(); i++ ){
d_tmap.erase( d_type_reps[t][i] );
}
}
}
+int RepSet::getNumRelevantGroundReps( TypeNode t ) {
+ std::map< TypeNode, int >::iterator it = d_type_rlv_rep.find( t );
+ if( it==d_type_rlv_rep.end() ){
+ return 0;
+ }else{
+ return it->second;
+ }
+}
+
void RepSet::toStream(std::ostream& out){
#if 0
for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){
//FIXME:
// terms in rep_set are now constants which mapped to terms through TheoryModel
// thus, should introduce a constant and a term. for now, just a term.
-
+
//Node c = d_qe->getTermDatabase()->getEnumerateTerm( tn, 0 );
Node var = d_qe->getModel()->getSomeDomainElement( tn );
Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl;
std::map< TypeNode, std::vector< Node > > d_type_reps;
std::map< TypeNode, bool > d_type_complete;
std::map< Node, int > d_tmap;
+ std::map< TypeNode, int > d_type_rlv_rep;
// map from values to terms they were assigned for
std::map< Node, Node > d_values_to_terms;
/** clear the set */
int getIndexFor( Node n ) const;
/** complete all values */
bool complete( TypeNode t );
+ /** get number of relevant ground representatives for type */
+ int getNumRelevantGroundReps( TypeNode t );
/** debug print */
void toStream(std::ostream& out);
};/* class RepSet */
tm->d_rep_set.add((*i).getType(), *i);
}
}
+ for( std::map< TypeNode, std::vector< Node > >::iterator it = tm->d_rep_set.d_type_reps.begin(); it != tm->d_rep_set.d_type_reps.end(); ++it ){
+ tm->d_rep_set.d_type_rlv_rep[it->first] = (int)it->second.size();
+ }
}
//modelBuilder-specific initialization
projects / cvc5.git / commitdiff