diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-05 11:44:21 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-05 11:44:21 -0600 |
commit | bfeedc822f39875c7d54dac0a744a63c5dc838bd (patch) | |
tree | e40b13a5763652db656fad133779c61e79a03d40 /src/parser/smt2 | |
parent | 2ef8fe2eefaecdb62653d36c88169fe906512b9d (diff) |
Make higher-order a flag in logic info. (#1318)
* Make higher-order a flag in logic info.
* Format
* Minor
* Format
Diffstat (limited to 'src/parser/smt2')
-rw-r--r-- | src/parser/smt2/smt2.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 0fc3678c7..a72b0ac6e 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -381,14 +381,16 @@ void Smt2::setLogic(std::string name) { } else { d_logic = name; } - - // if sygus is enabled, we must enable UF, datatypes and integer arithmetic + + // if sygus is enabled, we must enable UF, datatypes, integer arithmetic and + // higher-order if(sygus()) { // get unlocked copy, modify, copy and relock LogicInfo log(d_logic.getUnlockedCopy()); log.enableTheory(theory::THEORY_UF); log.enableTheory(theory::THEORY_DATATYPES); log.enableIntegers(); + log.enableHigherOrder(); d_logic = log; d_logic.lock(); } |