summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rwxr-xr-xcontrib/get-authors3
-rw-r--r--src/expr/expr_template.cpp7
-rw-r--r--src/expr/expr_template.h7
-rw-r--r--src/expr/node.cpp64
-rw-r--r--src/expr/node.h6
-rw-r--r--src/parser/smt2/Smt2.g11
-rw-r--r--src/parser/tptp/Tptp.g9
-rw-r--r--src/parser/tptp/tptp.cpp20
-rw-r--r--src/parser/tptp/tptp.h15
-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
17 files changed, 263 insertions, 54 deletions
diff --git a/contrib/get-authors b/contrib/get-authors
index 59187a81c..bdf331400 100755
--- a/contrib/get-authors
+++ b/contrib/get-authors
@@ -40,6 +40,9 @@ while [ $# -gt 0 ]; do
sed 's/guykatzz/Guy/' | \
sed 's/Guy Katz/Guy/' | \
sed 's/Guy/Guy Katz/' | \
+ sed 's/Martin Brain/Martin/' | \
+ sed 's/Martin/Martin Brain/' | \
+ sed 's/justinxu421/Justin Xu/' | \
eval "$strip_email" | \
sort | uniq -c | sort -nr | head -n 3 | \
( while read lines author; do
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 010b36e94..f812be5a3 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -530,6 +530,13 @@ bool Expr::isConst() const {
return d_node->isConst();
}
+bool Expr::hasFreeVariable() const
+{
+ ExprManagerScope ems(*this);
+ Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+ return d_node->hasFreeVar();
+}
+
void Expr::toStream(std::ostream& out, int depth, bool types, size_t dag,
OutputLanguage language) const {
ExprManagerScope ems(*this);
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index cb4534c08..3a27fca25 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -526,6 +526,13 @@ public:
*/
bool isConst() const;
+ /**
+ * Check if this expression contains a free variable.
+ *
+ * @return true if this node contains a free variable.
+ */
+ bool hasFreeVariable() const;
+
/* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance)..
*
* It has been decided for now to hold off on implementations of
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index b41014f9c..cb61362c5 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -137,9 +137,73 @@ bool NodeTemplate<ref_count>::hasBoundVar() {
return getAttribute(HasBoundVarAttr());
}
+template <bool ref_count>
+bool NodeTemplate<ref_count>::hasFreeVar()
+{
+ assertTNodeNotExpired();
+ std::unordered_set<TNode, TNodeHashFunction> bound_var;
+ std::unordered_map<TNode, bool, TNodeHashFunction> visited;
+ std::vector<TNode> visit;
+ TNode cur;
+ visit.push_back(*this);
+ do
+ {
+ cur = visit.back();
+ visit.pop_back();
+ // can skip if it doesn't have a bound variable
+ if (!cur.hasBoundVar())
+ {
+ continue;
+ }
+ Kind k = cur.getKind();
+ bool isQuant = k == kind::FORALL || k == kind::EXISTS || k == kind::LAMBDA
+ || k == kind::CHOICE;
+ std::unordered_map<TNode, bool, TNodeHashFunction>::iterator itv =
+ visited.find(cur);
+ if (itv == visited.end())
+ {
+ if (k == kind::BOUND_VARIABLE)
+ {
+ if (bound_var.find(cur) == bound_var.end())
+ {
+ return true;
+ }
+ }
+ else if (isQuant)
+ {
+ for (const TNode& cn : cur[0])
+ {
+ // should not shadow
+ Assert(bound_var.find(cn) == bound_var.end());
+ bound_var.insert(cn);
+ }
+ visit.push_back(cur);
+ }
+ // must visit quantifiers again to clean up below
+ visited[cur] = !isQuant;
+ for (const TNode& cn : cur)
+ {
+ visit.push_back(cn);
+ }
+ }
+ else if (!itv->second)
+ {
+ Assert(isQuant);
+ for (const TNode& cn : cur[0])
+ {
+ bound_var.erase(cn);
+ }
+ visited[cur] = true;
+ }
+ } while (!visit.empty());
+ return false;
+}
+
template bool NodeTemplate<true>::isConst() const;
template bool NodeTemplate<false>::isConst() const;
template bool NodeTemplate<true>::hasBoundVar();
template bool NodeTemplate<false>::hasBoundVar();
+template bool NodeTemplate<true>::hasFreeVar();
+template bool NodeTemplate<false>::hasFreeVar();
}/* CVC4 namespace */
diff --git a/src/expr/node.h b/src/expr/node.h
index e1b979570..14630bae1 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -436,6 +436,12 @@ public:
bool hasBoundVar();
/**
+ * Returns true iff this node contains a free variable.
+ * @return true iff this node contains a free variable.
+ */
+ bool hasFreeVar();
+
+ /**
* Convert this Node into an Expr using the currently-in-scope
* manager. Essentially this is like an "operator Expr()" but we
* don't want it to compete with implicit conversions between e.g.
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 2c26c824f..ae9d304f1 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -429,6 +429,17 @@ command [std::unique_ptr<CVC4::Command>* cmd]
csen->setMuted(true);
PARSER_STATE->preemptCommand(csen);
}
+ // if sygus, check whether it has a free variable
+ // this is because, due to the sygus format, one can write assertions
+ // that have free function variables in them
+ if (PARSER_STATE->sygus())
+ {
+ if (expr.hasFreeVariable())
+ {
+ PARSER_STATE->parseError("Assertion has free variable. Perhaps you "
+ "meant constraint instead of assert?");
+ }
+ }
}
| /* check-sat */
CHECK_SAT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 1bed63496..069534974 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -233,6 +233,14 @@ parseCommand returns [CVC4::Command* cmd = NULL]
}
| EOF
{
+ CommandSequence* seq = new CommandSequence();
+ // assert that all distinct constants are distinct
+ Expr aexpr = PARSER_STATE->getAssertionDistinctConstants();
+ if( !aexpr.isNull() )
+ {
+ seq->addCommand(new AssertCommand(aexpr, false));
+ }
+
std::string filename = PARSER_STATE->getInput()->getInputStreamName();
size_t i = filename.find_last_of('/');
if(i != std::string::npos) {
@@ -241,7 +249,6 @@ parseCommand returns [CVC4::Command* cmd = NULL]
if(filename.substr(filename.length() - 2) == ".p") {
filename = filename.substr(0, filename.length() - 2);
}
- CommandSequence* seq = new CommandSequence();
seq->addCommand(new SetInfoCommand("name", SExpr(filename)));
if(PARSER_STATE->hasConjecture()) {
seq->addCommand(new QueryCommand(MK_CONST(bool(false))));
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 70430bcae..09c3b3a2a 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -257,9 +257,9 @@ Expr Tptp::convertRatToUnsorted(Expr expr) {
Expr Tptp::convertStrToUnsorted(std::string str) {
Expr& e = d_distinct_objects[str];
- if (e.isNull()) {
- e = getExprManager()->mkConst(
- UninterpretedConstant(d_unsorted, d_distinct_objects.size() - 1));
+ if (e.isNull())
+ {
+ e = getExprManager()->mkVar(str, d_unsorted);
}
return e;
}
@@ -325,6 +325,20 @@ Expr Tptp::getAssertionExpr(FormulaRole fr, Expr expr) {
return d_nullExpr;
}
+Expr Tptp::getAssertionDistinctConstants()
+{
+ std::vector<Expr> constants;
+ for (std::pair<const std::string, Expr>& cs : d_distinct_objects)
+ {
+ constants.push_back(cs.second);
+ }
+ if (constants.size() > 1)
+ {
+ return getExprManager()->mkExpr(kind::DISTINCT, constants);
+ }
+ return d_nullExpr;
+}
+
Command* Tptp::makeAssertCommand(FormulaRole fr, Expr expr, bool cnf, bool inUnsatCore) {
// For SZS ontology compliance.
// if we're in cnf() though, conjectures don't result in "Theorem" or
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h
index 4e03bc576..e12a3020a 100644
--- a/src/parser/tptp/tptp.h
+++ b/src/parser/tptp/tptp.h
@@ -46,6 +46,11 @@ class Tptp : public Parser {
std::vector< Expr > getFreeVar();
Expr convertRatToUnsorted(Expr expr);
+ /**
+ * Returns a free constant corresponding to the string str. We ensure that
+ * these constants are one-to-one with str. We assert that all these free
+ * constants are pairwise distinct before issuing satisfiability queries.
+ */
Expr convertStrToUnsorted(std::string str);
// CNF and FOF are unsorted so we define this common type.
@@ -97,7 +102,15 @@ class Tptp : public Parser {
* For example, if the role is "conjecture", then the return value is the negation of expr.
*/
Expr getAssertionExpr(FormulaRole fr, Expr expr);
-
+
+ /** get assertion for distinct constants
+ *
+ * This returns a node of the form distinct( k1, ..., kn ) where k1, ..., kn
+ * are the distinct constants introduced by this parser (see
+ * convertStrToUnsorted) if n>1, or null otherwise.
+ */
+ Expr getAssertionDistinctConstants();
+
/** returns the appropriate AssertCommand, given a role, expression expr to assert,
* and information about the assertion.
* The assertion expr is literally what should be asserted (it is already been processed
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