From 1f4b954a2cc7667a56a3007fa75c125fba93ed23 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 2 Mar 2017 14:45:21 -0600 Subject: Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions. --- src/theory/quantifiers/alpha_equivalence.cpp | 2 +- src/theory/quantifiers/bounded_integers.cpp | 2 +- src/theory/quantifiers/candidate_generator.cpp | 2 +- src/theory/quantifiers/ce_guided_instantiation.cpp | 14 +++--- src/theory/quantifiers/ce_guided_single_inv.cpp | 14 +++--- .../quantifiers/ce_guided_single_inv_sol.cpp | 26 +++++----- src/theory/quantifiers/ceg_instantiator.cpp | 18 ++++++- src/theory/quantifiers/first_order_model.cpp | 2 +- src/theory/quantifiers/fun_def_process.cpp | 10 ++-- src/theory/quantifiers/inst_match_generator.cpp | 20 ++++---- src/theory/quantifiers/inst_propagator.cpp | 11 +++-- src/theory/quantifiers/inst_strategy_cbqi.cpp | 2 +- .../quantifiers/inst_strategy_e_matching.cpp | 4 +- src/theory/quantifiers/macros.cpp | 4 +- src/theory/quantifiers/model_builder.cpp | 2 +- src/theory/quantifiers/quant_conflict_find.cpp | 17 +++---- src/theory/quantifiers/quant_equality_engine.cpp | 40 +++++++-------- src/theory/quantifiers/quant_util.cpp | 4 +- src/theory/quantifiers/quantifiers_rewriter.cpp | 35 ++++++------- src/theory/quantifiers/rewrite_engine.cpp | 17 +------ src/theory/quantifiers/term_database.cpp | 57 +++++++++++++--------- src/theory/quantifiers/term_database.h | 2 + src/theory/quantifiers/trigger.cpp | 12 ++--- 23 files changed, 164 insertions(+), 153 deletions(-) (limited to 'src/theory/quantifiers') diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index a00d6d8a1..a5fd34c64 100644 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -72,7 +72,7 @@ Node AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersE Trace("alpha-eq") << "Alpha equivalent : " << std::endl; Trace("alpha-eq") << " " << q << std::endl; Trace("alpha-eq") << " " << aen->d_quant << std::endl; - lem = q.iffNode( aen->d_quant ); + lem = q.eqNode( aen->d_quant ); }else{ //do not reduce annotated quantified formulas based on alpha equivalence } diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index c488e8c23..37fbff03a 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -138,7 +138,7 @@ bool BoundedIntegers::IntRangeModel::proxyCurrentRange() { if( d_ranges_proxied.find( curr )==d_ranges_proxied.end() ){ d_ranges_proxied[curr] = true; Assert( d_range_literal.find( curr )!=d_range_literal.end() ); - Node lem = NodeManager::currentNM()->mkNode( IFF, d_range_literal[curr].negate(), + Node lem = NodeManager::currentNM()->mkNode( EQUAL, d_range_literal[curr].negate(), NodeManager::currentNM()->mkNode( LEQ, d_range, NodeManager::currentNM()->mkConst( Rational(curr) ) ) ); Trace("bound-int-lemma") << "*** bound int : proxy lemma : " << lem << std::endl; d_bi->getQuantifiersEngine()->addLemma( lem ); diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 8e8f34cac..7c9a6196f 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -227,7 +227,7 @@ Node CandidateGeneratorQELitEq::getNextCandidate(){ CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ) : CandidateGenerator( qe ), d_match_pattern( mpat ){ - Assert( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ); + Assert( d_match_pattern.getKind()==EQUAL ); d_match_pattern_type = d_match_pattern[0].getType(); } diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index f4b63f929..9903f14aa 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -710,13 +710,13 @@ Node CegInstantiation::getEagerUnfold( Node n, std::map< Node, Node >& visited ) } for( unsigned j=1; jmkConst(BitVector(1u, 1u)); - subs.push_back( nc.eqNode( c ) ); - }else{ - subs.push_back( nc ); - } + //if( var_list[j-1].getType().isBoolean() ){ + // //TODO: remove this case when boolean term conversion is eliminated + // Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u)); + // subs.push_back( nc.eqNode( c ) ); + //}else{ + subs.push_back( nc ); + //} Assert( subs[j-1].getType()==var_list[j-1].getType() ); } Assert( vars.size()==subs.size() ); diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 44ac135a7..92d62a177 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -758,13 +758,13 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& Assert( d_single_inv_arg_sk.size()==varList.getNumChildren() ); for( unsigned i=0; imkConst(BitVector(1u, 1u)); - vars.push_back( d_single_inv_arg_sk[i].eqNode( c ) ); - }else{ - vars.push_back( d_single_inv_arg_sk[i] ); - } + //if( varList[i].getType().isBoolean() ){ + // //TODO force boolean term conversion mode + // Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u)); + // vars.push_back( d_single_inv_arg_sk[i].eqNode( c ) ); + //}else{ + vars.push_back( d_single_inv_arg_sk[i] ); + //} d_sol->d_varList.push_back( varList[i] ); } Trace("csi-sol") << std::endl; diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp index 5cc46d163..d93898a1e 100644 --- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp @@ -215,7 +215,7 @@ Node CegConjectureSingleInvSol::flattenITEs( Node n, bool rec ) { if( n0.getKind()==ITE ){ n0 = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n0, n1 ), NodeManager::currentNM()->mkNode( AND, n0.negate(), n2 ) ); - }else if( n0.getKind()==IFF ){ + }else if( n0.getKind()==EQUAL ){ n0 = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n0, n1 ), NodeManager::currentNM()->mkNode( AND, n0.negate(), n1.negate() ) ); }else{ @@ -271,7 +271,7 @@ bool CegConjectureSingleInvSol::getAssign( bool pol, Node n, std::map< Node, boo } }else if( n.getKind()==NOT ){ return getAssign( !pol, n[0], assign, new_assign, vars, new_vars, new_subs ); - }else if( pol && ( n.getKind()==IFF || n.getKind()==EQUAL ) ){ + }else if( pol && n.getKind()==EQUAL ){ getAssignEquality( n, vars, new_vars, new_subs ); } } @@ -279,7 +279,7 @@ bool CegConjectureSingleInvSol::getAssign( bool pol, Node n, std::map< Node, boo } bool CegConjectureSingleInvSol::getAssignEquality( Node eq, std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs ) { - Assert( eq.getKind()==IFF || eq.getKind()==EQUAL ); + Assert( eq.getKind()==EQUAL ); //try to find valid argument for( unsigned r=0; r<2; r++ ){ if( std::find( d_varList.begin(), d_varList.end(), eq[r] )!=d_varList.end() ){ @@ -492,7 +492,7 @@ Node CegConjectureSingleInvSol::simplifySolutionNode( Node sol, TypeNode stn, st std::map< Node, bool >::iterator it = atoms.find( atom ); if( it==atoms.end() ){ atoms[atom] = pol; - if( status==0 && ( atom.getKind()==IFF || atom.getKind()==EQUAL ) ){ + if( status==0 && atom.getKind()==EQUAL ){ if( pol==( sol.getKind()==AND ) ){ Trace("csi-simp") << " ...equality." << std::endl; if( getAssignEquality( atom, vars, new_vars, new_subs ) ){ @@ -567,7 +567,7 @@ Node CegConjectureSingleInvSol::simplifySolutionNode( Node sol, TypeNode stn, st bool red = false; Node atom = children[i].getKind()==NOT ? children[i][0] : children[i]; bool pol = children[i].getKind()!=NOT; - if( status==0 && ( atom.getKind()==IFF || atom.getKind()==EQUAL ) ){ + if( status==0 && atom.getKind()==EQUAL ){ if( pol!=( sol.getKind()==AND ) ){ std::vector< Node > tmp_vars; std::vector< Node > tmp_subs; @@ -848,15 +848,19 @@ int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, in Node new_t; do{ new_t = Node::null(); - if( curr.getKind()==EQUAL && ( curr[0].getType().isInteger() || curr[0].getType().isReal() ) ){ - new_t = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, curr[0], curr[1] ), - NodeManager::currentNM()->mkNode( LEQ, curr[1], curr[0] ) ); + if( curr.getKind()==EQUAL ){ + if( curr[0].getType().isInteger() || curr[0].getType().isReal() ){ + new_t = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, curr[0], curr[1] ), + NodeManager::currentNM()->mkNode( LEQ, curr[1], curr[0] ) ); + }else if( curr[0].getType().isBoolean() ){ + new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, curr[0], curr[1] ), + NodeManager::currentNM()->mkNode( AND, curr[0].negate(), curr[1].negate() ) ); + }else{ + new_t = NodeManager::currentNM()->mkNode( NOT, NodeManager::currentNM()->mkNode( NOT, curr ) ); + } }else if( curr.getKind()==ITE ){ new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, curr[0], curr[1] ), NodeManager::currentNM()->mkNode( AND, curr[0].negate(), curr[2] ) ); - }else if( curr.getKind()==IFF ){ - new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, curr[0], curr[1] ), - NodeManager::currentNM()->mkNode( AND, curr[0].negate(), curr[1].negate() ) ); }else if( curr.getKind()==OR || curr.getKind()==AND ){ new_t = TermDb::simpleNegate( curr ).negate(); }else if( curr.getKind()==NOT ){ diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 61a20ad42..3dacfca3a 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -753,6 +753,12 @@ void CegInstantiator::processAssertions() { Trace("cbqi-proc") << "......add substitution : " << itae2->first << " -> " << itae2->second << std::endl; } } + }else if( atom.getKind()==BOOLEAN_TERM_VARIABLE ){ + if( std::find( d_aux_vars.begin(), d_aux_vars.end(), atom )!=d_aux_vars.end() ){ + Node val = NodeManager::currentNM()->mkConst( lit.getKind()!=NOT ); + aux_subs[ atom ] = val; + Trace("cbqi-proc") << "......add substitution : " << atom << " -> " << val << std::endl; + } } } } @@ -884,7 +890,7 @@ void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited ) d_is_nested_quant = true; }else if( visited.find( n )==visited.end() ){ visited[n] = true; - if( TermDb::isBoolConnective( n.getKind() ) ){ + if( TermDb::isBoolConnectiveTerm( n ) ){ for( unsigned i=0; i& lems, st //remove ITEs IteSkolemMap iteSkolemMap; - d_qe->getTheoryEngine()->getIteRemover()->run(lems, iteSkolemMap); + d_qe->getTheoryEngine()->getTermFormulaRemover()->run(lems, iteSkolemMap); //Assert( d_aux_vars.empty() ); d_aux_vars.clear(); d_aux_eq.clear(); @@ -965,6 +971,14 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st } } } + /*else if( lems[i].getKind()==EQUAL && lems[i][0].getType().isBoolean() ){ + //Boolean terms + if( std::find( d_aux_vars.begin(), d_aux_vars.end(), lems[i][0] )!=d_aux_vars.end() ){ + Node v = lems[i][0]; + d_aux_eq[rlem][v] = lems[i][1]; + Trace("cbqi-debug") << " " << rlem << " implies " << v << " = " << lems[i][1] << std::endl; + } + }*/ lems[i] = rlem; } //collect atoms from all lemmas: we will only do bounds coming from original body diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index b6743724b..88b5f5fb1 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -327,7 +327,7 @@ int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){ }else{ return 0; } - }else if( n.getKind()==IFF ){ + }else if( n.getKind()==EQUAL && n[0].getType().isBoolean() ){ int depIndex1; int eVal = evaluate( n[0], depIndex1, ri ); if( eVal!=0 ){ diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index 9109aab8a..1172fb92c 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -49,7 +49,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { Trace("fmf-fun-def-debug") << "Process function " << n << ", body = " << bd << std::endl; if( !bd.isNull() ){ d_funcs.push_back( f ); - bd = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, n, bd ); + bd = NodeManager::currentNM()->mkNode( EQUAL, n, bd ); //create a sort S that represents the inputs of the function std::stringstream ss; @@ -97,7 +97,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { for( unsigned i=0; i constraints; Trace("fmf-fun-def-rewrite") << "Rewriting " << assertions[i] << ", is_fd = " << is_fd << std::endl; Node n = simplifyFormula( assertions[i], true, true, constraints, is_fd==1 ? subs_head[i] : Node::null(), is_fd ); @@ -201,11 +201,7 @@ void FunDefFmf::simplifyTerm( Node n, std::vector< Node >& constraints ) { std::vector< Node > children; for( unsigned j=0; jmkNode( APPLY_UF, d_input_arg_inj[f][j], z ); - if( !n[j].getType().isBoolean() ){ - children.push_back( uz.eqNode( n[j] ) ); - }else{ - children.push_back( uz.iffNode( n[j] ) ); - } + children.push_back( uz.eqNode( n[j] ) ); } Node bd = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children ); bd = bd.negate(); diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 2a940f1fd..7cf9868bd 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -76,7 +76,7 @@ int InstMatchGenerator::getActiveScore( QuantifiersEngine * qe ) { unsigned ngtt = qe->getTermDatabase()->getNumTypeGroundTerms( tn ); Trace("trigger-active-sel-debug") << "Number of ground terms for " << tn << " is " << ngtt << std::endl; return ngtt; -// }else if( d_match_pattern_getKind()==EQUAL || d_match_pattern.getKind()==IFF ){ +// }else if( d_match_pattern_getKind()==EQUAL ){ }else{ return -1; @@ -90,7 +90,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< //we want to add the children of the NOT d_match_pattern = d_pattern[0]; } - if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==GEQ ){ + if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==GEQ ){ //make sure the matching portion of the equality is on the LHS of d_pattern // and record what d_match_pattern is for( unsigned i=0; i<2; i++ ){ @@ -150,7 +150,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< //we will be scanning lists trying to find d_match_pattern.getOperator() d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern ); //if matching on disequality, inform the candidate generator not to match on eqc - if( d_pattern.getKind()==NOT && ( d_pattern[0].getKind()==IFF || d_pattern[0].getKind()==EQUAL ) ){ + if( d_pattern.getKind()==NOT && d_pattern[0].getKind()==EQUAL ){ ((inst::CandidateGeneratorQE*)d_cg)->excludeEqc( d_eq_class_rel ); d_eq_class_rel = Node::null(); } @@ -166,7 +166,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< }else{ d_cg = new CandidateGeneratorQEAll( qe, d_match_pattern ); } - }else if( ( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ) && + }else if( d_match_pattern.getKind()==EQUAL && d_match_pattern[0].getKind()==INST_CONSTANT && d_match_pattern[1].getKind()==INST_CONSTANT ){ //we will be producing candidates via literal matching heuristics if( d_pattern.getKind()!=NOT ){ @@ -253,10 +253,12 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi } }else{ if( pat.getKind()==EQUAL ){ - Assert( t.getType().isReal() ); - t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermDatabase()->d_one); - }else if( pat.getKind()==IFF ){ - t_match = NodeManager::currentNM()->mkConst( !q->areEqual( qe->getTermDatabase()->d_true, t ) ); + if( t.getType().isBoolean() ){ + t_match = NodeManager::currentNM()->mkConst( !q->areEqual( qe->getTermDatabase()->d_true, t ) ); + }else{ + Assert( t.getType().isReal() ); + t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermDatabase()->d_one); + } }else if( pat.getKind()==GEQ ){ t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermDatabase()->d_one); }else if( pat.getKind()==GT ){ @@ -706,7 +708,7 @@ InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node q, Node pat, Quantifier }else{ d_pol = true; } - if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){ + if( d_match_pattern.getKind()==EQUAL ){ d_eqc = d_match_pattern[1]; d_match_pattern = d_match_pattern[0]; Assert( !quantifiers::TermDb::hasInstConstAttr( d_eqc ) ); diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp index 1f68fb787..41099552d 100644 --- a/src/theory/quantifiers/inst_propagator.cpp +++ b/src/theory/quantifiers/inst_propagator.cpp @@ -366,8 +366,13 @@ bool EqualityQueryInstProp::isPropagateLiteral( Node n ) { return false; }else{ Kind ak = n.getKind()==NOT ? n[0].getKind() : n.getKind(); - Assert( ak!=NOT ); - return ak!=AND && ak!=OR && ak!=IFF && ak!=ITE; + if( ak==EQUAL ){ + Node atom = n.getKind() ? n[0] : n; + return !atom[0].getType().isBoolean(); + }else{ + Assert( ak!=NOT ); + return ak!=AND && ak!=OR && ak!=ITE; + } } } @@ -466,7 +471,7 @@ Node EqualityQueryInstProp::evaluateTermExp( Node n, std::vector< Node >& exp, s addArgument( c, args, watch, is_watch ); abort_i = i; break; - }else if( k==kind::AND || k==kind::OR || k==kind::ITE || k==IFF ){ + }else if( k==kind::AND || k==kind::OR || k==kind::ITE || ( k==EQUAL && n[0].getType().isBoolean() ) ){ Trace("qip-eval-debug") << "Adding argument " << c << " to " << k << ", isProp = " << newHasPol << std::endl; if( ( k==kind::AND || k==kind::OR ) && c.getKind()==k ){ //flatten diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 895a0c93c..0023f7d0f 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -193,7 +193,7 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) { Assert( index<(int)d_nested_qe_waitlist[q].size() ); Node nq = d_nested_qe_waitlist[q][index]; Node nqeqn = doNestedQENode( d_nested_qe_info[nq].d_q, q, nq, d_nested_qe_info[nq].d_inst_terms, d_nested_qe_info[nq].d_doVts ); - Node dqelem = nq.iffNode( nqeqn ); + Node dqelem = nq.eqNode( nqeqn ); Trace("cbqi-lemma") << "Delayed nested quantifier elimination lemma : " << dqelem << std::endl; d_quantEngine->getOutputChannel().lemma( dqelem ); d_nested_qe_waitlist_proc[q] = index + 1; diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index c4bf61b28..f2ed81d8c 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -361,9 +361,9 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ Assert( Trigger::isAtomicTrigger( pat ) ); if( pat.getType().isBoolean() && rpoleq.isNull() ){ if( options::literalMatchMode()==LITERAL_MATCH_USE ){ - pat = NodeManager::currentNM()->mkNode( IFF, pat, NodeManager::currentNM()->mkConst( rpol==-1 ) ).negate(); + pat = NodeManager::currentNM()->mkNode( EQUAL, pat, NodeManager::currentNM()->mkConst( rpol==-1 ) ).negate(); }else if( options::literalMatchMode()!=LITERAL_MATCH_NONE ){ - pat = NodeManager::currentNM()->mkNode( IFF, pat, NodeManager::currentNM()->mkConst( rpol==1 ) ); + pat = NodeManager::currentNM()->mkNode( EQUAL, pat, NodeManager::currentNM()->mkConst( rpol==1 ) ); } }else{ Assert( !rpoleq.isNull() ); diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp index 976b81e60..96d682a77 100644 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp @@ -147,7 +147,7 @@ bool QuantifierMacros::containsBadOp( Node n, Node op, std::vector< Node >& opc, } bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){ - return pol && ( n.getKind()==EQUAL || n.getKind()==IFF ); + return pol && n.getKind()==EQUAL; } bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) { @@ -211,7 +211,7 @@ void QuantifierMacros::getMacroCandidates( Node n, std::vector< Node >& candidat } Node QuantifierMacros::solveInEquality( Node n, Node lit ){ - if( lit.getKind()==IFF || lit.getKind()==EQUAL ){ + if( lit.getKind()==EQUAL ){ //return the opposite side of the equality if defined that way for( int i=0; i<2; i++ ){ if( lit[i]==n ){ diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index a5ec16e3a..090f2735a 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -674,7 +674,7 @@ int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){ std::vector< Node > tr_terms; if( lit.getKind()==APPLY_UF ){ //only match predicates that are contrary to this one, use literal matching - Node eq = NodeManager::currentNM()->mkNode( IFF, lit, !phase ? fm->d_true : fm->d_false ); + Node eq = NodeManager::currentNM()->mkNode( EQUAL, lit, !phase ? fm->d_true : fm->d_false ); tr_terms.push_back( eq ); }else if( lit.getKind()==EQUAL ){ //collect trigger terms diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 1e484311c..420a3d2f7 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -622,7 +622,8 @@ bool QuantInfo::isPropagatingInstance( QuantConflictFind * p, Node n ) { if( n.getKind()==FORALL ){ //TODO? return true; - }else if( n.getKind()==NOT || n.getKind()==AND || n.getKind()==OR || n.getKind()==EQUAL || n.getKind()==ITE || n.getKind()==IFF ){ + }else if( n.getKind()==NOT || n.getKind()==AND || n.getKind()==OR || n.getKind()==EQUAL || n.getKind()==ITE || + ( n.getKind()==EQUAL && n[0].getType().isBoolean() ) ){ for( unsigned i=0; i& cbva void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars ) { Trace("qcf-qregister-debug") << "Determine variable order " << d_n << ", #bvars = " << bvars.size() << std::endl; - bool isComm = d_type==typ_formula && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF ); + bool isComm = d_type==typ_formula && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==EQUAL ); if( isComm ){ std::map< int, std::vector< int > > c_to_vars; std::map< int, std::vector< int > > vars_to_c; @@ -1563,7 +1564,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { success = true; } } - }else if( d_n.getKind()==IFF ){ + }else if( d_n.getKind()==EQUAL ){ //construct match based on both children if( d_child_counter%2==0 ){ if( getChild( 0 )->getNextMatch( p, qi ) ){ @@ -1660,7 +1661,7 @@ bool MatchGen::getExplanation( QuantConflictFind * p, QuantInfo * qi, std::vecto }else{ return getChild( d_child_counter )->getExplanation( p, qi, exp ); } - }else if( d_n.getKind()==IFF ){ + }else if( d_n.getKind()==EQUAL ){ for( unsigned i=0; i<2; i++ ){ if( !getChild( i )->getExplanation( p, qi, exp ) ){ return false; @@ -1861,7 +1862,7 @@ void MatchGen::setInvalid() { } bool MatchGen::isHandledBoolConnective( TNode n ) { - return TermDb::isBoolConnective( n.getKind() ) && ( n.getKind()!=ITE || n.getType().isBoolean() ) && n.getKind()!=SEP_STAR; + return TermDb::isBoolConnectiveTerm( n ) && n.getKind()!=SEP_STAR; } bool MatchGen::isHandledUfTerm( TNode n ) { @@ -1904,11 +1905,7 @@ d_conflict( c, false ) { } Node QuantConflictFind::mkEqNode( Node a, Node b ) { - if( a.getType().isBoolean() ){ - return a.iffNode( b ); - }else{ - return a.eqNode( b ); - } + return a.eqNode( b ); } //-------------------------------------------------- registration diff --git a/src/theory/quantifiers/quant_equality_engine.cpp b/src/theory/quantifiers/quant_equality_engine.cpp index 3f89a799c..46a8b7ce2 100644 --- a/src/theory/quantifiers/quant_equality_engine.cpp +++ b/src/theory/quantifiers/quant_equality_engine.cpp @@ -93,7 +93,7 @@ void QuantEqualityEngine::assertNode( Node n ) { bool success = true; Node t1; Node t2; - if( lit.getKind()==APPLY_UF || lit.getKind()==EQUAL || lit.getKind()==IFF ){ + if( lit.getKind()==APPLY_UF || lit.getKind()==EQUAL ){ lit = getTermDatabase()->getCanonicalTerm( lit ); Trace("qee-debug") << "Canonical : " << lit << ", pol = " << pol << std::endl; if( lit.getKind()==APPLY_UF ){ @@ -102,28 +102,30 @@ void QuantEqualityEngine::assertNode( Node n ) { 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; + if( lit[0].getType().isBoolean() ){ + 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{ 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{ success = false; diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index c0595d3d9..163c576f7 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -201,7 +201,7 @@ int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind } Node QuantArith::solveEqualityFor( Node lit, Node v ) { - Assert( lit.getKind()==EQUAL || lit.getKind()==IFF ); + Assert( lit.getKind()==EQUAL ); //first look directly at sides TypeNode tn = lit[0].getType(); for( unsigned r=0; r<2; r++ ){ @@ -513,7 +513,7 @@ Node QuantEPR::mkEPRAxiom( TypeNode tn ) { std::vector< Node > disj; Node x = NodeManager::currentNM()->mkBoundVar( tn ); for( unsigned i=0; imkNode( tn.isBoolean() ? IFF : EQUAL, x, d_consts[tn][i] ) ); + disj.push_back( NodeManager::currentNM()->mkNode( EQUAL, x, d_consts[tn][i] ) ); } Assert( !disj.empty() ); d_epr_axiom[tn] = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, x ), disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( OR, disj ) ); diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index fcd8d1829..2b7e19c48 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -55,7 +55,6 @@ bool QuantifiersRewriter::isLiteral( Node n ){ case IMPLIES: case XOR: case ITE: - case IFF: return false; break; case EQUAL: @@ -251,7 +250,7 @@ Node QuantifiersRewriter::computeElimSymbols( Node body ) { k = OR; negCh1 = true; }else if( ok==XOR ){ - k = IFF; + k = EQUAL; negCh1 = true; }else if( ok==NOT ){ if( body[0].getKind()==NOT ){ @@ -265,9 +264,9 @@ Node QuantifiersRewriter::computeElimSymbols( Node body ) { k = OR; negAllCh = true; body = body[0]; - }else if( body[0].getKind()==XOR || body[0].getKind()==IFF ){ - k = IFF; - negCh1 = ( body[0].getKind()==IFF ); + }else if( body[0].getKind()==XOR || ( body[0].getKind()==EQUAL && body[0][0].getType().isBoolean() ) ){ + k = EQUAL; + negCh1 = ( body[0].getKind()==EQUAL ); body = body[0]; }else if( body[0].getKind()==ITE ){ k = body[0].getKind(); @@ -277,7 +276,7 @@ Node QuantifiersRewriter::computeElimSymbols( Node body ) { }else{ return body; } - }else if( ok!=IFF && ok!=ITE && ok!=AND && ok!=OR ){ + }else if( ( ok!=EQUAL || !body[0].getType().isBoolean() ) && ok!=ITE && ok!=AND && ok!=OR ){ //a literal return body; } @@ -410,8 +409,8 @@ int getEntailedCond( Node n, std::map< Node, bool >& currCond ){ }else if( res==-1 ){ return getEntailedCond( n[2], currCond ); } - }else if( n.getKind()==IFF || n.getKind()==ITE ){ - unsigned start = n.getKind()==IFF ? 0 : 1; + }else if( ( n.getKind()==EQUAL && n[0].getType().isBoolean() ) || n.getKind()==ITE ){ + unsigned start = n.getKind()==EQUAL ? 0 : 1; int res1 = 0; for( unsigned j=start; j<=(start+1); j++ ){ int res = getEntailedCond( n[j], currCond ); @@ -423,7 +422,7 @@ int getEntailedCond( Node n, std::map< Node, bool >& currCond ){ Assert( res!=0 ); if( n.getKind()==ITE ){ return res1==res ? res : 0; - }else if( n.getKind()==IFF ){ + }else if( n.getKind()==EQUAL ){ return res1==res ? 1 : -1; } } @@ -512,7 +511,7 @@ Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& n Assert( !body.isNull() ); Trace("quantifiers-rewrite-debug") << "Decompose " << h << " / " << fbody << " as function definition for " << q << "." << std::endl; Node r = computeProcessTerms2( fbody, true, true, curr_cond, 0, cache, icache, new_vars, new_conds ); - return Rewriter::rewrite( NodeManager::currentNM()->mkNode( h.getType().isBoolean() ? IFF : EQUAL, h, r ) ); + return Rewriter::rewrite( NodeManager::currentNM()->mkNode( EQUAL, h, r ) ); }else{ return computeProcessTerms2( body, true, true, curr_cond, 0, cache, icache, new_vars, new_conds ); } @@ -773,7 +772,7 @@ Node QuantifiersRewriter::computeCondSplit( Node body, QAttributes& qa ){ } } if( options::condVarSplitQuant() ){ - if( body.getKind()==ITE || ( body.getKind()==IFF && options::condVarSplitQuantAgg() ) ){ + if( body.getKind()==ITE || ( body.getKind()==EQUAL && body[0].getType().isBoolean() && options::condVarSplitQuantAgg() ) ){ Assert( !qa.isFunDef() ); Trace("quantifiers-rewrite-debug") << "Conditional var elim split " << body << "?" << std::endl; bool do_split = false; @@ -1100,7 +1099,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, s NodeManager::currentNM()->mkNode( kind::OR, body[0].notNode(), body[1] ), NodeManager::currentNM()->mkNode( kind::OR, body[0], body[2] ) ); return computePrenex( nn, args, nargs, pol, prenexAgg ); - }else if( prenexAgg && body.getKind()==kind::IFF ){ + }else if( prenexAgg && body.getKind()==kind::EQUAL && body[0].getType().isBoolean() ){ Node nn = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::OR, body[0].notNode(), body[1] ), NodeManager::currentNM()->mkNode( kind::OR, body[0], body[1].notNode() ) ); @@ -1631,11 +1630,7 @@ Node QuantifiersRewriter::rewriteRewriteRule( Node r ) { case kind::RR_REWRITE: // Equality pattern.push_back( head ); - if( head.getType().isBoolean() ){ - body = head.iffNode(body); - }else{ - body = head.eqNode(body); - } + body = head.eqNode(body); break; case kind::RR_REDUCTION: case kind::RR_DEDUCTION: @@ -1780,7 +1775,7 @@ 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.getKind()==kind::ITE && n.getType().isBoolean() ) || n.getKind()==kind::IFF ){ + if( ( n.getKind()==kind::ITE && n.getType().isBoolean() ) || ( n.getKind()==kind::EQUAL && n[0].getType().isBoolean() ) ){ if( options::preSkolemQuantAgg() ){ Node nn; //must remove structure @@ -1788,12 +1783,10 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v 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 ){ + }else if( n.getKind()==kind::EQUAL ){ 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 ); } diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index ec1b41a98..3e6b0ffa9 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -230,27 +230,14 @@ void RewriteEngine::registerQuantifier( Node f ) { } std::vector< Node > cc; - //Node head = rr[2][0]; - //if( head!=d_true ){ - //Node head_eq = head.getType().isBoolean() ? head.iffNode( head ) : head.eqNode( head ); - //head_eq = head_eq.negate(); - //cc.push_back( head_eq ); - //Trace("rr-register-debug") << " head eq is " << head_eq << std::endl; - //} //add patterns for( unsigned i=1; i nc; for( unsigned j=0; jmkBoundVar( f[2][i][j].getType() ); - if( f[2][i][j].getType().isBoolean() ){ - if( f[2][i][j].getKind()!=APPLY_UF ){ - nn = f[2][i][j].negate(); - }else{ - nn = f[2][i][j].iffNode( nbv ).negate(); - bvl.push_back( nbv ); - } - //nn = f[2][i][j].negate(); + if( f[2][i][j].getType().isBoolean() && f[2][i][j].getKind()!=APPLY_UF ){ + nn = f[2][i][j].negate(); }else{ nn = f[2][i][j].eqNode( nbv ).negate(); bvl.push_back( nbv ); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 0bdfa2d24..d394c8fef 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -267,10 +267,10 @@ void TermDb::computeUfTerms( TNode f ) { }else{ if( at!=n && ee->areDisequal( at, n, false ) ){ std::vector< Node > lits; - lits.push_back( NodeManager::currentNM()->mkNode( at.getType().isBoolean() ? IFF : EQUAL, at, n ) ); + lits.push_back( NodeManager::currentNM()->mkNode( EQUAL, at, n ) ); for( unsigned i=0; imkNode( at[i].getType().isBoolean() ? IFF : EQUAL, at[i], n[i] ).negate() ); + lits.push_back( NodeManager::currentNM()->mkNode( EQUAL, at[i], n[i] ).negate() ); } } Node lem = lits.size()==1 ? lits[0] : NodeManager::currentNM()->mkNode( OR, lits ); @@ -484,7 +484,7 @@ bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, Assert( !qy->extendsEngine() ); Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol << std::endl; Assert( n.getType().isBoolean() ); - if( n.getKind()==EQUAL ){ + if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){ TNode n1 = getEntailedTerm2( n[0], subs, subsRep, hasSubs, qy ); if( !n1.isNull() ){ TNode n2 = getEntailedTerm2( n[1], subs, subsRep, hasSubs, qy ); @@ -518,10 +518,11 @@ bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, } } return !simPol; - }else if( n.getKind()==IFF || n.getKind()==ITE ){ + //Boolean equality here + }else if( n.getKind()==EQUAL || n.getKind()==ITE ){ for( unsigned i=0; i<2; i++ ){ if( isEntailed2( n[0], subs, subsRep, hasSubs, i==0, qy ) ){ - unsigned ch = ( n.getKind()==IFF || i==0 ) ? 1 : 2; + unsigned ch = ( n.getKind()==EQUAL || i==0 ) ? 1 : 2; bool reqPol = ( n.getKind()==ITE || i==0 ) ? pol : !pol; return isEntailed2( n[ch], subs, subsRep, hasSubs, reqPol, qy ); } @@ -1956,18 +1957,24 @@ Node TermDb::simpleNegate( Node n ){ } bool TermDb::isAssoc( Kind k ) { - return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF || + return k==PLUS || k==MULT || k==AND || k==OR || k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT || k==STRING_CONCAT; } bool TermDb::isComm( Kind k ) { - return k==EQUAL || k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF || + return k==EQUAL || k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR; } bool TermDb::isBoolConnective( Kind k ) { - return k==OR || k==AND || k==IFF || k==ITE || k==FORALL || k==NOT || k==SEP_STAR; + return k==OR || k==AND || k==EQUAL || k==ITE || k==FORALL || k==NOT || k==SEP_STAR; +} + +bool TermDb::isBoolConnectiveTerm( TNode n ) { + return isBoolConnective( n.getKind() ) && + ( n.getKind()!=EQUAL || n[0].getType().isBoolean() ) && + ( n.getKind()!=ITE || n.getType().isBoolean() ); } void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){ @@ -2018,7 +2025,7 @@ bool TermDb::isFunDefAnnotation( Node ipl ) { } Node TermDb::getFunDefHead( Node q ) { - //&& ( q[1].getKind()==EQUAL || q[1].getKind()==IFF ) && q[1][0].getKind()==APPLY_UF && + //&& q[1].getKind()==EQUAL && q[1][0].getKind()==APPLY_UF && if( q.getKind()==FORALL && q.getNumChildren()==3 ){ for( unsigned i=0; imkNode( AND, NodeManager::currentNM()->mkNode( LEQ, t[0], t[1] ), - NodeManager::currentNM()->mkNode( LEQ, t[1], t[0] ) ); + if( t.getKind()==EQUAL ){ + if( t[0].getType().isReal() ){ + return NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, t[0], t[1] ), + NodeManager::currentNM()->mkNode( LEQ, t[1], t[0] ) ); + }else if( t[0].getType().isBoolean() ){ + return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ), + NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[1].negate() ) ); + } }else if( t.getKind()==ITE && t.getType().isBoolean() ){ return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ), NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[2] ) ); - }else if( t.getKind()==IFF ){ - return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ), - NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[1].negate() ) ); } return Node::null(); } @@ -3248,13 +3257,13 @@ void TermDbSygus::registerEvalTerm( Node n ) { Assert( dt.isSygus() ); d_eval_args[n[0]].push_back( std::vector< Node >() ); for( unsigned j=1; jmkConst(BitVector(1u, 1u)); - d_eval_args[n[0]].back().push_back( n[j].eqNode( c ) ); - }else{ + //if( var_list[j-1].getType().isBoolean() ){ + // //TODO: remove this case when boolean term conversion is eliminated + // Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u)); + // d_eval_args[n[0]].back().push_back( n[j].eqNode( c ) ); + //}else{ d_eval_args[n[0]].back().push_back( n[j] ); - } + //} } Node a = getAnchor( n[0] ); d_subterms[a][n[0]] = true; @@ -3297,7 +3306,7 @@ void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& lems for( unsigned i=start; isecond.size(); i++ ){ Assert( vars.size()==it->second[i].size() ); Node sBTerm = bTerm.substitute( vars.begin(), vars.end(), it->second[i].begin(), it->second[i].end() ); - Node lem = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, d_evals[n][i], sBTerm ); + Node lem = NodeManager::currentNM()->mkNode(EQUAL, d_evals[n][i], sBTerm ); lem = NodeManager::currentNM()->mkNode( OR, antec, lem ); Trace("sygus-eager") << "Lemma : " << lem << std::endl; lems.push_back( lem ); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index d4fdaa5e5..9f43c1d35 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -499,6 +499,8 @@ public: static bool isComm( Kind k ); /** is bool connective */ static bool isBoolConnective( Kind k ); + /** is bool connective term */ + static bool isBoolConnectiveTerm( TNode n ); //for sygus private: diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 7ab9f7065..cca6543b6 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -255,7 +255,7 @@ Node Trigger::getIsUsableEq( Node q, Node n ) { Assert( isRelationalTrigger( n ) ); for( unsigned i=0; i<2; i++) { if( isUsableEqTerms( q, n[i], n[1-i] ) ){ - if( i==1 && ( n.getKind()==EQUAL || n.getKind()==IFF ) && !quantifiers::TermDb::hasInstConstAttr(n[0]) ){ + if( i==1 && n.getKind()==EQUAL && !quantifiers::TermDb::hasInstConstAttr(n[0]) ){ return NodeManager::currentNM()->mkNode( n.getKind(), n[1], n[0] ); }else{ return n; @@ -292,7 +292,7 @@ Node Trigger::getIsUsableTrigger( Node n, Node q ) { n = n[0]; } if( n.getKind()==INST_CONSTANT ){ - return pol ? n : NodeManager::currentNM()->mkNode( IFF, n, NodeManager::currentNM()->mkConst( true ) ).notNode(); + return pol ? n : NodeManager::currentNM()->mkNode( EQUAL, n, NodeManager::currentNM()->mkConst( true ) ).notNode(); }else if( isRelationalTrigger( n ) ){ Node rtr = getIsUsableEq( q, n ); if( rtr.isNull() && n[0].getType().isReal() ){ @@ -331,7 +331,7 @@ Node Trigger::getIsUsableTrigger( Node n, Node q ) { }else{ Trace("trigger-debug") << n << " usable : " << ( quantifiers::TermDb::getInstConstAttr(n)==q ) << " " << isAtomicTrigger( n ) << " " << isUsable( n, q ) << std::endl; if( isUsableAtomicTrigger( n, q ) ){ - return pol ? n : NodeManager::currentNM()->mkNode( IFF, n, NodeManager::currentNM()->mkConst( true ) ).notNode(); + return pol ? n : NodeManager::currentNM()->mkNode( EQUAL, n, NodeManager::currentNM()->mkConst( true ) ).notNode(); } } return Node::null(); @@ -362,7 +362,7 @@ bool Trigger::isRelationalTrigger( Node n ) { } bool Trigger::isRelationalTriggerKind( Kind k ) { - return k==EQUAL || k==IFF || k==GEQ; + return k==EQUAL || k==GEQ; } bool Trigger::isCbqiKind( Kind k ) { @@ -377,7 +377,7 @@ bool Trigger::isCbqiKind( Kind k ) { bool Trigger::isSimpleTrigger( Node n ){ Node t = n.getKind()==NOT ? n[0] : n; - if( t.getKind()==IFF || t.getKind()==EQUAL ){ + if( t.getKind()==EQUAL ){ if( !quantifiers::TermDb::hasInstConstAttr( t[1] ) ){ t = t[0]; } @@ -416,7 +416,7 @@ bool Trigger::collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, Assert( nu.getKind()!=NOT ); Trace("auto-gen-trigger-debug2") << "...found usable trigger : " << nu << std::endl; Node reqEq; - if( nu.getKind()==IFF || nu.getKind()==EQUAL ){ + if( nu.getKind()==EQUAL ){ if( isAtomicTrigger( nu[0] ) && !quantifiers::TermDb::hasInstConstAttr(nu[1]) ){ if( hasPol ){ reqEq = nu[1]; -- cgit v1.2.3