diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-20 14:23:04 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-20 14:23:04 +0100 |
| commit | a50f977b02c5653e03d4f3d9d8c7df1f9e2be48e (patch) | |
| tree | 9e8c569a9250c6c8c7eb7826539e63ae414133d9 /src/parser | |
| parent | 9e5b1fd1083c1c82d5bbc61a4a316211db629c43 (diff) | |
Mark datatypes as sygus. Add option to normalize sygus terms in search. Add sygus regressions.
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 1 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 2 |
2 files changed, 2 insertions, 1 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index d2f38cc82..a83299d3b 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -600,6 +600,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL] std::string dname = ss.str(); sorts.push_back(t); datatypes.push_back(Datatype(dname)); + datatypes.back().setSygusType( t ); ops.push_back(std::vector<Expr>()); cnames.push_back(std::vector<std::string>()); cargs.push_back(std::vector<std::vector<CVC4::Type> >()); diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 077f385b0..c6c3a896c 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -534,7 +534,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, testerId.append(name); checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); - CVC4::DatatypeConstructor c(name, testerId); + CVC4::DatatypeConstructor c(name, testerId, ops[i] ); for( unsigned j=0; j<cargs[i].size(); j++ ){ std::stringstream sname; sname << name << "_" << j; |