diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-10-03 10:19:12 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-10-03 10:19:12 -0700 |
commit | 51181eb3382ae9c94f90a39103e33ec6e9063dee (patch) | |
tree | 59fc47fc7ba9e1e50ba82cd359ba2bd8e8f679f2 /src/parser/smt2/smt2.h | |
parent | ba73019ebea069607ff1a66863bbdb6a5d501344 (diff) |
[SMT2 Parser] Move code of `sygusCommand` (#3335)
This commit moves the code in `sygusCommand` in the SMT2 parser to the
`Smt2` class. The original code was pushing and popping the current
scope inline. This commit adds a class `SynthFunFactory` that takes care
of that upon creation and destruction.
Diffstat (limited to 'src/parser/smt2/smt2.h')
-rw-r--r-- | src/parser/smt2/smt2.h | 91 |
1 files changed, 75 insertions, 16 deletions
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 178634693..5caedb934 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -198,6 +198,60 @@ class Smt2 : public Parser void resetAssertions(); /** + * Class for creating instances of `SynthFunCommand`s. Creating an instance + * of this class pushes the scope, destroying it pops the scope. + */ + class SynthFunFactory + { + public: + /** + * Creates an instance of `SynthFunFactory`. + * + * @param smt2 Pointer to the parser state + * @param fun Name of the function to synthesize + * @param isInv True if the goal is to synthesize an invariant, false + * otherwise + * @param range The return type of the function-to-synthesize + * @param sortedVarNames The parameters of the function-to-synthesize + */ + SynthFunFactory( + Smt2* smt2, + const std::string& fun, + bool isInv, + Type range, + std::vector<std::pair<std::string, CVC4::Type>>& sortedVarNames); + ~SynthFunFactory(); + + const std::vector<Expr>& getSygusVars() const { return d_sygusVars; } + + /** + * Create an instance of `SynthFunCommand`. + * + * @param grammar Optional grammar associated with the synth-fun command + * @return The instance of `SynthFunCommand` + */ + std::unique_ptr<Command> mkCommand(Type grammar); + + private: + Smt2* d_smt2; + std::string d_fun; + Expr d_synthFun; + Type d_sygusType; + bool d_isInv; + std::vector<Expr> d_sygusVars; + }; + + /** + * Creates a command that adds an invariant constraint. + * + * @param names Name of four symbols corresponding to the + * function-to-synthesize, precondition, postcondition, + * transition relation. + * @return The command that adds an invariant constraint + */ + std::unique_ptr<Command> invConstraint(const std::vector<std::string>& names); + + /** * Sets the logic for the current benchmark. Declares any logic and * theory symbols. * @@ -295,17 +349,21 @@ class Smt2 : public Parser void mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ); - void processSygusGTerm( CVC4::SygusGTerm& sgt, int index, - std::vector< CVC4::Datatype >& datatypes, - std::vector< CVC4::Type>& sorts, - std::vector< std::vector<CVC4::Expr> >& ops, - std::vector< std::vector<std::string> >& cnames, - std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, - std::vector< bool >& allow_const, - std::vector< std::vector< std::string > >& unresolved_gterm_sym, - std::vector<CVC4::Expr>& sygus_vars, - std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, - CVC4::Type& ret, bool isNested = false ); + void processSygusGTerm( + CVC4::SygusGTerm& sgt, + int index, + std::vector<CVC4::Datatype>& datatypes, + std::vector<CVC4::Type>& sorts, + std::vector<std::vector<CVC4::Expr>>& ops, + std::vector<std::vector<std::string>>& cnames, + std::vector<std::vector<std::vector<CVC4::Type>>>& cargs, + std::vector<bool>& allow_const, + std::vector<std::vector<std::string>>& unresolved_gterm_sym, + const std::vector<CVC4::Expr>& sygus_vars, + std::map<CVC4::Type, CVC4::Type>& sygus_to_builtin, + std::map<CVC4::Type, CVC4::Expr>& sygus_to_builtin_expr, + CVC4::Type& ret, + bool isNested = false); static bool pushSygusDatatypeDef( Type t, std::string& dname, std::vector< CVC4::Datatype >& datatypes, @@ -324,10 +382,11 @@ class Smt2 : public Parser std::vector< bool >& allow_const, std::vector< std::vector< std::string > >& unresolved_gterm_sym ); - void setSygusStartIndex( std::string& fun, int startIndex, - std::vector< CVC4::Datatype >& datatypes, - std::vector< CVC4::Type>& sorts, - std::vector< std::vector<CVC4::Expr> >& ops ); + void setSygusStartIndex(const std::string& fun, + int startIndex, + std::vector<CVC4::Datatype>& datatypes, + std::vector<CVC4::Type>& sorts, + std::vector<std::vector<CVC4::Expr>>& ops); void mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs, @@ -356,7 +415,7 @@ class Smt2 : public Parser * term (Variable type) is encountered. */ void addSygusConstructorVariables(Datatype& dt, - std::vector<Expr>& sygusVars, + const std::vector<Expr>& sygusVars, Type type) const; /** |