The SmtEngine now ensures that setLogicInternal() is called even if there is no expli...
authorMorgan Deters <mdeters@gmail.com>
Thu, 16 Aug 2012 22:41:07 +0000 (22:41 +0000)
committerMorgan Deters <mdeters@gmail.com>
Thu, 16 Aug 2012 22:41:07 +0000 (22:41 +0000)
commit958b0b56aad79df431376344420106115ab23778
tree803931308136c01077f67c3a6092920c045ebf8d
parent7b624d5052e196eb7d465a1979263fa1e3376f65
The SmtEngine now ensures that setLogicInternal() is called even if there is no explicit setLogic().  This is important for the CVC language, where the parser doesn't ensure that setLogic() is called, and for API uses.  setLogicInternal() should be called in order to properly set up heuristics, even if the logic is just ALL_SUPPORTED.

This means that the CVC language can now take advantage of statistics.

Also added the ability to set the logic from CVC presentation language via (e.g.)
  OPTION "logic" "QF_UFLIA";

Disabled the justification decision heuristic for ALL_SUPPORTED, as it interferes with incrementality.  Kshitij may have a fix (I warned him about this commit).
src/parser/cvc/Cvc.g
src/parser/smt/smt.h
src/parser/smt2/smt2.h
src/smt/smt_engine.cpp
src/theory/logic_info.h
test/unit/theory/logic_info_white.h