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
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
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]]
+++ /dev/null
-/********************* */
-/*! \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 )<d_tu->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; i<d_quantEngine->getModel()->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<Node> 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<d_ask_types[q].size(); ){
- TypeNode curr = d_ask_types[q][j];
- for( unsigned k=0; k<indices[curr].size(); k++ ){
- Assert(d_ask_types[q][j] == curr);
- d_ask_types_index[q].push_back( indices[curr][k] );
- j++;
- }
- }
- Assert(d_ask_types_index[q].size() == d_ask_types[q].size());
- }else{
- d_quant_sip.erase( q );
- }
- }
- //now, activate the quantified formula
- std::map< Node, std::vector< TypeNode > >::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<quants.size(); i++ ){
- Node q = quants[i];
- std::vector< int > eqcs;
- std::vector<Node> 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<eqcs.size(); j++ ){
- int id2 = eqcs[j];
- std::map< int, std::vector< Node > >::iterator itef = eqc_to_func.find( id2 );
- if( itef!=eqc_to_func.end() ){
- for( unsigned k=0; k<itef->second.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<quants.size(); i++ ){
- Trace("anti-sk") << " " << quants[i] << std::endl;
- }
-
- std::vector< Node > 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<quants.size(); i++ ){
- Node q = quants[i];
- Trace("anti-sk-debug") << "Process " << q << std::endl;
- std::vector< Node > 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<Node> 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<Node> 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 */
+++ /dev/null
-/********************* */
-/*! \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 <map>
-#include <vector>
-
-#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<Node, NodeHashFunction> 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
+++ /dev/null
-/********************* */
-/*! \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; i<d_eqci[n]->d_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; i<exp_to_add.size(); i++ ){
- if( n_re<(int)d_rep_exp_data[eqc].size() ){
- d_rep_exp_data[eqc][n_re] = exp_to_add[i];
- }else{
- d_rep_exp_data[eqc].push_back( exp_to_add[i] );
- }
- n_re++;
- }
- //for( unsigned i=0; i<exp_to_add.size(); i++ ){
- // eqci->d_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<Rational>();
- 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<exp.size(); i++ ){
- Trace("eq-infer-debug") << exp[i] << " ";
- }
- Trace("eq-infer-debug") << std::endl;
- }
- addToExplanationEqc( v_solve, exp );
- }
-
- std::vector< Node > 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; j<n_ul; j++ ){
- Node r = d_uselist_data[v_solve][j];
- //Trace("eq-infer-debug") << " use list size = " << eqci_solved->d_uselist.size() << std::endl;
- //for( unsigned j=0; j<eqci_solved->d_uselist.size(); j++ ){
- // Node r = eqci_solved->d_uselist[j];
- if( processed.find( r )==processed.end() ){
- processed[r] = true;
- std::map< Node, EqcInfo * >::iterator itt = d_eqci.find( r );
- if( itt!=d_eqci.end() && ( itt->second->d_valid || itt->second->d_solved ) ){
- std::map< Node, Node > msum2;
- if (ArithMSum::getMonomialSum(itt->second->d_rep.get(),
- msum2))
- {
- std::map< Node, Node >::iterator itm = msum2.find( v_solve );
- if( itm!=msum2.end() ){
- //substitute in solved form
- std::map< Node, Node >::iterator itm2 = msum2.find( v_value );
- if( itm2 == msum2.end() ){
- msum2[v_value] = itm->second;
- }else{
- msum2[v_value] = NodeManager::currentNM()->mkNode( PLUS, itm2->second.isNull() ? d_one : itm2->second,
- itm->second.isNull() ? d_one : itm->second );
- }
- msum2.erase( itm );
- Node rr = ArithMSum::mkNode(msum2);
- rr = Rewriter::rewrite( rr );
- Trace("eq-infer") << "......update " << itt->first << " => " << rr << std::endl;
- setEqcRep( itt->first, rr, exp, itt->second );
- //update use list
- for( unsigned i=0; i<new_use.size(); i++ ){
- addToUseList( new_use[i], r );
- }
- }
- }else{
- itt->second->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];
- }
-}
-
-}
+++ /dev/null
-/********************* */
-/*! \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 <iostream>
-#include <map>
-#include <vector>
-
-#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<Node> 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
#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"
d_fs(nullptr),
d_i_cbqi(nullptr),
d_qsplit(nullptr),
- d_anti_skolem(nullptr),
d_sygus_inst(nullptr)
{
}
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));
#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"
std::unique_ptr<InstStrategyCegqi> d_i_cbqi;
/** quantifiers splitting */
std::unique_ptr<QuantDSplit> d_qsplit;
- /** quantifiers anti-skolemization */
- std::unique_ptr<QuantAntiSkolem> d_anti_skolem;
/** SyGuS instantiation engine */
std::unique_ptr<SygusInst> d_sygus_inst;
};
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
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:
-; COMMAND-LINE: --cegqi --quant-anti-skolem
+; COMMAND-LINE: --sygus-inference
; EXPECT: unsat
(set-logic ALL_SUPPORTED)
(set-info :status unsat)
projects / cvc5.git / commitdiff