diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-08 12:10:41 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-08 12:10:41 -0600 |
commit | 346c85d145f6938ce7dce74e7e7cb855d5a6025a (patch) | |
tree | fb9cc78736360756e2af81fc3457c4ed9929f32f /src/theory/quantifiers/quant_equality_engine.cpp | |
parent | b4c7be882b88c6741212ecd9c6be4e91fec76087 (diff) |
Extend synthesis solver to handle single invocation with additional universal quantification. Refactor query/check-sat to call one internal function in SmtEngine. Make check-synth its own command. Minor work on quant ee.
Diffstat (limited to 'src/theory/quantifiers/quant_equality_engine.cpp')
-rw-r--r-- | src/theory/quantifiers/quant_equality_engine.cpp | 139 |
1 files changed, 107 insertions, 32 deletions
diff --git a/src/theory/quantifiers/quant_equality_engine.cpp b/src/theory/quantifiers/quant_equality_engine.cpp index 54a931196..06ca6f98c 100644 --- a/src/theory/quantifiers/quant_equality_engine.cpp +++ b/src/theory/quantifiers/quant_equality_engine.cpp @@ -32,6 +32,7 @@ d_conflict(c, false), d_quant_red(c), d_quant_unproc(c){ d_uequalityEngine.addFunctionKind( kind::APPLY_UF ); + d_intType = NodeManager::currentNM()->integerType(); } void QuantEqualityEngine::conflict(TNode t1, TNode t2) { @@ -86,56 +87,130 @@ void QuantEqualityEngine::registerQuantifier( Node q ) { void QuantEqualityEngine::assertNode( Node n ) { Assert( n.getKind()==FORALL ); Trace("qee-debug") << "QEE assert : " << n << std::endl; - Node lit = n[1].getKind()==NOT ? n[1][0] : n[1]; - bool pol = n[1].getKind()!=NOT; - if( lit.getKind()==APPLY_UF || lit.getKind()==EQUAL ){ - lit = getTermDatabase()->getCanonicalTerm( lit ); - Trace("qee-debug") << "Canonical : " << lit << ", pol = " << pol << std::endl; - Node t1 = lit.getKind()==APPLY_UF ? lit : lit[0]; + if( !d_conflict ){ + Node lit = n[1].getKind()==NOT ? n[1][0] : n[1]; + bool pol = n[1].getKind()!=NOT; + bool success = true; + Node t1; Node t2; - if( lit.getKind()==APPLY_UF ){ - t2 = pol ? getTermDatabase()->d_true : getTermDatabase()->d_false; - pol = true; + if( lit.getKind()==APPLY_UF || lit.getKind()==EQUAL || lit.getKind()==IFF ){ + lit = getTermDatabase()->getCanonicalTerm( lit ); + Trace("qee-debug") << "Canonical : " << lit << ", pol = " << pol << std::endl; + if( lit.getKind()==APPLY_UF ){ + t1 = getFunctionAppForPredicateApp( lit ); + t2 = pol ? getTermDatabase()->d_one : getTermDatabase()->d_zero; + pol = true; + lit = NodeManager::currentNM()->mkNode( EQUAL, t1, t2 ); + }else if( lit.getKind()==EQUAL ){ + t1 = lit[0]; + t2 = lit[1]; + }else if( lit.getKind()==IFF ){ + if( lit[0].getKind()==NOT ){ + t1 = lit[0][0]; + pol = !pol; + }else{ + t1 = lit[0]; + } + if( lit[1].getKind()==NOT ){ + t2 = lit[1][0]; + pol = !pol; + }else{ + t2 = lit[1]; + } + if( t1.getKind()==APPLY_UF && t2.getKind()==APPLY_UF ){ + t1 = getFunctionAppForPredicateApp( t1 ); + t2 = getFunctionAppForPredicateApp( t2 ); + lit = NodeManager::currentNM()->mkNode( EQUAL, t1, t2 ); + }else{ + success = false; + } + } }else{ - t2 = lit[1]; - } - bool alreadyHolds = false; - if( pol && areUnivEqual( t1, t2 ) ){ - alreadyHolds = true; - }else if( !pol && areUnivDisequal( t1, t2 ) ){ - alreadyHolds = true; + success = false; } + if( success ){ + bool alreadyHolds = false; + if( pol && areUnivEqualInternal( t1, t2 ) ){ + alreadyHolds = true; + }else if( !pol && areUnivDisequalInternal( t1, t2 ) ){ + alreadyHolds = true; + } - if( alreadyHolds ){ - d_quant_red.push_back( n ); - Trace("qee-debug") << "...add to redundant" << std::endl; - }else{ - Trace("qee-debug") << "...assert" << std::endl; - Trace("qee-assert") << "QEE : assert : " << lit << ", pol = " << pol << ", kind = " << lit.getKind() << std::endl; - if( lit.getKind()==APPLY_UF ){ - d_uequalityEngine.assertPredicate(lit, pol, n); + if( alreadyHolds ){ + d_quant_red.push_back( n ); + Trace("qee-debug") << "...add to redundant" << std::endl; }else{ - d_uequalityEngine.assertEquality(lit, pol, n); + Trace("qee-debug") << "...assert" << std::endl; + Trace("qee-assert") << "QEE : assert : " << lit << ", pol = " << pol << ", kind = " << lit.getKind() << std::endl; + if( lit.getKind()==APPLY_UF ){ + d_uequalityEngine.assertPredicate(lit, pol, n); + }else{ + d_uequalityEngine.assertEquality(lit, pol, n); + } } + }else{ + d_quant_unproc[n] = true; + Trace("qee-debug") << "...add to unprocessed (" << lit.getKind() << ")" << std::endl; } - }else{ - d_quant_unproc[n] = true; - Trace("qee-debug") << "...add to unprocessed (" << lit.getKind() << ")" << std::endl; } } -bool QuantEqualityEngine::areUnivDisequal( TNode n1, TNode n2 ) { +bool QuantEqualityEngine::areUnivDisequalInternal( TNode n1, TNode n2 ) { return n1!=n2 && d_uequalityEngine.hasTerm( n1 ) && d_uequalityEngine.hasTerm( n2 ) && d_uequalityEngine.areDisequal( n1, n2, false ); } -bool QuantEqualityEngine::areUnivEqual( TNode n1, TNode n2 ) { +bool QuantEqualityEngine::areUnivEqualInternal( TNode n1, TNode n2 ) { return n1==n2 || ( d_uequalityEngine.hasTerm( n1 ) && d_uequalityEngine.hasTerm( n2 ) && d_uequalityEngine.areEqual( n1, n2 ) ); } -TNode QuantEqualityEngine::getUnivRepresentative( TNode n ) { +TNode QuantEqualityEngine::getUnivRepresentativeInternal( TNode n ) { if( d_uequalityEngine.hasTerm( n ) ){ return d_uequalityEngine.getRepresentative( n ); }else{ return n; } -}
\ No newline at end of file +} +bool QuantEqualityEngine::areUnivDisequal( TNode n1, TNode n2 ) { + //TODO: must convert to internal representation + return areUnivDisequalInternal( n1, n2 ); +} + +bool QuantEqualityEngine::areUnivEqual( TNode n1, TNode n2 ) { + //TODO: must convert to internal representation + return areUnivEqualInternal( n1, n2 ); +} + +TNode QuantEqualityEngine::getUnivRepresentative( TNode n ) { + //TODO: must convert to internal representation + return getUnivRepresentativeInternal( n ); +} + +Node QuantEqualityEngine::getFunctionForPredicate( Node f ) { + std::map< Node, Node >::iterator it = d_pred_to_func.find( f ); + if( it==d_pred_to_func.end() ){ + std::vector< TypeNode > argTypes; + TypeNode tn = f.getType(); + for( unsigned i=0; i<(tn.getNumChildren()-1); i++ ){ + argTypes.push_back( tn[i] ); + } + TypeNode ftn = NodeManager::currentNM()->mkFunctionType( argTypes, d_intType ); + std::stringstream ss; + ss << "ee_" << f; + Node op = NodeManager::currentNM()->mkSkolem( ss.str(), ftn, "op created for internal ee" ); + d_pred_to_func[f] = op; + return op; + }else{ + return it->second; + } +} + +Node QuantEqualityEngine::getFunctionAppForPredicateApp( Node n ) { + Assert( n.getKind()==APPLY_UF ); + std::vector< Node > children; + children.push_back( getFunctionForPredicate( n.getOperator() ) ); + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + children.push_back( n[i] ); + } + return NodeManager::currentNM()->mkNode( APPLY_UF, children ); +} + |