From: ajreynol Date: Mon, 28 Mar 2016 21:26:57 +0000 (-0500) Subject: Minor cleanup from last commit (quant util, equality infer). Do not set fmfBoundIntLa... X-Git-Tag: cvc5-1.0.0~6049^2~84 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f582b382a25463cead88bc1a46b93dd5c8099fad;p=cvc5.git Minor cleanup from last commit (quant util, equality infer). Do not set fmfBoundIntLazy for stringsExp. --- diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index bbaa07af5..98ed9c4fd 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1310,15 +1310,7 @@ void SmtEngine::setDefaults() { Trace("smt") << "turning on quantifier logic, for strings-exp" << std::endl; } - if(! options::finiteModelFind.wasSetByUser()) { - options::finiteModelFind.set( true ); - Trace("smt") << "turning on finite-model-find, for strings-exp" - << std::endl; - } if(! options::fmfBoundInt.wasSetByUser()) { - if(! options::fmfBoundIntLazy.wasSetByUser()) { - options::fmfBoundIntLazy.set( true ); - } options::fmfBoundInt.set( true ); Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl; } diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 0a038f0ed..4287bd620 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -87,19 +87,19 @@ private: d_dt.conflict(t1, t2); } void eqNotifyNewClass(TNode t) { - Debug("dt") << "NotifyClass::eqNotifyNewClass(" << t << std::endl; + Debug("dt") << "NotifyClass::eqNotifyNewClass(" << t << ")" << std::endl; d_dt.eqNotifyNewClass(t); } void eqNotifyPreMerge(TNode t1, TNode t2) { - Debug("dt") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << std::endl; + Debug("dt") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << ")" << std::endl; d_dt.eqNotifyPreMerge(t1, t2); } void eqNotifyPostMerge(TNode t1, TNode t2) { - Debug("dt") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << std::endl; + Debug("dt") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << ")" << std::endl; d_dt.eqNotifyPostMerge(t1, t2); } void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { - Debug("dt") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << std::endl; + Debug("dt") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << ")" << std::endl; d_dt.eqNotifyDisequal(t1, t2, reason); } };/* class TheoryDatatypes::NotifyClass */ diff --git a/src/theory/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h index 4a6943119..70b05c351 100644 --- a/src/theory/quantifiers/equality_infer.h +++ b/src/theory/quantifiers/equality_infer.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef EQUALITY_INFER_H -#define EQUALITY_INFER_H +#ifndef __CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H +#define __CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H #include #include @@ -60,14 +60,17 @@ private: /** use list */ NodeListMap d_uselist; void addToUseList( Node used, Node eqc ); + /** pending merges */ + NodeList d_pending_merges; public: EqualityInference(context::Context* c); virtual ~EqualityInference(); - /** notification when equality engine is updated */ + /** input : notification when equality engine is updated */ void eqNotifyNewClass(TNode t); void eqNotifyMerge(TNode t1, TNode t2); - - NodeList d_pending_merges; + /** output : inferred equalities */ + unsigned getNumPendingMerges() { return d_pending_merges.size(); } + Node getPendingMerge( unsigned i ) { return d_pending_merges[i]; } }; } diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 3d649f302..1f1efa2a8 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -113,9 +113,8 @@ Node QuantArith::mkNode( std::map< Node, Node >& msum ) { // given (msum 0), solve (veq_c * v val) or (val veq_c * v), where: // veq_c is either null (meaning 1), or positive. -// return value -1: veq_c*v is LHS. - -int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k, bool doCoeff ) { +// return value 1: veq_c*v is RHS, -1: veq_c*v is LHS, 0: failed. +int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Node & val, Kind k ) { std::map< Node, Node >::iterator itv = msum.find( v ); if( itv!=msum.end() ){ std::vector< Node > children; @@ -136,75 +135,20 @@ int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind children.push_back(m); } } - veq = children.size()>1 ? NodeManager::currentNM()->mkNode( PLUS, children ) : + val = children.size()>1 ? NodeManager::currentNM()->mkNode( PLUS, children ) : (children.size()==1 ? children[0] : NodeManager::currentNM()->mkConst( Rational(0) )); - Node vc = v; - if( !r.isOne() && !r.isNegativeOne() ){ - if( vc.getType().isInteger() ){ - if( doCoeff ){ - vc = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( r.abs() ), vc ); - }else{ - return 0; - } - }else{ - veq = NodeManager::currentNM()->mkNode( MULT, veq, NodeManager::currentNM()->mkConst( Rational(1) / r.abs() ) ); - } - } - if( r.sgn()==1 ){ - veq = negate(veq); - } - veq = Rewriter::rewrite( veq ); - bool inOrder = r.sgn()==1 || k==EQUAL; - veq = NodeManager::currentNM()->mkNode( k, inOrder ? vc : veq, inOrder ? veq : vc ); - return inOrder ? 1 : -1; - } - } - return 0; -} - -int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Node & val, Kind k ) { - Node vatom; - //isolate pv in the inequality - int ires = isolate( v, msum, vatom, k, true ); - if( ires!=0 ){ - val = vatom[ ires==1 ? 1 : 0 ]; - Node pvm = vatom[ ires==1 ? 0 : 1 ]; - //get monomial - if( pvm!=v ){ - Node veq_v; - if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){ - Assert( veq_v==v ); - } - } - } - return ires; -} - -/* -int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Node & val, Kind k ) { - Assert( k==EQUAL || k==GEQ ); - std::map< Node, Node >::iterator itv = msum.find( v ); - if( itv!=msum.end() ){ - Rational r = itv->second.isNull() ? Rational(1) : itv->second.getConst(); - if( r.sgn()!=0 ){ - veq_c = itv->second; - msum.erase( itv ); - val = mkNode( msum ); - msum[v] = veq_c; if( !r.isOne() && !r.isNegativeOne() ){ if( v.getType().isInteger() ){ veq_c = NodeManager::currentNM()->mkConst( r.abs() ); }else{ val = NodeManager::currentNM()->mkNode( MULT, val, NodeManager::currentNM()->mkConst( Rational(1) / r.abs() ) ); - veq_c = Node::null(); } - }else{ - veq_c = Node::null(); } if( r.sgn()==1 ){ - val = negate( val ); + val = negate(val); + }else{ + val = Rewriter::rewrite( val ); } - val = Rewriter::rewrite( val ); return ( r.sgn()==1 || k==EQUAL ) ? 1 : -1; } } @@ -230,7 +174,6 @@ int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind } return ires; } -*/ Node QuantArith::solveEqualityFor( Node lit, Node v ) { Assert( lit.getKind()==EQUAL || lit.getKind()==IFF ); @@ -241,7 +184,7 @@ Node QuantArith::solveEqualityFor( Node lit, Node v ) { return lit[1-r]; } } - if( tn.isInteger() || tn.isReal() ){ + if( tn.isReal() ){ if( quantifiers::TermDb::containsTerm( lit, v ) ){ std::map< Node, Node > msum; if( QuantArith::getMonomialSumLit( lit, msum ) ){ diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 0327651d7..31743d352 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -38,8 +38,8 @@ public: static bool getMonomialSumLit( Node lit, std::map< Node, Node >& msum ); static Node mkNode( std::map< Node, Node >& msum ); //return 1 : solved on LHS, return -1 : solved on RHS, return 0: failed - static int isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k, bool doCoeff = false ); static int isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Node & val, Kind k ); + static int isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k, bool doCoeff = false ); static Node solveEqualityFor( Node lit, Node v ); static Node negate( Node t ); static Node offset( Node t, int i ); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index a2ce9c368..3b74cf352 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -319,14 +319,6 @@ TNode TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsR TNode nn = d_func_map_trie[f].existsTerm( args ); Trace("term-db-eval") << "Got term " << nn << std::endl; return nn; - if( !nn.isNull() ){ - if( ee->hasTerm( nn ) ){ - Trace("term-db-eval") << "return rep " << std::endl; - return ee->getRepresentative( nn ); - }else{ - //Assert( false ); - } - } } } } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 86e15485a..01229a171 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -1317,59 +1317,9 @@ void EqualityQueryQuantifiersEngine::reset( Theory::Effort e ){ void EqualityQueryQuantifiersEngine::processInferences( Theory::Effort e ) { if( options::inferArithTriggerEq() ){ eq::EqualityEngine* ee = getEngine(); - //naive implementation - /* - std::vector< Node > infer; - std::vector< Node > infer_exp; - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); - while( !eqcs_i.isFinished() ){ - TNode r = (*eqcs_i); - TypeNode tr = r.getType(); - if( tr.isReal() ){ - std::vector< Node > eqc; - eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); - while( !eqc_i.isFinished() ){ - TNode n = (*eqc_i); - //accumulate equivalence class - eqc.push_back( n ); - ++eqc_i; - } - for( unsigned i=0; i msum; - QuantArith::getMonomialSum( n, msum ); - for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ - //if the term is a trigger - Node t = it->first; - if( inst::Trigger::isAtomicTrigger( t ) ){ - for( unsigned j=0; jhasTerm( v ) && ee->getRepresentative( v )!=r ){ - Trace("quant-engine-ee-proc") << "processInferences : Infer : " << t << " == " << v << " from " << n << " == " << eqc[j] << std::endl; - infer.push_back( t.eqNode( v ) ); - infer_exp.push_back( n.eqNode( eqc[j] ) ); - } - } - } - } - } - } - } - } - ++eqcs_i; - } - for( unsigned i=0; iassertEquality( infer[i], true, infer_exp[i] ); - } - */ //updated implementation - while( d_eqi_counter.get()d_pending_merges.size() ){ - Node eq = d_eq_inference->d_pending_merges[d_eqi_counter.get()]; + while( d_eqi_counter.get()getNumPendingMerges() ){ + Node eq = d_eq_inference->getPendingMerge( d_eqi_counter.get() ); Trace("quant-engine-ee-proc") << "processInferences : Infer : " << eq << std::endl; Assert( ee->hasTerm( eq[0] ) ); Assert( ee->hasTerm( eq[1] ) ); diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 48aee1c35..d4a1e5ca4 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -1206,12 +1206,12 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st Node a = d_nodes[currentNode]; Node b = d_nodes[d_equalityEdges[currentEdge].getNodeId()]; - if (d_pathReconstructionTriggers.find(reasonType) != d_pathReconstructionTriggers.end()) { - d_pathReconstructionTriggers.find(reasonType)->second->notify(reasonType, reason, a, b, - equalities, eqpc); - } - if (eqpc) { + //apply proof reconstruction processing (when eqpc is non-null) + if (d_pathReconstructionTriggers.find(reasonType) != d_pathReconstructionTriggers.end()) { + d_pathReconstructionTriggers.find(reasonType)->second->notify(reasonType, reason, a, b, + equalities, eqpc); + } if (reasonType == MERGED_THROUGH_EQUALITY) { eqpc->d_node = reason; } else {