From 56a523d9c4dd04cedbd812570cd80e3bc94cce4c Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 7 Nov 2014 11:37:43 +0100 Subject: [PATCH] Properly distinguish which EQC to assign values in datatypes, use assertRepresentative. Disable regression related to records. Enable fmf-fun related regression (modified). Apply modified version of Morgan's patch to fix tuples/records in model. Fix bug with sort inference + patterns. Minor infrastructure. --- src/theory/datatypes/theory_datatypes.cpp | 23 ++++++++++++------- .../quantifiers/ce_guided_instantiation.cpp | 3 +++ .../quantifiers/ce_guided_instantiation.h | 1 + src/theory/quantifiers_engine.cpp | 10 +++++--- src/theory/quantifiers_engine.h | 2 ++ src/theory/theory_model.cpp | 5 +++- src/util/sort_inference.cpp | 5 ++-- test/regress/regress0/arrays/Makefile.am | 3 ++- test/regress/regress0/fmf/Makefile.am | 5 ++-- .../regress0/fmf/lst-no-self-rev-exp.smt2 | 6 ++++- 10 files changed, 44 insertions(+), 19 deletions(-) diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 22c0477d8..72d0c6b2b 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -1183,8 +1183,10 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ Node c = ei->d_constructor.get(); cons.push_back( c ); eqc_cons[ eqc ] = c; + m->assertRepresentative( c ); }else{ //if eqc contains a symbol known to datatypes (a selector), then we must assign +#if 0 bool shouldConsider = false; eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); while( !eqc_i.isFinished() ){ @@ -1196,9 +1198,10 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ } ++eqc_i; } -/* +#else + //should assign constructors to EQC if they have a selector or a tester bool shouldConsider = ( ei && ei->d_selectors ) || hasTester( eqc ); - */ +#endif if( shouldConsider ){ nodes.push_back( eqc ); } @@ -1217,6 +1220,8 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ bool addCons = false; const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype(); if( !d_equalityEngine.hasTerm( eqc ) ){ + Assert( false ); + /* if( !dt.isCodatatype() ){ Trace("dt-cmi") << "NOTICE : Datatypes: need to assign constructor for " << eqc << std::endl; Trace("dt-cmi") << " Type : " << eqc.getType() << std::endl; @@ -1263,6 +1268,7 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ neqc = *te; } } + */ }else{ Trace("dt-cmi") << "NOTICE : Datatypes: no constructor in equivalence class " << eqc << std::endl; Trace("dt-cmi") << " Type : " << eqc.getType() << std::endl; @@ -1280,12 +1286,12 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ //must try the infinite ones first if( pcons[i] && (r==1)==dt[ i ].isFinite() ){ neqc = DatatypesRewriter::getInstCons( eqc, dt, i ); - for( unsigned j=0; jassertEquality( eqc, neqc, true ); eqc_cons[ eqc ] = neqc; + m->assertRepresentative( neqc ); } //m->assertRepresentative( neqc ); if( addCons ){ diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 5c7b31d33..ffe64beba 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -88,6 +88,9 @@ bool CegInstantiation::needsCheck( Theory::Effort e ) { bool CegInstantiation::needsModel( Theory::Effort e ) { return true; } +bool CegInstantiation::needsFullModel( Theory::Effort e ) { + return false; +} 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 67125a8ad..235f2b01c 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -99,6 +99,7 @@ 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_engine.cpp b/src/theory/quantifiers_engine.cpp index 88b56b6bb..46995653f 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -258,6 +258,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ CodeTimer codeTimer(d_time); bool needsCheck = false; bool needsModel = false; + bool needsFullModel = false; std::vector< QuantifiersModule* > qm; if( d_model->getNumAssertedQuantifiers()>0 ){ needsCheck = e>=Theory::EFFORT_LAST_CALL; //always need to check at or above last call @@ -267,6 +268,9 @@ void QuantifiersEngine::check( Theory::Effort e ){ needsCheck = true; if( d_modules[i]->needsModel( e ) ){ needsModel = true; + if( d_modules[i]->needsFullModel( e ) ){ + needsFullModel = true; + } } } } @@ -328,9 +332,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 = " << d_builder->optBuildAtFullModel() << "..." << std::endl; + Trace("quant-engine-debug") << "Build model, fullModel = " << ( needsFullModel || d_builder->optBuildAtFullModel() ) << "..." << std::endl; d_builder->d_addedLemmas = 0; - d_builder->buildModel( d_model, d_builder->optBuildAtFullModel() ); + d_builder->buildModel( d_model, needsFullModel || d_builder->optBuildAtFullModel() ); //we are done if model building was unsuccessful if( d_builder->d_addedLemmas>0 ){ success = false; @@ -349,7 +353,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() && !d_builder->optBuildAtFullModel() ){ + }else if( quant_e==QEFFORT_MODEL && needsModel && options::produceModels() && !needsFullModel && !d_builder->optBuildAtFullModel() ){ Trace("quant-engine-debug") << "Build completed model..." << std::endl; d_builder->buildModel( d_model, true ); } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 75b55ca4a..f56cd0d19 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -55,6 +55,8 @@ public: virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; } /* whether this module needs a model built */ virtual bool needsModel( Theory::Effort e ) { return false; } + /* whether this module needs a model built */ + virtual bool needsFullModel( Theory::Effort e ) { return false; } /* reset at a round */ virtual void reset_round( Theory::Effort e ){} /* Call during quantifier engine's check */ diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 7e1129e7b..b67140db8 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -681,7 +681,10 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) continue; } TypeNode t = TypeSet::getType(it); - TypeNode tb = t.getBaseType(); + if(t.isTuple() || t.isRecord()) { + t = NodeManager::currentNM()->getDatatypeForTupleRecord(t); + } + TypeNode tb = t.getBaseType(); if (!assignOne) { set* repSet = typeRepSet.getSet(tb); if (repSet != NULL && !repSet->empty()) { diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp index 179bb1a23..066ba6103 100644 --- a/src/util/sort_inference.cpp +++ b/src/util/sort_inference.cpp @@ -23,6 +23,7 @@ #include "theory/uf/options.h" #include "smt/options.h" #include "theory/rewriter.h" +#include "theory/quantifiers/options.h" using namespace CVC4; using namespace std; @@ -333,7 +334,7 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound ){ for( size_t i=0; i=1; } if( processChild ){ children.push_back( n[i] ); @@ -531,7 +532,7 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){ for( size_t i=0; i=1; + processChild = options::userPatternsQuant()==theory::quantifiers::USER_PAT_MODE_IGNORE ? i==1 : i>=1; } if( processChild ){ children.push_back( simplify( n[i], var_bound ) ); diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am index 804987da2..a1232196e 100644 --- a/test/regress/regress0/arrays/Makefile.am +++ b/test/regress/regress0/arrays/Makefile.am @@ -40,7 +40,6 @@ TESTS = \ swap_t1_np_nf_ai_00005_007.cvc.smt \ x2.smt \ x3.smt \ - parsing_ringer.cvc \ bug272.smt \ bug272.minimized.smt \ constarr.smt2 \ @@ -61,6 +60,8 @@ EXTRA_DIST = $(TESTS) # and make sure to distribute it #EXTRA_DIST += \ # error.cvc +# disabled for now (problem is related to records in model): +# parsing_ringer.cvc # synonyms for "check" .PHONY: regress regress0 test diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index e3e514496..ca3907b0b 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -35,12 +35,11 @@ TESTS = \ fc-unsat-pent.smt2 \ fc-pigeonhole19.smt2 \ Hoare-z3.931718.smt \ - bug0909.smt2 + bug0909.smt2 \ + lst-no-self-rev-exp.smt2 EXTRA_DIST = $(TESTS) -# disabled for now : -# lst-no-self-rev-exp.smt2 #if CVC4_BUILD_PROFILE_COMPETITION #else diff --git a/test/regress/regress0/fmf/lst-no-self-rev-exp.smt2 b/test/regress/regress0/fmf/lst-no-self-rev-exp.smt2 index e86d8c60e..5e1f3de30 100644 --- a/test/regress/regress0/fmf/lst-no-self-rev-exp.smt2 +++ b/test/regress/regress0/fmf/lst-no-self-rev-exp.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find --uf-ss-fair +; COMMAND-LINE: --finite-model-find --dt-rewrite-error-sel ; EXPECT: sat (set-logic ALL_SUPPORTED) (declare-datatypes () ((Nat (succ (pred Nat)) (zero)) (Lst (cons (hd Nat) (tl Lst)) (nil)))) @@ -9,6 +9,10 @@ (declare-sort I_app 0) (declare-sort I_rev 0) +(declare-fun a () I_app) +(declare-fun b () I_app) +(assert (not (= a b))) + (declare-fun app_0_3 (I_app) Lst) (declare-fun app_1_4 (I_app) Lst) (declare-fun rev_0_5 (I_rev) Lst) -- 2.30.2