diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/expr_template.cpp | 7 | ||||
-rw-r--r-- | src/expr/expr_template.h | 7 | ||||
-rw-r--r-- | src/expr/node.cpp | 64 | ||||
-rw-r--r-- | src/expr/node.h | 6 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 11 | ||||
-rw-r--r-- | src/parser/tptp/Tptp.g | 9 | ||||
-rw-r--r-- | src/parser/tptp/tptp.cpp | 20 | ||||
-rw-r--r-- | src/parser/tptp/tptp.h | 15 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.cpp | 17 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.h | 21 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/single_inv_partition.cpp | 39 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 79 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.h | 14 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 1 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 2 |
16 files changed, 260 insertions, 54 deletions
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); |