summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/smt/smt_engine.cpp7
-rw-r--r--src/theory/quantifiers/first_order_model.cpp5
-rw-r--r--src/theory/quantifiers/first_order_model.h4
-rw-r--r--src/theory/quantifiers/fun_def_process.cpp2
-rw-r--r--src/theory/quantifiers/model_engine.cpp83
-rw-r--r--src/theory/quantifiers/model_engine.h2
-rw-r--r--src/theory/quantifiers/modes.cpp18
-rw-r--r--src/theory/quantifiers/modes.h9
-rw-r--r--src/theory/quantifiers/options9
-rw-r--r--src/theory/quantifiers/options_handlers.h34
-rw-r--r--src/theory/quantifiers/term_database.h4
-rw-r--r--src/theory/rep_set.cpp14
-rw-r--r--src/theory/rep_set.h3
-rw-r--r--src/theory/theory_model.cpp3
14 files changed, 81 insertions, 116 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4874b076e..0af5c7fc1 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -739,7 +739,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
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);
}
@@ -1364,6 +1364,11 @@ void SmtEngine::setDefaults() {
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 );
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 346631889..36d055b69 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -32,7 +32,7 @@ using namespace CVC4::theory::quantifiers::fmcheck;
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 ){
}
@@ -40,9 +40,6 @@ void FirstOrderModel::assertQuantifier( Node n, bool reduced ){
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 );
}
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 25d71984d..a31e85d7e 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -47,8 +47,6 @@ class FirstOrderModel : public TheoryModel
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 */
@@ -68,8 +66,6 @@ public: //for Theory Quantifiers:
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;
diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp
index 0197bda6b..632e19a18 100644
--- a/src/theory/quantifiers/fun_def_process.cpp
+++ b/src/theory/quantifiers/fun_def_process.cpp
@@ -55,6 +55,8 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
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
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 2ad8be3a1..752e88c5a 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -52,7 +52,7 @@ bool ModelEngine::needsCheck( Theory::Effort e ) {
}
unsigned ModelEngine::needsModel( Theory::Effort e ) {
- return QuantifiersEngine::QEFFORT_MODEL;
+ return QuantifiersEngine::QEFFORT_MODEL;
}
void ModelEngine::reset_round( Theory::Effort e ) {
@@ -64,7 +64,7 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_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") ){
@@ -88,7 +88,7 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){
}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;
@@ -143,8 +143,6 @@ bool ModelEngine::optOneQuantPerRound(){
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;
@@ -192,52 +190,59 @@ int ModelEngine::checkModel(){
}
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();
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index c357c2876..1fb4255b2 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -34,6 +34,8 @@ private:
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:
diff --git a/src/theory/quantifiers/modes.cpp b/src/theory/quantifiers/modes.cpp
index ebc1088a8..253f23561 100644
--- a/src/theory/quantifiers/modes.cpp
+++ b/src/theory/quantifiers/modes.cpp
@@ -59,24 +59,6 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::LiteralMatchMod
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:
diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index 94ba7daaf..9502fd362 100644
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -49,15 +49,6 @@ typedef enum {
} 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,
/** no mbqi */
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 74ce3cc6c..a31fbe6e7 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -110,9 +110,6 @@ option fullSaturateQuantRd --full-saturate-quant-rd bool :default true
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
@@ -120,8 +117,10 @@ option finiteModelFind finite-model-find --finite-model-find bool :default false
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
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index e5e484625..f27b98a3d 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -60,24 +60,6 @@ predicate\n\
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\
@@ -292,22 +274,6 @@ inline void checkLiteralMatchMode(std::string option, LiteralMatchMode mode, Smt
}
}
-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;
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 7c136a186..477b964ee 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -92,6 +92,10 @@ typedef expr::Attribute< LtePartialInstAttributeId, bool > LtePartialInstAttribu
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{
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 6a64f762e..a90a4cf17 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -29,6 +29,7 @@ void RepSet::clear(){
d_type_complete.clear();
d_tmap.clear();
d_values_to_terms.clear();
+ d_type_rlv_rep.clear();
}
bool RepSet::hasRep( TypeNode tn, Node n ) {
@@ -91,7 +92,7 @@ int RepSet::getIndexFor( Node n ) const {
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] );
}
@@ -116,6 +117,15 @@ bool RepSet::complete( TypeNode t ){
}
}
+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 ){
@@ -193,7 +203,7 @@ bool RepSetIterator::initialize(){
//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;
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index f1114edcf..2df824b5d 100644
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -33,6 +33,7 @@ public:
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 */
@@ -49,6 +50,8 @@ public:
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 */
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index c4bc94bd2..92f834bff 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -824,6 +824,9 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback