summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/quantifiers/quantifiers_attributes.cpp17
-rw-r--r--src/theory/quantifiers/quantifiers_attributes.h21
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.cpp2
-rw-r--r--src/theory/quantifiers/single_inv_partition.cpp39
-rw-r--r--src/theory/quantifiers/sygus/sygus_grammar_cons.cpp79
-rw-r--r--src/theory/quantifiers/sygus/sygus_grammar_cons.h14
-rw-r--r--src/theory/quantifiers/theory_quantifiers.cpp1
-rw-r--r--src/theory/theory_engine.cpp2
8 files changed, 126 insertions, 49 deletions
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index d1a420e3d..0e8dfc9f4 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -29,6 +29,11 @@ namespace CVC4 {
namespace theory {
namespace quantifiers {
+bool QAttributes::isStandard() const
+{
+ return !d_sygus && !d_quant_elim && !isFunDef() && d_name.isNull();
+}
+
QuantAttributes::QuantAttributes( QuantifiersEngine * qe ) :
d_quantEngine(qe) {
@@ -52,6 +57,12 @@ void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::ve
Trace("quant-attr-debug") << "Set sygus " << n << std::endl;
SygusAttribute ca;
n.setAttribute( ca, true );
+ }
+ else if (attr == "quant-name")
+ {
+ Trace("quant-attr-debug") << "Set quant-name " << n << std::endl;
+ QuantNameAttribute qna;
+ n.setAttribute(qna, true);
} else if (attr == "sygus-synth-grammar") {
Assert( node_values.size()==1 );
Trace("quant-attr-debug") << "Set sygus synth grammar " << n << " to "
@@ -265,6 +276,12 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){
Trace("quant-attr") << "Attribute : sygus : " << q << std::endl;
qa.d_sygus = true;
}
+ if (avar.getAttribute(QuantNameAttribute()))
+ {
+ Trace("quant-attr") << "Attribute : quantifier name : " << avar
+ << " for " << q << std::endl;
+ qa.d_name = avar;
+ }
if( avar.getAttribute(SynthesisAttribute()) ){
Trace("quant-attr") << "Attribute : synthesis : " << q << std::endl;
qa.d_synthesis = true;
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index 87315de7c..fcb519712 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -51,6 +51,12 @@ typedef expr::Attribute< QuantElimPartialAttributeId, bool > QuantElimPartialAtt
struct SygusAttributeId {};
typedef expr::Attribute< SygusAttributeId, bool > SygusAttribute;
+/**Attribute to give names to quantified formulas */
+struct QuantNameAttributeId
+{
+};
+typedef expr::Attribute<QuantNameAttributeId, bool> QuantNameAttribute;
+
/** Attribute true for quantifiers that are synthesis conjectures */
struct SynthesisAttributeId {};
typedef expr::Attribute< SynthesisAttributeId, bool > SynthesisAttribute;
@@ -112,12 +118,23 @@ struct QAttributes
/** the instantiation pattern list for this quantified formula (its 3rd child)
*/
Node d_ipl;
+ /** the name of this quantified formula */
+ Node d_name;
/** the quantifier id associated with this formula */
Node d_qid_num;
/** is this quantified formula a rewrite rule? */
- bool isRewriteRule() { return !d_rr.isNull(); }
+ bool isRewriteRule() const { return !d_rr.isNull(); }
/** is this quantified formula a function definition? */
- bool isFunDef() { return !d_fundef_f.isNull(); }
+ bool isFunDef() const { return !d_fundef_f.isNull(); }
+ /**
+ * Is this a standard quantifier? A standard quantifier is one that we can
+ * perform destructive updates (variable elimination, miniscoping, etc).
+ *
+ * A quantified formula is not standard if it is sygus, one for which
+ * we are performing quantifier elimination, is a function definition, or
+ * has a name.
+ */
+ bool isStandard() const;
};
/** This class caches information about attributes of quantified formulas
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index bc298fa9c..a8089d229 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -1705,7 +1705,7 @@ Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& arg
bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& qa ){
bool is_strict_trigger = qa.d_hasPattern && options::userPatternsQuant()==USER_PAT_MODE_TRUST;
- bool is_std = !qa.d_sygus && !qa.d_quant_elim && !qa.isFunDef() && !is_strict_trigger;
+ bool is_std = qa.isStandard() && !is_strict_trigger;
if (computeOption == COMPUTE_ELIM_SYMBOLS)
{
return true;
diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp
index 890b7fcd3..0a0dac4ba 100644
--- a/src/theory/quantifiers/single_inv_partition.cpp
+++ b/src/theory/quantifiers/single_inv_partition.cpp
@@ -250,37 +250,28 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs,
// now must check if it has other bound variables
std::vector<Node> bvs;
TermUtil::getBoundVars(cr, bvs);
- if (bvs.size() > d_si_vars.size())
+ // bound variables must be contained in the single invocation variables
+ for (const Node& bv : bvs)
{
- // getBoundVars also collects functions in the rare case that we are
- // synthesizing a function with 0 arguments
- // take these into account below.
- unsigned n_const_synth_fun = 0;
- for (unsigned j = 0; j < bvs.size(); j++)
+ if (std::find(d_si_vars.begin(), d_si_vars.end(), bv)
+ == d_si_vars.end())
{
- if (std::find(d_input_funcs.begin(), d_input_funcs.end(), bvs[j])
- != d_input_funcs.end())
+ // getBoundVars also collects functions in the rare case that we are
+ // synthesizing a function with 0 arguments, take this into account
+ // here.
+ if (std::find(d_input_funcs.begin(), d_input_funcs.end(), bv)
+ == d_input_funcs.end())
{
- n_const_synth_fun++;
+ Trace("si-prt")
+ << "...not ground single invocation." << std::endl;
+ ngroundSingleInvocation = true;
+ singleInvocation = false;
}
}
- if (bvs.size() - n_const_synth_fun > d_si_vars.size())
- {
- Trace("si-prt") << "...not ground single invocation." << std::endl;
- ngroundSingleInvocation = true;
- singleInvocation = false;
- }
- else
- {
- Trace("si-prt") << "...ground single invocation : success, after "
- "removing 0-arg synth functions."
- << std::endl;
- }
}
- else
+ if (singleInvocation)
{
- Trace("si-prt") << "...ground single invocation : success."
- << std::endl;
+ Trace("si-prt") << "...ground single invocation" << std::endl;
}
}
else
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 322d49af6..b6a780b6c 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -87,9 +87,10 @@ void CegGrammarConstructor::collectTerms( Node n, std::map< TypeNode, std::vecto
} while (!visit.empty());
}
-
-
-Node CegGrammarConstructor::process( Node q, std::map< Node, Node >& templates, std::map< Node, Node >& templates_arg ) {
+Node CegGrammarConstructor::process(Node q,
+ const std::map<Node, Node>& templates,
+ const std::map<Node, Node>& templates_arg)
+{
// convert to deep embedding and finalize single invocation here
// now, construct the grammar
Trace("cegqi") << "CegConjecture : convert to deep embedding..." << std::endl;
@@ -101,10 +102,7 @@ Node CegGrammarConstructor::process( Node q, std::map< Node, Node >& templates,
NodeManager* nm = NodeManager::currentNM();
- std::vector< Node > qchildren;
- std::map< Node, Node > synth_fun_vars;
std::vector< Node > ebvl;
- Node qbody_subs = q[1];
for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
Node sf = q[0][i];
// if non-null, v encodes the syntactic restrictions (via an inductive
@@ -161,19 +159,68 @@ Node CegGrammarConstructor::process( Node q, std::map< Node, Node >& templates,
// normalize type
SygusGrammarNorm sygus_norm(d_qe);
tn = sygus_norm.normalizeSygusType(tn, sfvl);
- // check if there is a template
- std::map< Node, Node >::iterator itt = templates.find( sf );
+
+ std::map<Node, Node>::const_iterator itt = templates.find(sf);
if( itt!=templates.end() ){
Node templ = itt->second;
- TNode templ_arg = templates_arg[sf];
+ std::map<Node, Node>::const_iterator itta = templates_arg.find(sf);
+ Assert(itta != templates_arg.end());
+ TNode templ_arg = itta->second;
Assert( !templ_arg.isNull() );
- Trace("cegqi-debug") << "Template for " << sf << " is : " << templ << " with arg " << templ_arg << std::endl;
// if there is a template for this argument, make a sygus type on top of it
if( options::sygusTemplEmbedGrammar() ){
+ Trace("cegqi-debug") << "Template for " << sf << " is : " << templ
+ << " with arg " << templ_arg << std::endl;
Trace("cegqi-debug") << " embed this template as a grammar..." << std::endl;
tn = mkSygusTemplateType( templ, templ_arg, tn, sfvl, ss.str() );
- }else{
- // otherwise, apply it as a preprocessing pass
+ }
+ }
+
+ // ev is the first-order variable corresponding to this synth fun
+ std::stringstream ssf;
+ ssf << "f" << sf;
+ Node ev = nm->mkBoundVar(ssf.str(), tn);
+ ebvl.push_back(ev);
+ Trace("cegqi") << "...embedding synth fun : " << sf << " -> " << ev
+ << std::endl;
+ }
+ return process(q, templates, templates_arg, ebvl);
+}
+
+Node CegGrammarConstructor::process(Node q,
+ const std::map<Node, Node>& templates,
+ const std::map<Node, Node>& templates_arg,
+ const std::vector<Node>& ebvl)
+{
+ Assert(q[0].getNumChildren() == ebvl.size());
+
+ NodeManager* nm = NodeManager::currentNM();
+
+ std::vector<Node> qchildren;
+ Node qbody_subs = q[1];
+ std::map<Node, Node> synth_fun_vars;
+ for (unsigned i = 0, size = q[0].getNumChildren(); i < size; i++)
+ {
+ Node sf = q[0][i];
+ synth_fun_vars[sf] = ebvl[i];
+ Node sfvl = getSygusVarList(sf);
+ TypeNode tn = ebvl[i].getType();
+ // check if there is a template
+ std::map<Node, Node>::const_iterator itt = templates.find(sf);
+ if (itt != templates.end())
+ {
+ Node templ = itt->second;
+ std::map<Node, Node>::const_iterator itta = templates_arg.find(sf);
+ Assert(itta != templates_arg.end());
+ TNode templ_arg = itta->second;
+ Assert(!templ_arg.isNull());
+ // if there is a template for this argument, make a sygus type on top of
+ // it
+ if (!options::sygusTemplEmbedGrammar())
+ {
+ // otherwise, apply it as a preprocessing pass
+ Trace("cegqi-debug") << "Template for " << sf << " is : " << templ
+ << " with arg " << templ_arg << std::endl;
Trace("cegqi-debug") << " apply this template as a substituion during preprocess..." << std::endl;
std::vector< Node > schildren;
std::vector< Node > largs;
@@ -212,14 +259,6 @@ Node CegGrammarConstructor::process( Node q, std::map< Node, Node >& templates,
if( !dt.getSygusAllowAll() ){
d_is_syntax_restricted = true;
}
-
- // ev is the first-order variable corresponding to this synth fun
- std::stringstream ssf;
- ssf << "f" << sf;
- Node ev = nm->mkBoundVar(ssf.str(), tn);
- ebvl.push_back( ev );
- synth_fun_vars[sf] = ev;
- Trace("cegqi") << "...embedding synth fun : " << sf << " -> " << ev << std::endl;
}
qchildren.push_back(nm->mkNode(kind::BOUND_VAR_LIST, ebvl));
if( qbody_subs!=q[1] ){
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
index 16f4672b0..39f95527f 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
@@ -35,6 +35,7 @@ public:
CegGrammarConstructor(QuantifiersEngine* qe, CegConjecture* p);
~CegGrammarConstructor() {}
/** process
+ *
* This converts node q based on its deep embedding
* (Section 4 of Reynolds et al CAV 2015).
* The syntactic restrictions are associated with
@@ -48,8 +49,17 @@ public:
* for some t if !templates[i].isNull().
*/
Node process(Node q,
- std::map<Node, Node>& templates,
- std::map<Node, Node>& templates_arg);
+ const std::map<Node, Node>& templates,
+ const std::map<Node, Node>& templates_arg);
+ /**
+ * Same as above, but we have already determined that the set of first-order
+ * datatype variables that will quantify the deep embedding conjecture are
+ * the vector ebvl.
+ */
+ Node process(Node q,
+ const std::map<Node, Node>& templates,
+ const std::map<Node, Node>& templates_arg,
+ const std::vector<Node>& ebvl);
/** is the syntax restricted? */
bool isSyntaxRestricted() { return d_is_syntax_restricted; }
/** does the syntax allow ITE expressions? */
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index f4e44ff2f..74d8269f9 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -44,6 +44,7 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, Output
out.handleUserAttribute( "conjecture", this );
out.handleUserAttribute( "fun-def", this );
out.handleUserAttribute( "sygus", this );
+ out.handleUserAttribute("quant-name", this);
out.handleUserAttribute("sygus-synth-grammar", this);
out.handleUserAttribute( "sygus-synth-fun-var-list", this );
out.handleUserAttribute( "synthesis", this );
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index f3489f5ad..de71a8b5e 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -393,6 +393,8 @@ void TheoryEngine::preRegister(TNode preprocessed) {
d_sharedTerms.addEqualityToPropagate(preprocessed);
}
+ // the atom should not have free variables
+ Assert(!preprocessed.hasFreeVar());
// Pre-register the terms in the atom
Theory::Set theories = NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed);
theories = Theory::setRemove(THEORY_BOOL, theories);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback