summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/quant_equality_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/quant_equality_engine.cpp')
-rw-r--r--src/theory/quantifiers/quant_equality_engine.cpp219
1 files changed, 0 insertions, 219 deletions
diff --git a/src/theory/quantifiers/quant_equality_engine.cpp b/src/theory/quantifiers/quant_equality_engine.cpp
deleted file mode 100644
index 859c4f3ea..000000000
--- a/src/theory/quantifiers/quant_equality_engine.cpp
+++ /dev/null
@@ -1,219 +0,0 @@
-/********************* */
-/*! \file quant_equality_engine.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Andrew Reynolds, Paul Meng
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** Congruence closure with free variables
- **/
-
-#include <vector>
-
-#include "theory/quantifiers/quant_equality_engine.h"
-#include "theory/rewriter.h"
-#include "theory/quantifiers/term_util.h"
-
-using namespace CVC4;
-using namespace std;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-using namespace CVC4::kind;
-
-QuantEqualityEngine::QuantEqualityEngine( QuantifiersEngine * qe, context::Context* c ) :
-QuantifiersModule( qe ),
-d_notify( *this ),
-d_uequalityEngine(d_notify, c, "theory::quantifiers::QuantEqualityEngine", true),
-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) {
- //report conflict through quantifiers engine output channel
- std::vector<TNode> assumptions;
- d_uequalityEngine.explainEquality(t1, t2, true, assumptions, NULL);
- Node conflict;
- if( assumptions.size()==1 ){
- conflict = assumptions[0];
- }else{
- conflict = NodeManager::currentNM()->mkNode( AND, assumptions );
- }
- d_conflict = true;
- Trace("qee-conflict") << "Quantifier equality engine conflict : " << conflict << std::endl;
- d_quantEngine->getOutputChannel().conflict( conflict );
-}
-
-void QuantEqualityEngine::eqNotifyNewClass(TNode t){
-
-}
-void QuantEqualityEngine::eqNotifyPreMerge(TNode t1, TNode t2){
-
-}
-void QuantEqualityEngine::eqNotifyPostMerge(TNode t1, TNode t2){
-
-}
-void QuantEqualityEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
-
-}
-
-/* whether this module needs to check this round */
-bool QuantEqualityEngine::needsCheck( Theory::Effort e ) {
- return e>=Theory::EFFORT_LAST_CALL;
-}
-
-/* reset at a round */
-void QuantEqualityEngine::reset_round( Theory::Effort e ){
- //TODO
-}
-
-/* Call during quantifier engine's check */
-void QuantEqualityEngine::check(Theory::Effort e, QEffort quant_e)
-{
- //TODO
-}
-
-/* Called for new quantifiers */
-void QuantEqualityEngine::registerQuantifier( Node q ) {
- //TODO
-}
-
-/** called for everything that gets asserted */
-void QuantEqualityEngine::assertNode( Node n ) {
- Assert( n.getKind()==FORALL );
- Trace("qee-debug") << "QEE assert : " << n << std::endl;
- 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 || lit.getKind()==EQUAL ){
- lit = getTermUtil()->getCanonicalTerm( lit );
- Trace("qee-debug") << "Canonical : " << lit << ", pol = " << pol << std::endl;
- if( lit.getKind()==APPLY_UF ){
- t1 = getFunctionAppForPredicateApp( lit );
- t2 = pol ? getTermUtil()->d_one : getTermUtil()->d_zero;
- pol = true;
- lit = NodeManager::currentNM()->mkNode( EQUAL, t1, t2 );
- }else if( lit.getKind()==EQUAL ){
- 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];
- t2 = lit[1];
- }
- }
- }else{
- 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);
- }else{
- d_uequalityEngine.assertEquality(lit, pol, n);
- }
- }
- }else{
- d_quant_unproc[n] = true;
- Trace("qee-debug") << "...add to unprocessed (" << lit.getKind() << ")" << std::endl;
- }
- }
-}
-
-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::areUnivEqualInternal( TNode n1, TNode n2 ) {
- return n1==n2 || ( d_uequalityEngine.hasTerm( n1 ) && d_uequalityEngine.hasTerm( n2 ) && d_uequalityEngine.areEqual( n1, n2 ) );
-}
-
-TNode QuantEqualityEngine::getUnivRepresentativeInternal( TNode n ) {
- if( d_uequalityEngine.hasTerm( n ) ){
- return d_uequalityEngine.getRepresentative( n );
- }else{
- return n;
- }
-}
-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 );
-}
-
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback