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/smt2/smt2.cpp | |
| parent | 9e5b1fd1083c1c82d5bbc61a4a316211db629c43 (diff) | |
Mark datatypes as sygus. Add option to normalize sygus terms in search. Add sygus regressions.
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
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; |