From: Andrew Reynolds Date: Tue, 26 Jan 2021 20:11:10 +0000 (-0600) Subject: Remove deprecated quantifiers modules (#5820) X-Git-Tag: cvc5-1.0.0~2353 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=06e367c39bf080b9a82dea82ebdf8b9fb79409d5;p=cvc5.git Remove deprecated quantifiers modules (#5820) --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 53420d395..1f7fc8bac 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -622,8 +622,6 @@ libcvc4_add_sources( theory/output_channel.h theory/quantifiers/alpha_equivalence.cpp theory/quantifiers/alpha_equivalence.h - theory/quantifiers/anti_skolem.cpp - theory/quantifiers/anti_skolem.h theory/quantifiers/bv_inverter.cpp theory/quantifiers/bv_inverter.h theory/quantifiers/bv_inverter_utils.cpp @@ -677,8 +675,6 @@ libcvc4_add_sources( theory/quantifiers/ematching/trigger_trie.h theory/quantifiers/ematching/var_match_generator.cpp theory/quantifiers/ematching/var_match_generator.h - theory/quantifiers/equality_infer.cpp - theory/quantifiers/equality_infer.h theory/quantifiers/equality_query.cpp theory/quantifiers/equality_query.h theory/quantifiers/expr_miner.cpp diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 3499da7de..d3b3502fc 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1829,14 +1829,6 @@ header = "options/quantifiers_options.h" name = "agg" help = "Aggressively split quantified formulas." -[[option]] - name = "quantAntiSkolem" - category = "regular" - long = "quant-anti-skolem" - type = "bool" - default = "false" - help = "perform anti-skolemization for quantified formulas" - ### Higher-order options [[option]] diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp deleted file mode 100644 index c91ba419b..000000000 --- a/src/theory/quantifiers/anti_skolem.cpp +++ /dev/null @@ -1,305 +0,0 @@ -/********************* */ -/*! \file anti_skolem.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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 - ** - ** \brief Implementation of anti-skolemization, e.g.: - ** ( forall x. P[ f( x ) ] ^ forall x. Q[ f( x ) ] ) => forall x. exists y. ( P[ y ] ^ Q[ y ] ) - **/ - -#include "theory/quantifiers/anti_skolem.h" - -#include "expr/term_canonize.h" -#include "options/quantifiers_options.h" -#include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers_engine.h" - -using namespace std; -using namespace CVC4::kind; -using namespace CVC4::context; - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -struct sortTypeOrder { - expr::TermCanonize* d_tu; - bool operator() (TypeNode i, TypeNode j) { - return d_tu->getIdForType( i )getIdForType( j ); - } -}; - -void QuantAntiSkolem::SkQuantTypeCache::add( std::vector< TypeNode >& typs, Node q, unsigned index ) { - if( index==typs.size() ){ - Assert(std::find(d_quants.begin(), d_quants.end(), q) == d_quants.end()); - d_quants.push_back( q ); - }else{ - d_children[typs[index]].add( typs, q, index+1 ); - } -} - -void QuantAntiSkolem::SkQuantTypeCache::sendLemmas( QuantAntiSkolem * ask ) { - for( std::map< TypeNode, SkQuantTypeCache >::iterator it = d_children.begin(); it != d_children.end(); ++it ){ - it->second.sendLemmas( ask ); - } - if( !d_quants.empty() ){ - ask->sendAntiSkolemizeLemma( d_quants ); - } -} - -bool QuantAntiSkolem::CDSkQuantCache::add( context::Context* c, std::vector< Node >& quants, unsigned index ) { - if( index==quants.size() ){ - if( !d_valid.get() ){ - d_valid.set( true ); - return true; - }else{ - return false; - } - }else{ - Node n = quants[index]; - std::map< Node, CDSkQuantCache* >::iterator it = d_data.find( n ); - CDSkQuantCache* skc; - if( it==d_data.end() ){ - skc = new CDSkQuantCache( c ); - d_data[n] = skc; - }else{ - skc = it->second; - } - return skc->add( c, quants, index+1 ); - } -} - -QuantAntiSkolem::CDSkQuantCache::~CDSkQuantCache() { - for(std::map< Node, CDSkQuantCache* >::iterator i = d_data.begin(), iend = d_data.end(); - i != iend; ++i){ - CDSkQuantCache* current = (*i).second; - Assert(current != NULL); - delete current; - } -} - -QuantAntiSkolem::QuantAntiSkolem(QuantifiersEngine* qe, QuantifiersState& qs) - : QuantifiersModule(qs, qe) -{ - d_sqc = new CDSkQuantCache(qs.getUserContext()); -} - -QuantAntiSkolem::~QuantAntiSkolem() { delete d_sqc; } - -/* Call during quantifier engine's check */ -void QuantAntiSkolem::check(Theory::Effort e, QEffort quant_e) -{ - if (quant_e == QEFFORT_STANDARD) - { - d_sqtc.clear(); - for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ - Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); - if( d_quant_processed.find( q )==d_quant_processed.end() ){ - d_quant_processed[q] = true; - Trace("anti-sk") << "Process quantified formula : " << q << std::endl; - bool success = false; - if( d_quant_sip[q].init( q[1] ) ){ - Trace("anti-sk") << "- Partitioned to single invocation parts : " << std::endl; - d_quant_sip[q].debugPrint( "anti-sk" ); - //check if it is single invocation - if( d_quant_sip[q].isPurelySingleInvocation() ){ - //for now, only do purely single invocation - success = true; - } - }else{ - Trace("anti-sk") << "- Failed to initialize." << std::endl; - } - if( success ){ - //sort the argument variables - std::vector sivars; - d_quant_sip[q].getSingleInvocationVariables(sivars); - for (const Node& v : sivars) - { - d_ask_types[q].push_back(v.getType()); - } - std::map< TypeNode, std::vector< unsigned > > indices; - for (unsigned j = 0, size = d_ask_types[q].size(); j < size; j++) - { - indices[d_ask_types[q][j]].push_back( j ); - } - sortTypeOrder sto; - sto.d_tu = d_quantEngine->getTermCanonize(); - std::sort( d_ask_types[q].begin(), d_ask_types[q].end(), sto ); - //increment j on inner loop - for( unsigned j=0; j >::iterator it = d_ask_types.find( q ); - if( it!=d_ask_types.end() ){ - d_sqtc.add( it->second, q ); - } - } - Trace("anti-sk-debug") << "Process lemmas..." << std::endl; - //send out lemmas for each anti-skolemizable group of quantified formulas - d_sqtc.sendLemmas( this ); - Trace("anti-sk-debug") << "...Finished process lemmas" << std::endl; - } -} - -bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool pconnected ) { - Assert(!quants.empty()); - std::sort( quants.begin(), quants.end() ); - if (d_sqc->add(d_qstate.getUserContext(), quants)) - { - //partition into connected components - if( pconnected && quants.size()>1 ){ - Trace("anti-sk-debug") << "Partition into connected components..." << std::endl; - int eqc_count = 0; - std::map< Node, int > func_to_eqc; - std::map< int, std::vector< Node > > eqc_to_func; - std::map< int, std::vector< Node > > eqc_to_quant; - for( unsigned i=0; i eqcs; - std::vector funcs; - d_quant_sip[q].getFunctions(funcs); - for (const Node& f : funcs) - { - std::map< Node, int >::iterator itf = func_to_eqc.find( f ); - if( itf == func_to_eqc.end() ){ - if( eqcs.empty() ){ - func_to_eqc[f] = eqc_count; - eqc_to_func[eqc_count].push_back( f ); - eqc_count++; - }else{ - func_to_eqc[f] = eqcs[0]; - eqc_to_func[eqcs[0]].push_back( f ); - } - } - if( std::find( eqcs.begin(), eqcs.end(), func_to_eqc[f] )==eqcs.end() ){ - eqcs.push_back( func_to_eqc[f] ); - } - } - Assert(!eqcs.empty()); - //merge equivalence classes - int id = eqcs[0]; - eqc_to_quant[id].push_back( q ); - for( unsigned j=1; j >::iterator itef = eqc_to_func.find( id2 ); - if( itef!=eqc_to_func.end() ){ - for( unsigned k=0; ksecond.size(); k++ ){ - func_to_eqc[itef->second[k]] = id; - eqc_to_func[id].push_back( itef->second[k] ); - } - eqc_to_func.erase( id2 ); - } - itef = eqc_to_quant.find( id2 ); - if( itef!=eqc_to_quant.end() ){ - eqc_to_quant[id].insert( eqc_to_quant[id].end(), itef->second.begin(), itef->second.end() ); - eqc_to_quant.erase( id2 ); - } - } - } - if( eqc_to_quant.size()>1 ){ - bool addedLemma = false; - for( std::map< int, std::vector< Node > >::iterator it = eqc_to_quant.begin(); it != eqc_to_quant.end(); ++it ){ - Assert(it->second.size() < quants.size()); - bool ret = sendAntiSkolemizeLemma( it->second, false ); - addedLemma = addedLemma || ret; - } - return addedLemma; - } - } - - Trace("anti-sk") << "Anti-skolemize group : " << std::endl; - for( unsigned i=0; i outer_vars; - std::vector< Node > inner_vars; - Node q0 = quants[0]; - for (unsigned i = 0, size = d_ask_types[q0].size(); i < size; i++) - { - Node v = NodeManager::currentNM()->mkBoundVar(d_ask_types[q0][i]); - Trace("anti-sk-debug") << "Outer var " << i << " : " << v << std::endl; - outer_vars.push_back( v ); - } - - std::map< Node, Node > func_to_var; - std::vector< Node > conj; - for( unsigned i=0; i subs_lhs; - std::vector< Node > subs_rhs; - //get outer variable substitution - Assert(d_ask_types_index[q].size() == d_ask_types[q].size()); - std::vector sivars; - d_quant_sip[q].getSingleInvocationVariables(sivars); - for (unsigned j = 0, size = d_ask_types_index[q].size(); j < size; j++) - { - Trace("anti-sk-debug") - << " o_subs : " << sivars[d_ask_types_index[q][j]] << " -> " - << outer_vars[j] << std::endl; - subs_lhs.push_back(sivars[d_ask_types_index[q][j]]); - subs_rhs.push_back( outer_vars[j] ); - } - //get function substitution - std::vector funcs; - d_quant_sip[q].getFunctions(funcs); - for (const Node& f : funcs) - { - Node fv = d_quant_sip[q].getFirstOrderVariableForFunction(f); - if( func_to_var.find( f )==func_to_var.end() ){ - Node v = NodeManager::currentNM()->mkBoundVar( fv.getType() ); - Trace("anti-sk-debug") << "Inner var for " << f << " : " << v << std::endl; - inner_vars.push_back( v ); - func_to_var[f] = v; - } - subs_lhs.push_back( fv ); - subs_rhs.push_back( func_to_var[f] ); - Trace("anti-sk-debug") << " i_subs : " << fv << " -> " << func_to_var[f] << std::endl; - } - Node c = d_quant_sip[q].getSingleInvocation(); - if( !subs_lhs.empty() ){ - c = c.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() ); - } - conj.push_back( c ); - } - Node body = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( kind::AND, conj ); - if( !inner_vars.empty() ){ - Node bvl = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, inner_vars ); - body = NodeManager::currentNM()->mkNode( kind::EXISTS, bvl, body ); - } - if( !outer_vars.empty() ){ - Node bvl = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, outer_vars ); - body = NodeManager::currentNM()->mkNode( kind::FORALL, bvl, body ); - } - Trace("anti-sk") << "Produced : " << body << std::endl; - quants.push_back( body.negate() ); - Node lem = NodeManager::currentNM()->mkNode( kind::AND, quants ).negate(); - Trace("anti-sk-lemma") << "Anti-skolemize lemma : " << lem << std::endl; - quants.pop_back(); - return d_quantEngine->addLemma( lem ); - }else{ - return false; - } -} - -}/* namespace CVC4::theory::quantifiers */ -}/* namespace CVC4::theory */ -}/* namespace CVC4 */ diff --git a/src/theory/quantifiers/anti_skolem.h b/src/theory/quantifiers/anti_skolem.h deleted file mode 100644 index 21faa0361..000000000 --- a/src/theory/quantifiers/anti_skolem.h +++ /dev/null @@ -1,86 +0,0 @@ -/********************* */ -/*! \file anti_skolem.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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 - ** - ** \brief anti-skolemization - **/ - -#include "cvc4_private.h" - -#ifndef CVC4__THEORY__QUANT_ANTI_SKOLEM_H -#define CVC4__THEORY__QUANT_ANTI_SKOLEM_H - -#include -#include - -#include "context/cdhashset.h" -#include "context/cdo.h" -#include "expr/node.h" -#include "expr/type_node.h" -#include "theory/quantifiers/quant_util.h" -#include "theory/quantifiers/single_inv_partition.h" - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -class QuantAntiSkolem : public QuantifiersModule { - public: - QuantAntiSkolem(QuantifiersEngine* qe, QuantifiersState& qs); - virtual ~QuantAntiSkolem(); - - bool sendAntiSkolemizeLemma( std::vector< Node >& quants, - bool pconnected = true ); - - /* Call during quantifier engine's check */ - void check(Theory::Effort e, QEffort quant_e) override; - /* Called for new quantifiers */ - void registerQuantifier(Node q) override {} - void assertNode(Node n) override {} - /** Identify this module (for debugging, dynamic configuration, etc..) */ - std::string identify() const override { return "QuantAntiSkolem"; } - - private: - typedef context::CDHashSet NodeSet; - - std::map< Node, bool > d_quant_processed; - std::map< Node, SingleInvocationPartition > d_quant_sip; - std::map< Node, std::vector< TypeNode > > d_ask_types; - std::map< Node, std::vector< unsigned > > d_ask_types_index; - - class SkQuantTypeCache { - public: - std::map< TypeNode, SkQuantTypeCache > d_children; - std::vector< Node > d_quants; - void add( std::vector< TypeNode >& typs, Node q, unsigned index = 0 ); - void clear() { - d_children.clear(); - d_quants.clear(); - } - void sendLemmas( QuantAntiSkolem * ask ); - }; - SkQuantTypeCache d_sqtc; - - class CDSkQuantCache { - public: - CDSkQuantCache( context::Context* c ) : d_valid( c, false ){} - ~CDSkQuantCache(); - std::map< Node, CDSkQuantCache* > d_data; - context::CDO< bool > d_valid; - bool add( context::Context* c, std::vector< Node >& quants, unsigned index = 0 ); - }; - CDSkQuantCache * d_sqc; -}; /* class QuantAntiSkolem */ - -}/* namespace CVC4::theory::quantifiers */ -}/* namespace CVC4::theory */ -}/* namespace CVC4 */ - -#endif diff --git a/src/theory/quantifiers/equality_infer.cpp b/src/theory/quantifiers/equality_infer.cpp deleted file mode 100644 index 63fecdd9e..000000000 --- a/src/theory/quantifiers/equality_infer.cpp +++ /dev/null @@ -1,440 +0,0 @@ -/********************* */ -/*! \file equality_infer.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Tianyi Liang - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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 - ** - ** \brief Method for inferring equalities between arithmetic equivalence classes, - ** inspired by "A generalization of Shostak's method for combining decision procedures" Barrett et al. Figure 1. - ** - **/ - -#include "theory/quantifiers/equality_infer.h" - -#include "context/context_mm.h" -#include "theory/rewriter.h" -#include "theory/arith/arith_msum.h" - -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; -using namespace std; - -namespace CVC4 { - -EqualityInference::EqcInfo::EqcInfo(context::Context* c) : d_rep( c ), d_valid( c, false ), d_solved( c, false ), d_master(c) -//, d_rep_exp(c), d_uselist(c) -{ - -} - -EqualityInference::EqualityInference( context::Context* c, bool trackExp ) : -d_c( c ), d_trackExplain( trackExp ), d_elim_vars( c ), -d_rep_to_eqc( c ), d_rep_exp( c ), d_uselist( c ), d_pending_merges( c ), d_pending_merge_exp( c ){ - d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); - d_true = NodeManager::currentNM()->mkConst( true ); -} - -EqualityInference::~EqualityInference(){ - for( std::map< Node, EqcInfo * >::iterator it = d_eqci.begin(); it != d_eqci.end(); ++it ){ - delete it->second; - } -} - -void EqualityInference::addToExplanation( std::vector< Node >& exp, Node e ) { - if( std::find( exp.begin(), exp.end(), e )==exp.end() ){ - Trace("eq-infer-debug2") << "......add to explanation " << e << std::endl; - exp.push_back( e ); - } -} - -void EqualityInference::addToExplanationEqc( std::vector< Node >& exp, Node eqc ) { - NodeIntMap::iterator re_i = d_rep_exp.find( eqc ); - if( re_i!=d_rep_exp.end() ){ - for( int i=0; i<(*re_i).second; i++ ){ - addToExplanation( exp, d_rep_exp_data[eqc][i] ); - } - } - //for( unsigned i=0; id_rep_exp.size(); i++ ){ - // addToExplanation( exp, d_eqci[n]->d_rep_exp[i] ); - //} -} - -void EqualityInference::addToExplanationEqc( Node eqc, std::vector< Node >& exp_to_add ) { - NodeIntMap::iterator re_i = d_rep_exp.find( eqc ); - int n_re = 0; - if( re_i != d_rep_exp.end() ){ - n_re = (*re_i).second; - } - d_rep_exp[eqc] = n_re + exp_to_add.size(); - for( unsigned i=0; id_rep_exp.push_back( exp_to_add[i] ); - //} -} - -Node EqualityInference::getMaster( Node t, EqcInfo * eqc, bool& updated, Node new_m ) { - if( !eqc->d_master.get().isNull() ){ - if( eqc->d_master.get()==t ){ - if( !new_m.isNull() && t!=new_m ){ - eqc->d_master = new_m; - updated = true; - return new_m; - }else{ - return t; - } - }else{ - Assert(d_eqci.find(eqc->d_master.get()) != d_eqci.end()); - EqcInfo * eqc_m = d_eqci[eqc->d_master.get()]; - Node m = getMaster( eqc->d_master.get(), eqc_m, updated, new_m ); - eqc->d_master = m; - return m; - } - }else{ - return Node::null(); - } -} - -//update the internal "master" representative of the equivalence class, return true if the merge was non-redundant -bool EqualityInference::updateMaster( Node t1, Node t2, EqcInfo * eqc1, EqcInfo * eqc2 ) { - bool updated = false; - Node m1 = getMaster( t1, eqc1, updated ); - if( m1.isNull() ){ - eqc1->d_master = t2; - if( eqc2->d_master.get().isNull() ){ - eqc2->d_master = t2; - } - return true; - }else{ - updated = false; - Node m2 = getMaster( t2, eqc2, updated, m1); - if( m2.isNull() ){ - eqc2->d_master = m1; - return true; - }else{ - return updated; - } - } -} - -void EqualityInference::eqNotifyNewClass(TNode t) { - if( t.getType().isReal() ){ - Trace("eq-infer") << "Notify equivalence class : " << t << std::endl; - EqcInfo * eqci; - std::map< Node, EqcInfo * >::iterator itec = d_eqci.find( t ); - if( itec==d_eqci.end() ){ - eqci = new EqcInfo( d_c ); - d_eqci[t] = eqci; - }else{ - eqci = itec->second; - } - Assert(!eqci->d_valid.get()); - if( !eqci->d_solved.get() ){ - //somewhat strange: t may not be in rewritten form - Node r = Rewriter::rewrite( t ); - std::map< Node, Node > msum; - if (ArithMSum::getMonomialSum(r, msum)) - { - Trace("eq-infer-debug2") << "...process monomial sum, size = " << msum.size() << std::endl; - eqci->d_valid = true; - bool changed = false; - std::vector< Node > exp; - std::vector< Node > children; - for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ) { - Trace("eq-infer-debug2") << "...process child " << it->first << ", " << it->second << std::endl; - if( !it->first.isNull() ){ - Node n = it->first; - BoolMap::const_iterator itv = d_elim_vars.find( n ); - if( itv!=d_elim_vars.end() ){ - changed = true; - Assert(d_eqci.find(n) != d_eqci.end()); - Assert(n != t); - Assert(d_eqci[n]->d_solved.get()); - Trace("eq-infer-debug2") << "......its solved form is " << d_eqci[n]->d_rep.get() << std::endl; - if( d_trackExplain ){ - //track the explanation: justified by explanation for each substitution - addToExplanationEqc( exp, n ); - } - n = d_eqci[n]->d_rep; - Assert(!n.isNull()); - } - if( it->second.isNull() ){ - children.push_back( n ); - }else{ - children.push_back( NodeManager::currentNM()->mkNode( MULT, it->second, n ) ); - } - }else{ - Assert(!it->second.isNull()); - children.push_back( it->second ); - } - } - Trace("eq-infer-debug2") << "...children size = " << children.size() << std::endl; - bool mvalid = true; - if( changed ){ - r = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( PLUS, children ); - Trace("eq-infer-debug2") << "...pre-rewrite : " << r << std::endl; - r = Rewriter::rewrite( r ); - msum.clear(); - if (!ArithMSum::getMonomialSum(r, msum)) - { - mvalid = false; - } - } - Trace("eq-infer") << "...value is " << r << std::endl; - setEqcRep( t, r, exp, eqci ); - if( mvalid ){ - for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ - if( !it->first.isNull() ){ - addToUseList( it->first, t ); - } - } - } - }else{ - eqci->d_valid = false; - } - } - } -} - -void EqualityInference::addToUseList( Node used, Node eqc ) { -#if 1 - NodeIntMap::iterator ul_i = d_uselist.find( used ); - int n_ul = 0; - if( ul_i != d_uselist.end() ){ - n_ul = (*ul_i).second; - } - d_uselist[ used ] = n_ul + 1; - Trace("eq-infer-debug") << " add to use list : " << used << " -> " << eqc << std::endl; - if( n_ul<(int)d_uselist_data[used].size() ){ - d_uselist_data[used][n_ul] = eqc; - }else{ - d_uselist_data[used].push_back( eqc ); - } -#else - std::map< Node, EqcInfo * >::iterator itu = d_eqci.find( used ); - EqcInfo * eqci_used; - if( itu==d_eqci.end() ){ - eqci_used = new EqcInfo( d_c ); - d_eqci[used] = eqci_used; - }else{ - eqci_used = itu->second; - } - Trace("eq-infer-debug") << " add to use list : " << used << " -> " << eqc << std::endl; - eqci_used->d_uselist.push_back( eqc ); -#endif -} - -void EqualityInference::setEqcRep( Node t, Node r, std::vector< Node >& exp_to_add, EqcInfo * eqci ) { - eqci->d_rep = r; - if( d_trackExplain ){ - addToExplanationEqc( t, exp_to_add ); - } - //if this is an active equivalence class - if( eqci->d_valid.get() ){ - Trace("eq-infer-debug") << "Set eqc rep " << t << " -> " << r << std::endl; - NodeMap::const_iterator itr = d_rep_to_eqc.find( r ); - if( itr==d_rep_to_eqc.end() ){ - d_rep_to_eqc[r] = t; - }else{ - //merge two equivalence classes - Node t2 = (*itr).second; - //check if it is valid - std::map< Node, EqcInfo * >::iterator itc = d_eqci.find( t2 ); - if( itc!=d_eqci.end() && itc->second->d_valid.get() ){ - //if we haven't already determined they should be merged - if( updateMaster( t, t2, eqci, itc->second ) ){ - Trace("eq-infer") << "Infer two equivalence classes are equal : " << t << " " << t2 << std::endl; - Trace("eq-infer") << " since they both normalize to : " << r << std::endl; - d_pending_merges.push_back( t.eqNode( t2 ) ); - if( d_trackExplain ){ - std::vector< Node > exp; - for( unsigned j=0; j<2; j++ ){ - addToExplanationEqc( exp, j==0 ? t : t2 ); - } - Node exp_n = exp.empty() ? d_true : ( exp.size()==1 ? exp[0] : NodeManager::currentNM()->mkNode( AND, exp ) ); - Trace("eq-infer") << " explanation : " << exp_n << std::endl; - d_pending_merge_exp.push_back( exp_n ); - } - } - } - } - } -} - -void EqualityInference::eqNotifyMerge(TNode t1, TNode t2) { - Assert(!t1.isNull()); - Assert(!t2.isNull()); - std::map< Node, EqcInfo * >::iterator itv1 = d_eqci.find( t1 ); - if( itv1!=d_eqci.end() ){ - std::map< Node, EqcInfo * >::iterator itv2 = d_eqci.find( t2 ); - if( itv2!=d_eqci.end() ){ - Trace("eq-infer") << "Merge equivalence classes : " << t2 << " into " << t1 << std::endl; - Node tr1 = itv1->second->d_rep; - Node tr2 = itv2->second->d_rep; - itv2->second->d_valid = false; - Trace("eq-infer") << "Representatives : " << tr2 << " into " << tr1 << std::endl; - if( tr1!=tr2 ){ - Node eq = tr1.eqNode( tr2 ); - std::map< Node, Node > msum; - if (ArithMSum::getMonomialSumLit(eq, msum)) - { - Node v_solve; - //solve for variables with no coefficient - if( Trace.isOn("eq-infer-debug2") ){ - Trace("eq-infer-debug2") << "Monomial sum : " << std::endl; - for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ) { - Trace("eq-infer-debug2") << " " << it->first << " * " << it->second << std::endl; - } - } - for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ) { - Node n = it->first; - if( !n.isNull() ){ - bool canSolve = false; - if( it->second.isNull() ){ - canSolve = true; - }else{ - //Assert( it->second.isConst() ); - Rational r = it->second.getConst(); - canSolve = r.isOne() || r.isNegativeOne(); - } - if( canSolve ){ - v_solve = n; - break; - } - } - } - Trace("eq-infer-debug") << "solve for variable : " << v_solve << std::endl; - if( !v_solve.isNull() ){ - //solve for v_solve - Node veq; - if (ArithMSum::isolate(v_solve, msum, veq, kind::EQUAL, true) == 1) - { - Node v_value = veq[1]; - Trace("eq-infer") << "...solved " << v_solve << " == " << v_value << std::endl; - Assert(d_elim_vars.find(v_solve) == d_elim_vars.end()); - d_elim_vars[v_solve] = true; - //store value in eqc info - EqcInfo * eqci_solved; - std::map< Node, EqcInfo * >::iterator itec = d_eqci.find( v_solve ); - if( itec==d_eqci.end() ){ - eqci_solved = new EqcInfo( d_c ); - d_eqci[v_solve] = eqci_solved; - }else{ - eqci_solved = itec->second; - } - eqci_solved->d_solved = true; - eqci_solved->d_rep = v_value; - //track the explanation - std::vector< Node > exp; - if( d_trackExplain ){ - //explanation is t1 = t2 + their explanations - exp.push_back( t1.eqNode( t2 ) ); - for( unsigned i=0; i<2; i++ ){ - addToExplanationEqc( exp, i==0 ? t1 : t2 ); - } - if( Trace.isOn("eq-infer-debug") ){ - Trace("eq-infer-debug") << " explanation for solving " << v_solve << " is "; - for( unsigned i=0; i new_use; - for( std::map< Node, Node >::iterator itmm = msum.begin(); itmm != msum.end(); ++itmm ){ - Node n = itmm->first; - if( !n.isNull() && n!=v_solve ){ - new_use.push_back( n ); - addToUseList( n, v_solve ); - } - } - - //go through all equivalence classes that may refer to v_solve - std::map< Node, bool > processed; - processed[v_solve] = true; - NodeIntMap::iterator ul_i = d_uselist.find( v_solve ); - if( ul_i != d_uselist.end() ){ - int n_ul = (*ul_i).second; - Trace("eq-infer-debug") << " use list size = " << n_ul << std::endl; - for( int j=0; jfirst << " => " << rr << std::endl; - setEqcRep( itt->first, rr, exp, itt->second ); - //update use list - for( unsigned i=0; isecond->d_valid = false; - } - } - } - } - } - Trace("eq-infer") << "...finished solved." << std::endl; - } - } - } - } - }else{ - //no information to merge - } - }else{ - //carry information (this might happen for non-linear t1 and linear t2?) - std::map< Node, EqcInfo * >::iterator itv2 = d_eqci.find( t2 ); - if( itv2!=d_eqci.end() ){ - d_eqci[t1] = d_eqci[t2]; - d_eqci[t2] = NULL; - } - } -} - -Node EqualityInference::getPendingMergeExplanation( unsigned i ) { - if( d_trackExplain ){ - return d_pending_merge_exp[i]; - }else{ - return d_pending_merges[i]; - } -} - -} diff --git a/src/theory/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h deleted file mode 100644 index fed458ade..000000000 --- a/src/theory/quantifiers/equality_infer.h +++ /dev/null @@ -1,103 +0,0 @@ -/********************* */ -/*! \file equality_infer.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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 - ** - ** \brief additional inference for equalities - **/ - -#include "cvc4_private.h" - -#ifndef CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H -#define CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H - -#include -#include -#include - -#include "context/cdhashmap.h" -#include "context/cdhashset.h" -#include "context/context.h" -#include "context/context_mm.h" -#include "theory/theory.h" - - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -class EqualityInference -{ - typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap; - typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; - typedef context::CDList NodeList; - typedef context::CDHashMap< Node, int, NodeHashFunction > NodeIntMap; -private: - context::Context * d_c; - Node d_one; - Node d_true; - class EqcInfo { - public: - EqcInfo(context::Context* c); - ~EqcInfo(){} - context::CDO< Node > d_rep; - //whether the eqc of this info is a representative and d_rep can been computed successfully - context::CDO< bool > d_valid; - //whether the eqc of this info is a solved variable - context::CDO< bool > d_solved; - //master equivalence class (a union find) - context::CDO< Node > d_master; - //a vector of equalities t1=t2 for which eqNotifyMerge(t1,t2) was called that explains d_rep - //NodeList d_rep_exp; - //the list of other eqc where this variable may be appear - //NodeList d_uselist; - }; - - /** track explanations */ - bool d_trackExplain; - /** information necessary for equivalence classes */ - BoolMap d_elim_vars; - std::map< Node, EqcInfo * > d_eqci; - NodeMap d_rep_to_eqc; - NodeIntMap d_rep_exp; - std::map< Node, std::vector< Node > > d_rep_exp_data; - /** set eqc rep */ - void setEqcRep( Node t, Node r, std::vector< Node >& exp_to_add, EqcInfo * eqci ); - /** use list */ - NodeIntMap d_uselist; - std::map< Node, std::vector< Node > > d_uselist_data; - void addToUseList( Node used, Node eqc ); - /** pending merges */ - NodeList d_pending_merges; - NodeList d_pending_merge_exp; - /** add to explanation */ - void addToExplanation( std::vector< Node >& exp, Node e ); - void addToExplanationEqc( std::vector< Node >& exp, Node eqc ); - void addToExplanationEqc( Node eqc, std::vector< Node >& exp_to_add ); - /** for setting master/slave */ - Node getMaster( Node t, EqcInfo * eqc, bool& updated, Node new_m = Node::null() ); - bool updateMaster( Node t1, Node t2, EqcInfo * eqc1, EqcInfo * eqc2 ); -public: - //second argument is whether explanations should be tracked - EqualityInference(context::Context* c, bool trackExp = false); - virtual ~EqualityInference(); - /** input : notification when equality engine is updated */ - void eqNotifyNewClass(TNode t); - void eqNotifyMerge(TNode t1, TNode t2); - /** output : inferred equalities */ - unsigned getNumPendingMerges() { return d_pending_merges.size(); } - Node getPendingMerge( unsigned i ) { return d_pending_merges[i]; } - Node getPendingMergeExplanation( unsigned i ); -}; - -} -} -} - -#endif diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index 3887c583b..b8515df91 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -15,7 +15,6 @@ #include "theory/quantifiers/equality_query.h" #include "options/quantifiers_options.h" -#include "theory/quantifiers/equality_infer.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp index d8b4062fc..719cc3de1 100644 --- a/src/theory/quantifiers/quantifiers_modules.cpp +++ b/src/theory/quantifiers/quantifiers_modules.cpp @@ -33,7 +33,6 @@ QuantifiersModules::QuantifiersModules() d_fs(nullptr), d_i_cbqi(nullptr), d_qsplit(nullptr), - d_anti_skolem(nullptr), d_sygus_inst(nullptr) { } @@ -85,11 +84,6 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe, d_qsplit.reset(new QuantDSplit(qe, qs)); modules.push_back(d_qsplit.get()); } - if (options::quantAntiSkolem()) - { - d_anti_skolem.reset(new QuantAntiSkolem(qe, qs)); - modules.push_back(d_anti_skolem.get()); - } if (options::quantAlphaEquiv()) { d_alpha_equiv.reset(new AlphaEquivalence(qe)); diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h index e83a13ea7..5aa8cf1d5 100644 --- a/src/theory/quantifiers/quantifiers_modules.h +++ b/src/theory/quantifiers/quantifiers_modules.h @@ -18,7 +18,6 @@ #define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H #include "theory/quantifiers/alpha_equivalence.h" -#include "theory/quantifiers/anti_skolem.h" #include "theory/quantifiers/conjecture_generator.h" #include "theory/quantifiers/ematching/instantiation_engine.h" #include "theory/quantifiers/fmf/bounded_integers.h" @@ -81,8 +80,6 @@ class QuantifiersModules std::unique_ptr d_i_cbqi; /** quantifiers splitting */ std::unique_ptr d_qsplit; - /** quantifiers anti-skolemization */ - std::unique_ptr d_anti_skolem; /** SyGuS instantiation engine */ std::unique_ptr d_sygus_inst; }; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index ad066cf1e..52bdd6854 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1695,7 +1695,6 @@ set(regress_1_tests regress1/quantifiers/RNDPRE_4_1-dd-nqe.smt2 regress1/quantifiers/RND_4_1-existing-inst.smt2 regress1/quantifiers/RND_4_16.smt2 - regress1/quantifiers/anti-sk-simp.smt2 regress1/quantifiers/ari118-bv-2occ-x.smt2 regress1/quantifiers/arith-rec-fun.smt2 regress1/quantifiers/array-unsat-simp3.smt2 @@ -2488,6 +2487,8 @@ set(regression_disabled_tests regress1/nl/NAVIGATION2.smt2 # sat or unknown in different builds regress1/nl/issue3307.smt2 + # slow with sygus-inference after removing anti-skolemization + regress1/quantifiers/anti-sk-simp.smt2 # no longer support snorm option regress1/quantifiers/arith-snorm.smt2 # ajreynol: different error messages on production and debug: diff --git a/test/regress/regress1/quantifiers/anti-sk-simp.smt2 b/test/regress/regress1/quantifiers/anti-sk-simp.smt2 index a5f576f86..a9f06d8f0 100644 --- a/test/regress/regress1/quantifiers/anti-sk-simp.smt2 +++ b/test/regress/regress1/quantifiers/anti-sk-simp.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi --quant-anti-skolem +; COMMAND-LINE: --sygus-inference ; EXPECT: unsat (set-logic ALL_SUPPORTED) (set-info :status unsat)