diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2018-10-18 10:07:18 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-10-18 10:07:18 -0500 |
commit | 406bcd32cbf8a1ee48af02fc6cddc618158762f0 (patch) | |
tree | 2c879879426023392988e0218d0357270f6dd433 /src/smt/smt_engine.h | |
parent | 9a3adaec00e4d36619a2eb78756914b22cde2a36 (diff) |
Introducing internal commands for SyGuS commands (#2627)
Diffstat (limited to 'src/smt/smt_engine.h')
-rw-r--r-- | src/smt/smt_engine.h | 77 |
1 files changed, 76 insertions, 1 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 08bb773d6..5aa59fad7 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -608,11 +608,86 @@ class CVC4_PUBLIC SmtEngine { */ std::vector<Expr> getUnsatAssumptions(void); + /*------------------- sygus commands ------------------*/ + + /** adds a variable declaration + * + * Declared SyGuS variables may be used in SyGuS constraints, in which they + * are assumed to be universally quantified. + */ + void declareSygusVar(const std::string& id, Expr var, Type type); + /** stores information for debugging sygus invariants setup + * + * Since in SyGuS the commands "declare-primed-var" are not necessary for + * building invariant constraints, we only use them to check that the number + * of variables declared corresponds to the number of arguments of the + * invariant-to-synthesize. + */ + void declareSygusPrimedVar(const std::string& id, Type type); + /** adds a function variable declaration + * + * Is SyGuS semantics declared functions are treated in the same manner as + * declared variables, i.e. as universally quantified (function) variables + * which can occur in the SyGuS constraints that compose the conjecture to + * which a function is being synthesized. + */ + void declareSygusFunctionVar(const std::string& id, Expr var, Type type); + /** adds a function-to-synthesize declaration + * + * The given type may not correspond to the actual function type but to a + * datatype encoding the syntax restrictions for the + * function-to-synthesize. In this case this information is stored to be used + * during solving. + * + * vars contains the arguments of the function-to-synthesize. These variables + * are also stored to be used during solving. + * + * isInv determines whether the function-to-synthesize is actually an + * invariant. This information is necessary if we are dumping a command + * corresponding to this declaration, so that it can be properly printed. + */ + void declareSynthFun(const std::string& id, + Expr func, + Type type, + bool isInv, + const std::vector<Expr>& vars); + /** adds a regular sygus constraint */ + void assertSygusConstraint(Expr constraint); + /** adds an invariant constraint + * + * Invariant constraints are not explicitly declared: they are given in terms + * of the invariant-to-synthesize, the pre condition, transition relation and + * post condition. The actual constraint is built based on the inputs of these + * place holder predicates : + * + * PRE(x) -> INV(x) + * INV() ^ TRANS(x, x') -> INV(x') + * INV(x) -> POST(x) + * + * The regular and primed variables are retrieved from the declaration of the + * invariant-to-synthesize. + */ + void assertSygusInvConstraint(const Expr& inv, + const Expr& pre, + const Expr& trans, + const Expr& post); /** * Assert a synthesis conjecture to the current context and call * check(). Returns sat, unsat, or unknown result. + * + * The actual synthesis conjecture is built based on the previously + * communicated information to this module (universal variables, defined + * functions, functions-to-synthesize, and which constraints compose it). The + * built conjecture is a higher-order formula of the form + * + * exists f1...fn . forall v1...vm . F + * + * in which f1...fn are the functions-to-synthesize, v1...vm are the declared + * universal variables and F is the set of declared constraints. */ - Result checkSynth(const Expr& e) /* throw(Exception) */; + Result checkSynth() /* throw(Exception) */; + + /*------------------- end of sygus commands-------------*/ /** * Simplify a formula without doing "much" work. Does not involve |