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 \
#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"
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() ){
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() ){
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 );
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; i<dto.getNumConstructors(); i++ ){
if( d_sygus_pc_nred[tnno][csIndex][osIndex][i] ){
int pc = d_tds->getKindArg( 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 );
}
}
if( parent==MINUS || parent==BITVECTOR_SUB ){
-
-
+
+
}
return true;
}
--- /dev/null
+/********************* */
+/*! \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 )<d_tdb->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; i<q[0].getNumChildren(); i++ ){
+ TypeNode tn = q[0][i].getType();
+ typ_count[tn]++;
+ if( std::find( typs.begin(), typs.end(), tn )==typs.end() ){
+ typs.push_back( tn );
+ }
+ }
+ sortTypeOrder sto;
+ sto.d_tdb = d_qe->getTermDatabase();
+ 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;
+}
--- /dev/null
+/********************* */
+/*! \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
}
Node sol0 = Rewriter::rewrite( sol );
Trace("csi-sol") << "now : " << sol0 << std::endl;
-
+
Node curr_sol = sol0;
Node prev_sol;
do{
curr_sol = sol4;
}
}while( curr_sol!=prev_sol );
-
+
return curr_sol;
}
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; i<min_t.getNumChildren(); i++ ){
}
Node ConjectureGenerator::getFreeVar( TypeNode tn, unsigned i ) {
- Assert( !tn.isNull() );
- while( d_free_var[tn].size()<=i ){
- std::stringstream oss;
- oss << tn;
- std::string typ_name = oss.str();
- while( typ_name[0]=='(' ){
- typ_name.erase( typ_name.begin() );
- }
- std::stringstream os;
- os << typ_name[0] << i;
- Node x = NodeManager::currentNM()->mkBoundVar( 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; i<n.getNumChildren(); i++ ){
- Node cn = getCanonicalTerm( n[i], var_count, subs );
- if( cn.isNull() ){
- return Node::null();
- }else{
- children.push_back( cn );
- }
- }
- return NodeManager::currentNM()->mkNode( n.getKind(), children );
- }
+ return d_quantEngine->getTermDatabase()->getCanonicalFreeVar( tn, i );
}
bool ConjectureGenerator::isHandledTerm( TNode n ){
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 ){
typ_to_subs_index[it->first] = sum;
sum += it->second;
for( unsigned i=0; i<it->second; i++ ){
- gsubs_vars.push_back( getFreeVar( it->first, i ) );
+ gsubs_vars.push_back( d_quantEngine->getTermDatabase()->getCanonicalFreeVar( it->first, i ) );
}
}
}
}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( vn<it->second ){
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; i<t.getNumChildren(); i++ ){
+ if( !isRelevantTerm( t[i] ) ){
+ return false;
+ }
+ }
+ }
+ return true;
+}
+
TermDb * TermGenEnv::getTermDatabase() {
return d_cg->getTermDatabase();
}
bool considerCurrentTermCanon( unsigned tg_id );
void changeContext( bool add );
bool isRelevantFunc( Node f );
+ bool isRelevantTerm( Node t );
//carry
TermDb * getTermDatabase();
Node getGroundEqc( TNode r );
/** 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;
+++ /dev/null
-/********************* */
-/*! \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 <vector>
-
-#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<Node> & lits ){
- if( n.getKind()==FORALL ){
- collectLits( n[1], lits );
- }else if( n.getKind()==OR ){
- for(unsigned j=0; j<n.getNumChildren(); j++) {
- collectLits(n[j], lits );
- }
- }else{
- lits.push_back( n );
- }
-}
-
-void FirstOrderPropagation::simplify( std::vector< Node >& assertions ){
- for( unsigned i=0; i<assertions.size(); i++) {
- Trace("fo-rsn") << "Assert : " << assertions[i] << std::endl;
- }
-
- //process all assertions
- int num_processed;
- int num_true = 0;
- int num_rounds = 0;
- do {
- num_processed = 0;
- for( unsigned i=0; i<assertions.size(); i++ ){
- if( d_assertion_true.find(assertions[i])==d_assertion_true.end() ){
- std::vector< Node > 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; j<unitLit.getNumChildren(); j++) {
- if( unitLit[j].getKind()==BOUND_VARIABLE ){
- if( std::find(unique_vars.begin(), unique_vars.end(), unitLit[j])==unique_vars.end() ){
- unique_vars.push_back( unitLit[j] );
- }else{
- success = false;
- break;
- }
- }else{
- success = false;
- break;
- }
- }
- if( success ){
- d_const_def[unitLit.getOperator()] = NodeManager::currentNM()->mkConst(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; i<assertions.size(); i++ ){
- Node curr = simplify( assertions[i] );
- if( curr!=assertions[i] ){
- curr = Rewriter::rewrite( curr );
- PROOF( ProofManager::currentPM()->addDependence(curr, assertions[i]); );
- assertions[i] = curr;
- }
- }
-}
-
-Node FirstOrderPropagation::process(Node a, std::vector< Node > & lits) {
- int index = -1;
- for( unsigned i=0; i<lits.size(); i++) {
- bool pol = lits[i].getKind()!=NOT;
- Node n = lits[i].getKind()==NOT ? lits[i][0] : lits[i];
- Node litDef;
- if( n.getKind()==APPLY_UF ){
- if( d_const_def.find(n.getOperator())!=d_const_def.end() ){
- litDef = d_const_def[n.getOperator()];
- }
- }else if( n.getKind()==VARIABLE ){
- if( d_const_def.find(n)!=d_const_def.end() ){
- litDef = d_const_def[n];
- }
- }
- if( !litDef.isNull() ){
- Node poln = NodeManager::currentNM()->mkConst( 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; i<n.getNumChildren(); i++) {
- children.push_back( simplify(n[i]) );
- }
- return NodeManager::currentNM()->mkNode( n.getKind(), children );
- }
-}
+++ /dev/null
-/********************* */
-/*! \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 <iostream>
-#include <string>
-#include <vector>
-#include <map>
-#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<Node> & lits );
- Node simplify( Node n );
-public:
- FirstOrderPropagation(){}
- ~FirstOrderPropagation(){}
-
- void simplify( std::vector< Node >& assertions );
-};
-
-}
-}
-}
-
-#endif
# 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
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
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
}
}
-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() ){
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())<b.getAttribute(InstVarNumAttribute());
+ }else{
+ return true;
+ }
+ }else if( b.getKind()!=BOUND_VARIABLE ){
+ Node aop = a.hasOperator() ? a.getOperator() : a;
+ Node bop = b.hasOperator() ? b.getOperator() : b;
+ Trace("aeq-debug2") << a << "...op..." << aop << std::endl;
+ Trace("aeq-debug2") << b << "...op..." << bop << std::endl;
+ if( aop==bop ){
+ if( aop.getNumChildren()==bop.getNumChildren() ){
+ for( unsigned i=0; i<a.getNumChildren(); i++ ){
+ if( a[i]!=b[i] ){
+ //first distinct child determines the ordering
+ return getTermOrder( a[i], b[i] );
+ }
+ }
+ }else{
+ return aop.getNumChildren()<bop.getNumChildren();
+ }
+ }else{
+ return getIdForOperator( aop )<getIdForOperator( bop );
+ }
+ }
+ return false;
+}
+
+
+
+Node TermDb::getCanonicalFreeVar( TypeNode tn, unsigned i ) {
+ Assert( !tn.isNull() );
+ while( d_cn_free_var[tn].size()<=i ){
+ std::stringstream oss;
+ oss << tn;
+ std::string typ_name = oss.str();
+ while( typ_name[0]=='(' ){
+ typ_name.erase( typ_name.begin() );
+ }
+ std::stringstream os;
+ os << typ_name[0] << i;
+ Node x = NodeManager::currentNM()->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; i<n.getNumChildren(); i++ ){
+ cchildren.push_back( n[i] );
+ }
+ //if applicable, first sort by term order
+ if( apply_torder && isComm( n.getKind() ) ){
+ sortTermOrder sto;
+ sto.d_tdb = this;
+ std::sort( cchildren.begin(), cchildren.end(), sto );
+ }
+ //now make canonical
+ for( unsigned i=0; i<cchildren.size(); i++ ){
+ cchildren[i] = getCanonicalTerm( cchildren[i], var_count, subs, apply_torder );
+ }
+ if( n.hasOperator() ){
+ cchildren.insert( cchildren.begin(), n.getOperator() );
+ }
+ return NodeManager::currentNM()->mkNode( 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;
}
}
+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() ){
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<rmax; r++ ){
bool success = true;
int end = d_const_list[tn1].size()-d_const_list_pos[tn1];
for( int i=start; i>=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 );
}
}
-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;
std::stringstream body_out;
printSygusTerm( body_out, let_body, new_lvs );
std::string body = body_out.str();
- for( unsigned i=0; i<dt[cIndex].getNumSygusLetArgs(); i++ ){
+ for( unsigned i=0; i<dt[cIndex].getNumSygusLetArgs(); i++ ){
std::stringstream old_str;
old_str << new_lvs[i];
std::stringstream new_str;
unsigned getNumGroundTerms( Node f );
/** count number of non-redundant ground terms per operator */
std::map< Node, int > 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 */
/** 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:
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 */
#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"
}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;
}
}
+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() ){
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{
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 );
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);
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(){
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(){
}
}
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
class ConjectureGenerator;
class CegInstantiation;
class LtePartialInst;
+ class AlphaEquivalence;
}/* CVC4::theory::quantifiers */
namespace inst {
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 */
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;
~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();
/** 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 */
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 */
projects / cvc5.git / commitdiff