Searched refs:setDisequal (Results 1 – 3 of 3) sorted by relevance
| /dports/math/cvc4/CVC4-1.7/src/theory/uf/ |
| H A D | theory_uf_strong_solver.cpp | 78 r->setDisequal( n, (*it).first, t, false ); in takeNode()
81 setDisequal( (*it).first, n, 0, false ); in takeNode()
82 setDisequal( (*it).first, n, 1, true ); in takeNode()
83 setDisequal( n, (*it).first, 1, true ); in takeNode()
85 setDisequal( n, (*it).first, 0, true ); in takeNode()
89 r->setDisequal( (*it).first, n, 0, true ); in takeNode()
90 setDisequal( n, (*it).first, 0, true ); in takeNode()
143 setDisequal( a, n, t, true ); in setEqual()
144 nr->setDisequal( n, a, t, true ); in setEqual()
146 setDisequal( b, n, t, false ); in setEqual()
[all …]
|
| H A D | theory_uf_strong_solver.h | 75 void setDisequal( Node n, bool valid ){ in setDisequal() function
186 void setDisequal( Node n1, Node n2, int type, bool valid );
|
| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | sort_inference.h | 59 void setDisequal( int t1, int t2 ){ d_deq.push_back( std::pair< int, int >( t1, t2 ) ); } in setDisequal() function
|