From b4c7be882b88c6741212ecd9c6be4e91fec76087 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 7 Mar 2016 12:39:50 -0600 Subject: Minor change to F-Length inference in strings. No internal tracking of cardinality assertions in uf. Change fullModel false array collectModelInfo to assign constants. --- src/theory/arrays/theory_arrays.cpp | 8 +++++--- src/theory/quantifiers/full_model_check.cpp | 14 +++++++------ src/theory/strings/theory_strings.cpp | 11 +++++++--- src/theory/uf/theory_uf_strong_solver.cpp | 31 +++++++++++++++++++---------- src/theory/uf/theory_uf_strong_solver.h | 2 -- 5 files changed, 41 insertions(+), 25 deletions(-) (limited to 'src') diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 8f1ba5fca..631785437 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -1133,7 +1133,7 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ) TypeSet defaultValuesSet; // Compute all default values already in use - if (fullModel) { + //if (fullModel) { for (size_t i=0; imkConst(ArrayStoreAll(nrep.getType().toType(), rep.toExpr())); + /* } else { std::hash_map::iterator it = d_skolemCache.find(n); @@ -1182,6 +1183,7 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ) rep = (*it).second; } } +*/ // For each read, require that the rep stores the right value vector& reads = selects[nrep]; diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index e44a322b5..98cd175fd 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -461,7 +461,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ } } if( !isStar && !ri.isConst() ){ - Trace("fmc-warn") << "Warning : model has non-constant argument in model " << ri << " (from " << c[i] << ")" << std::endl; + Trace("fmc-warn") << "Warning : model for " << op << " has non-constant argument in model " << ri << " (from " << c[i] << ")" << std::endl; Assert( false ); } entry_children.push_back(ri); @@ -469,7 +469,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children ); Node nv = fm->getUsedRepresentative( v ); if( !nv.isConst() ){ - Trace("fmc-warn") << "Warning : model has non-constant value in model " << nv << std::endl; + Trace("fmc-warn") << "Warning : model for " << op << " has non-constant value in model " << nv << std::endl; Assert( false ); } Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children ); @@ -690,10 +690,12 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, }else{ Trace("fmc-debug-inst") << "** Instantiation was duplicate." << std::endl; //this can happen if evaluation is unknown, or if we are generalizing a star that already has a value - if( !hasStar && d_quant_models[f].d_value[i]==d_false ){ - Trace("fmc-warn") << "**** FMC warning: inconsistent duplicate instantiation." << std::endl; - } - Assert( hasStar || d_quant_models[f].d_value[i]!=d_false ); + //if( !hasStar && d_quant_models[f].d_value[i]==d_false ){ + // Trace("fmc-warn") << "**** FMC warning: inconsistent duplicate instantiation." << std::endl; + //} + //this assertion can happen if two instantiations from this round are identical + // (0,1)->false (1,0)->false for forall xy. f( x, y ) = f( y, x ) + //Assert( hasStar || d_quant_models[f].d_value[i]!=d_false ); //might try it next effort level d_star_insts[f].push_back(i); } diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 9f474a3ca..634c1b130 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1417,8 +1417,9 @@ void TheoryStrings::checkFlatForms() { }else{ Node curr = d_flat_form[a][count]; Node curr_c = d_eqc_to_const[curr]; + Node ac = a[d_flat_form_index[a][count]]; std::vector< Node > lexp; - Node lcurr = getLength( curr, lexp ); + Node lcurr = getLength( ac, lexp ); for( unsigned i=1; isecond.size(); i++ ){ b = it->second[i]; if( std::find( inelig.begin(), inelig.end(), b )==inelig.end() ){ @@ -1438,7 +1439,6 @@ void TheoryStrings::checkFlatForms() { }else{ Node cc = d_flat_form[b][count]; if( cc!=curr ){ - Node ac = a[d_flat_form_index[a][count]]; Node bc = b[d_flat_form_index[b][count]]; inelig.push_back( b ); Assert( !areEqual( curr, cc ) ); @@ -1463,10 +1463,14 @@ void TheoryStrings::checkFlatForms() { }else{ //if lengths are the same, apply LengthEq std::vector< Node > lexp2; - Node lcc = getLength( cc, lexp2 ); + Node lcc = getLength( bc, lexp2 ); if( areEqual( lcurr, lcc ) ){ Trace("strings-ff-debug") << "Infer " << ac << " == " << bc << " since " << lcurr << " == " << lcc << std::endl; //exp_n.push_back( getLength( curr, true ).eqNode( getLength( cc, true ) ) ); + Trace("strings-ff-debug") << "Explanation for " << lcurr << " is "; + for( unsigned j=0; j& exp, std::vector< Node > for( unsigned i=0; igetTheory()->d_valuation.hasSatValue( cn, value ) ){ Trace("uf-ss-dec") << "UFSS : Get next decision " << d_type << " " << i << std::endl; return cn; }else{ - Trace("uf-ss-dec-debug") << " dec : " << cn << " already asserted " << d_cardinality_assertions[cn].get() << std::endl; + Trace("uf-ss-dec-debug") << " dec : " << cn << " already asserted " << value << std::endl; + Assert( !value ); } } } @@ -846,7 +848,6 @@ void StrongSolverTheoryUF::SortModel::assertCardinality( OutputChannel* out, int Trace("uf-ss-assert") << d_thss->getTheory()->d_valuation.getAssertionLevel() << std::endl; Assert( c>0 ); Node cl = getCardinalityLiteral( c ); - d_cardinality_assertions[ cl ] = val; if( val ){ bool doCheckRegions = !d_hasCard; bool prevHasCard = d_hasCard; @@ -890,8 +891,9 @@ void StrongSolverTheoryUF::SortModel::assertCardinality( OutputChannel* out, int bool needsCard = true; for( std::map< int, Node >::iterator it = d_cardinality_literal.begin(); it!=d_cardinality_literal.end(); ++it ){ if( it->first<=d_aloc_cardinality.get() ){ - if( d_cardinality_assertions.find( it->second )==d_cardinality_assertions.end() ){ - Debug("fmf-card-debug") << "..does not need allocate because of " << it->second << std::endl; + bool value; + if( !d_thss->getTheory()->d_valuation.hasSatValue( it->second, value ) ){ + Debug("fmf-card-debug") << "..does not need allocate because we are waiting for " << it->second << std::endl; needsCard = false; break; } @@ -1028,14 +1030,21 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){ //allocate the lowest such that it is not asserted Node cl; + bool increment; do { + increment = false; d_aloc_cardinality = d_aloc_cardinality + 1; cl = getCardinalityLiteral( d_aloc_cardinality ); - }while( d_cardinality_assertions.find( cl )!=d_cardinality_assertions.end() && !d_cardinality_assertions[cl] ); - //if one is already asserted postively, abort - if( d_cardinality_assertions.find( cl )!=d_cardinality_assertions.end() ){ - return; - } + bool value; + if( d_thss->getTheory()->d_valuation.hasSatValue( cl, value ) ){ + if( value ){ + //if one is already asserted postively, abort + return; + }else{ + increment = true; + } + } + }while( increment ); //check for abort case if( options::ufssAbortCardinality()==d_aloc_cardinality ){ diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index db4c50423..3dfaed663 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -232,8 +232,6 @@ public: std::map< int, Node > d_cardinality_literal; /** cardinality lemmas */ std::map< int, Node > d_cardinality_lemma; - /** cardinality assertions (indexed by cardinality literals ) */ - NodeBoolMap d_cardinality_assertions; /** whether a positive cardinality constraint has been asserted */ context::CDO< bool > d_hasCard; /** clique lemmas that have been asserted */ -- cgit v1.2.3