From 3f2c2c745ae2f13441c1cabd363e6539c9bdaeb9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 1 Nov 2017 23:20:09 -0500 Subject: [PATCH] (Move-only) Split quant util (#1306) * Initial draft of splitting quant util. * Minor * Document recursive term builder. * Rename file, minor. * Clang format --- src/Makefile.am | 6 + src/theory/quantifiers/inst_strategy_cbqi.cpp | 3 +- .../quantifiers/inst_strategy_e_matching.cpp | 3 +- src/theory/quantifiers/quant_epr.cpp | 187 ++++++++++++++ src/theory/quantifiers/quant_epr.h | 104 ++++++++ src/theory/quantifiers/quant_relevance.cpp | 97 +++++++ src/theory/quantifiers/quant_relevance.h | 80 ++++++ src/theory/quantifiers/quant_util.cpp | 238 +----------------- src/theory/quantifiers/quant_util.h | 88 +------ src/theory/quantifiers/sygus_explain.cpp | 112 +++++++++ src/theory/quantifiers/sygus_explain.h | 90 +++++++ src/theory/quantifiers/term_database_sygus.h | 5 +- src/theory/quantifiers_engine.cpp | 6 +- src/theory/quantifiers_engine.h | 12 +- src/theory/sep/theory_sep.cpp | 18 +- 15 files changed, 710 insertions(+), 339 deletions(-) create mode 100644 src/theory/quantifiers/quant_epr.cpp create mode 100644 src/theory/quantifiers/quant_epr.h create mode 100644 src/theory/quantifiers/quant_relevance.cpp create mode 100644 src/theory/quantifiers/quant_relevance.h create mode 100644 src/theory/quantifiers/sygus_explain.cpp create mode 100644 src/theory/quantifiers/sygus_explain.h diff --git a/src/Makefile.am b/src/Makefile.am index e8910e182..5ddfbf5c7 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -410,8 +410,12 @@ libcvc4_la_SOURCES = \ theory/quantifiers/model_engine.h \ theory/quantifiers/quant_conflict_find.cpp \ theory/quantifiers/quant_conflict_find.h \ + theory/quantifiers/quant_epr.cpp \ + theory/quantifiers/quant_epr.h \ theory/quantifiers/quant_equality_engine.cpp \ theory/quantifiers/quant_equality_engine.h \ + theory/quantifiers/quant_relevance.cpp \ + theory/quantifiers/quant_relevance.h \ theory/quantifiers/quant_split.cpp \ theory/quantifiers/quant_split.h \ theory/quantifiers/quant_util.cpp \ @@ -426,6 +430,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/rewrite_engine.h \ theory/quantifiers/skolemize.cpp \ theory/quantifiers/skolemize.h \ + theory/quantifiers/sygus_explain.cpp \ + theory/quantifiers/sygus_explain.h \ theory/quantifiers/sygus_grammar_cons.cpp \ theory/quantifiers/sygus_grammar_cons.h \ theory/quantifiers/sygus_process_conj.cpp \ diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 93505b494..8b5332c9d 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -19,11 +19,12 @@ #include "theory/arith/theory_arith.h" #include "theory/arith/theory_arith_private.h" #include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/quant_epr.h" #include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers/trigger.h" -#include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/theory_engine.h" using namespace std; diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index dcc863f3e..f7e5891f9 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/inst_strategy_e_matching.h" #include "theory/quantifiers/inst_match_generator.h" +#include "theory/quantifiers/quant_relevance.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" @@ -471,7 +472,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ if( indexgetQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[0].getOperator() ); } diff --git a/src/theory/quantifiers/quant_epr.cpp b/src/theory/quantifiers/quant_epr.cpp new file mode 100644 index 000000000..187466aaa --- /dev/null +++ b/src/theory/quantifiers/quant_epr.cpp @@ -0,0 +1,187 @@ +/********************* */ +/*! \file quant_epr.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Morgan Deters, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 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 quantifier EPR. + **/ + +#include "theory/quantifiers/quant_epr.h" + +#include "theory/quantifiers/quant_util.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +void QuantEPR::registerNode(Node n, + std::map >& visited, + bool beneathQuant, + bool hasPol, + bool pol) +{ + int vindex = hasPol ? (pol ? 1 : -1) : 0; + if (visited[vindex].find(n) == visited[vindex].end()) + { + visited[vindex][n] = true; + Trace("quant-epr-debug") << "QuantEPR::registerNode " << n << std::endl; + if (n.getKind() == FORALL) + { + if (beneathQuant || !hasPol || !pol) + { + for (unsigned i = 0; i < n[0].getNumChildren(); i++) + { + TypeNode tn = n[0][i].getType(); + if (d_non_epr.find(tn) == d_non_epr.end()) + { + Trace("quant-epr") << "Sort " << tn + << " is non-EPR because of nested or possible " + "existential quantification." + << std::endl; + d_non_epr[tn] = true; + } + } + } + else + { + beneathQuant = true; + } + } + TypeNode tn = n.getType(); + + if (n.getNumChildren() > 0) + { + if (tn.isSort()) + { + if (d_non_epr.find(tn) == d_non_epr.end()) + { + Trace("quant-epr") << "Sort " << tn << " is non-EPR because of " << n + << std::endl; + d_non_epr[tn] = true; + } + } + for (unsigned i = 0; i < n.getNumChildren(); i++) + { + bool newHasPol; + bool newPol; + QuantPhaseReq::getPolarity(n, i, hasPol, pol, newHasPol, newPol); + registerNode(n[i], visited, beneathQuant, newHasPol, newPol); + } + } + else if (tn.isSort()) + { + if (n.getKind() == BOUND_VARIABLE) + { + if (d_consts.find(tn) == d_consts.end()) + { + // mark that at least one constant must occur + d_consts[tn].clear(); + } + } + else if (std::find(d_consts[tn].begin(), d_consts[tn].end(), n) + == d_consts[tn].end()) + { + d_consts[tn].push_back(n); + Trace("quant-epr") << "...constant of type " << tn << " : " << n + << std::endl; + } + } + } +} + +void QuantEPR::registerAssertion(Node assertion) +{ + std::map > visited; + registerNode(assertion, visited, false, true, true); +} + +void QuantEPR::finishInit() +{ + Trace("quant-epr-debug") << "QuantEPR::finishInit" << std::endl; + for (std::map >::iterator it = d_consts.begin(); + it != d_consts.end(); + ++it) + { + Assert(d_epr_axiom.find(it->first) == d_epr_axiom.end()); + Trace("quant-epr-debug") << "process " << it->first << std::endl; + if (d_non_epr.find(it->first) != d_non_epr.end()) + { + Trace("quant-epr-debug") << "...non-epr" << std::endl; + it->second.clear(); + } + else + { + Trace("quant-epr-debug") << "...epr, #consts = " << it->second.size() + << std::endl; + if (it->second.empty()) + { + it->second.push_back(NodeManager::currentNM()->mkSkolem( + "e", it->first, "EPR base constant")); + } + if (Trace.isOn("quant-epr")) + { + Trace("quant-epr") << "Type " << it->first + << " is EPR, with constants : " << std::endl; + for (unsigned i = 0; i < it->second.size(); i++) + { + Trace("quant-epr") << " " << it->second[i] << std::endl; + } + } + } + } +} + +bool QuantEPR::isEPRConstant(TypeNode tn, Node k) +{ + return std::find(d_consts[tn].begin(), d_consts[tn].end(), k) + != d_consts[tn].end(); +} + +void QuantEPR::addEPRConstant(TypeNode tn, Node k) +{ + Assert(isEPR(tn)); + Assert(d_epr_axiom.find(tn) == d_epr_axiom.end()); + if (!isEPRConstant(tn, k)) + { + d_consts[tn].push_back(k); + } +} + +Node QuantEPR::mkEPRAxiom(TypeNode tn) +{ + Assert(isEPR(tn)); + std::map::iterator ita = d_epr_axiom.find(tn); + if (ita == d_epr_axiom.end()) + { + std::vector disj; + Node x = NodeManager::currentNM()->mkBoundVar(tn); + for (unsigned i = 0; i < d_consts[tn].size(); i++) + { + disj.push_back( + NodeManager::currentNM()->mkNode(EQUAL, x, d_consts[tn][i])); + } + Assert(!disj.empty()); + d_epr_axiom[tn] = NodeManager::currentNM()->mkNode( + FORALL, + NodeManager::currentNM()->mkNode(BOUND_VAR_LIST, x), + disj.size() == 1 ? disj[0] + : NodeManager::currentNM()->mkNode(OR, disj)); + return d_epr_axiom[tn]; + } + else + { + return ita->second; + } +} + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ diff --git a/src/theory/quantifiers/quant_epr.h b/src/theory/quantifiers/quant_epr.h new file mode 100644 index 000000000..f191da68e --- /dev/null +++ b/src/theory/quantifiers/quant_epr.h @@ -0,0 +1,104 @@ +/********************* */ +/*! \file quant_epr.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 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 quantifier util + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANT_EPR_H +#define __CVC4__THEORY__QUANT_EPR_H + +#include + +#include "expr/node.h" +#include "expr/type_node.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** Quant EPR + * + * This class maintains information required for + * approaches for effectively propositional logic (EPR), + * also called the Bernays-Schoenfinkel fragment. + * + * It maintains for each type whether the type + * has a finite Herbrand universe, stored in d_consts. + * This class is used in counterexample-guided instantiation + * for EPR, described in Reynolds et al., + * "Reasoning in the Bernays-Schonfinkel-Ramsey Fragment of + * Separation Logic", VMCAI 2017. + * + * Below, we say a type is an "EPR type" if its + * Herbrand universe can be restricted to a finite set + * based on the set of input assertions, + * and a "non-EPR type" otherwise. + */ +class QuantEPR +{ + public: + QuantEPR() {} + virtual ~QuantEPR() {} + /** constants per type */ + std::map > d_consts; + /** register an input assertion with this class + * This updates whether types are EPR are not + * based on the constraints in assertion. + */ + void registerAssertion(Node assertion); + /** finish initialize + * This ensures all EPR sorts are non-empty + * (that is, they have at least one term in d_consts), + * and clears non-EPR sorts from d_consts. + */ + void finishInit(); + /** is type tn an EPR type? */ + bool isEPR(TypeNode tn) const + { + return d_non_epr.find(tn) == d_non_epr.end(); + } + /** is k an EPR constant for type tn? */ + bool isEPRConstant(TypeNode tn, Node k); + /** add EPR constant k of type tn. */ + void addEPRConstant(TypeNode tn, Node k); + /** get EPR axiom for type + * This is a formula of the form: + * forall x : U. ( x = c1 V ... x = cn ) + * where c1...cn are the constants in the Herbrand + * universe of U. + */ + Node mkEPRAxiom(TypeNode tn); + /** does this class have an EPR axiom for type tn? */ + bool hasEPRAxiom(TypeNode tn) const + { + return d_epr_axiom.find(tn) != d_epr_axiom.end(); + } + + private: + /** register the node */ + void registerNode(Node n, + std::map >& visited, + bool beneathQuant, + bool hasPol, + bool pol); + /** map from types to a flag says whether they are not EPR */ + std::map d_non_epr; + /** EPR axioms for each type. */ + std::map d_epr_axiom; +}; + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANT_EPR_H */ diff --git a/src/theory/quantifiers/quant_relevance.cpp b/src/theory/quantifiers/quant_relevance.cpp new file mode 100644 index 000000000..1f814263f --- /dev/null +++ b/src/theory/quantifiers/quant_relevance.cpp @@ -0,0 +1,97 @@ +/********************* */ +/*! \file quant_relevance.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 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 quantifier relevance + **/ + +#include "theory/quantifiers/quant_relevance.h" + +using namespace std; +using namespace CVC4::kind; +using namespace CVC4::context; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +void QuantRelevance::registerQuantifier(Node f) +{ + // compute symbols in f + std::vector syms; + computeSymbols(f[1], syms); + d_syms[f].insert(d_syms[f].begin(), syms.begin(), syms.end()); + // set initial relevance + int minRelevance = -1; + for (int i = 0; i < (int)syms.size(); i++) + { + d_syms_quants[syms[i]].push_back(f); + int r = getRelevance(syms[i]); + if (r != -1 && (minRelevance == -1 || r < minRelevance)) + { + minRelevance = r; + } + } + if (minRelevance != -1) + { + setRelevance(f, minRelevance + 1); + } +} + +/** compute symbols */ +void QuantRelevance::computeSymbols(Node n, std::vector& syms) +{ + if (n.getKind() == APPLY_UF) + { + Node op = n.getOperator(); + if (std::find(syms.begin(), syms.end(), op) == syms.end()) + { + syms.push_back(op); + } + } + if (n.getKind() != FORALL) + { + for (int i = 0; i < (int)n.getNumChildren(); i++) + { + computeSymbols(n[i], syms); + } + } +} + +/** set relevance */ +void QuantRelevance::setRelevance(Node s, int r) +{ + if (d_computeRel) + { + int rOld = getRelevance(s); + if (rOld == -1 || r < rOld) + { + d_relevance[s] = r; + if (s.getKind() == FORALL) + { + for (int i = 0; i < (int)d_syms[s].size(); i++) + { + setRelevance(d_syms[s][i], r); + } + } + else + { + for (int i = 0; i < (int)d_syms_quants[s].size(); i++) + { + setRelevance(d_syms_quants[s][i], r + 1); + } + } + } + } +} + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ diff --git a/src/theory/quantifiers/quant_relevance.h b/src/theory/quantifiers/quant_relevance.h new file mode 100644 index 000000000..3182df34b --- /dev/null +++ b/src/theory/quantifiers/quant_relevance.h @@ -0,0 +1,80 @@ +/********************* */ +/*! \file quant_relevance.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 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 quantifier relevance + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANT_RELEVANCE_H +#define __CVC4__THEORY__QUANT_RELEVANCE_H + +#include + +#include "theory/quantifiers/quant_util.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** QuantRelevance + * +* This class is used for implementing SinE-style heuristics +* (e.g. see Hoder et al. CADE 2011) +* This is enabled by the option --relevant-triggers. +*/ +class QuantRelevance : public QuantifiersUtil +{ + public: + /** constructor + * cr is whether relevance is computed by this class. + * if this is false, then all calls to getRelevance + * return -1. + */ + QuantRelevance(bool cr) : d_computeRel(cr) {} + ~QuantRelevance() {} + /** reset */ + virtual bool reset(Theory::Effort e) override { return true; } + /** register quantifier */ + virtual void registerQuantifier(Node q) override; + /** identify */ + virtual std::string identify() const override { return "QuantRelevance"; } + /** set relevance of symbol s to r */ + void setRelevance(Node s, int r); + /** get relevance of symbol s */ + int getRelevance(Node s) + { + return d_relevance.find(s) == d_relevance.end() ? -1 : d_relevance[s]; + } + /** get number of quantifiers for symbol s */ + unsigned getNumQuantifiersForSymbol(Node s) + { + return d_syms_quants[s].size(); + } + + private: + /** for computing relevance */ + bool d_computeRel; + /** map from quantifiers to symbols they contain */ + std::map > d_syms; + /** map from symbols to quantifiers */ + std::map > d_syms_quants; + /** relevance for quantifiers and symbols */ + std::map d_relevance; + /** compute symbols */ + void computeSymbols(Node n, std::vector& syms); +}; + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANT_RELEVANCE_H */ diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 88fdec6f3..b8e29280d 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -19,11 +19,11 @@ #include "theory/quantifiers_engine.h" using namespace std; -using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; -using namespace CVC4::theory; +namespace CVC4 { +namespace theory { unsigned QuantifiersModule::needsModel( Theory::Effort e ) { return QuantifiersEngine::QEFFORT_NONE; @@ -291,62 +291,6 @@ void QuantArith::debugPrintMonomialSum( std::map< Node, Node >& msum, const char Trace(c) << std::endl; } - -void QuantRelevance::registerQuantifier( Node f ){ - //compute symbols in f - std::vector< Node > syms; - computeSymbols( f[1], syms ); - d_syms[f].insert( d_syms[f].begin(), syms.begin(), syms.end() ); - //set initial relevance - int minRelevance = -1; - for( int i=0; i<(int)syms.size(); i++ ){ - d_syms_quants[ syms[i] ].push_back( f ); - int r = getRelevance( syms[i] ); - if( r!=-1 && ( minRelevance==-1 || r& syms ){ - if( n.getKind()==APPLY_UF ){ - Node op = n.getOperator(); - if( std::find( syms.begin(), syms.end(), op )==syms.end() ){ - syms.push_back( op ); - } - } - if( n.getKind()!=FORALL ){ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - computeSymbols( n[i], syms ); - } - } -} - -/** set relevance */ -void QuantRelevance::setRelevance( Node s, int r ){ - if( d_computeRel ){ - int rOld = getRelevance( s ); - if( rOld==-1 || r >& visited, bool beneathQuant, bool hasPol, bool pol ) { - int vindex = hasPol ? ( pol ? 1 : -1 ) : 0; - if( visited[vindex].find( n )==visited[vindex].end() ){ - visited[vindex][n] = true; - Trace("quant-epr-debug") << "QuantEPR::registerNode " << n << std::endl; - if( n.getKind()==FORALL ){ - if( beneathQuant || !hasPol || !pol ){ - for( unsigned i=0; i0 ){ - if( tn.isSort() ){ - if( d_non_epr.find( tn )==d_non_epr.end() ){ - Trace("quant-epr") << "Sort " << tn << " is non-EPR because of " << n << std::endl; - d_non_epr[tn] = true; - } - } - for( unsigned i=0; i > visited; - registerNode( assertion, visited, false, true, true ); -} - -void QuantEPR::finishInit() { - Trace("quant-epr-debug") << "QuantEPR::finishInit" << std::endl; - for( std::map< TypeNode, std::vector< Node > >::iterator it = d_consts.begin(); it != d_consts.end(); ++it ){ - Assert( d_epr_axiom.find( it->first )==d_epr_axiom.end() ); - Trace("quant-epr-debug") << "process " << it->first << std::endl; - if( d_non_epr.find( it->first )!=d_non_epr.end() ){ - Trace("quant-epr-debug") << "...non-epr" << std::endl; - it->second.clear(); - }else{ - Trace("quant-epr-debug") << "...epr, #consts = " << it->second.size() << std::endl; - if( it->second.empty() ){ - it->second.push_back( NodeManager::currentNM()->mkSkolem( "e", it->first, "EPR base constant" ) ); - } - if( Trace.isOn("quant-epr") ){ - Trace("quant-epr") << "Type " << it->first << " is EPR, with constants : " << std::endl; - for( unsigned i=0; isecond.size(); i++ ){ - Trace("quant-epr") << " " << it->second[i] << std::endl; - } - } - } - } -} - -bool QuantEPR::isEPRConstant( TypeNode tn, Node k ) { - return std::find( d_consts[tn].begin(), d_consts[tn].end(), k )!=d_consts[tn].end(); -} - -void QuantEPR::addEPRConstant( TypeNode tn, Node k ) { - Assert( isEPR( tn ) ); - Assert( d_epr_axiom.find( tn )==d_epr_axiom.end() ); - if( !isEPRConstant( tn, k ) ){ - d_consts[tn].push_back( k ); - } -} - -Node QuantEPR::mkEPRAxiom( TypeNode tn ) { - Assert( isEPR( tn ) ); - std::map< TypeNode, Node >::iterator ita = d_epr_axiom.find( tn ); - if( ita==d_epr_axiom.end() ){ - std::vector< Node > disj; - Node x = NodeManager::currentNM()->mkBoundVar( tn ); - for( unsigned i=0; imkNode( EQUAL, x, d_consts[tn][i] ) ); - } - Assert( !disj.empty() ); - d_epr_axiom[tn] = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, x ), disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( OR, disj ) ); - return d_epr_axiom[tn]; - }else{ - return ita->second; - } -} - - -void TermRecBuild::addTerm( Node n ) { - d_term.push_back( n ); - std::vector< Node > currc; - d_kind.push_back( n.getKind() ); - if( n.getMetaKind()==kind::metakind::PARAMETERIZED ){ - currc.push_back( n.getOperator() ); - d_has_op.push_back( true ); - }else{ - d_has_op.push_back( false ); - } - for( unsigned i=0; i children; - unsigned o = d_has_op[d] ? 1 : 0; - for( unsigned i=0; imkNode( d_kind[d], children ); -} - +} /* namespace CVC4::theory */ +} /* namespace CVC4 */ diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index ad6ab509d..95cd7e5e4 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -316,41 +316,6 @@ public: static void debugPrintMonomialSum(std::map& msum, const char* c); }; -/** QuantRelevance -* This class is used for implementing SinE-style heuristics (e.g. see Hoder et -* al CADE 2011) -* This is enabled by the option --relevant-triggers. -*/ -class QuantRelevance : public QuantifiersUtil -{ -private: - /** for computing relevance */ - bool d_computeRel; - /** map from quantifiers to symbols they contain */ - std::map< Node, std::vector< Node > > d_syms; - /** map from symbols to quantifiers */ - std::map< Node, std::vector< Node > > d_syms_quants; - /** relevance for quantifiers and symbols */ - std::map< Node, int > d_relevance; - /** compute symbols */ - void computeSymbols( Node n, std::vector< Node >& syms ); -public: - QuantRelevance( bool cr ) : d_computeRel( cr ){} - ~QuantRelevance(){} - virtual bool reset(Theory::Effort e) override { return true; } - /** Called for new quantifiers after ownership of quantified formulas are - * finalized */ - virtual void registerQuantifier(Node q) override; - /** Identify this module (for debugging, dynamic configuration, etc..) */ - virtual std::string identify() const override { return "QuantRelevance"; } - /** set relevance */ - void setRelevance( Node s, int r ); - /** get relevance */ - int getRelevance( Node s ) { return d_relevance.find( s )==d_relevance.end() ? -1 : d_relevance[s]; } - /** get number of quantifiers for symbol s */ - int getNumQuantifiersForSymbol( Node s ) { return (int)d_syms_quants[s].size(); } -}; - class QuantPhaseReq { private: @@ -400,58 +365,7 @@ public: virtual TNode getCongruentTerm( Node f, std::vector< TNode >& args ) = 0; };/* class EqualityQuery */ -class QuantEPR -{ -private: - void registerNode( Node n, std::map< int, std::map< Node, bool > >& visited, bool beneathQuant, bool hasPol, bool pol ); - /** non-epr */ - std::map< TypeNode, bool > d_non_epr; - /** axioms for epr */ - std::map< TypeNode, Node > d_epr_axiom; -public: - QuantEPR(){} - virtual ~QuantEPR(){} - /** constants per type */ - std::map< TypeNode, std::vector< Node > > d_consts; - /* reset */ - //bool reset( Theory::Effort e ) {} - /** identify */ - //std::string identify() const { return "QuantEPR"; } - /** register assertion */ - void registerAssertion( Node assertion ); - /** finish init */ - void finishInit(); - /** is EPR */ - bool isEPR( TypeNode tn ) const { return d_non_epr.find( tn )==d_non_epr.end(); } - /** is EPR constant */ - bool isEPRConstant( TypeNode tn, Node k ); - /** add EPR constant */ - void addEPRConstant( TypeNode tn, Node k ); - /** get EPR axiom */ - Node mkEPRAxiom( TypeNode tn ); - /** has EPR axiom */ - bool hasEPRAxiom( TypeNode tn ) const { return d_epr_axiom.find( tn )!=d_epr_axiom.end(); } -}; - -class TermRecBuild { -private: - std::vector< Node > d_term; - std::vector< std::vector< Node > > d_children; - std::vector< Kind > d_kind; - std::vector< bool > d_has_op; - std::vector< unsigned > d_pos; - void addTerm( Node n ); -public: - TermRecBuild(){} - void init( Node n ); - void push( unsigned p ); - void pop(); - void replaceChild( unsigned i, Node n ); - Node getChild( unsigned i ); - Node build( unsigned p=0 ); -}; - } } -#endif +#endif /* __CVC4__THEORY__QUANT_UTIL_H */ diff --git a/src/theory/quantifiers/sygus_explain.cpp b/src/theory/quantifiers/sygus_explain.cpp new file mode 100644 index 000000000..558e1b36b --- /dev/null +++ b/src/theory/quantifiers/sygus_explain.cpp @@ -0,0 +1,112 @@ +/********************* */ +/*! \file sygus_explain.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 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 techniques for sygus explanations + **/ + +#include "theory/quantifiers/sygus_explain.h" + +using namespace CVC4::kind; +using namespace std; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +void TermRecBuild::addTerm(Node n) +{ + d_term.push_back(n); + std::vector currc; + d_kind.push_back(n.getKind()); + if (n.getMetaKind() == kind::metakind::PARAMETERIZED) + { + currc.push_back(n.getOperator()); + d_has_op.push_back(true); + } + else + { + d_has_op.push_back(false); + } + for (unsigned i = 0; i < n.getNumChildren(); i++) + { + currc.push_back(n[i]); + } + d_children.push_back(currc); +} + +void TermRecBuild::init(Node n) +{ + Assert(d_term.empty()); + addTerm(n); +} + +void TermRecBuild::push(unsigned p) +{ + Assert(!d_term.empty()); + unsigned curr = d_term.size() - 1; + Assert(d_pos.size() == curr); + Assert(d_pos.size() + 1 == d_children.size()); + Assert(p < d_term[curr].getNumChildren()); + addTerm(d_term[curr][p]); + d_pos.push_back(p); +} + +void TermRecBuild::pop() +{ + Assert(!d_pos.empty()); + d_pos.pop_back(); + d_kind.pop_back(); + d_has_op.pop_back(); + d_children.pop_back(); + d_term.pop_back(); +} + +void TermRecBuild::replaceChild(unsigned i, Node r) +{ + Assert(!d_term.empty()); + unsigned curr = d_term.size() - 1; + unsigned o = d_has_op[curr] ? 1 : 0; + d_children[curr][i + o] = r; +} + +Node TermRecBuild::getChild(unsigned i) +{ + unsigned curr = d_term.size() - 1; + unsigned o = d_has_op[curr] ? 1 : 0; + return d_children[curr][i + o]; +} + +Node TermRecBuild::build(unsigned d) +{ + Assert(d_pos.size() + 1 == d_term.size()); + Assert(d < d_term.size()); + int p = d < d_pos.size() ? d_pos[d] : -2; + std::vector children; + unsigned o = d_has_op[d] ? 1 : 0; + for (unsigned i = 0; i < d_children[d].size(); i++) + { + Node nc; + if (p + o == i) + { + nc = build(d + 1); + } + else + { + nc = d_children[d][i]; + } + children.push_back(nc); + } + return NodeManager::currentNM()->mkNode(d_kind[d], children); +} + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ diff --git a/src/theory/quantifiers/sygus_explain.h b/src/theory/quantifiers/sygus_explain.h new file mode 100644 index 000000000..f47be00b3 --- /dev/null +++ b/src/theory/quantifiers/sygus_explain.h @@ -0,0 +1,90 @@ +/********************* */ +/*! \file sygus_explain.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 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 sygus explanations + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__SYGUS_EXPLAIN_H +#define __CVC4__SYGUS_EXPLAIN_H + +#include + +#include "expr/node.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** Recursive term builder + * + * This is a utility used to generate variants + * of a term n, where subterms of n can be replaced + * by others via calls to replaceChild(...). + * + * This class maintains a "context", which indicates + * a position in term n. Below, we call the subterm of + * the initial term n at this position the "active term". + * + */ +class TermRecBuild +{ + public: + TermRecBuild() {} + /** set the initial term to n + * + * The context initially empty, that is, + * the active term is initially n. + */ + void init(Node n); + /** push the context + * + * This updates the context so that the + * active term is updated to curr[p], where + * curr is the previously active term. + */ + void push(unsigned p); + /** pop the context */ + void pop(); + /** indicates that the i^th child of the active + * term should be replaced by r in calls to build(). + */ + void replaceChild(unsigned i, Node r); + /** get the i^th child of the active term */ + Node getChild(unsigned i); + /** build the (modified) version of the term + * we intialized via the call to init(). + */ + Node build(unsigned p = 0); + + private: + /** stack of active terms */ + std::vector d_term; + /** stack of children of active terms + * Notice that these may be modified with calls to replaceChild(...). + */ + std::vector > d_children; + /** stack the kind of active terms */ + std::vector d_kind; + /** stack of whether the active terms had an operator */ + std::vector d_has_op; + /** stack of positions that were pushed via calls to push(...) */ + std::vector d_pos; + /** add term to the context stack */ + void addTerm(Node n); +}; + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ + +#endif /* __CVC4__SYGUS_INVARIANCE_H */ diff --git a/src/theory/quantifiers/term_database_sygus.h b/src/theory/quantifiers/term_database_sygus.h index 030963b58..c819bc781 100644 --- a/src/theory/quantifiers/term_database_sygus.h +++ b/src/theory/quantifiers/term_database_sygus.h @@ -17,6 +17,7 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H #define __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H +#include "theory/quantifiers/sygus_explain.h" #include "theory/quantifiers/term_database.h" namespace CVC4 { @@ -25,6 +26,7 @@ namespace quantifiers { class CegConjecture; +// TODO (as part of #1235) move to sygus_invariance.h class SygusInvarianceTest { protected: // check whether nvn[ x ] should be excluded @@ -239,7 +241,8 @@ public: // for symmetry breaking int solveForArgument( TypeNode tnp, unsigned cindex, unsigned arg ); //for eager instantiation -private: + // TODO (as part of #1235) move some of these functions to sygus_explain.h + private: std::map< Node, std::map< Node, bool > > d_subterms; std::map< Node, std::vector< Node > > d_evals; std::map< Node, std::vector< std::vector< Node > > > d_eval_args; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index e742b8be9..ac0de29e3 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -39,7 +39,9 @@ #include "theory/quantifiers/local_theory_ext.h" #include "theory/quantifiers/model_engine.h" #include "theory/quantifiers/quant_conflict_find.h" +#include "theory/quantifiers/quant_epr.h" #include "theory/quantifiers/quant_equality_engine.h" +#include "theory/quantifiers/quant_relevance.h" #include "theory/quantifiers/quant_split.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_rewriter.h" @@ -129,7 +131,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl; if( options::relevantTriggers() ){ - d_quant_rel = new QuantRelevance( false ); + d_quant_rel = new quantifiers::QuantRelevance(false); d_util.push_back(d_quant_rel); }else{ d_quant_rel = NULL; @@ -137,7 +139,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, if( options::quantEpr() ){ Assert( !options::incrementalSolving() ); - d_qepr = new QuantEPR; + d_qepr = new quantifiers::QuantEPR; }else{ d_qepr = NULL; } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 9743588a7..ffede2a5b 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -59,6 +59,8 @@ namespace quantifiers { class TermEnumeration; class FirstOrderModel; class QuantAttributes; + class QuantEPR; + class QuantRelevance; class RelevantDomain; class BvInverter; class InstPropagator; @@ -116,7 +118,7 @@ private: /** equality inference class */ quantifiers::EqualityInference* d_eq_inference; /** for computing relevance of quantifiers */ - QuantRelevance * d_quant_rel; + quantifiers::QuantRelevance* d_quant_rel; /** relevant domain */ quantifiers::RelevantDomain* d_rel_dom; /** inversion utility for BV instantiation */ @@ -126,7 +128,7 @@ private: /** model builder */ quantifiers::QModelBuilder* d_builder; /** utility for effectively propositional logic */ - QuantEPR * d_qepr; + quantifiers::QuantEPR* d_qepr; /** term database */ quantifiers::TermDb* d_term_db; /** sygus term database */ @@ -253,12 +255,12 @@ public: /** get the BV inverter utility */ quantifiers::BvInverter * getBvInverter() { return d_bv_invert; } /** get quantifier relevance */ - QuantRelevance* getQuantifierRelevance() { return d_quant_rel; } + quantifiers::QuantRelevance* getQuantifierRelevance() { return d_quant_rel; } /** get the model builder */ quantifiers::QModelBuilder* getModelBuilder() { return d_builder; } /** get utility for EPR */ - QuantEPR* getQuantEPR() { return d_qepr; } -public: //modules + quantifiers::QuantEPR* getQuantEPR() { return d_qepr; } + public: // modules /** get instantiation engine */ quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; } /** get model engine */ diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 92ecc0393..71cde2841 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -14,20 +14,20 @@ ** Implementation of the theory of sep. **/ - #include "theory/sep/theory_sep.h" -#include "theory/valuation.h" -#include "expr/kind.h" #include -#include "theory/rewriter.h" -#include "theory/theory_model.h" +#include "expr/kind.h" +#include "options/quantifiers_options.h" #include "options/sep_options.h" #include "options/smt_options.h" #include "smt/logic_exception.h" -#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/quant_epr.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" -#include "options/quantifiers_options.h" +#include "theory/quantifiers_engine.h" +#include "theory/rewriter.h" +#include "theory/theory_model.h" +#include "theory/valuation.h" using namespace std; @@ -1089,7 +1089,9 @@ void TheorySep::initializeBounds() { for( std::map< TypeNode, TypeNode >::iterator it = d_loc_to_data_type.begin(); it != d_loc_to_data_type.end(); ++it ){ TypeNode tn = it->first; Trace("sep-bound") << "Initialize bounds for " << tn << "..." << std::endl; - QuantEPR * qepr = getLogicInfo().isQuantified() ? getQuantifiersEngine()->getQuantEPR() : NULL; + quantifiers::QuantEPR* qepr = getLogicInfo().isQuantified() + ? getQuantifiersEngine()->getQuantEPR() + : NULL; //if pto had free variable reference if( d_bound_kind[tn]==bound_herbrand ){ //include Herbrand universe of tn -- 2.30.2