diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-12-01 09:07:42 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-12-01 09:07:42 -0600 |
| commit | f40d813048599b58327fc968344301d39f156da2 (patch) | |
| tree | 6441035d51eccca0156ed15d142ced27eb7187d4 /src/parser | |
| parent | 9f3ea3328213e08bf39b8ceeea272205255fd7ed (diff) | |
Refactor and generalize PBE strategies (#1410)
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index c542e5917..3e8d5f0bb 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -985,7 +985,8 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, Debug("parser-sygus") << "SMT2 sygus parser : Making constructors for sygus datatype " << dt.getName() << std::endl; Debug("parser-sygus") << " add constructors..." << std::endl; - for (unsigned i = 0, size = cnames.size(); i < size; i++) + // size of cnames changes, this loop must check size + for (unsigned i = 0; i < cnames.size(); i++) { bool is_dup = false; bool is_dup_op = false; @@ -1121,8 +1122,12 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, std::stringstream ss; ss << dt.getName() << "_" << i << "_" << cnames[i]; cnames[i] = ss.str(); + Debug("parser-sygus") << " construct the datatype " << cnames[i] << "..." + << std::endl; // add the sygus constructor dt.addSygusConstructor(ops[i], cnames[i], cargs[i], spc); + Debug("parser-sygus") << " finished constructing the datatype" + << std::endl; } } |