From 35ac65b0034eacf2766d9e94be1c7fe9c116bb75 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Mon, 1 Oct 2012 22:11:26 +0000 Subject: "Fix" (disable) portfolio when using quantifiers Other changes: * fix compile error in smt_engine in debug builds * add getLogicInfo in smt_engine * remove "empty-channel" and "disable-lemma-sharing" debug tags (this commit was certified error- and warning-free by the test-and-commit script.) --- src/smt/smt_engine.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'src/smt/smt_engine.cpp') diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 069e5473e..08fdbec95 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -576,6 +576,10 @@ void SmtEngine::setLogic(const std::string& s) throw(ModalException) { setLogic(LogicInfo(s)); } +LogicInfo SmtEngine::getLogicInfo() const { + return d_logic; +} + // This function is called when d_logic has just been changed. // The LogicInfo isn't passed in explicitly, because that might // tempt people in the code to use the (potentially unlocked) @@ -1094,7 +1098,7 @@ Node SmtEnginePrivate::preSkolemizeQuantifiers( Node n, bool polarity, std::vect } return preSkolemizeQuantifiers( nn, polarity, fvs ); }else{ - Assert( n.getKind()==AND || n.getKind()==OR ); + Assert( n.getKind() == kind::AND || n.getKind() == kind::OR ); std::vector< Node > children; for( int i=0; i<(int)n.getNumChildren(); i++ ){ children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvs ) ); -- cgit v1.2.3