From a401cd2deb921c3499d8fdbe0d14cfee67c92737 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 29 Jun 2015 13:30:44 +0200 Subject: [PATCH] Module to infer alpha equivalence of quantified formulas. Minor clean up of options. --- src/Makefile.am | 4 +- src/smt/smt_engine.cpp | 14 +- src/theory/datatypes/datatypes_sygus.cpp | 10 +- src/theory/quantifiers/alpha_equivalence.cpp | 105 +++++++++++ src/theory/quantifiers/alpha_equivalence.h | 57 ++++++ .../quantifiers/ce_guided_single_inv_sol.cpp | 6 +- .../quantifiers/conjecture_generator.cpp | 95 ++++------ src/theory/quantifiers/conjecture_generator.h | 7 +- .../quantifiers/first_order_reasoning.cpp | 175 ------------------ .../quantifiers/first_order_reasoning.h | 49 ----- src/theory/quantifiers/options | 12 +- src/theory/quantifiers/term_database.cpp | 154 +++++++++++++-- src/theory/quantifiers/term_database.h | 38 +++- src/theory/quantifiers_engine.cpp | 94 +++++++--- src/theory/quantifiers_engine.h | 12 +- 15 files changed, 464 insertions(+), 368 deletions(-) create mode 100755 src/theory/quantifiers/alpha_equivalence.cpp create mode 100755 src/theory/quantifiers/alpha_equivalence.h delete mode 100644 src/theory/quantifiers/first_order_reasoning.cpp delete mode 100644 src/theory/quantifiers/first_order_reasoning.h diff --git a/src/Makefile.am b/src/Makefile.am index 60f3bc7c2..16ac45de2 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -311,8 +311,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/full_model_check.cpp \ theory/quantifiers/bounded_integers.h \ theory/quantifiers/bounded_integers.cpp \ - theory/quantifiers/first_order_reasoning.h \ - theory/quantifiers/first_order_reasoning.cpp \ + theory/quantifiers/alpha_equivalence.h \ + theory/quantifiers/alpha_equivalence.cpp \ theory/quantifiers/rewrite_engine.h \ theory/quantifiers/rewrite_engine.cpp \ theory/quantifiers/relevant_domain.h \ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 55e83ee14..6fdfadbd3 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -82,10 +82,8 @@ #include "prop/options.h" #include "theory/arrays/options.h" #include "util/sort_inference.h" -#include "theory/quantifiers/quant_conflict_find.h" #include "theory/quantifiers/macros.h" #include "theory/quantifiers/fun_def_process.h" -#include "theory/quantifiers/first_order_reasoning.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/options.h" #include "theory/datatypes/options.h" @@ -1496,8 +1494,8 @@ void SmtEngine::setDefaults() { if( !options::preSkolemQuantNested.wasSetByUser() ){ options::preSkolemQuantNested.set( false ); } - } - + } + //until bugs 371,431 are fixed if( ! options::minisatUseElim.wasSetByUser()){ if( d_logic.isQuantified() || options::produceModels() || options::produceAssignments() || options::checkModels() ){ @@ -3282,16 +3280,12 @@ void SmtEnginePrivate::processAssertions() { success = qm.simplify( d_assertions.ref(), true ); }while( success ); } + + //fmf-fun : assume admissible functions, applying preprocessing reduction to FMF if( options::fmfFunWellDefined() ){ quantifiers::FunDefFmf fdf; fdf.simplify( d_assertions.ref() ); } - - Trace("fo-rsn-enable") << std::endl; - if( options::foPropQuant() ){ - quantifiers::FirstOrderPropagation fop; - fop.simplify( d_assertions.ref() ); - } } if( options::sortInference() ){ diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 851f97624..a8121b67d 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -88,7 +88,7 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node > Kind k = d_tds->getArgKind( tnnp, csIndex ); //size comparison for arguments (if necessary) Node sz_leq; - if( tn1==tnn && d_tds->isComm( k ) ){ + if( tn1==tnn && quantifiers::TermDb::isComm( k ) ){ sz_leq = NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkNode( DT_SIZE, n ), NodeManager::currentNM()->mkNode( DT_SIZE, arg1 ) ); } std::map< int, std::vector< int > >::iterator it = d_sygus_pc_arg_pos[tnn][csIndex].find( i ); @@ -327,7 +327,7 @@ void SygusSplit::registerSygusTypeConstructorArg( TypeNode tnn, const Datatype& Assert( d_sygus_pc_nred[tnn][csIndex].find( sIndex )!=d_sygus_pc_nred[tnn][csIndex].end() ); Assert( d_sygus_pc_nred[tnno][csIndex].find( osIndex )!=d_sygus_pc_nred[tnno][csIndex].end() ); - bool isPComm = d_tds->isComm( parentKind ); + bool isPComm = quantifiers::TermDb::isComm( parentKind ); std::map< int, bool > larg_consider; for( unsigned i=0; igetKindArg( tnp, parent ); if( k==parent ){ //check for associativity - if( d_tds->isAssoc( k ) ){ + if( quantifiers::TermDb::isAssoc( k ) ){ //if the operator is associative, then a repeated occurrence should only occur in the leftmost argument position int firstArg = getFirstArgOccurrence( pdt[pc], dt ); Assert( firstArg!=-1 ); @@ -511,8 +511,8 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt } } if( parent==MINUS || parent==BITVECTOR_SUB ){ - - + + } return true; } diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp new file mode 100755 index 000000000..e4dcccdff --- /dev/null +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -0,0 +1,105 @@ +/********************* */ +/*! \file alpha_equivalence.cpp + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2015 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Alpha equivalence checking + ** + **/ + +#include "theory/quantifiers/alpha_equivalence.h" +#include "theory/quantifiers/term_database.h" + +using namespace CVC4; +using namespace std; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; +using namespace CVC4::kind; + +struct sortTypeOrder { + TermDb* d_tdb; + bool operator() (TypeNode i, TypeNode j) { + return d_tdb->getIdForType( i )getIdForType( j ); + } +}; + +bool AlphaEquivalenceNode::registerNode( QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ) { + if( tt.size()==arg_index.size()+1 ){ + Node t = tt.back(); + Node op = t.hasOperator() ? t.getOperator() : t; + arg_index.push_back( 0 ); + Trace("aeq-debug") << op << " "; + return d_children[op][t.getNumChildren()].registerNode( qe, q, tt, arg_index ); + }else if( tt.empty() ){ + //we are finished + Trace("aeq-debug") << std::endl; + if( d_quant.isNull() ){ + d_quant = q; + return true; + }else{ + //lemma ( q <=> d_quant ) + Trace("alpha-eq") << "Alpha equivalent : " << std::endl; + Trace("alpha-eq") << " " << q << std::endl; + Trace("alpha-eq") << " " << d_quant << std::endl; + qe->getOutputChannel().lemma( q.iffNode( d_quant ) ); + return false; + } + }else{ + Node t = tt.back(); + int i = arg_index.back(); + if( i==(int)t.getNumChildren() ){ + tt.pop_back(); + arg_index.pop_back(); + }else{ + tt.push_back( t[i] ); + arg_index[arg_index.size()-1]++; + } + return registerNode( qe, q, tt, arg_index ); + } +} + +bool AlphaEquivalenceTypeNode::registerNode( QuantifiersEngine* qe, Node q, Node t, std::vector< TypeNode >& typs, std::map< TypeNode, int >& typ_count, int index ){ + if( index==(int)typs.size() ){ + std::vector< Node > tt; + std::vector< int > arg_index; + tt.push_back( t ); + Trace("aeq-debug") << " : "; + return d_data.registerNode( qe, q, tt, arg_index ); + }else{ + TypeNode curr = typs[index]; + Assert( typ_count.find( curr )!=typ_count.end() ); + Trace("aeq-debug") << "[" << curr << " " << typ_count[curr] << "] "; + return d_children[curr][typ_count[curr]].registerNode( qe, q, t, typs, typ_count, index+1 ); + } +} + +bool AlphaEquivalence::registerQuantifier( Node q ) { + Assert( q.getKind()==FORALL ); + Trace("aeq") << "Alpha equivalence : register " << q << std::endl; + //construct canonical quantified formula + Node t = d_qe->getTermDatabase()->getCanonicalTerm( q[1], true ); + Trace("aeq") << " canonical form: " << t << std::endl; + //compute variable type counts + std::map< TypeNode, int > typ_count; + std::vector< TypeNode > typs; + for( unsigned i=0; igetTermDatabase(); + std::sort( typs.begin(), typs.end(), sto ); + Trace("aeq-debug") << " "; + bool ret = d_ae_typ_trie.registerNode( d_qe, q, t, typs, typ_count ); + Trace("aeq") << " ...result : " << ret << std::endl; + return ret; +} diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h new file mode 100755 index 000000000..fa2109ccc --- /dev/null +++ b/src/theory/quantifiers/alpha_equivalence.h @@ -0,0 +1,57 @@ +/********************* */ +/*! \file alpha_equivalence.h + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2015 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Alpha equivalence checking + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__ALPHA_EQUIVALENCE_H +#define __CVC4__ALPHA_EQUIVALENCE_H + + +#include "theory/quantifiers_engine.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class AlphaEquivalenceNode { +public: + std::map< Node, std::map< int, AlphaEquivalenceNode > > d_children; + Node d_quant; + bool registerNode( QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ); +}; + +class AlphaEquivalenceTypeNode { +public: + std::map< TypeNode, std::map< int, AlphaEquivalenceTypeNode > > d_children; + AlphaEquivalenceNode d_data; + bool registerNode( QuantifiersEngine* qe, Node q, Node t, std::vector< TypeNode >& typs, std::map< TypeNode, int >& typ_count, int index = 0 ); +}; + +class AlphaEquivalence { +private: + QuantifiersEngine* d_qe; + //per # of variables per type + AlphaEquivalenceTypeNode d_ae_typ_trie; +public: + AlphaEquivalence( QuantifiersEngine* qe ) : d_qe( qe ){} + ~AlphaEquivalence(){} + + bool registerQuantifier( Node q ); +}; + +} +} +} + +#endif diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp index 845e20795..0429abac9 100644 --- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp @@ -309,7 +309,7 @@ Node CegConjectureSingleInvSol::simplifySolution( Node sol, TypeNode stn ){ } Node sol0 = Rewriter::rewrite( sol ); Trace("csi-sol") << "now : " << sol0 << std::endl; - + Node curr_sol = sol0; Node prev_sol; do{ @@ -359,7 +359,7 @@ Node CegConjectureSingleInvSol::simplifySolution( Node sol, TypeNode stn ){ curr_sol = sol4; } }while( curr_sol!=prev_sol ); - + return curr_sol; } @@ -726,7 +726,7 @@ int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, in if( karg!=-1 ){ //collect the children of min_t std::vector< Node > tchildren; - if( min_t.getNumChildren()>dt[karg].getNumArgs() && d_qe->getTermDatabaseSygus()->isAssoc( min_t.getKind() ) && dt[karg].getNumArgs()==2 ){ + if( min_t.getNumChildren()>dt[karg].getNumArgs() && quantifiers::TermDb::isAssoc( min_t.getKind() ) && dt[karg].getNumArgs()==2 ){ tchildren.push_back( min_t[0] ); std::vector< Node > rem_children; for( unsigned i=1; imkBoundVar( os.str().c_str(), tn ); - d_free_var_num[x] = d_free_var[tn].size(); - d_free_var[tn].push_back( x ); - } - return d_free_var[tn][i]; -} - - - -Node ConjectureGenerator::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs ) { - if( n.getKind()==BOUND_VARIABLE ){ - std::map< TNode, TNode >::iterator it = subs.find( n ); - if( it==subs.end() ){ - TypeNode tn = n.getType(); - //allocate variable - unsigned vn = var_count[tn]; - var_count[tn]++; - subs[n] = getFreeVar( tn, vn ); - return subs[n]; - }else{ - return it->second; - } - }else{ - std::vector< Node > children; - if( n.getKind()!=EQUAL ){ - if( n.hasOperator() ){ - TNode op = n.getOperator(); - if( !d_tge.isRelevantFunc( op ) ){ - return Node::null(); - } - children.push_back( op ); - }else{ - return Node::null(); - } - } - for( unsigned i=0; imkNode( n.getKind(), children ); - } + return d_quantEngine->getTermDatabase()->getCanonicalFreeVar( tn, i ); } bool ConjectureGenerator::isHandledTerm( TNode n ){ @@ -555,11 +501,14 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { TNode nr = q[1][r==0 ? 1 : 0]; Node eq = nl.eqNode( nr ); if( r==1 || std::find( d_conjectures.begin(), d_conjectures.end(), q )==d_conjectures.end() ){ - //must make it canonical - std::map< TypeNode, unsigned > var_count; - std::map< TNode, TNode > subs; - Trace("sg-proc-debug") << "get canonical " << eq << std::endl; - eq = getCanonicalTerm( eq, var_count, subs ); + //check if it contains only relevant functions + if( d_tge.isRelevantTerm( eq ) ){ + //make it canonical + Trace("sg-proc-debug") << "get canonical " << eq << std::endl; + eq = d_quantEngine->getTermDatabase()->getCanonicalTerm( eq ); + }else{ + eq = Node::null(); + } } if( !eq.isNull() ){ if( r==0 ){ @@ -697,7 +646,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { typ_to_subs_index[it->first] = sum; sum += it->second; for( unsigned i=0; isecond; i++ ){ - gsubs_vars.push_back( getFreeVar( it->first, i ) ); + gsubs_vars.push_back( d_quantEngine->getTermDatabase()->getCanonicalFreeVar( it->first, i ) ); } } } @@ -993,7 +942,7 @@ unsigned ConjectureGenerator::collectFunctions( TNode opat, TNode pat, std::map< }else{ //check for max/min TypeNode tn = pat.getType(); - unsigned vn = d_free_var_num[pat]; + unsigned vn = pat.getAttribute(InstVarNumAttribute()); std::map< TypeNode, unsigned >::iterator it = mnvn.find( tn ); if( it!=mnvn.end() ){ if( vnsecond ){ @@ -2012,6 +1961,28 @@ bool TermGenEnv::considerCurrentTermCanon( unsigned tg_id ){ bool TermGenEnv::isRelevantFunc( Node f ) { return std::find( d_funcs.begin(), d_funcs.end(), f )!=d_funcs.end(); } + +bool TermGenEnv::isRelevantTerm( Node t ) { + if( t.getKind()!=BOUND_VARIABLE ){ + if( t.getKind()!=EQUAL ){ + if( t.hasOperator() ){ + TNode op = t.getOperator(); + if( !isRelevantFunc( op ) ){ + return false; + } + }else{ + return false; + } + } + for( unsigned i=0; igetTermDatabase(); } diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index 6f99777f4..3aa932296 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -171,6 +171,7 @@ public: bool considerCurrentTermCanon( unsigned tg_id ); void changeContext( bool add ); bool isRelevantFunc( Node f ); + bool isRelevantTerm( Node t ); //carry TermDb * getTermDatabase(); Node getGroundEqc( TNode r ); @@ -307,14 +308,8 @@ private: //information regarding the conjectures /** conjecture index */ TheoremIndex d_thm_index; private: //free variable list - //free variables - std::map< TypeNode, std::vector< Node > > d_free_var; - //map from free variable to FV# - std::map< TNode, unsigned > d_free_var_num; // get canonical free variable #i of type tn Node getFreeVar( TypeNode tn, unsigned i ); - // get canonical term, return null if it contains a term apart from handled signature - Node getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs ); private: //information regarding the terms //relevant patterns (the LHS's) std::map< TypeNode, std::vector< Node > > d_rel_patterns; diff --git a/src/theory/quantifiers/first_order_reasoning.cpp b/src/theory/quantifiers/first_order_reasoning.cpp deleted file mode 100644 index 23e18bb02..000000000 --- a/src/theory/quantifiers/first_order_reasoning.cpp +++ /dev/null @@ -1,175 +0,0 @@ -/********************* */ -/*! \file first_order_reasoning.cpp - ** \verbatim - ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief first order reasoning module - ** - **/ - -#include - -#include "theory/quantifiers/first_order_reasoning.h" -#include "theory/rewriter.h" -#include "proof/proof_manager.h" - -using namespace CVC4; -using namespace std; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; -using namespace CVC4::kind; - - -void FirstOrderPropagation::collectLits( Node n, std::vector & lits ){ - if( n.getKind()==FORALL ){ - collectLits( n[1], lits ); - }else if( n.getKind()==OR ){ - for(unsigned j=0; j& assertions ){ - for( unsigned i=0; i fo_lits; - collectLits( assertions[i], fo_lits ); - Node unitLit = process( assertions[i], fo_lits ); - if( !unitLit.isNull() ){ - Trace("fo-rsn-debug") << "...possible unit literal : " << unitLit << " from " << assertions[i] << std::endl; - bool pol = unitLit.getKind()!=NOT; - unitLit = unitLit.getKind()==NOT ? unitLit[0] : unitLit; - if( unitLit.getKind()==EQUAL ){ - - }else if( unitLit.getKind()==APPLY_UF ){ - //make sure all are unique vars; - bool success = true; - std::vector< Node > unique_vars; - for( unsigned j=0; jmkConst(pol); - Trace("fo-rsn") << "Propagate : " << unitLit.getOperator() << " == " << pol << std::endl; - Trace("fo-rsn") << " from : " << assertions[i] << std::endl; - d_assertion_true[assertions[i]] = true; - num_processed++; - } - }else if( unitLit.getKind()==VARIABLE ){ - d_const_def[unitLit] = NodeManager::currentNM()->mkConst(pol); - Trace("fo-rsn") << "Propagate variable : " << unitLit << " == " << pol << std::endl; - Trace("fo-rsn") << " from : " << assertions[i] << std::endl; - d_assertion_true[assertions[i]] = true; - num_processed++; - } - } - if( d_assertion_true.find(assertions[i])!=d_assertion_true.end() ){ - num_true++; - } - } - } - num_rounds++; - }while( num_processed>0 ); - Trace("fo-rsn-sum") << "Simplified " << num_true << " / " << assertions.size() << " in " << num_rounds << " rounds." << std::endl; - for( unsigned i=0; iaddDependence(curr, assertions[i]); ); - assertions[i] = curr; - } - } -} - -Node FirstOrderPropagation::process(Node a, std::vector< Node > & lits) { - int index = -1; - for( unsigned i=0; imkConst( pol ); - if( litDef==poln ){ - Trace("fo-rsn-debug") << "Assertion " << a << " is true because of " << lits[i] << std::endl; - d_assertion_true[a] = true; - return Node::null(); - } - } - if( litDef.isNull() ){ - if( index==-1 ){ - //store undefined index - index = i; - }else{ - //two undefined, return null - return Node::null(); - } - } - } - if( index!=-1 ){ - return lits[index]; - }else{ - return Node::null(); - } -} - -Node FirstOrderPropagation::simplify( Node n ) { - if( n.getKind()==VARIABLE ){ - if( d_const_def.find(n)!=d_const_def.end() ){ - return d_const_def[n]; - } - }else if( n.getKind()==APPLY_UF ){ - if( d_const_def.find(n.getOperator())!=d_const_def.end() ){ - return d_const_def[n.getOperator()]; - } - } - if( n.getNumChildren()==0 ){ - return n; - }else{ - std::vector< Node > children; - if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ - children.push_back( n.getOperator() ); - } - for(unsigned i=0; imkNode( n.getKind(), children ); - } -} diff --git a/src/theory/quantifiers/first_order_reasoning.h b/src/theory/quantifiers/first_order_reasoning.h deleted file mode 100644 index 100cf34b6..000000000 --- a/src/theory/quantifiers/first_order_reasoning.h +++ /dev/null @@ -1,49 +0,0 @@ -/********************* */ -/*! \file first_order_reasoning.h - ** \verbatim - ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Pre-process step for first-order reasoning - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__FIRST_ORDER_REASONING_H -#define __CVC4__FIRST_ORDER_REASONING_H - -#include -#include -#include -#include -#include "expr/node.h" -#include "expr/type_node.h" - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -class FirstOrderPropagation { -private: - std::map< Node, Node > d_const_def; - std::map< Node, bool > d_assertion_true; - Node process(Node a, std::vector< Node > & lits); - void collectLits( Node n, std::vector & lits ); - Node simplify( Node n ); -public: - FirstOrderPropagation(){} - ~FirstOrderPropagation(){} - - void simplify( std::vector< Node >& assertions ); -}; - -} -} -} - -#endif diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 2af66e60a..e34465d9b 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -54,10 +54,7 @@ option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false # Whether to perform quantifier macro expansion option macrosQuant --macros-quant bool :default false perform quantifiers macro expansions -# Whether to perform first-order propagation -option foPropQuant --fo-prop-quant bool :default false - perform first-order propagation on quantifiers - + #### E-matching options option eMatching --e-matching bool :read-write :default true @@ -227,7 +224,7 @@ option sygusNormalFormGlobalArg --sygus-nf-sym-arg bool :default true option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true generalize based on content in global search space narrowing -# older implementation +# approach applied to general quantified formulas option cbqi --cbqi bool :read-write :default false turns on counterexample-based quantifier instantiation option cbqi2 --cbqi2 bool :read-write :default false @@ -246,4 +243,9 @@ option ltePartialInst --lte-partial-inst bool :default false option lteRestrictInstClosure --lte-restrict-inst-closure bool :default false treat arguments of inst closure as restricted terms for instantiation +### reduction options + +option quantAlphaEquiv --quant-alpha-equiv bool :default false + infer alpha equivalence between quantified formulas + endmodule diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 20d622122..84cb63617 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -77,7 +77,7 @@ void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) { } } -TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_ccount( u ) { +TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_ccount( u ), d_op_id_count( 0 ), d_typ_id_count( 0 ) { d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); if( options::ceGuidedInst() ){ @@ -1154,6 +1154,133 @@ void TermDb::filterInstances( std::vector< Node >& nodes ){ nodes.insert( nodes.begin(), temp.begin(), temp.end() ); } +int TermDb::getIdForOperator( Node op ) { + std::map< Node, int >::iterator it = d_op_id.find( op ); + if( it==d_op_id.end() ){ + d_op_id[op] = d_op_id_count; + d_op_id_count++; + return d_op_id[op]; + }else{ + return it->second; + } +} + +int TermDb::getIdForType( TypeNode t ) { + std::map< TypeNode, int >::iterator it = d_typ_id.find( t ); + if( it==d_typ_id.end() ){ + d_typ_id[t] = d_typ_id_count; + d_typ_id_count++; + return d_typ_id[t]; + }else{ + return it->second; + } +} + +bool TermDb::getTermOrder( Node a, Node b ) { + if( a.getKind()==BOUND_VARIABLE ){ + if( b.getKind()==BOUND_VARIABLE ){ + return a.getAttribute(InstVarNumAttribute())mkBoundVar( os.str().c_str(), tn ); + InstVarNumAttribute ivna; + x.setAttribute(ivna,d_cn_free_var[tn].size()); + d_cn_free_var[tn].push_back( x ); + } + return d_cn_free_var[tn][i]; +} + +struct sortTermOrder { + TermDb* d_tdb; + bool operator() (Node i, Node j) { + return d_tdb->getTermOrder( i, j ); + } +}; + +//this function makes a canonical representation of a term ( +// - orders variables left to right +// - if apply_torder, then sort direct subterms of commutative operators +Node TermDb::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder ) { + if( n.getKind()==BOUND_VARIABLE ){ + std::map< TNode, TNode >::iterator it = subs.find( n ); + if( it==subs.end() ){ + TypeNode tn = n.getType(); + //allocate variable + unsigned vn = var_count[tn]; + var_count[tn]++; + subs[n] = getCanonicalFreeVar( tn, vn ); + return subs[n]; + }else{ + return it->second; + } + }else if( n.getNumChildren()>0 ){ + //collect children + std::vector< Node > cchildren; + for( unsigned i=0; imkNode( n.getKind(), cchildren ); + }else{ + return n; + } +} + +Node TermDb::getCanonicalTerm( TNode n, bool apply_torder ){ + std::map< TypeNode, unsigned > var_count; + std::map< TNode, TNode > subs; + return getCanonicalTerm( n, var_count, subs, apply_torder ); +} + bool TermDb::containsTerm( Node n, Node t ) { if( n==t ){ return true; @@ -1179,6 +1306,15 @@ Node TermDb::simpleNegate( Node n ){ } } +bool TermDb::isAssoc( Kind k ) { + return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF || + k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT; +} + +bool TermDb::isComm( Kind k ) { + return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF || + k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR; +} void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){ if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){ @@ -1440,7 +1576,7 @@ bool TermDbSygus::getMatch2( Node p, Node n, std::map< int, Node >& s, std::vect return p==n; }else if( n.getKind()==p.getKind() && n.getNumChildren()==p.getNumChildren() ){ //try both ways? - unsigned rmax = isComm( n.getKind() ) && n.getNumChildren()==2 ? 2 : 1; + unsigned rmax = TermDb::isComm( n.getKind() ) && n.getNumChildren()==2 ? 2 : 1; std::vector< int > new_tmp; for( unsigned r=0; r=end; --i ){ Node c1 = d_const_list[tn1][i]; - //only consider if smaller than c, and + //only consider if smaller than c, and if( doCompare( c1, c, ck ) ){ Node c2 = NodeManager::currentNM()->mkNode( pkm, c, c1 ); c2 = Rewriter::rewrite( c2 ); @@ -1768,16 +1904,6 @@ int TermDbSygus::getSygusTermSize( Node n ){ } } -bool TermDbSygus::isAssoc( Kind k ) { - return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF || - k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT; -} - -bool TermDbSygus::isComm( Kind k ) { - return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF || - k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR; -} - bool TermDbSygus::isAntisymmetric( Kind k, Kind& dk ) { if( k==GT ){ dk = LT; @@ -2257,7 +2383,7 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node > std::stringstream body_out; printSygusTerm( body_out, let_body, new_lvs ); std::string body = body_out.str(); - for( unsigned i=0; i d_op_nonred_count; - /** map from APPLY_UF operators to ground terms for that operator */ + /** map from operators to ground terms for that operator */ std::map< Node, std::vector< Node > > d_op_map; /** has map */ std::map< Node, bool > d_has_map; /** map from reps to a term in eqc in d_has_map */ std::map< Node, Node > d_term_elig_eqc; - /** map from APPLY_UF functions to trie */ + /** map from operators to trie */ std::map< Node, TermArgTrie > d_func_map_trie; std::map< Node, TermArgTrie > d_func_map_eqc_trie; /**mapping from UF terms to representatives of their arguments */ @@ -326,12 +326,42 @@ public: /** filter all nodes that have instances */ void filterInstances( std::vector< Node >& nodes ); +//for term ordering +private: + /** operator id count */ + int d_op_id_count; + /** map from operators to id */ + std::map< Node, int > d_op_id; + /** type id count */ + int d_typ_id_count; + /** map from type to id */ + std::map< TypeNode, int > d_typ_id; + //free variables + std::map< TypeNode, std::vector< Node > > d_cn_free_var; + // get canonical term, return null if it contains a term apart from handled signature + Node getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder ); +public: + /** get id for operator */ + int getIdForOperator( Node op ); + /** get id for type */ + int getIdForType( TypeNode t ); + /** get term order */ + bool getTermOrder( Node a, Node b ); + /** get canonical free variable #i of type tn */ + Node getCanonicalFreeVar( TypeNode tn, unsigned i ); + /** get canonical term */ + Node getCanonicalTerm( TNode n, bool apply_torder = false ); + //general utilities public: /** simple check for contains term */ static bool containsTerm( Node n, Node t ); /** simple negate */ static Node simpleNegate( Node n ); + /** is assoc */ + static bool isAssoc( Kind k ); + /** is comm */ + static bool isComm( Kind k ); //for sygus private: @@ -441,10 +471,6 @@ public: void registerSygusType( TypeNode tn ); /** get arg type */ TypeNode getArgType( const DatatypeConstructor& c, int i ); - /** is assoc */ - bool isAssoc( Kind k ); - /** is comm */ - bool isComm( Kind k ); /** isAntisymmetric */ bool isAntisymmetric( Kind k, Kind& dk ); /** is idempotent arg */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 2d9ba5713..c202f9cb1 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -32,6 +32,7 @@ #include "theory/quantifiers/ce_guided_instantiation.h" #include "theory/quantifiers/local_theory_ext.h" #include "theory/quantifiers/relevant_domain.h" +#include "theory/quantifiers/alpha_equivalence.h" #include "theory/uf/options.h" #include "theory/uf/theory_uf.h" #include "theory/quantifiers/full_model_check.h" @@ -163,6 +164,11 @@ d_lemmas_produced_c(u){ }else{ d_lte_part_inst = NULL; } + if( options::quantAlphaEquiv() ){ + d_alpha_equiv = new quantifiers::AlphaEquivalence( this ); + }else{ + d_alpha_equiv = NULL; + } if( needsBuilder ){ Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl; @@ -422,6 +428,38 @@ void QuantifiersEngine::check( Theory::Effort e ){ } } +bool QuantifiersEngine::reduceQuantifier( Node q ) { + std::map< Node, bool >::iterator it = d_quants_red.find( q ); + if( it==d_quants_red.end() ){ + if( d_alpha_equiv ){ + Trace("quant-engine-debug") << "Alpha equivalence " << q << "?" << std::endl; + //add equivalence with another quantified formula + if( !d_alpha_equiv->registerQuantifier( q ) ){ + Trace("quant-engine-debug") << "...alpha equivalence success." << std::endl; + ++(d_statistics.d_red_alpha_equiv); + d_quants_red[q] = true; + return true; + } + } + if( d_lte_part_inst && !q.getAttribute(LtePartialInstAttribute()) ){ + //will partially instantiate + Trace("quant-engine-debug") << "LTE: Partially instantiate " << q << "?" << std::endl; + if( d_lte_part_inst->addQuantifier( q ) ){ + Trace("quant-engine-debug") << "...LTE partially instantiate success." << std::endl; + //delayed reduction : assert to model + d_model->assertQuantifier( q, true ); + ++(d_statistics.d_red_lte_partial_inst); + d_quants_red[q] = true; + return true; + } + } + d_quants_red[q] = false; + return false; + }else{ + return it->second; + } +} + bool QuantifiersEngine::registerQuantifier( Node f ){ std::map< Node, bool >::iterator it = d_quants.find( f ); if( it==d_quants.end() ){ @@ -431,15 +469,7 @@ bool QuantifiersEngine::registerQuantifier( Node f ){ Assert( f.getKind()==FORALL ); //check whether we should apply a reduction - bool reduced = false; - if( d_lte_part_inst && !f.getAttribute(LtePartialInstAttribute()) ){ - Trace("lte-partial-inst") << "LTE: Partially instantiate " << f << "?" << std::endl; - if( d_lte_part_inst->addQuantifier( f ) ){ - reduced = true; - } - } - if( reduced ){ - d_model->assertQuantifier( f, true ); + if( reduceQuantifier( f ) ){ d_quants[f] = false; return false; }else{ @@ -482,26 +512,26 @@ void QuantifiersEngine::registerPattern( std::vector & pattern) { void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ if( !pol ){ - //do skolemization - if( d_skolemized.find( f )==d_skolemized.end() ){ - Node body = d_term_db->getSkolemizedBody( f ); - NodeBuilder<> nb(kind::OR); - nb << f << body.notNode(); - Node lem = nb; - if( Trace.isOn("quantifiers-sk") ){ - Node slem = Rewriter::rewrite( lem ); - Trace("quantifiers-sk") << "Skolemize lemma : " << slem << std::endl; + //if not reduced + if( !reduceQuantifier( f ) ){ + //do skolemization + if( d_skolemized.find( f )==d_skolemized.end() ){ + Node body = d_term_db->getSkolemizedBody( f ); + NodeBuilder<> nb(kind::OR); + nb << f << body.notNode(); + Node lem = nb; + if( Trace.isOn("quantifiers-sk") ){ + Node slem = Rewriter::rewrite( lem ); + Trace("quantifiers-sk") << "Skolemize lemma : " << slem << std::endl; + } + getOutputChannel().lemma( lem, false, true ); + d_skolemized[f] = true; } - getOutputChannel().lemma( lem, false, true ); - d_skolemized[f] = true; } - } - //assert to modules TODO : handle !pol - if( pol ){ - //register the quantifier - bool nreduced = registerQuantifier( f ); - //assert it to each module - if( nreduced ){ + }else{ + //assert to modules TODO : also for !pol? + //register the quantifier, assert it to each module + if( registerQuantifier( f ) ){ d_model->assertQuantifier( f ); for( int i=0; i<(int)d_modules.size(); i++ ){ d_modules[i]->assertNode( f ); @@ -975,7 +1005,9 @@ QuantifiersEngine::Statistics::Statistics(): d_triggers("QuantifiersEngine::Triggers", 0), d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0), d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0), - d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0) + d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0), + d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0), + d_red_lte_partial_inst("QuantifiersEngine::Reductions_Lte_Partial_Inst", 0) { StatisticsRegistry::registerStat(&d_num_quant); StatisticsRegistry::registerStat(&d_instantiation_rounds); @@ -987,6 +1019,8 @@ QuantifiersEngine::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_simple_triggers); StatisticsRegistry::registerStat(&d_multi_triggers); StatisticsRegistry::registerStat(&d_multi_trigger_instantiations); + StatisticsRegistry::registerStat(&d_red_alpha_equiv); + StatisticsRegistry::registerStat(&d_red_lte_partial_inst); } QuantifiersEngine::Statistics::~Statistics(){ @@ -1000,6 +1034,8 @@ QuantifiersEngine::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_simple_triggers); StatisticsRegistry::unregisterStat(&d_multi_triggers); StatisticsRegistry::unregisterStat(&d_multi_trigger_instantiations); + StatisticsRegistry::unregisterStat(&d_red_alpha_equiv); + StatisticsRegistry::unregisterStat(&d_red_lte_partial_inst); } eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){ @@ -1138,7 +1174,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, } } if( r_best.isNull() ){ - Trace("internal-rep-warn") << "No valid choice for representative in eqc class." << std::endl; + Trace("internal-rep-warn") << "No valid choice for representative in eqc class." << std::endl; r_best = r; } //now, make sure that no other member of the class is an instance diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index c9f14b2c4..3040a35c7 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -92,6 +92,7 @@ namespace quantifiers { class ConjectureGenerator; class CegInstantiation; class LtePartialInst; + class AlphaEquivalence; }/* CVC4::theory::quantifiers */ namespace inst { @@ -119,6 +120,8 @@ private: QuantRelevance * d_quant_rel; /** relevant domain */ quantifiers::RelevantDomain* d_rel_dom; + /** alpha equivalence */ + quantifiers::AlphaEquivalence * d_alpha_equiv; /** model builder */ quantifiers::QModelBuilder* d_builder; /** phase requirements for each quantifier for each instantiation literal */ @@ -150,6 +153,8 @@ public: //effort levels private: /** list of all quantifiers seen */ std::map< Node, bool > d_quants; + /** quantifiers reduced */ + std::map< Node, bool > d_quants_red; /** list of all lemmas produced */ //std::map< Node, bool > d_lemmas_produced; BoolMap d_lemmas_produced_c; @@ -186,8 +191,7 @@ public: ~QuantifiersEngine(); /** get theory engine */ TheoryEngine* getTheoryEngine() { return d_te; } - /** get equality query object for the given type. The default is the - generic one */ + /** get equality query */ EqualityQueryQuantifiersEngine* getEqualityQuery(); /** get default sat context for quantifiers engine */ context::Context* getSatContext(); @@ -250,6 +254,8 @@ public: /** get next decision request */ Node getNextDecisionRequest(); private: + /** reduce quantifier */ + bool reduceQuantifier( Node q ); /** compute term vector */ void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms ); /** instantiate f with arguments terms */ @@ -322,6 +328,8 @@ public: IntStat d_simple_triggers; IntStat d_multi_triggers; IntStat d_multi_trigger_instantiations; + IntStat d_red_alpha_equiv; + IntStat d_red_lte_partial_inst; Statistics(); ~Statistics(); };/* class QuantifiersEngine::Statistics */ -- 2.30.2