diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 262 |
1 files changed, 254 insertions, 8 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 196da6b9c..a2dd8276b 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -497,6 +497,31 @@ class SmtEnginePrivate : public NodeManagerListener { /* Finishes the initialization of the private portion of SMTEngine. */ void finishInit(); + /*------------------- sygus utils ------------------*/ + /** + * sygus variables declared (from "declare-var" and "declare-fun" commands) + * + * The SyGuS semantics for declared variables is that they are implicitly + * universally quantified in the constraints. + */ + std::vector<Node> d_sygusVars; + /** types of sygus primed variables (for debugging) */ + std::vector<Type> d_sygusPrimedVarTypes; + /** sygus constraints */ + std::vector<Node> d_sygusConstraints; + /** functions-to-synthesize */ + std::vector<Node> d_sygusFunSymbols; + /** maps functions-to-synthesize to their respective input variables lists */ + std::map<Node, std::vector<Node>> d_sygusFunVars; + /** maps functions-to-synthesize to their respective syntactic restrictions + * + * If function has syntactic restrictions, these are encoded as a SyGuS + * datatype type + */ + std::map<Node, TypeNode> d_sygusFunSyntax; + + /*------------------- end of sygus utils ------------------*/ + private: std::unique_ptr<PreprocessingPassContext> d_preprocessingPassContext; @@ -3692,14 +3717,6 @@ vector<Expr> SmtEngine::getUnsatAssumptions(void) return res; } -Result SmtEngine::checkSynth(const Expr& e) -{ - SmtScope smts(this); - Trace("smt") << "Check synth: " << e << std::endl; - Trace("smt-synth") << "Check synthesis conjecture: " << e << std::endl; - return checkSatisfiability(e, true, false); -} - Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) { Assert(ex.getExprManager() == d_exprManager); @@ -3724,6 +3741,235 @@ Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) return quickCheck().asValidityResult(); }/* SmtEngine::assertFormula() */ +/* + -------------------------------------------------------------------------- + Handling SyGuS commands + -------------------------------------------------------------------------- +*/ + +void SmtEngine::declareSygusVar(const std::string& id, Expr var, Type type) +{ + d_private->d_sygusVars.push_back(Node::fromExpr(var)); + Trace("smt") << "SmtEngine::declareSygusVar: " << var << "\n"; +} + +void SmtEngine::declareSygusPrimedVar(const std::string& id, Type type) +{ +#ifdef CVC4_ASSERTIONS + d_private->d_sygusPrimedVarTypes.push_back(type); +#endif + Trace("smt") << "SmtEngine::declareSygusPrimedVar: " << id << "\n"; +} + +void SmtEngine::declareSygusFunctionVar(const std::string& id, + Expr var, + Type type) +{ + d_private->d_sygusVars.push_back(Node::fromExpr(var)); + Trace("smt") << "SmtEngine::declareSygusFunctionVar: " << var << "\n"; +} + +void SmtEngine::declareSynthFun(const std::string& id, + Expr func, + Type sygusType, + bool isInv, + const std::vector<Expr>& vars) +{ + Node fn = Node::fromExpr(func); + d_private->d_sygusFunSymbols.push_back(fn); + std::vector<Node> var_nodes; + for (const Expr& v : vars) + { + var_nodes.push_back(Node::fromExpr(v)); + } + d_private->d_sygusFunVars[fn] = var_nodes; + // whether sygus type encodes syntax restrictions + if (sygusType.isDatatype() + && static_cast<DatatypeType>(sygusType).getDatatype().isSygus()) + { + d_private->d_sygusFunSyntax[fn] = TypeNode::fromType(sygusType); + } + Trace("smt") << "SmtEngine::declareSynthFun: " << func << "\n"; +} + +void SmtEngine::assertSygusConstraint(Expr constraint) +{ + d_private->d_sygusConstraints.push_back(constraint); + + Trace("smt") << "SmtEngine::assertSygusConstrant: " << constraint << "\n"; +} + +void SmtEngine::assertSygusInvConstraint(const Expr& inv, + const Expr& pre, + const Expr& trans, + const Expr& post) +{ + SmtScope smts(this); + // build invariant constraint + + // get variables (regular and their respective primed versions) + std::vector<Node> terms, vars, primed_vars; + terms.push_back(Node::fromExpr(inv)); + terms.push_back(Node::fromExpr(pre)); + terms.push_back(Node::fromExpr(trans)); + terms.push_back(Node::fromExpr(post)); + // variables are built based on the invariant type + FunctionType t = static_cast<FunctionType>(inv.getType()); + std::vector<Type> argTypes = t.getArgTypes(); + for (const Type& ti : argTypes) + { + TypeNode tn = TypeNode::fromType(ti); + vars.push_back(d_nodeManager->mkBoundVar(tn)); + d_private->d_sygusVars.push_back(vars.back()); + std::stringstream ss; + ss << vars.back() << "'"; + primed_vars.push_back(d_nodeManager->mkBoundVar(ss.str(), tn)); + d_private->d_sygusVars.push_back(primed_vars.back()); +#ifdef CVC4_ASSERTIONS + bool find_new_declared_var = false; + for (const Type& t : d_private->d_sygusPrimedVarTypes) + { + if (t == ti) + { + d_private->d_sygusPrimedVarTypes.erase( + std::find(d_private->d_sygusPrimedVarTypes.begin(), + d_private->d_sygusPrimedVarTypes.end(), + t)); + find_new_declared_var = true; + break; + } + } + if (!find_new_declared_var) + { + Warning() + << "warning: declared primed variables do not match invariant's " + "type\n"; + } +#endif + } + + // make relevant terms; 0 -> Inv, 1 -> Pre, 2 -> Trans, 3 -> Post + for (unsigned i = 0; i < 4; ++i) + { + Node op = terms[i]; + Trace("smt-debug") << "Make inv-constraint term #" << i << " : " << op + << " with type " << op.getType() << "...\n"; + std::vector<Node> children; + children.push_back(op); + // transition relation applied over both variable lists + if (i == 2) + { + children.insert(children.end(), vars.begin(), vars.end()); + children.insert(children.end(), primed_vars.begin(), primed_vars.end()); + } + else + { + children.insert(children.end(), vars.begin(), vars.end()); + } + terms[i] = + d_nodeManager->mkNode(i == 0 ? kind::APPLY_UF : kind::APPLY, children); + // make application of Inv on primed variables + if (i == 0) + { + children.clear(); + children.push_back(op); + children.insert(children.end(), primed_vars.begin(), primed_vars.end()); + terms.push_back(d_nodeManager->mkNode(kind::APPLY_UF, children)); + } + } + // make constraints + std::vector<Node> conj; + conj.push_back(d_nodeManager->mkNode(kind::IMPLIES, terms[1], terms[0])); + Node term0_and_2 = d_nodeManager->mkNode(kind::AND, terms[0], terms[2]); + conj.push_back(d_nodeManager->mkNode(kind::IMPLIES, term0_and_2, terms[4])); + conj.push_back(d_nodeManager->mkNode(kind::IMPLIES, terms[0], terms[3])); + Node constraint = d_nodeManager->mkNode(kind::AND, conj); + + d_private->d_sygusConstraints.push_back(constraint); + + Trace("smt") << "SmtEngine::assertSygusInvConstrant: " << constraint << "\n"; +} + +Result SmtEngine::checkSynth() +{ + SmtScope smts(this); + // build synthesis conjecture from asserted constraints and declared + // variables/functions + Node sygusVar = + d_nodeManager->mkSkolem("sygus", d_nodeManager->booleanType()); + Node inst_attr = d_nodeManager->mkNode(kind::INST_ATTRIBUTE, sygusVar); + Node sygusAttr = d_nodeManager->mkNode(kind::INST_PATTERN_LIST, inst_attr); + std::vector<Node> bodyv; + Trace("smt") << "Sygus : Constructing sygus constraint...\n"; + unsigned n_constraints = d_private->d_sygusConstraints.size(); + Node body = n_constraints == 0 + ? d_nodeManager->mkConst(true) + : (n_constraints == 1 + ? d_private->d_sygusConstraints[0] + : d_nodeManager->mkNode( + kind::AND, d_private->d_sygusConstraints)); + body = body.notNode(); + Trace("smt") << "...constructed sygus constraint " << body << std::endl; + if (!d_private->d_sygusVars.empty()) + { + Node boundVars = + d_nodeManager->mkNode(kind::BOUND_VAR_LIST, d_private->d_sygusVars); + body = d_nodeManager->mkNode(kind::EXISTS, boundVars, body); + Trace("smt") << "...constructed exists " << body << std::endl; + } + if (!d_private->d_sygusFunSymbols.empty()) + { + Node boundVars = d_nodeManager->mkNode(kind::BOUND_VAR_LIST, + d_private->d_sygusFunSymbols); + body = d_nodeManager->mkNode(kind::FORALL, boundVars, body, sygusAttr); + } + Trace("smt") << "...constructed forall " << body << std::endl; + + // set attribute for synthesis conjecture + setUserAttribute("sygus", sygusVar.toExpr(), {}, ""); + + // set attributes for functions-to-synthesize + for (const Node& synth_fun : d_private->d_sygusFunSymbols) + { + // associate var list with function-to-synthesize + Assert(d_private->d_sygusFunVars.find(synth_fun) + != d_private->d_sygusFunVars.end()); + const std::vector<Node>& vars = d_private->d_sygusFunVars[synth_fun]; + Node bvl; + if (!vars.empty()) + { + bvl = d_nodeManager->mkNode(kind::BOUND_VAR_LIST, vars); + } + std::vector<Expr> attr_val_bvl; + attr_val_bvl.push_back(bvl.toExpr()); + setUserAttribute( + "sygus-synth-fun-var-list", synth_fun.toExpr(), attr_val_bvl, ""); + // If the function has syntax restrition, bulid a variable "sfproxy" which + // carries the type, a SyGuS datatype that corresponding to the syntactic + // restrictions. + std::map<Node, TypeNode>::const_iterator it = + d_private->d_sygusFunSyntax.find(synth_fun); + if (it != d_private->d_sygusFunSyntax.end()) + { + Node sym = d_nodeManager->mkBoundVar("sfproxy", it->second); + std::vector<Expr> attr_value; + attr_value.push_back(sym.toExpr()); + setUserAttribute( + "sygus-synth-grammar", synth_fun.toExpr(), attr_value, ""); + } + } + + Trace("smt") << "Check synthesis conjecture: " << body << std::endl; + + return checkSatisfiability(body.toExpr(), true, false); +} + +/* + -------------------------------------------------------------------------- + End of Handling SyGuS commands + -------------------------------------------------------------------------- +*/ + Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const { return node; } |