summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/arrays/theory_arrays.cpp8
-rw-r--r--src/theory/quantifiers/full_model_check.cpp14
-rw-r--r--src/theory/strings/theory_strings.cpp11
-rw-r--r--src/theory/uf/theory_uf_strong_solver.cpp31
-rw-r--r--src/theory/uf/theory_uf_strong_solver.h2
5 files changed, 41 insertions, 25 deletions
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; i<arrays.size(); ++i) {
TNode nrep = d_equalityEngine.getRepresentative(arrays[i]);
d_mayEqualEqualityEngine.addTerm(nrep); // add the term in case it isn't there already
@@ -1143,14 +1143,14 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel )
defaultValuesSet.add(nrep.getType().getArrayConstituentType(), (*it).second);
}
}
- }
+ //}
// Loop through all array equivalence classes that need a representative computed
for (size_t i=0; i<arrays.size(); ++i) {
TNode n = arrays[i];
TNode nrep = d_equalityEngine.getRepresentative(n);
- if (fullModel) {
+ //if (fullModel) {
// Compute default value for this array - there is one default value for every mayEqual equivalence class
TNode mayRep = d_mayEqualEqualityEngine.getRepresentative(nrep);
it = d_defValues.find(mayRep);
@@ -1171,6 +1171,7 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel )
// Build the STORE_ALL term with the default value
rep = nm->mkConst(ArrayStoreAll(nrep.getType().toType(), rep.toExpr()));
+ /*
}
else {
std::hash_map<Node, Node, NodeHashFunction>::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<Node>& 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; i<it->second.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<lexp.size(); j++ ) { Trace("strings-ff-debug") << lexp[j] << std::endl; }
+ Trace("strings-ff-debug") << "Explanation for " << lcc << " is ";
+ for( unsigned j=0; j<lexp2.size(); j++ ) { Trace("strings-ff-debug") << lexp2[j] << std::endl; }
exp.insert( exp.end(), lexp.begin(), lexp.end() );
exp.insert( exp.end(), lexp2.begin(), lexp2.end() );
addToExplanation( lcurr, lcc, exp );
@@ -2755,6 +2759,7 @@ void TheoryStrings::sendInference( std::vector< Node >& exp, std::vector< Node >
for( unsigned i=0; i<exp_n.size(); i++ ){
Trace("strings-infer-debug") << " N:" << exp_n[i] << std::endl;
}
+ //Trace("strings-infer-debug") << "as lemma : " << asLemma << std::endl;
}
bool doSendLemma = ( asLemma || eq==d_false || eq.getKind()==kind::OR || options::stringInferAsLemmas() );
if( doSendLemma ){
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 977b9f4c1..1f18416c5 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -407,7 +407,7 @@ void StrongSolverTheoryUF::SortModel::Region::debugPrint( const char* c, bool in
StrongSolverTheoryUF::SortModel::SortModel( Node n, context::Context* c, context::UserContext* u, StrongSolverTheoryUF* thss ) : d_type( n.getType() ),
d_thss( thss ), d_regions_index( c, 0 ), d_regions_map( c ), d_split_score( c ), d_disequalities_index( c, 0 ),
d_reps( c, 0 ), d_conflict( c, false ), d_cardinality( c, 1 ), d_aloc_cardinality( u, 0 ),
- d_cardinality_assertions( c ), d_hasCard( c, false ), d_maxNegCard( c, 0 ), d_initialized( u, false ), d_lemma_cache( u ){
+ d_hasCard( c, false ), d_maxNegCard( c, 0 ), d_initialized( u, false ), d_lemma_cache( u ){
d_cardinality_term = n;
//if( d_type.isSort() ){
// TypeEnumerator te(tn);
@@ -723,11 +723,13 @@ Node StrongSolverTheoryUF::SortModel::getNextDecisionRequest(){
if( !d_hasCard || i<d_cardinality ){
Node cn = d_cardinality_literal[ i ];
Assert( !cn.isNull() );
- if( d_cardinality_assertions.find( cn )==d_cardinality_assertions.end() ){
+ bool value;
+ if( !d_thss->getTheory()->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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback