diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-23 11:33:09 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-23 11:33:09 -0600 |
commit | ad3036f0bcaf634489b7e745dcf87bd2102d92aa (patch) | |
tree | faaa7ce5f9f5a8ab8ead7f2de16c81a7347c63b8 /src/theory/quantifiers | |
parent | 2150eb22aaff94f9d0d9f0ee0854ea44675fd854 (diff) |
Fix term database for non-equal, congruent terms in master equality engine. Disable ITE terms in quant conflict find.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/full_model_check.cpp | 61 | ||||
-rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 18 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 53 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 18 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 1 |
6 files changed, 76 insertions, 79 deletions
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index ff0da13e1..e44a322b5 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -411,6 +411,11 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ Node r = fm->getUsedRepresentative(n); Trace("fmc-model-debug") << n << " -> " << r << std::endl; //AlwaysAssert( fm->areEqual( fm->d_uf_terms[op][i], r ) ); + }else{ + if( Trace.isOn("fmc-model-debug") ){ + Node r = fm->getUsedRepresentative(n); + Trace("fmc-model-debug") << "[redundant] " << n << " -> " << r << std::endl; + } } } Trace("fmc-model-debug") << std::endl; @@ -614,7 +619,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, //consider all entries going to non-true for (unsigned i=0; i<d_quant_models[f].d_cond.size(); i++) { - if( d_quant_models[f].d_value[i]!=d_true) { + if( d_quant_models[f].d_value[i]!=d_true ) { Trace("fmc-inst") << "Instantiate based on " << d_quant_models[f].d_cond[i] << "..." << std::endl; bool hasStar = false; std::vector< Node > inst; @@ -684,7 +689,11 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, } }else{ Trace("fmc-debug-inst") << "** Instantiation was duplicate." << std::endl; - //this can happen if evaluation is unknown + //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 ); //might try it next effort level d_star_insts[f].push_back(i); } @@ -780,11 +789,11 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No for( int i=0; i<riter.getNumTerms(); i++ ){ Node rr = riter.getTerm( i ); Node r = rr; - if( r.getType().isSort() ){ - r = fm->getUsedRepresentative( r ); - }else{ - r = fm->getCurrentModelValue( r ); - } + //if( r.getType().isSort() ){ + r = fm->getUsedRepresentative( r ); + //}else{ + // r = fm->getCurrentModelValue( r ); + //} debugPrint("fmc-exh-debug", r); Trace("fmc-exh-debug") << " (term : " << rr << ")"; ev_inst.push_back( r ); @@ -846,38 +855,12 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n d.addEntry(fm, mkCondDefault(fm, f), Node::null()); } else if( n.getType().isArray() ){ - //make the definition - bool success = false; - /* - Node r = fm->getRepresentative(n); - Trace("fmc-debug") << "Representative for array is " << r << std::endl; - while( r.getKind() == kind::STORE ){ - Node i = fm->getUsedRepresentative( r[1] ); - Node e = fm->getUsedRepresentative( r[2] ); - d.addEntry(fm, mkArrayCond(i), e ); - r = fm->getRepresentative( r[0] ); - } - Node defC = mkArrayCond(fm->getStar(n.getType().getArrayIndexType())); - bool success = false; - Node odefaultValue; - if( r.getKind() == kind::STORE_ALL ){ - ArrayStoreAll storeAll = r.getConst<ArrayStoreAll>(); - odefaultValue = Node::fromExpr(storeAll.getExpr()); - Node defaultValue = fm->getUsedRepresentative( odefaultValue, true ); - if( !defaultValue.isNull() ){ - d.addEntry(fm, defC, defaultValue); - success = true; - } - } - */ - if( !success ){ - //Trace("fmc-warn") << "WARNING : ARRAYS : Can't process base array " << r << std::endl; - //Trace("fmc-warn") << " Default value was : " << odefaultValue << std::endl; - //Trace("fmc-debug") << "Can't process base array " << r << std::endl; - //can't process this array - d.reset(); - d.addEntry(fm, mkCondDefault(fm, f), Node::null()); - } + //Trace("fmc-warn") << "WARNING : ARRAYS : Can't process base array " << r << std::endl; + //Trace("fmc-warn") << " Default value was : " << odefaultValue << std::endl; + //Trace("fmc-debug") << "Can't process base array " << r << std::endl; + //can't process this array + d.reset(); + d.addEntry(fm, mkCondDefault(fm, f), Node::null()); } else if( n.getNumChildren()==0 ){ Node r = n; diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 95b674cca..a698b33e1 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -50,8 +50,8 @@ bool QModelBuilder::optUseModel() { void QModelBuilder::debugModel( FirstOrderModel* fm ){ //debug the model: cycle through all instantiations for all quantifiers, report ones that are not true - if( Trace.isOn("quant-model-warn") ){ - Trace("quant-model-warn") << "Testing quantifier instantiations..." << std::endl; + if( Trace.isOn("quant-check-model") ){ + Trace("quant-check-model") << "Testing quantifier instantiations..." << std::endl; int tests = 0; int bad = 0; for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ @@ -71,20 +71,20 @@ void QModelBuilder::debugModel( FirstOrderModel* fm ){ Node n = d_qe->getInstantiation( f, vars, terms ); Node val = fm->getValue( n ); if( val!=fm->d_true ){ - Trace("quant-model-warn") << "******* Instantiation " << n << " for " << std::endl; - Trace("quant-model-warn") << " " << f << std::endl; - Trace("quant-model-warn") << " Evaluates to " << val << std::endl; + Trace("quant-check-model") << "******* Instantiation " << n << " for " << std::endl; + Trace("quant-check-model") << " " << f << std::endl; + Trace("quant-check-model") << " Evaluates to " << val << std::endl; bad++; } riter.increment(); } - Trace("quant-model-warn") << "Tested " << tests << " instantiations"; + Trace("quant-check-model") << "Tested " << tests << " instantiations"; if( bad>0 ){ - Trace("quant-model-warn") << ", " << bad << " failed" << std::endl; + Trace("quant-check-model") << ", " << bad << " failed" << std::endl; } - Trace("quant-model-warn") << "." << std::endl; + Trace("quant-check-model") << "." << std::endl; }else{ - Trace("quant-model-warn") << "Warning: Could not test quantifier " << f << std::endl; + Trace("quant-check-model") << "Warning: Could not test quantifier " << f << std::endl; } } } diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index a890276f7..5cff55d21 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -801,6 +801,7 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ) if( isVar ){ Assert( qi->d_var_num.find( n )!=qi->d_var_num.end() ); if( n.getKind()==ITE ){ + /* d_type = typ_ite_var; d_type_not = false; d_n = n; @@ -817,8 +818,9 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ) } } }else{ +*/ d_type = typ_invalid; - } + //} }else{ d_type = isHandledUfTerm( n ) ? typ_var : typ_tsym; d_qni_var_num[0] = qi->getVarNum( n ); diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 3c155c421..ff55c5c9b 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1739,31 +1739,29 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v //check if it contains a quantifier as a subterm //if so, we will write this node if( containsQuantifiers( n ) ){ - if( n.getType().isBoolean() ){ - if( n.getKind()==kind::ITE || n.getKind()==kind::IFF || n.getKind()==kind::XOR || n.getKind()==kind::IMPLIES ){ - if( options::preSkolemQuantAgg() ){ - Node nn; - //must remove structure - if( n.getKind()==kind::ITE ){ - nn = NodeManager::currentNM()->mkNode( kind::AND, - NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ), - NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) ); - }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){ - nn = NodeManager::currentNM()->mkNode( kind::AND, - NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ), - NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) ); - }else if( n.getKind()==kind::IMPLIES ){ - nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ); - } - return preSkolemizeQuantifiers( nn, polarity, fvTypes, fvs ); - } - }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){ - vector< Node > children; - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvTypes, fvs ) ); + if( ( n.getKind()==kind::ITE && n.getType().isBoolean() ) || n.getKind()==kind::IFF ){ + if( options::preSkolemQuantAgg() ){ + Node nn; + //must remove structure + if( n.getKind()==kind::ITE ){ + nn = NodeManager::currentNM()->mkNode( kind::AND, + NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ), + NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) ); + }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){ + nn = NodeManager::currentNM()->mkNode( kind::AND, + NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ), + NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) ); + }else if( n.getKind()==kind::IMPLIES ){ + nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ); } - return NodeManager::currentNM()->mkNode( n.getKind(), children ); + return preSkolemizeQuantifiers( nn, polarity, fvTypes, fvs ); + } + }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){ + vector< Node > children; + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvTypes, fvs ) ); } + return NodeManager::currentNM()->mkNode( n.getKind(), children ); } } } @@ -1771,15 +1769,20 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v } Node QuantifiersRewriter::preprocess( Node n, bool isInst ) { + Node prev = n; if( options::preSkolemQuant() ){ if( !isInst || !options::preSkolemQuantNested() ){ - //apply pre-skolemization to existential quantifiers Trace("quantifiers-preprocess-debug") << "Pre-skolemize " << n << "..." << std::endl; + //apply pre-skolemization to existential quantifiers std::vector< TypeNode > fvTypes; std::vector< TNode > fvs; - n = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( n, true, fvTypes, fvs ); + n = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs ); } } + if( n!=prev ){ + Trace("quantifiers-preprocess") << "Preprocess " << prev<< std::endl; + Trace("quantifiers-preprocess") << "..returned " << n << std::endl; + } return n; } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 3e5e30bd7..cb23b8bb7 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -59,16 +59,20 @@ TNode TermArgTrie::existsTerm( std::vector< TNode >& reps, int argIndex ) { } bool TermArgTrie::addTerm( TNode n, std::vector< TNode >& reps, int argIndex ){ + return addOrGetTerm( n, reps, argIndex )==n; +} + +TNode TermArgTrie::addOrGetTerm( TNode n, std::vector< TNode >& reps, int argIndex ) { if( argIndex==(int)reps.size() ){ if( d_data.empty() ){ //store n in d_data (this should be interpretted as the "data" and not as a reference to a child) d_data[n].clear(); - return true; + return n; }else{ - return false; + return d_data.begin()->first; } }else{ - return d_data[reps[argIndex]].addTerm( n, reps, argIndex+1 ); + return d_data[reps[argIndex]].addOrGetTerm( n, reps, argIndex+1 ); } } @@ -502,9 +506,12 @@ void TermDb::reset( Theory::Effort effort ){ Trace("term-db-debug") << d_arg_reps[n] << " "; } Trace("term-db-debug") << std::endl; + if( ee->hasTerm( n ) ){ + Trace("term-db-debug") << " and value : " << ee->getRepresentative( n ) << std::endl; + } } - - if( !d_func_map_trie[ it->first ].addTerm( n, d_arg_reps[n] ) ){ + Node at = d_func_map_trie[ it->first ].addOrGetTerm( n, d_arg_reps[n] ); + if( at!=n && ee->areEqual( at, n ) ){ NoMatchAttribute nma; n.setAttribute(nma,true); Trace("term-db-debug") << n << " is redundant." << std::endl; @@ -514,6 +521,7 @@ void TermDb::reset( Theory::Effort effort ){ d_op_nonred_count[ it->first ]++; } }else{ + Trace("term-db-debug") << n << " is already redundant." << std::endl; congruentCount++; alreadyCongruentCount++; } diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index c770f0e6f..5560098c9 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -121,6 +121,7 @@ public: std::map< TNode, TermArgTrie > d_data; public: TNode existsTerm( std::vector< TNode >& reps, int argIndex = 0 ); + TNode addOrGetTerm( TNode n, std::vector< TNode >& reps, int argIndex = 0 ); bool addTerm( TNode n, std::vector< TNode >& reps, int argIndex = 0 ); void debugPrint( const char * c, Node n, unsigned depth = 0 ); void clear() { d_data.clear(); } |