summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/printer/smt2/smt2_printer.cpp10
-rw-r--r--src/theory/quantifiers/ce_guided_instantiation.cpp3
-rw-r--r--src/theory/quantifiers/ce_guided_instantiation.h1
-rw-r--r--src/theory/quantifiers/full_model_check.cpp11
-rw-r--r--src/theory/quantifiers/full_model_check.h3
-rw-r--r--src/theory/quantifiers/fun_def_process.cpp1
-rw-r--r--src/theory/quantifiers/model_builder.h2
-rw-r--r--src/theory/quantifiers_engine.cpp10
8 files changed, 14 insertions, 27 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index a98a106a1..7648a1587 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -32,6 +32,7 @@
#include "theory/theory_model.h"
#include "theory/arrays/theory_arrays_rewriter.h"
+#include "theory/quantifiers/term_database.h"
using namespace std;
@@ -589,9 +590,14 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
case kind::INST_PATTERN:
break;
case kind::INST_PATTERN_LIST:
- // TODO user patterns
for(unsigned i=0; i<n.getNumChildren(); i++) {
- out << ":pattern " << n[i];
+ if( n[i].getKind()==kind::INST_ATTRIBUTE ){
+ if( n[i][0].getAttribute(theory::FunDefAttribute()) ){
+ out << ":fun-def";
+ }
+ }else{
+ out << ":pattern " << n[i];
+ }
}
return;
break;
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index ea97513b8..e1fc9e793 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -141,9 +141,6 @@ bool CegInstantiation::needsCheck( Theory::Effort e ) {
bool CegInstantiation::needsModel( Theory::Effort e ) {
return true;
}
-bool CegInstantiation::needsFullModel( Theory::Effort e ) {
- return true;
-}
void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) {
if( quant_e==QuantifiersEngine::QEFFORT_MODEL ){
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 786db12a9..f5077ad04 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -119,7 +119,6 @@ public:
public:
bool needsCheck( Theory::Effort e );
bool needsModel( Theory::Effort e );
- bool needsFullModel( Theory::Effort e );
/* Call during quantifier engine's check */
void check( Theory::Effort e, unsigned quant_e );
/* Called for new quantifiers */
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index c0a734c35..c3a723fce 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -325,15 +325,9 @@ QModelBuilder( c, qe ){
d_false = NodeManager::currentNM()->mkConst(false);
}
-bool FullModelChecker::optBuildAtFullModel() {
- //need to build after full model has taken effect if we are constructing interval models
- // this is because we need to have a constant in all integer equivalence classes
- return options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL;
-}
-
void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();
- if( fullModel==optBuildAtFullModel() ){
+ if( !fullModel ){
Trace("fmc") << "---Full Model Check reset() " << std::endl;
fm->initialize();
d_quant_models.clear();
@@ -514,8 +508,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
}
*/
}
- }
- if( fullModel ){
+ }else{
//make function values
for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ){
m->d_uf_models[ it->first ] = getFunctionValue( fm, it->first, "$x" );
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index 9a7b05090..29913d98d 100644
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -135,9 +135,6 @@ public:
FullModelChecker( context::Context* c, QuantifiersEngine* qe );
~FullModelChecker() throw() {}
- bool optBuildAtFullModel();
-
-
void debugPrintCond(const char * tr, Node n, bool dispStar = false);
void debugPrint(const char * tr, Node n, bool dispStar = false);
diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp
index 22dac2225..a46aca3c8 100644
--- a/src/theory/quantifiers/fun_def_process.cpp
+++ b/src/theory/quantifiers/fun_def_process.cpp
@@ -46,6 +46,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
}
Node bd = TermDb::getFunDefBody( assertions[i] );
+ Trace("fmf-fun-def-debug") << "Process function " << n << ", body = " << bd << std::endl;
Assert( !bd.isNull() );
bd = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, n, bd );
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index a3d239d18..d9ed3f092 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -42,8 +42,6 @@ public:
virtual bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { return false; }
//whether to construct model
virtual bool optUseModel();
- //whether to construct model at fullModel = true
- virtual bool optBuildAtFullModel() { return false; }
/** number of lemmas generated while building model */
//is the exhaustive instantiation incomplete?
bool d_incomplete_check;
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 3fa3b2a1b..f6645c493 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -267,7 +267,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
}
bool needsCheck = !d_lemmas_waiting.empty();
bool needsModel = false;
- bool needsFullModel = false;
std::vector< QuantifiersModule* > qm;
if( d_model->checkNeeded() ){
needsCheck = needsCheck || e>=Theory::EFFORT_LAST_CALL; //always need to check at or above last call
@@ -277,9 +276,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
needsCheck = true;
if( d_modules[i]->needsModel( e ) ){
needsModel = true;
- if( d_modules[i]->needsFullModel( e ) ){
- needsFullModel = true;
- }
}
}
}
@@ -347,9 +343,9 @@ void QuantifiersEngine::check( Theory::Effort e ){
//build the model if any module requested it
if( quant_e==QEFFORT_MODEL && needsModel ){
Assert( d_builder!=NULL );
- Trace("quant-engine-debug") << "Build model, fullModel = " << ( needsFullModel || d_builder->optBuildAtFullModel() ) << "..." << std::endl;
+ Trace("quant-engine-debug") << "Build model..." << std::endl;
d_builder->d_addedLemmas = 0;
- d_builder->buildModel( d_model, needsFullModel || d_builder->optBuildAtFullModel() );
+ d_builder->buildModel( d_model, false );
//we are done if model building was unsuccessful
if( d_builder->d_addedLemmas>0 ){
success = false;
@@ -368,7 +364,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
if( d_hasAddedLemma ){
break;
//otherwise, complete the model generation if necessary
- }else if( quant_e==QEFFORT_MODEL && needsModel && options::produceModels() && !needsFullModel && !d_builder->optBuildAtFullModel() ){
+ }else if( quant_e==QEFFORT_MODEL && needsModel && options::produceModels() ){
Trace("quant-engine-debug") << "Build completed model..." << std::endl;
d_builder->buildModel( d_model, true );
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback