summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Makefile.am6
-rw-r--r--src/theory/quantifiers/inst_strategy_cbqi.cpp3
-rw-r--r--src/theory/quantifiers/inst_strategy_e_matching.cpp3
-rw-r--r--src/theory/quantifiers/quant_epr.cpp187
-rw-r--r--src/theory/quantifiers/quant_epr.h104
-rw-r--r--src/theory/quantifiers/quant_relevance.cpp97
-rw-r--r--src/theory/quantifiers/quant_relevance.h80
-rw-r--r--src/theory/quantifiers/quant_util.cpp238
-rw-r--r--src/theory/quantifiers/quant_util.h88
-rw-r--r--src/theory/quantifiers/sygus_explain.cpp112
-rw-r--r--src/theory/quantifiers/sygus_explain.h90
-rw-r--r--src/theory/quantifiers/term_database_sygus.h5
-rw-r--r--src/theory/quantifiers_engine.cpp6
-rw-r--r--src/theory/quantifiers_engine.h12
-rw-r--r--src/theory/sep/theory_sep.cpp18
15 files changed, 710 insertions, 339 deletions
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( index<patTerms.size() ){
//Notice() << "check add additional" << std::endl;
//check if similar patterns exist, and if so, add them additionally
- int nqfs_curr = 0;
+ unsigned nqfs_curr = 0;
if( options::relevantTriggers() ){
nqfs_curr = d_quantEngine->getQuantifierRelevance()->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<int, std::map<Node, bool> >& 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<int, std::map<Node, bool> > 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; 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<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; 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 <map>
+
+#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<TypeNode, std::vector<Node> > 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<int, std::map<Node, bool> >& visited,
+ bool beneathQuant,
+ bool hasPol,
+ bool pol);
+ /** map from types to a flag says whether they are not EPR */
+ std::map<TypeNode, bool> d_non_epr;
+ /** EPR axioms for each type. */
+ std::map<TypeNode, Node> 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<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 < minRelevance))
+ {
+ minRelevance = r;
+ }
+ }
+ if (minRelevance != -1)
+ {
+ setRelevance(f, minRelevance + 1);
+ }
+}
+
+/** compute symbols */
+void QuantRelevance::computeSymbols(Node n, std::vector<Node>& 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 <map>
+
+#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<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);
+};
+
+} /* 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<minRelevance ) ){
- minRelevance = r;
- }
- }
- if( minRelevance!=-1 ){
- setRelevance( f, minRelevance+1 );
- }
-}
-
-
-/** compute symbols */
-void QuantRelevance::computeSymbols( Node n, std::vector< Node >& 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 );
- }
- }
- }
- }
-}
-
-
QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){
initialize( n, computeEq );
}
@@ -456,179 +400,5 @@ void QuantPhaseReq::getEntailPolarity( Node n, int child, bool hasPol, bool pol,
}
}
-void QuantEPR::registerNode( Node n, std::map< int, std::map< Node, bool > >& 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< int, std::map< Node, bool > > 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; 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< 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; 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;
- }
-}
-
-
-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<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 n ) {
- Assert( !d_term.empty() );
- unsigned curr = d_term.size()-1;
- unsigned o = d_has_op[curr] ? 1 : 0;
- d_children[curr][i+o] = n;
-}
-
-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< Node > 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 );
-}
-
+} /* 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<Node, Node>& 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<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 < 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<Node> 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 <vector>
+
+#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<Node> d_term;
+ /** stack of children of active terms
+ * Notice that these may be modified with calls to replaceChild(...).
+ */
+ std::vector<std::vector<Node> > d_children;
+ /** stack the kind of active terms */
+ std::vector<Kind> d_kind;
+ /** stack of whether the active terms had an operator */
+ std::vector<bool> d_has_op;
+ /** stack of positions that were pushed via calls to push(...) */
+ std::vector<unsigned> 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 <map>
-#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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback