summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/term_database.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r--src/theory/quantifiers/term_database.cpp57
1 files changed, 33 insertions, 24 deletions
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; i<at.getNumChildren(); i++ ){
if( at[i]!=n[i] ){
- lits.push_back( NodeManager::currentNM()->mkNode( 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; i<q[2].getNumChildren(); i++ ){
@@ -2034,7 +2041,7 @@ Node TermDb::getFunDefHead( Node q ) {
Node TermDb::getFunDefBody( Node q ) {
Node h = getFunDefHead( q );
if( !h.isNull() ){
- if( q[1].getKind()==EQUAL || q[1].getKind()==IFF ){
+ if( q[1].getKind()==EQUAL ){
if( q[1][0]==h ){
return q[1][1];
}else if( q[1][1]==h ){
@@ -2718,7 +2725,7 @@ bool TermDbSygus::isIdempotentArg( Node n, Kind ik, int arg ) {
return arg==1;
}
}else if( n==getTypeMaxValue( tn ) ){
- if( ik==IFF || ik==BITVECTOR_AND || ik==BITVECTOR_XNOR ){
+ if( ik==EQUAL || ik==BITVECTOR_AND || ik==BITVECTOR_XNOR ){
return true;
}
}
@@ -3063,15 +3070,17 @@ Node TermDbSygus::minimizeBuiltinTerm( Node n ) {
}
Node TermDbSygus::expandBuiltinTerm( Node t ){
- if( t.getKind()==EQUAL && ( t[0].getType().isInteger() || 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] ) );
+ 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; j<n.getNumChildren(); j++ ){
- 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{
+ //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; i<it->second.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 );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback